Invertible ideal sheaves: locality and stability

Invertibility of an ideal sheaf (IdealSheafData.IsInvertible) is local and stable under localization, and the unit ideal sheaf, products of invertible ideal sheaves and comaps along open immersions are invertible. The ring-level statements are in Hironaka.Scheme.BlowUp.Invertible; compare the proof of [TSPA, Tag 01WS].

Main declarations

• Ideal.IsInvertible.map_ringEquiv, Ideal.IsInvertible.map_of_isLocalization_away: transport of invertibility along ring isomorphisms and to any localization away from an element.
• AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_iff_forall_ideal, isInvertible_iff_of_iSup_eq_top, isInvertible_ideal_affineBasicOpen: locality.
• AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_top, IsInvertible.mul, IsInvertible.comap_of_isOpenImmersion: stability.

The arguments

Locality. The defining condition of Ideal.IsInvertible is pointwise on primes, and the points of an affine open U are the primes of Γ(X, U) (IsAffineOpen.primeIdealOf, fromSpec). If J(U) is invertible at the prime of x, the basic open D(s) ∋ x of U has J(D(s)) = J(U)_s = (a) with a a nonzerodivisor. Conversely if J is invertible at x ∈ U, with J(V) = (g) on an affine V ∋ x, a basic open D(s) = D(t) of both U and V around x has J(D(s)) = (g) with g a nonzerodivisor (localization preserves nonzerodivisors), and g is a unit multiple of the image of an element a ∈ J(U), which is the datum at the prime of x.

Stability. Local generators multiply on a common basic open; the unit ideal is generated by 1; for an open immersion f, (J.comap f)(V) = J(f(V)) transported along the isomorphism Γ(X, f(V)) ≅ Γ(Y, V), and a basic open of X inside the image of f is the image of an affine open of Y.

Conventions

Statements about J(W) for a basic open W = D(s) ⊆ U are transported along the equality of affine opens D(s) = D(t) as propositions, never by rewriting the section rings.

theorem Ideal.IsRegularGeneratorIn.map_ringEquiv {A B : Type u} [CommRing A] [CommRing B] (e : A ≃+* B) {J : Ideal A} {s a : A} (h : J.IsRegularGeneratorIn (Localization.Away s) a) : (map (↑e) J).IsRegularGeneratorIn (Localization.Away (e s)) (e a)

The datum of a regular generator passes along a ring isomorphism of the base.

theorem Ideal.IsInvertible.map_ringEquiv {A B : Type u} [CommRing A] [CommRing B] (e : A ≃+* B) {J : Ideal A} (hJ : J.IsInvertible) : (map (↑e) J).IsInvertible

Invertibility passes along ring isomorphisms.

theorem Ideal.IsInvertible.map_of_isLocalization_away {A : Type u} [CommRing A] {J : Ideal A} (hJ : J.IsInvertible) (s : A) (C : Type u) [CommRing C] [Algebra A C] [IsLocalization.Away s C] : (map (algebraMap A C) J).IsInvertible

Invertibility passes to any localization away from an element.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_affineBasicOpen_eq_map {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) (s : ↑(X.presheaf.obj (Opposite.op ↑U))) : J.ideal (X.affineBasicOpen s) = Ideal.map (algebraMap ↑(X.presheaf.obj (Opposite.op ↑U)) ↑(X.presheaf.obj (Opposite.op (X.basicOpen s)))) (J.ideal U)

The ideal of J on a basic open D(s) ⊆ U is the extension of J(U) along the localization map Γ(X, U) → Γ(X, D(s)).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_regular_generator_affineBasicOpen {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) {f : ↑(X.presheaf.obj (Opposite.op ↑U))} (hf : f ∈ nonZeroDivisors ↑(X.presheaf.obj (Opposite.op ↑U))) (hJ : J.ideal U = Ideal.span {f}) (s : ↑(X.presheaf.obj (Opposite.op ↑U))) : ∃ g ∈ nonZeroDivisors ↑(X.presheaf.obj (Opposite.op (X.basicOpen s))), J.ideal (X.affineBasicOpen s) = Ideal.span {g}

A regular generator of J(U) restricts to a regular generator of J(D(s)).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_ideal_affineBasicOpen {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) (hU : (J.ideal U).IsInvertible) (s : ↑(X.presheaf.obj (Opposite.op ↑U))) : (J.ideal (X.affineBasicOpen s)).IsInvertible

J(U) invertible implies J(D(s)) invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.fromSpec_mem_basicOpen_iff {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) (p : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))) (s : ↑(X.presheaf.obj (Opposite.op U))) : hU.fromSpec p ∈ X.basicOpen s ↔ s ∉ p.asIdeal

The point of U at a prime of Γ(X, U) lies in D(s) iff s is not in the prime.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_affineOpens_mem {X : Scheme} (x : ↥X) : ∃ (U : ↑X.affineOpens), x ∈ ↑U

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_of_forall_exists_affine {X : Scheme} (J : X.IdealSheafData) (h : ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ (J.ideal U).IsInvertible) : J.IsInvertible

Pointwise form of locality: J is invertible if every point has an affine open neighbourhood on which the ideal of J is invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.ideal {X : Scheme} (J : X.IdealSheafData) (hJ : J.IsInvertible) (U : ↑X.affineOpens) : (J.ideal U).IsInvertible

The ideal of an invertible ideal sheaf on any affine open is invertible (compare the proof of [TSPA, Tag 01WS]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_iff_forall_ideal {X : Scheme} (J : X.IdealSheafData) : J.IsInvertible ↔ ∀ (U : ↑X.affineOpens), (J.ideal U).IsInvertible

An ideal sheaf is invertible iff its ideal on every affine open is invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_iff_of_iSup_eq_top {X : Scheme} (J : X.IdealSheafData) {ι : Type u_1} (U : ι → ↑X.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) : J.IsInvertible ↔ ∀ (i : ι), (J.ideal (U i)).IsInvertible

An ideal sheaf is invertible iff its ideals on the members of an affine open cover are invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_top {X : Scheme} : ⊤.IsInvertible

The unit ideal sheaf is invertible.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.mul {X : Scheme} {J₁ J₂ : X.IdealSheafData} (h₁ : J₁.IsInvertible) (h₂ : J₂.IsInvertible) : (J₁ * J₂).IsInvertible

A product of invertible ideal sheaves is invertible: multiply the local generators on a common basic open.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.comap_of_isOpenImmersion {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] {J : X.IdealSheafData} (hJ : J.IsInvertible) : (J.comap f).IsInvertible

The comap of an invertible ideal sheaf along an open immersion is invertible.