31.2 Associated points to 31.15 Effective Cartier…

Section31.2 Associated points #

Section 31.2 of the Stacks Project, Tag 02OI. 11 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02OJ, a definition

Tag 02OJ in the Stacks Project.

Stacks.Divisors.IsAssociatedPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints.lean, line 57. The attribute's comment: “part (1)”.

A point x is associated to an 𝒪_X-module F when the maximal ideal of the local ring 𝒪_{X, x} is an associated prime of the stalk F_x.

abbrev IsAssociatedPoint (F : X.Modules) (x : X) : Prop

Stacks.Divisors.associatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints.lean, line 64. The attribute's comment: “part (2)”.

The set Ass(F) of points associated to an 𝒪_X-module F.

abbrev associatedPoints (F : X.Modules) : Set X

Stacks.Divisors.schemeAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints.lean, line 76. The attribute's comment: “part (3)”.

The associated points Ass(X) of a scheme X are the associated points of its structure sheaf.

abbrev schemeAssociatedPoints (X : Scheme.{u}) : Set X

Tag 02OK, a lemma

Tag 02OK in the Stacks Project.

AlgebraicGeometry.isAssociatedPoint_of_isAssociatedPrime_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/AffineComparison.lean, line 121. The attribute's comment: “part (1)”.

Stacks 02OK, part (1). An associated prime of the sections of a quasi-coherent sheaf on an affine open gives an associated point of the sheaf.

theorem isAssociatedPoint_of_isAssociatedPrime_sections {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] (U : X.Opens) (hU : IsAffineOpen U) {x : X} (hx : x ∈ U)
    (h : IsAssociatedPrimeStacks Γ(X, U) Γ(F, U) (hU.primeIdealOf ⟨x, hx⟩).asIdeal) :
    Stacks.Divisors.IsAssociatedPoint F x

AlgebraicGeometry.isAssociatedPrime_sections_of_isAssociatedPoint_of_fg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/AffineComparison.lean, line 163. The attribute's comment: “part (2)”.

Stacks 02OK, part (2). If the prime corresponding to an associated point is finitely generated, then it is associated to the module of sections on the affine open.

theorem isAssociatedPrime_sections_of_isAssociatedPoint_of_fg {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] (U : X.Opens) (hU : IsAffineOpen U) {x : X} (hx : x ∈ U)
    (hfg : (hU.primeIdealOf ⟨x, hx⟩).asIdeal.FG) (h : Stacks.Divisors.IsAssociatedPoint F x) :
    IsAssociatedPrimeStacks Γ(X, U) Γ(F, U) (hU.primeIdealOf ⟨x, hx⟩).asIdeal

AlgebraicGeometry.isAssociatedPrime_sections_iff_isAssociatedPoint_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/AffineComparison.lean, line 184. The attribute's comment: “locally Noetherian case”. References: EGA IV (3.1.2), “more general”.

Stacks 02OK, locally Noetherian case. On a locally Noetherian scheme, the prime corresponding to a point of an affine open is associated to the module of sections exactly when the point is associated to the sheaf.

theorem isAssociatedPrime_sections_iff_isAssociatedPoint_of_isLocallyNoetherian
    {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules) [F.IsQuasicoherent] (U : X.Opens)
    (hU : IsAffineOpen U) {x : X} (hx : x ∈ U) :
    IsAssociatedPrimeStacks Γ(X, U) Γ(F, U) (hU.primeIdealOf ⟨x, hx⟩).asIdeal ↔
      Stacks.Divisors.IsAssociatedPoint F x

Tag 05AD, a lemma

Tag 05AD in the Stacks Project.

AlgebraicGeometry.associatedPoints_subset_support, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Basic.lean, line 54.

Stacks Project, Tag 05AD. Every associated point of a sheaf of modules lies in its support.

lemma associatedPoints_subset_support {X : Scheme.{u}} (F : X.Modules) :
    Stacks.Divisors.associatedPoints F ⊆ SheafOfModules.supp F

Tag 05AE, a lemma

Tag 05AE in the Stacks Project.

AlgebraicGeometry.associatedPoints_subset_of_mono, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Basic.lean, line 82. The attribute's comment: “associated_points_subsheaf_subset”.

Stacks Project, Tag 05AE. The associated points of a subsheaf are associated points of the ambient sheaf.

theorem associatedPoints_subset_of_mono {X : Scheme.{u}} {F₁ F₂ : X.Modules} (f : F₁ ⟶ F₂)
    [Mono f] :
    Stacks.Divisors.associatedPoints F₁ ⊆ Stacks.Divisors.associatedPoints F₂

AlgebraicGeometry.associatedPoints_subset_union_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Basic.lean, line 135. The attribute's comment: “associated_points_middle_subset_union”.

Stacks Project, Tag 05AE. The associated points of the middle term of a short exact sequence lie in the union of those of its outer terms.

theorem associatedPoints_subset_union_of_shortExact {X : Scheme.{u}}
    (S : ShortComplex X.Modules) (hS : S.ShortExact) :
    Stacks.Divisors.associatedPoints S.X₂ ⊆
      Stacks.Divisors.associatedPoints S.X₁ ∪ Stacks.Divisors.associatedPoints S.X₃

Tag 05AF, a lemma

Tag 05AF in the Stacks Project.

AlgebraicGeometry.associatedPoints_inter_finite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Finite.lean, line 70.

Stacks Project, Tag 05AF. A coherent module on a locally Noetherian scheme has only finitely many associated points in a quasi-compact open subset.

theorem associatedPoints_inter_finite {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules)
    [F.IsCoherent] (U : X.Opens) (hU : IsCompact (U : Set X)) :
    (Stacks.Divisors.associatedPoints F ∩ (U : Set X)).Finite

Tag 05AG, a lemma

Tag 05AG in the Stacks Project.

AlgebraicGeometry.isZero_iff_associatedPoints_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Vanishing.lean, line 95.

A quasi-coherent module on a locally Noetherian scheme is zero if and only if its set of associated points is empty.

theorem isZero_iff_associatedPoints_eq_empty (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsQuasicoherent] :
    IsZero F ↔ Stacks.Divisors.associatedPoints F = ∅

Tag 05AI, an example

Tag 05AI in the Stacks Project.

AlgebraicGeometry.maximalIdeal_locallyNilpotent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Counterexample.lean, line 94. The attribute's comment: “locally nilpotent maximal ideal”.

Stacks 05AI. The maximal ideal of the square-zero-variable quotient is locally nilpotent.

theorem maximalIdeal_locallyNilpotent (k : Type u) [Field k] :
    (IsLocalRing.maximalIdeal (S k)).LocallyNilpotent

AlgebraicGeometry.no_maximalIdeal_annihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Counterexample.lean, line 101. The attribute's comment: “no maximal-ideal annihilator”.

Stacks 05AI. No element of the quotient has its maximal ideal as annihilator.

theorem no_maximalIdeal_annihilator (k : Type u) [Field k] (s : S k) :
    annElem s ≠ IsLocalRing.maximalIdeal (S k)

AlgebraicGeometry.spectrum_associatedPoints_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Counterexample.lean, line 113. The attribute's comment: “no associated points”.

Stacks 05AI. The spectrum of the square-zero-variable quotient has no associated points.

theorem spectrum_associatedPoints_eq_empty (k : Type u) [Field k] :
    Stacks.Divisors.schemeAssociatedPoints (Spec (.of (S k))) = ∅

Stacks.SquareZero.isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/SquareZeroQuotient.lean, line 96. The attribute's comment: “local ring”.

Stacks 05AI. The quotient by the squares of countably many variables is local.

theorem isLocalRing (k : Type u) [Field k] : IsLocalRing (S k)

Declarations registered for the tag:

assExact_S_eq_empty, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Counterexample.lean, line 108 (StacksFrontier): “no associated primes”.

Tag 0B3L, a lemma

Tag 0B3L in the Stacks Project.

AlgebraicGeometry.restriction_injective_of_associatedPoints_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Restriction.lean, line 202.

Stacks Project, Tag 0B3L. Restriction of sections of a quasi-coherent sheaf on a locally Noetherian scheme to an open subset containing all associated points is injective.

theorem restriction_injective_of_associatedPoints_subset (X : Scheme.{u})
    [IsLocallyNoetherian X] (F : X.Modules) [F.IsQuasicoherent] (U : X.Opens)
    (hU : Stacks.Divisors.associatedPoints F ⊆ (U : Set X)) :
    Function.Injective (F.presheaf.map (homOfLE (show U ≤ (⊤ : X.Opens) from le_top)).op)

Tag 05AH, a lemma

Tag 05AH in the Stacks Project.

AlgebraicGeometry.mem_associatedPoints_of_mem_supp_of_specialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/MinimalSupport.lean, line 133. The attribute's comment: “minimal point of the support”.

Stacks Project, Tag 05AH. A point of the support of a quasi-coherent module on a locally Noetherian scheme which is not a specialization of another point of the support is associated to the module.

theorem mem_associatedPoints_of_mem_supp_of_specialization (X : Scheme.{u})
    [IsLocallyNoetherian X] (F : X.Modules) [F.IsQuasicoherent] (x : X)
    (hx : x ∈ SheafOfModules.supp F)
    (hmin : ∀ y : X, y ∈ SheafOfModules.supp F → y ⤳ x → y = x) :
    x ∈ Stacks.Divisors.associatedPoints F

AlgebraicGeometry.mem_schemeAssociatedPoints_of_isGenericPoint_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/MinimalSupport.lean, line 155. The attribute's comment: “generic points of irreducible components”.

Stacks Project, Tag 05AH. Every generic point of an irreducible component of a locally Noetherian scheme is an associated point of the scheme.

theorem mem_schemeAssociatedPoints_of_isGenericPoint_irreducibleComponent (X : Scheme.{u})
    [IsLocallyNoetherian X] {Z : Set X} (hZ : Z ∈ irreducibleComponents X) {x : X}
    (hx : IsGenericPoint x Z) :
    x ∈ Stacks.Divisors.schemeAssociatedPoints X

Tag 0AVL, a lemma

Tag 0AVL in the Stacks Project.

Stacks.AlgebraicGeometry.AssociatedPointsMono.mono_of_stalk_injective_on_associatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AssociatedPointsMono/Basic.lean, line 267.

Stacks Project, Tag 0AVL. A morphism of quasi-coherent modules on a locally Noetherian scheme is a monomorphism if it is injective on the stalk at every associated point of its source.

theorem mono_of_stalk_injective_on_associatedPoints
    {X : Scheme.{u}} [IsLocallyNoetherian X] {F G : X.Modules}
    [F.IsQuasicoherent] [G.IsQuasicoherent] (f : F ⟶ G)
    (hf : ∀ x : X,
      Function.Injective
        ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
          ((PresheafOfModules.toPresheaf X.ringCatSheaf.obj).map f.val)).hom ∨
        x ∉ associatedPoints F) :
    Mono f

Tag 0AVM, a lemma

Tag 0AVM in the Stacks Project.

AlgebraicGeometry.isIso_of_stalk_isIso_or_depth_two_and_not_associated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Depth.lean, line 384.

Stacks Project, Tag 0AVM. A map from a coherent sheaf to a quasi-coherent sheaf is an isomorphism if, at every point, it is an isomorphism on stalks, or the source stalk has depth at least two and the point is not associated to the target.

The clause on associated points is what settles the degenerate case, and it cannot be dropped: Tag 00LI sets depth_I(M) = ∞ when IM = M, hence ⊤ for M = 0 (Module.depth_eq_top_of_subsingleton), so for F = 0 and G nonzero the alternative depth(F_x) ≥ 2 holds at every point on its own while 0 ⟶ G is not an isomorphism. See AlgebraicGeometry.isIso_of_stalk_isIso_or_depth_two_and_not_associated_of_isTorsionFree, which is the integral, torsion-free case of Tag 0AVS, and the counterexample recorded alongside it.

theorem isIso_of_stalk_isIso_or_depth_two_and_not_associated {X : Scheme.{u}}
    [IsLocallyNoetherian X] {F G : X.Modules} [F.IsQuasicoherent] [G.IsQuasicoherent]
    [F.IsCoherent] (f : F ⟶ G)
    (hf : ∀ x : X,
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) F.val x
      IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
        ((PresheafOfModules.toPresheaf X.ringCatSheaf.obj).map f.val)) ∨
      ((2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
          (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) ∧
        x ∉ Stacks.Divisors.associatedPoints G)) :
    IsIso f

Sources

LeanStacks.Divisors.IsAssociatedPoint · Stacks.Divisors.associatedPoints · Stacks.Divisors.schemeAssociatedPoints · AlgebraicGeometry.isAssociatedPoint_of_isAssociatedPrime_sections · AlgebraicGeometry.isAssociatedPrime_sections_of_isAssociatedPoint_of_fg · AlgebraicGeometry.isAssociatedPrime_sections_iff_isAssociatedPoint_of_isLocallyNoetherian · AlgebraicGeometry.associatedPoints_subset_support · AlgebraicGeometry.associatedPoints_subset_of_mono

Section31.3 Morphisms and associated points #

Section 31.3 of the Stacks Project, Tag 05DA. 1 tag here is carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05DB, a lemma

Tag 05DB in the Stacks Project.

AlgebraicGeometry.relativeAssassin_subset_associatedPoints_tensor_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassin/TensorPullback.lean, line 523. The attribute's comment: “the inclusion”. References: EGA IV (3.3.1), “inclusion (3.3.1.1)”; EGA IV (3.3.6), “⊇ only, one factor =”.

Stacks Project, Tag 05DB, inclusion. The associated points of the tensor product with a pulled-back module contain the images of the associated points of F on scheme-theoretic fibres over associated points of G.

theorem relativeAssassin_subset_associatedPoints_tensor_pullback
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (G : S.Modules)
    [F.IsQuasicoherent] [G.IsQuasicoherent]
    (hF : IsFlatOver f.toLRSHom.toShHom F) :
    (⋃ s ∈ Stacks.Divisors.associatedPoints G,
      f.fiberι s ''
        Stacks.Divisors.associatedPoints
          ((Scheme.Modules.pullback (f.fiberι s)).obj F)) ⊆
    Stacks.Divisors.associatedPoints
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf, ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (((Scheme.Modules.pullback f).obj G))))

AlgebraicGeometry.associatedPoints_tensor_pullback_eq_relativeAssassin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassin/TensorPullback.lean, line 556. The attribute's comment: “equality for a locally Noetherian base”. References: EGA IV (3.3.1), “equality (Noetherian)”; EGA IV (3.3.6), “one factor = base”.

Stacks Project, Tag 05DB, equality. Over a locally Noetherian base, the associated points of the tensor product are exactly the images of the associated points of F on fibres over associated points of G.

theorem associatedPoints_tensor_pullback_eq_relativeAssassin
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) (G : S.Modules)
    [F.IsQuasicoherent] [G.IsQuasicoherent]
    (hF : IsFlatOver f.toLRSHom.toShHom F)
    [IsLocallyNoetherian S] :
    Stacks.Divisors.associatedPoints
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨((X.toLocallyRingedSpace.toRingedSpace)).presheaf, ((X.toLocallyRingedSpace.toRingedSpace)).IsSheaf⟩).obj (F)).obj (((Scheme.Modules.pullback f).obj G)))) =
      ⋃ s ∈ Stacks.Divisors.associatedPoints G,
        f.fiberι s ''
          Stacks.Divisors.associatedPoints
            ((Scheme.Modules.pullback (f.fiberι s)).obj F)

Sources

LeanAlgebraicGeometry.relativeAssassin_subset_associatedPoints_tensor_pullback · AlgebraicGeometry.associatedPoints_tensor_pullback_eq_relativeAssassin

Section31.4 Embedded points #

Section 31.4 of the Stacks Project, Tag 05AJ. 7 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05AK, a definition

Tag 05AK in the Stacks Project.

AlgebraicGeometry.IsEmbeddedAssociatedPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Embedded.lean, line 69. The attribute's comment: “part (1)”.

Stacks 05AK, part (1). An associated point is embedded when it is a proper specialization of another associated point.

noncomputable abbrev IsEmbeddedAssociatedPoint {X : Scheme.{u}} (F : X.Modules) (x : X) : Prop

AlgebraicGeometry.IsEmbeddedPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Embedded.lean, line 80. The attribute's comment: “part (2)”.

Stacks 05AK, part (2). An embedded point of a scheme is an embedded associated point of its structure sheaf.

noncomputable abbrev IsEmbeddedPoint (X : Scheme.{u}) (x : X) : Prop

AlgebraicGeometry.IsEmbeddedComponent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Embedded.lean, line 88. The attribute's comment: “part (3)”.

Stacks 05AK, part (3). An embedded component is the closure of an embedded point.

noncomputable abbrev IsEmbeddedComponent (X : Scheme.{u}) (Z : Set X) : Prop

Tag 05AL, a lemma

Tag 05AL in the Stacks Project.

AlgebraicGeometry.mem_associatedPoints_of_isGenericPoint_irreducibleComponent_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/EmbeddedCharacterization.lean, line 83. The attribute's comment: “part (1)”. References: EGA IV (3.1.3), “special case”.

Stacks 05AL, part (1). The generic point of an irreducible component of the support of a coherent sheaf is associated to that sheaf.

theorem mem_associatedPoints_of_isGenericPoint_irreducibleComponent_supp (X : Scheme.{u})
    [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    {Z : Set (↥(SheafOfModules.supp F))}
    (hZ : Z ∈ irreducibleComponents (↥(SheafOfModules.supp F))) {x : X}
    (hx : IsGenericPoint x (Subtype.val '' Z)) :
    x ∈ Stacks.Divisors.associatedPoints F

AlgebraicGeometry.isEmbeddedAssociatedPoint_iff_not_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/EmbeddedCharacterization.lean, line 98. The attribute's comment: “part (2)”.

Stacks 05AL, part (2). An associated point of a coherent sheaf is embedded exactly when it is not generic in any irreducible component of its support.

theorem isEmbeddedAssociatedPoint_iff_not_genericPoint (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (x : X) :
    IsEmbeddedAssociatedPoint F x ↔
      x ∈ Stacks.Divisors.associatedPoints F ∧
        ¬ ∃ Z ∈ irreducibleComponents (↥(SheafOfModules.supp F)),
          IsGenericPoint x (Subtype.val '' Z)

AlgebraicGeometry.isEmbeddedPoint_iff_not_genericPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/EmbeddedCharacterization.lean, line 125. The attribute's comment: “embedded points of the scheme”.

Stacks 05AL, concluding assertion. The embedded points of a locally Noetherian scheme are precisely its non-generic associated points.

theorem isEmbeddedPoint_iff_not_genericPoint (X : Scheme.{u}) [IsLocallyNoetherian X] (x : X) :
    IsEmbeddedPoint X x ↔
      x ∈ Stacks.Divisors.schemeAssociatedPoints X ∧
        ¬ ∃ Z ∈ irreducibleComponents X, IsGenericPoint x Z

Tag 0346, a lemma

Tag 0346 in the Stacks Project.

AlgebraicGeometry.hasNoEmbeddedAssociatedPoints_iff_hasPropertySk_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Serre.lean, line 230.

Stacks Project, Tag 0346. A coherent sheaf on a locally Noetherian scheme has no embedded associated points if and only if it satisfies Serre's condition (S₁).

theorem hasNoEmbeddedAssociatedPoints_iff_hasPropertySk_one (X : Scheme.{u})
    [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent] :
    HasNoEmbeddedAssociatedPoints F ↔ SheafHasPropertySk X F 1

Tag 0BXG, a lemma

Tag 0BXG in the Stacks Project.

AlgebraicGeometry.isCohenMacaulay_iff_hasNoEmbeddedPoints_of_topologicalKrullDim_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EmbeddedPoints/DimensionOne.lean, line 91. References: EGA IV (7.2.1.1), “a) <=> c)”; EGA IV (5.7.8), “more general”.

A locally Noetherian scheme of dimension at most one is Cohen--Macaulay if and only if it has no embedded points.

theorem isCohenMacaulay_iff_hasNoEmbeddedPoints_of_topologicalKrullDim_le_one
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hX : topologicalKrullDim X ≤ 1) :
    IsCohenMacaulay X ↔ HasNoEmbeddedPoints X

Tag 083P, a lemma

Tag 083P in the Stacks Project.

AlgebraicGeometry.isSchemeTheoreticallyDense_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticallyDense.lean, line 189.

Stacks Project, Tag 083P. For an open subscheme of a locally Noetherian scheme, scheme-theoretic density is equivalent to topological density together with containment of every embedded point, and also to containment of every associated point.

theorem isSchemeTheoreticallyDense_tfae (X : Scheme.{u}) [IsLocallyNoetherian X] (U : X.Opens) :
    List.TFAE [
      Scheme.Opens.IsSchemeTheoreticallyDense U,
      Dense (U : Set X) ∧ (∀ x : X, IsEmbeddedPoint X x → x ∈ U),
      Stacks.Divisors.schemeAssociatedPoints X ⊆ (U : Set X)]

Tag 02OL, a lemma

Tag 02OL in the Stacks Project.

Stacks.AlgebraicGeometry.CoherentSubquotients.exists_greatest_isNowhereDenseCoherentSubobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/NowhereDense.lean, line 545. The attribute's comment: “greatest subsheaf”.

[Stacks, Tag 02OL]. Among the coherent subsheaves of a coherent sheaf F on a locally Noetherian scheme whose support is nowhere dense in the support of F there is a greatest one.

public theorem exists_greatest_isNowhereDenseCoherentSubobject
    {X : Scheme.{u}} [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent] :
    ∃ K : Subobject F,
      IsNowhereDenseCoherentSubobject F K ∧
        ∀ L : Subobject F, IsNowhereDenseCoherentSubobject F L → L ≤ K

Stacks.AlgebraicGeometry.CoherentSubquotients.supp_cokernel_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/NowhereDense.lean, line 562. The attribute's comment: “part (1): support of the quotient”.

[Stacks, Tag 02OL], part (1). The quotient of F by a coherent subsheaf with nowhere dense support has the same support as F.

public theorem supp_cokernel_eq {X : Scheme.{u}} [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (K : Subobject F)
    (hK : IsNowhereDenseCoherentSubobject F K) :
    (⟨(cokernel K.arrow).val, (cokernel K.arrow).isSheaf⟩ :
      RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp =
      (⟨F.val, F.isSheaf⟩ : RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp

Stacks.AlgebraicGeometry.CoherentSubquotients.cokernel_hasNoEmbeddedAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/NowhereDense.lean, line 739. The attribute's comment: “part (2): no embedded associated points”.

[Stacks, Tag 02OL], part (2). The quotient of F by a coherent subsheaf with nowhere dense support has no embedded associated points.

public theorem cokernel_hasNoEmbeddedAssociatedPoints
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (K : Subobject F)
    (hK : IsNowhereDenseCoherentSubobject F K)
    (hmax : ∀ L : Subobject F, IsNowhereDenseCoherentSubobject F L → L ≤ K) :
    AlgebraicGeometry.HasNoEmbeddedAssociatedPoints (cokernel K.arrow)

Stacks.AlgebraicGeometry.CoherentSubquotients.exists_denseOpen_cokernel_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentSubquotients/NowhereDense.lean, line 787. The attribute's comment: “part (3): agreement on a dense open”.

[Stacks, Tag 02OL], part (3). There is a dense open subset, meeting the support of F densely, over every open subset of which the quotient map is an isomorphism on sections.

public theorem exists_denseOpen_cokernel_iso
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (K : Subobject F)
    (hK : IsNowhereDenseCoherentSubobject F K) :
    ∃ U : X.Opens,
      Dense (U : Set X) ∧
      Dense {x : ↥((⟨F.val, F.isSheaf⟩ :
            RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp) | (x : X) ∈ U} ∧
          ∀ V : X.Opens, V ≤ U →
            IsIso ((cokernel.π K.arrow).val.app (op V))

Stacks.AlgebraicGeometry.EmbeddedPoints.exists_greatest_isNowhereDenseCoherentSubobject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EmbeddedPoints/Remove.lean, line 138. The attribute's comment: “greatest subsheaf”.

Stacks Project, Tag 02OL, maximal subsheaf. The coherent subsheaves whose support is nowhere dense in the support of F have a greatest member.

theorem exists_greatest_isNowhereDenseCoherentSubobject [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] :
    ∃ K : Subobject F,
      IsNowhereDenseCoherentSubobject F K ∧
        ∀ L : Subobject F, IsNowhereDenseCoherentSubobject F L → L ≤ K

Stacks.AlgebraicGeometry.EmbeddedPoints.supp_cokernel_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EmbeddedPoints/Remove.lean, line 216. The attribute's comment: “part (1): support of the quotient”.

Stacks Project, Tag 02OL, part (1). The quotient has the same support.

theorem supp_cokernel_eq [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent] (K : Subobject F)
    (hK : IsNowhereDenseCoherentSubobject F K) :
    (⟨(cokernel K.arrow).val, (cokernel K.arrow).isSheaf⟩ :
      RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp =
      (⟨F.val, F.isSheaf⟩ : RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp

Stacks.AlgebraicGeometry.EmbeddedPoints.cokernel_hasNoEmbeddedAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EmbeddedPoints/Remove.lean, line 245. The attribute's comment: “part (2): no embedded associated points”.

Stacks Project, Tag 02OL, part (2). The quotient by a greatest nowhere dense coherent subobject has no embedded associated points.

theorem cokernel_hasNoEmbeddedAssociatedPoints [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (K : Subobject F)
    (hK : IsNowhereDenseCoherentSubobject F K)
    (hmax : ∀ L : Subobject F, IsNowhereDenseCoherentSubobject F L → L ≤ K) :
    HasNoEmbeddedAssociatedPoints (cokernel K.arrow)

Stacks.AlgebraicGeometry.EmbeddedPoints.exists_denseOpen_cokernel_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EmbeddedPoints/Remove.lean, line 363. The attribute's comment: “part (3): agreement on a dense open”.

Stacks Project, Tag 02OL, part (3). The canonical quotient map becomes an isomorphism on a dense open meeting the support densely.

theorem exists_denseOpen_cokernel_iso [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (K : Subobject F) (hK : IsNowhereDenseCoherentSubobject F K) :
    ∃ U : X.Opens,
      Dense (U : Set X) ∧
      Dense {x : ↥((⟨F.val, F.isSheaf⟩ :
            RingedSpace.ModuleSheaf.{u} X.toRingedSpace).supp) | (x : X) ∈ U} ∧
          ∀ V : X.Opens, V ≤ U →
            IsIso ((cokernel.π K.arrow).val.app (op V))

Tag 02OM, a lemma

Tag 02OM in the Stacks Project.

AlgebraicGeometry.hasNoEmbeddedPoints_annihilatorIdeal_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 162. The attribute's comment: “absence of embedded points on the support”.

[Stacks, Tag 02OM]. The closed subscheme cut out by the annihilator of a coherent module with no embedded associated points has no embedded points.

theorem hasNoEmbeddedPoints_annihilatorIdeal_subscheme [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (hF : HasNoEmbeddedAssociatedPoints F) :
    HasNoEmbeddedPoints (annihilatorIdeal' F).subscheme

AlgebraicGeometry.exists_isCoherent_submodule_eq_annihilatorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 287. The attribute's comment: “coherence of the defining ideal”.

[Stacks, Tag 02OM]. The ideals cutting out the scheme-theoretic support over the affine opens are the sections of a coherent subsheaf of the structure sheaf, namely the annihilator sheaf of [Stacks, Tag 0H2H].

theorem exists_isCoherent_submodule_eq_annihilatorIdeal [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] :
    ∃ I : (SheafOfModules.unit X.ringCatSheaf).Submodule,
      I.toSheafOfModules.IsCoherent ∧
        I = Stacks.SheafOfModules.annihilatorSheaf X.toRingedSpace F ∧
          ∀ U : X.affineOpens, (annihilatorIdeal' F).ideal U =
            (show Ideal Γ(X, U.1) from I.toSubmodule.obj (op U.1))

AlgebraicGeometry.isCoherent_of_pushforward_iso_annihilatorIdeal_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 319. The attribute's comment: “coherence of the descended sheaf”.

[Stacks, Tag 02OM]. Every quasi-coherent module on the scheme-theoretic support whose direct image is F is itself coherent.

theorem isCoherent_of_pushforward_iso_annihilatorIdeal_subscheme [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (G : (annihilatorIdeal' F).subscheme.Modules)
    [G.IsQuasicoherent]
    (e : (Scheme.Modules.pushforward (annihilatorIdeal' F).subschemeι).obj G ≅ F) :
    G.IsCoherent

AlgebraicGeometry.hasNoEmbeddedAssociatedPoints_of_pushforward_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 336. The attribute's comment: “absence of embedded associated points on the descended sheaf”.

[Stacks, Tag 02OM]. Every quasi-coherent module on the scheme-theoretic support whose direct image is F inherits from F the absence of embedded associated points.

theorem hasNoEmbeddedAssociatedPoints_of_pushforward_iso [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (hF : HasNoEmbeddedAssociatedPoints F)
    (G : (annihilatorIdeal' F).subscheme.Modules) [G.IsQuasicoherent]
    (e : (Scheme.Modules.pushforward (annihilatorIdeal' F).subschemeι).obj G ≅ F) :
    HasNoEmbeddedAssociatedPoints G

AlgebraicGeometry.exists_coherent_module_on_annihilatorIdeal_subscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 414. The attribute's comment: “existence and properties of the descended sheaf”.

[Stacks, Tag 02OM]. A coherent module with no embedded associated points on a locally Noetherian scheme descends along the inclusion of its scheme-theoretic support to a coherent module with full support and again no embedded associated points.

theorem exists_coherent_module_on_annihilatorIdeal_subscheme [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (hF : HasNoEmbeddedAssociatedPoints F) :
    ∃ G : (annihilatorIdeal' F).subscheme.Modules,
      G.IsCoherent ∧ HasNoEmbeddedAssociatedPoints G ∧
        SheafOfModules.supp G = Set.univ ∧
          Nonempty ((Scheme.Modules.pushforward
            (annihilatorIdeal' F).subschemeι).obj G ≅ F)

AlgebraicGeometry.annihilatorIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticSupport/Basic.lean, line 142. The attribute's comment: “the ideal sheaf cutting out the support”. References: EGA IV (4.6.16); EGA IV (4.6.18); SGA 4 XVII (6.3.4), “special case”.

[Stacks, Tag 02OM] the ideal sheaf cutting out the scheme-theoretic support. The annihilators of the sections of a coherent module on a locally Noetherian scheme form an ideal sheaf; the closed subscheme it cuts out is the scheme-theoretic support of the module.

noncomputable def annihilatorIdeal [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent] :
    X.IdealSheafData

AlgebraicGeometry.exists_isCoherent_pushforward_iso_subschemeι_annihilatorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticSupport/Basic.lean, line 197. The attribute's comment: “existence of the coherent module on the support”.

[Stacks, Tag 02OM], the descended module. A coherent module on a locally Noetherian scheme is the direct image of a coherent module on its scheme-theoretic support.

This is [Stacks, Tag 087T]'s coherent descent applied to annihilatorIdeal_smul_eq_zero.

theorem exists_isCoherent_pushforward_iso_subschemeι_annihilatorIdeal [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] :
    ∃ G : (annihilatorIdeal F).subscheme.Modules, G.IsCoherent ∧
      Nonempty ((Scheme.Modules.pushforward (annihilatorIdeal F).subschemeι).obj G ≅ F)

AlgebraicGeometry.hasNoEmbeddedPoints_subscheme_annihilatorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticSupport/Basic.lean, line 345. The attribute's comment: “absence of embedded points on the support”.

[Stacks, Tag 02OM], no embedded points on the support. If a coherent module on a locally Noetherian scheme has no embedded associated points, then the closed subscheme cut out by its annihilator has no embedded points.

The subscheme's ring of functions over the preimage of an affine open U is Γ(X, U) ⧸ Ann Γ(F, U), which has no embedded primes by Tag 02M8 because Γ(F, U) has none by sections_hasNoEmbeddedAssociatedPrimes; an embedded point of the subscheme would give two nested associated primes there.

theorem hasNoEmbeddedPoints_subscheme_annihilatorIdeal [IsLocallyNoetherian X] (F : X.Modules)
    [F.IsCoherent] (hF : HasNoEmbeddedAssociatedPoints F) :
    HasNoEmbeddedPoints (annihilatorIdeal F).subscheme

AlgebraicGeometry.exists_isCoherent_pushforward_iso_of_hasNoEmbeddedAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SchemeTheoreticSupport/Basic.lean, line 400. The attribute's comment: “the descended module on a support without embedded points”.

[Stacks, Tag 02OM]. A coherent module without embedded associated points on a locally Noetherian scheme is the direct image of a coherent module on a closed subscheme without embedded points, and that module has full support.

This is the source's statement with clause (b) — that the descended module itself has no embedded associated points — omitted; see the module docstring.

theorem exists_isCoherent_pushforward_iso_of_hasNoEmbeddedAssociatedPoints [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsCoherent] (hF : HasNoEmbeddedAssociatedPoints F) :
    HasNoEmbeddedPoints (annihilatorIdeal F).subscheme ∧
      ∃ G : (annihilatorIdeal F).subscheme.Modules, G.IsCoherent ∧
        SheafOfModules.supp G = Set.univ ∧
        Nonempty ((Scheme.Modules.pushforward (annihilatorIdeal F).subschemeι).obj G ≅ F)

Declarations registered for the tag:

AlgebraicGeometry.annihilatorIdeal', declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 218 (StacksFrontier): “the ideal sheaf cutting out the support”.
Stacks.SheafOfModules.isCoherent_annihilatorSheaf, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/SchemeTheoreticSupport.lean, line 220 (StacksFrontier): “coherence of the annihilator”.

Sources

LeanAlgebraicGeometry.IsEmbeddedAssociatedPoint · AlgebraicGeometry.IsEmbeddedPoint · AlgebraicGeometry.IsEmbeddedComponent · AlgebraicGeometry.mem_associatedPoints_of_isGenericPoint_irreducibleComponent_supp · AlgebraicGeometry.isEmbeddedAssociatedPoint_iff_not_genericPoint · AlgebraicGeometry.isEmbeddedPoint_iff_not_genericPoint · AlgebraicGeometry.hasNoEmbeddedAssociatedPoints_iff_hasPropertySk_one · AlgebraicGeometry.isCohenMacaulay_iff_hasNoEmbeddedPoints_of_topologicalKrullDim_le_one

Section31.5 Weakly associated points #

Section 31.5 of the Stacks Project, Tag 056K. 12 tags here are carried by 19 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 056L, a definition

Tag 056L in the Stacks Project.

Stacks.Divisors.IsWeaklyAssociatedPoint, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociated.lean, line 87. The attribute's comment: “part (1)”.

Stacks 056L, part (1). A point x is weakly associated to an 𝒪_X-module F when the maximal ideal of the local ring 𝒪_{X, x} is a weakly associated prime of the stalk F_x, that is, when it is minimal among the primes containing the annihilator of some element of F_x.

abbrev IsWeaklyAssociatedPoint (F : X.Modules) (x : X) : Prop

Stacks.Divisors.weaklyAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociated.lean, line 95. The attribute's comment: “part (2)”.

Stacks 056L, part (2). The set WeakAss(F) of points weakly associated to an 𝒪_X-module F.

abbrev weaklyAssociatedPoints (F : X.Modules) : Set X

Stacks.Divisors.schemeWeaklyAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociated.lean, line 107. The attribute's comment: “part (3)”.

Stacks 056L, part (3). The weakly associated points WeakAss(X) of a scheme X are the weakly associated points of its structure sheaf.

abbrev schemeWeaklyAssociatedPoints (X : Scheme.{u}) : Set X

Tag 056M, a lemma

Tag 056M in the Stacks Project.

AlgebraicGeometry.isWeaklyAssociatedPrime_iff_isWeaklyAssociatedPoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/AffineComparison.lean, line 246.

Stacks Project, Tag 056M. On an affine open, a point is weakly associated to a quasi-coherent sheaf if and only if its corresponding prime ideal is weakly associated to the module of sections.

theorem isWeaklyAssociatedPrime_iff_isWeaklyAssociatedPoint {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] (U : X.Opens) (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) :
    IsWeaklyAssociatedPrime Γ(X, U) Γ(F, U) (hU.primeIdealOf ⟨x, hx⟩).asIdeal ↔
      Stacks.Divisors.IsWeaklyAssociatedPoint F x

Tag 05AM, a lemma

Tag 05AM in the Stacks Project.

AlgebraicGeometry.associatedPoints_subset_weaklyAssociatedPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 62. The attribute's comment: “associated points”.

Stacks Project, Tag 05AM. Every associated point of a sheaf of modules is weakly associated.

lemma associatedPoints_subset_weaklyAssociatedPoints {X : Scheme.{u}} (F : X.Modules) :
    Stacks.Divisors.associatedPoints F ⊆ Stacks.Divisors.weaklyAssociatedPoints F

AlgebraicGeometry.weaklyAssociatedPoints_subset_supp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 69. The attribute's comment: “weakly associated points”.

Stacks Project, Tag 05AM. Every weakly associated point of a sheaf of modules belongs to its support.

lemma weaklyAssociatedPoints_subset_supp {X : Scheme.{u}} (F : X.Modules) :
    Stacks.Divisors.weaklyAssociatedPoints F ⊆ SheafOfModules.supp F

Tag 05AN, a lemma

Tag 05AN in the Stacks Project.

AlgebraicGeometry.weaklyAssociatedPoints_subset_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 78. The attribute's comment: “subsheaf_inclusion”.

Stacks Project, Tag 05AN. In a short exact sequence of quasi-coherent modules on a scheme, the weakly associated points of the first module are weakly associated points of the middle module.

theorem weaklyAssociatedPoints_subset_of_shortExact {X : Scheme.{u}}
    (S : ShortComplex X.Modules) [S.X₁.IsQuasicoherent] [S.X₂.IsQuasicoherent]
    [S.X₃.IsQuasicoherent] (hS : S.ShortExact) :
    Stacks.Divisors.weaklyAssociatedPoints S.X₁ ⊆ Stacks.Divisors.weaklyAssociatedPoints S.X₂

AlgebraicGeometry.weaklyAssociatedPoints_subset_union_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 89. The attribute's comment: “middle_term_inclusion”.

Stacks Project, Tag 05AN. In a short exact sequence of sheaves of modules, every weakly associated point of the middle term is weakly associated to an outer term.

theorem weaklyAssociatedPoints_subset_union_of_shortExact {X : Scheme.{u}}
    (S : ShortComplex X.Modules) (hS : S.ShortExact) :
    Stacks.Divisors.weaklyAssociatedPoints S.X₂ ⊆
      Stacks.Divisors.weaklyAssociatedPoints S.X₁ ∪
        Stacks.Divisors.weaklyAssociatedPoints S.X₃

Tag 05AP, a lemma

Tag 05AP in the Stacks Project.

AlgebraicGeometry.isZero_iff_weaklyAssociatedPoints_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Vanishing.lean, line 47.

A quasi-coherent sheaf of modules is zero if and only if it has no weakly associated points.

theorem isZero_iff_weaklyAssociatedPoints_eq_empty {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] : IsZero F ↔ Stacks.Divisors.weaklyAssociatedPoints F = ∅

Tag 0B3M, a lemma

Tag 0B3M in the Stacks Project.

AlgebraicGeometry.restriction_injective_of_weaklyAssociatedPoints_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Restriction.lean, line 156.

Stacks Project, Tag 0B3M. Restriction of sections of a quasi-coherent module to an open containing all its weakly associated points is injective.

theorem restriction_injective_of_weaklyAssociatedPoints_subset {X : Scheme.{u}} (F : X.Modules)
    [F.IsQuasicoherent] (U : X.Opens)
    (hU : Stacks.Divisors.weaklyAssociatedPoints F ⊆ U) :
    Function.Injective (F.presheaf.map (homOfLE le_top : U ⟶ ⊤).op)

Tag 05AQ, a lemma

Tag 05AQ in the Stacks Project.

AlgebraicGeometry.mem_weaklyAssociatedPoints_of_mem_supp_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/MinimalSupport.lean, line 108. The attribute's comment: “minimal point of the support”.

Stacks Project, Tag 05AQ. A point of the support of a quasi-coherent module which is not a specialization of another point of the support is weakly associated to the module.

theorem mem_weaklyAssociatedPoints_of_mem_supp_of_specializes (X : Scheme.{u}) (F : X.Modules)
    [F.IsQuasicoherent] (x : X) (hx : x ∈ SheafOfModules.supp F)
    (hmin : ∀ y : X, y ∈ SheafOfModules.supp F → Specializes y x → y = x) :
    x ∈ Stacks.Divisors.weaklyAssociatedPoints F

AlgebraicGeometry.mem_weaklyAssociatedPointsOfScheme_of_isGenericPoint_irreducibleComponent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/MinimalSupport.lean, line 120. The attribute's comment: “generic points of irreducible components”.

Stacks Project, Tag 05AQ. Every generic point of an irreducible component of a scheme is weakly associated to its structure sheaf.

theorem mem_weaklyAssociatedPointsOfScheme_of_isGenericPoint_irreducibleComponent
    (X : Scheme.{u}) {Z : Set X} (hZ : Z ∈ irreducibleComponents X) {x : X}
    (hx : IsGenericPoint x Z) :
    x ∈ Stacks.Divisors.schemeWeaklyAssociatedPoints X

Tag 05AR, a lemma

Tag 05AR in the Stacks Project.

AlgebraicGeometry.mem_associatedPoints_iff_mem_weaklyAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 104. The attribute's comment: “finite_generated_maximal_ideal”.

Stacks Project, Tag 05AR. At a point whose local-ring maximal ideal is finitely generated, associated and weakly associated membership of a sheaf of modules coincide.

theorem mem_associatedPoints_iff_mem_weaklyAssociatedPoints {X : Scheme.{u}} (F : X.Modules)
    (x : X) (h : (IsLocalRing.maximalIdeal (X.presheaf.stalk x)).FG) :
    x ∈ Stacks.Divisors.associatedPoints F ↔
      x ∈ Stacks.Divisors.weaklyAssociatedPoints F

AlgebraicGeometry.associatedPoints_eq_weaklyAssociatedPoints, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/WeaklyAssociated.lean, line 120. The attribute's comment: “locally_noetherian”.

Stacks Project, Tag 05AR. On a locally Noetherian scheme, the associated points and weakly associated points of a sheaf of modules coincide.

lemma associatedPoints_eq_weaklyAssociatedPoints (X : Scheme.{u}) [IsLocallyNoetherian X]
    (F : X.Modules) :
    Stacks.Divisors.associatedPoints F = Stacks.Divisors.weaklyAssociatedPoints F

Tag 0AVN, a lemma

Tag 0AVN in the Stacks Project.

Stacks.AlgebraicGeometry.WeakAssPushforward.not_isWeaklyAssociatedPoint_pushforward_of_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/WeakAssPushforward.lean, line 282.

Stacks Project, Tag 0AVN. A point outside the image of a quasi-compact, quasi-separated morphism is not weakly associated to the pushforward of a quasi-coherent module.

Neither quasi-separatedness nor quasi-coherence is used in the proof.

public theorem not_isWeaklyAssociatedPoint_pushforward_of_not_mem_range
    {X S : Scheme.{u}} (f : X ⟶ S) [QuasiCompact f] [QuasiSeparated f]
    (F : X.Modules) [F.IsQuasicoherent] (s : S) (hs : s ∉ Set.range f) :
    ¬ IsWeaklyAssociatedPoint ((Scheme.Modules.pushforward f).obj F) s

Tag 0AVP, a lemma

Tag 0AVP in the Stacks Project.

AlgebraicGeometry.mono_of_stalk_injective_on_weaklyAssociatedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Mono.lean, line 69.

Stacks Project, Tag 0AVP. A map of quasi-coherent modules is a monomorphism if its map on stalks is injective at every weakly associated point of its source.

theorem mono_of_stalk_injective_on_weaklyAssociatedPoints {X : Scheme.{u}} {F G : X.Modules}
    [F.IsQuasicoherent] [G.IsQuasicoherent] (f : F ⟶ G)
    (hf : ∀ x : X,
      (Function.Injective
        ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
          ((PresheafOfModules.toPresheaf X.ringCatSheaf.obj).map f.val)).hom) ∨
        x ∉ Stacks.Divisors.weaklyAssociatedPoints F) :
    Mono f

Tag 0E9I, a lemma

Tag 0E9I in the Stacks Project.

AlgebraicGeometry.isIso_unit_restrict_pushforward_of_depth_ge_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/HartogsExtension/Basic.lean, line 116. The attribute's comment: “canonical sheaf isomorphism”. References: EGA IV (5.10.6), “sufficiency”.

Stacks Project, Tag 0E9I. A coherent sheaf with depth at least two along the complement of an open subscheme is canonically the pushforward of its restriction.

theorem isIso_unit_restrict_pushforward_of_depth_ge_two
    (X : Scheme.{u}) [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (U : X.Opens)
    (hdepth : ∀ x : X, x ∉ (U : Set X) →
      let M := TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x
      letI : Module (X.presheaf.stalk x) M :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          F.val x
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) M) :
    IsIso ((Scheme.Modules.pullbackPushforwardAdjunction U.ι).unit.app F)

AlgebraicGeometry.restriction_bijective_of_depth_ge_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/HartogsExtension/Basic.lean, line 176. The attribute's comment: “global sections”.

Stacks Project, Tag 0E9I. Under the same depth hypothesis, every section on the open subscheme extends uniquely to a global section.

theorem restriction_bijective_of_depth_ge_two
    (X : Scheme.{u}) [IsLocallyNoetherian X] (F : X.Modules) [F.IsCoherent]
    (U : X.Opens)
    (hdepth : ∀ x : X, x ∉ (U : Set X) →
      let M := TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x
      letI : Module (X.presheaf.stalk x) M :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          F.val x
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) M) :
    Function.Bijective
      (F.presheaf.map (homOfLE (show U ≤ (⊤ : X.Opens) from le_top)).op)

Tag 0EME, a lemma

Tag 0EME in the Stacks Project.

AlgebraicGeometry.weaklyAssociatedPointsOfScheme_eq_genericPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/Reduced.lean, line 66.

Stacks Project, Tag 0EME. The weakly associated points of a reduced scheme are exactly the generic points of its irreducible components.

theorem weaklyAssociatedPointsOfScheme_eq_genericPoints (X : Scheme.{u}) [IsReduced X] :
    Stacks.Divisors.schemeWeaklyAssociatedPoints X = genericPoints X

Sources

LeanStacks.Divisors.IsWeaklyAssociatedPoint · Stacks.Divisors.weaklyAssociatedPoints · Stacks.Divisors.schemeWeaklyAssociatedPoints · AlgebraicGeometry.isWeaklyAssociatedPrime_iff_isWeaklyAssociatedPoint · AlgebraicGeometry.associatedPoints_subset_weaklyAssociatedPoints · AlgebraicGeometry.weaklyAssociatedPoints_subset_supp · AlgebraicGeometry.weaklyAssociatedPoints_subset_of_shortExact · AlgebraicGeometry.weaklyAssociatedPoints_subset_union_of_shortExact

Section31.6 Morphisms and weakly associated points #

Section 31.6 of the Stacks Project, Tag 05EW. 6 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05EX, a lemma

Tag 05EX in the Stacks Project.

AlgebraicGeometry.weaklyAssociatedPoints_pushforward_subset_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/Pushforward.lean, line 112.

Stacks Project, Tag 05EX. Every weakly associated point of the pushforward along an affine morphism is the image of a weakly associated point of the original module.

theorem weaklyAssociatedPoints_pushforward_subset_image
    {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f]
    (F : X.Modules) [F.IsQuasicoherent] :
    Stacks.Divisors.weaklyAssociatedPoints ((Scheme.Modules.pushforward f).obj F) ⊆
      f '' Stacks.Divisors.weaklyAssociatedPoints F

Tag 05EY, a lemma

Tag 05EY in the Stacks Project.

AlgebraicGeometry.image_associatedPoints_eq_associatedPoints_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/Pushforward.lean, line 184. The attribute's comment: “associated points”.

Stacks Project, Tag 05EY. The associated points of a quasi-coherent pushforward along an affine morphism are the images of the associated points on the locally Noetherian source.

theorem image_associatedPoints_eq_associatedPoints_pushforward
    {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsQuasicoherent] :
    f '' Stacks.Divisors.associatedPoints F =
      Stacks.Divisors.associatedPoints ((Scheme.Modules.pushforward f).obj F)

AlgebraicGeometry.associatedPoints_pushforward_eq_weaklyAssociatedPoints_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/Pushforward.lean, line 197. The attribute's comment: “associated and weakly associated points of the pushforward”.

Stacks Project, Tag 05EY. The associated and weakly associated points of the pushforward along an affine morphism agree when the source is locally Noetherian.

theorem associatedPoints_pushforward_eq_weaklyAssociatedPoints_pushforward
    {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsQuasicoherent] :
    Stacks.Divisors.associatedPoints ((Scheme.Modules.pushforward f).obj F) =
      Stacks.Divisors.weaklyAssociatedPoints ((Scheme.Modules.pushforward f).obj F)

AlgebraicGeometry.weaklyAssociatedPoints_pushforward_eq_image_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/Pushforward.lean, line 212. The attribute's comment: “weakly associated points”.

Stacks Project, Tag 05EY. The weakly associated points of a quasi-coherent pushforward along an affine morphism are the images of the weakly associated points on the locally Noetherian source.

theorem weaklyAssociatedPoints_pushforward_eq_image_of_isAffineHom
    {X S : Scheme.{u}} (f : X ⟶ S) [IsAffineHom f] [IsLocallyNoetherian X]
    (F : X.Modules) [F.IsQuasicoherent] :
    Stacks.Divisors.weaklyAssociatedPoints ((Scheme.Modules.pushforward f).obj F) =
      f '' Stacks.Divisors.weaklyAssociatedPoints F

Tag 05EZ, a lemma

Tag 05EZ in the Stacks Project.

AlgebraicGeometry.weaklyAssociatedPoints_pushforward_eq_image_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/Pushforward.lean, line 224.

Stacks Project, Tag 05EZ. For a finite morphism, the weakly associated points of the pushforward of a quasi-coherent module are the images of its weakly associated points.

theorem weaklyAssociatedPoints_pushforward_eq_image_of_isFinite
    {X S : Scheme.{u}} (f : X ⟶ S) [IsFinite f]
    (F : X.Modules) [F.IsQuasicoherent] :
    Stacks.Divisors.weaklyAssociatedPoints ((Scheme.Modules.pushforward f).obj F) =
      f '' Stacks.Divisors.weaklyAssociatedPoints F

Tag 05F0, a lemma

Tag 05F0 in the Stacks Project.

AlgebraicGeometry.isWeaklyAssociatedPoint_pullback_of_isGenericPoint_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismWeaklyAssociated/FlatPullback.lean, line 154.

Stacks Project, Tag 05F0. A point which is generic in its fibre and at which a morphism is flat is weakly associated to the pullback of a module whenever its image is weakly associated to the original module.

theorem isWeaklyAssociatedPoint_pullback_of_isGenericPoint_fiber
    {X S : Scheme.{u}} (f : X ⟶ S) (G : S.Modules) (x : X)
    (hflat : IsFlatAt f.toLRSHom.toShHom x)
    (hgeneric : f.asFiber x ∈ genericPoints (f.fiber (f x)))
    (hweak : Stacks.Divisors.IsWeaklyAssociatedPoint G (f x)) :
    Stacks.Divisors.IsWeaklyAssociatedPoint ((Scheme.Modules.pullback f).obj G) x

Stacks.Divisors.IsWeaklyAssociatedPoint.pullback_of_isGenericPoint_fiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociatedFlatPullback.lean, line 146.

Stacks Project, Tag 05F0. A point which is generic in its fibre and at which a morphism is flat is weakly associated to the pullback of a module whenever its image is weakly associated to the original module.

theorem IsWeaklyAssociatedPoint.pullback_of_isGenericPoint_fiber
    {X S : Scheme.{u}} (f : X ⟶ S) (G : S.Modules) (x : X)
    (hflat : IsFlatAt f.toLRSHom.toShHom x)
    (hgeneric : f.asFiber x ∈ genericPoints (f.fiber (f x)))
    (hweak : IsWeaklyAssociatedPoint G (f x)) :
    IsWeaklyAssociatedPoint ((Scheme.Modules.pullback f).obj G) x

Tag 0CUC, a lemma

Tag 0CUC in the Stacks Project.

AlgebraicGeometry.isWeaklyAssociatedPoint_of_baseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/BaseChange.lean, line 303.

Stacks Project, Tag 0CUC. If a point of a field base change is weakly associated to the pullback of a quasi-coherent module, then its image is weakly associated to the original module.

lemma isWeaklyAssociatedPoint_of_baseChange {k K : Type u} [Field k] [Field K] [Algebra k K]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of k)) (F : X.Modules) [F.IsQuasicoherent]
    (y : (pullback f (Spec.map (CommRingCat.ofHom (algebraMap k K))) : Scheme.{u})) (x : X)
    (hyx : (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K)))).base y = x)
    (hy : Stacks.Divisors.IsWeaklyAssociatedPoint
      ((Scheme.Modules.pullback
        (pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap k K))))).obj F) y) :
    Stacks.Divisors.IsWeaklyAssociatedPoint F x

Tag 0EY0, a lemma

Tag 0EY0 in the Stacks Project.

Stacks.AlgebraicGeometry.PushforwardRegularity.isWeaklyRegular_stalk_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/Basic.lean, line 827. The attribute's comment: “pushforward_two_step”.

[Stacks, Tag 0EY0] part (5). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let F be a quasi-coherent 𝒪_X-module flat over S. If a, b is a weakly regular sequence on 𝒪_{S,s}, then it is weakly regular on the stalk of f_* F at s: a is a nonzerodivisor on (f_* F)_s and b is a nonzerodivisor on (f_* F)_s / a (f_* F)_s.

The source assumes in addition that a and b lie in the maximal ideal of 𝒪_{S,s}; that hypothesis is used there only to pass to the depth statements, so it is omitted. The conclusion is weak regularity rather than regularity because the pushforward stalk may be zero. Quasi-coherence of F is recorded because the source assumes it, but the proof does not use it: see isWeaklyRegular_stalk_pushforward'.

public theorem isWeaklyRegular_stalk_pushforward [QuasiCompact f] [QuasiSeparated f]
    [F.IsQuasicoherent] (s : S) (hflat : IsFlatOver f.toLRSHom.toShHom F)
    (a b : S.presheaf.stalk s)
    (hab : RingTheory.Sequence.IsWeaklyRegular (S.presheaf.stalk s) [a, b]) :
    RingTheory.Sequence.IsWeaklyRegular (TopCat.Presheaf.stalk (C := Ab.{u})
      ((Scheme.Modules.pushforward f).obj F).val.presheaf s) [a, b]

Stacks.AlgebraicGeometry.PushforwardRegularity.min_depth_le_depth_stalk_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/Depth.lean, line 103. The attribute's comment: “flat_pushforward_depth”.

[Stacks, Tag 0EY0] part (6). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let F be a quasi-coherent 𝒪_X-module flat over S. If the stalk (f_* F)_s is finite over 𝒪_{S,s}, then

min(2, depth 𝒪_{S,s}) ≤ depth (f_* F)_s.

The source assumes 𝒪_{S,s} Noetherian; that hypothesis is used there only through the description of the depth of a finite module as the supremum of the lengths of the weakly regular sequences in the maximal ideal, which holds over any commutative ring, so it is omitted.

public theorem min_depth_le_depth_stalk_pushforward [QuasiCompact f] [QuasiSeparated f]
    [F.IsQuasicoherent] (hflat : IsFlatOver f.toLRSHom.toShHom F) (s : S)
    (hfinite : Module.Finite (S.presheaf.stalk s) (TopCat.Presheaf.stalk (C := Ab.{u})
      ((Scheme.Modules.pushforward f).obj F).val.presheaf s)) :
    min (2 : ℕ∞) (Module.depth (S.presheaf.stalk s)
        (IsLocalRing.maximalIdeal (S.presheaf.stalk s)) (S.presheaf.stalk s)) ≤
      Module.depth (S.presheaf.stalk s) (IsLocalRing.maximalIdeal (S.presheaf.stalk s))
        (TopCat.Presheaf.stalk (C := Ab.{u})
          ((Scheme.Modules.pushforward f).obj F).val.presheaf s)

Stacks.AlgebraicGeometry.OpenStalkExactness.exists_nbhd_openStalkComparison_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/OpenStalkExactness.lean, line 508. The attribute's comment: “stalk exactness after shrinking the base”.

The step inside the proof of [Stacks, Tag 0EY0] that shrinks the base. For f quasi-compact and quasi-separated and F flat over S, every nonzerodivisor a ∈ 𝒪_{S,s} is the germ of a global section r of the structure sheaf of an open neighbourhood U ∋ s; the stalk comparison map c : (f_* F)_s ⟶ (f'_* F')_t for the square cutting out X ×_S U is semilinear over U.ι.stalkMap t; and an element of (f_* F)_s dies in (f'_* (F'/rF'))_t exactly when it is divisible by a.

This is the clause of Tag 0EY0 that is stated over a shrunken base; part (4) over S itself is isSMulRegular_stalk_pushforward.

theorem exists_nbhd_openStalkComparison_exact [QuasiCompact f] [QuasiSeparated f]
    (hflat : IsFlatOver f.toLRSHom.toShHom F) (s : S) (a : S.presheaf.stalk s)
    (ha : IsSMulRegular (S.presheaf.stalk s) a) :
    ∃ (U : S.Opens) (hs : s ∈ U) (r : Γ(U.toScheme, (⊤ : U.toScheme.Opens))),
      let t : U.toScheme := ⟨s, hs⟩
      U.ι.stalkMap t a = U.toScheme.presheaf.germ ⊤ t trivial r ∧
      (∀ (z : S.presheaf.stalk s)
          (x : TopCat.Presheaf.stalk (C := Ab.{u})
            ((Scheme.Modules.pushforward f).obj F).val.presheaf s),
        openStalkComparison f U F t (z • x) =
          U.ι.stalkMap t z • openStalkComparison f U F t x) ∧
      ∀ (m : (Scheme.Modules.pullback (pullback.fst f U.ι)).obj F ⟶
          (Scheme.Modules.pullback (pullback.fst f U.ι)).obj F),
        (∀ (W : (pullback f U.ι).Opens)
          (hW : W ≤ pullback.snd f U.ι ⁻¹ᵁ (⊤ : U.toScheme.Opens))
          (z : Γ((Scheme.Modules.pullback (pullback.fst f U.ι)).obj F, W)),
          m.app W z = ((pullback.snd f U.ι).appLE ⊤ W hW r) • z) →
        ∀ x : TopCat.Presheaf.stalk (C := Ab.{u})
            ((Scheme.Modules.pushforward f).obj F).val.presheaf s,
          (TopCat.Presheaf.stalkFunctor Ab.{u} t).map
              ((Scheme.Modules.pushforward (pullback.snd f U.ι)).map
                (cokernel.π m)).mapPresheaf
              (openStalkComparison f U F t x) = 0 ↔
            ∃ y, x = a • y

Stacks.AlgebraicGeometry.PushforwardRegularity.not_isAssociatedPoint_pushforward_of_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/OutsideImage.lean, line 52. The attribute's comment: “outside_association”.

Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let F be a quasi-coherent 𝒪_X-module. A point of S outside the image of f is not an associated point of f_* F.

public theorem not_isAssociatedPoint_pushforward_of_not_mem_range {X S : Scheme.{u}} (f : X ⟶ S)
    [QuasiCompact f] [QuasiSeparated f] (F : X.Modules) [F.IsQuasicoherent] (s : S)
    (hs : s ∉ Set.range f) :
    ¬ Stacks.Divisors.IsAssociatedPoint ((Scheme.Modules.pushforward f).obj F) s

Stacks.AlgebraicGeometry.PushforwardRegularity.two_le_depth_stalk_of_isIso_unit_of_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/OutsideImageDepth.lean, line 492. The attribute's comment: “part (3), for an open immersion rather than a general quasi-compact quasi-separated morphism, and with S locally Noetherian in place of the tag's Noetherian 𝒪_{S,s} — which is the form both consumers of hdepthOutside use”.

Stacks Project, Tag 0EY0, part (3), for an open immersion. Let X be a locally Noetherian scheme, let V ⊆ X be open and let ℋ be an 𝒪_X-module of finite type which is canonically the pushforward of its restriction to V. Then the stalk of ℋ at a point outside V has depth at least two.

Restriction Hom(𝒪_{X,y}, ℋ_y) → Hom(𝔪_y, ℋ_y) is bijective, which is the criterion Module.two_le_depth_of_bijective_restrict_maximalIdeal; its two halves are eq_zero_of_germ_smul_eq_zero and exists_germ_smul_eq.

public theorem two_le_depth_stalk_of_isIso_unit_of_notMem [IsLocallyNoetherian X]
    [H.IsFiniteType]
    (hunit : IsIso ((Scheme.Modules.pullbackPushforwardAdjunction V.ι).unit.app H))
    (y : X) (hy : y ∉ (V : Set X)) :
    (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk y)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk y))
      (TopCat.Presheaf.stalk (C := Ab.{u}) H.val.presheaf y)

Stacks.AlgebraicGeometry.PushforwardRegularity.two_le_depth_stalk_pushforward_of_notMem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/OutsideImageDepthGeneral.lean, line 579. The attribute's comment: “part (3)”.

[Stacks, Tag 0EY0] part (3). Let f : X ⟶ S be a quasi-compact and quasi-separated morphism of schemes and let F be a quasi-coherent 𝒪_X-module. Let s ∈ S be a point outside the image of f. If (f_* F)_s is a finite 𝒪_{S,s}-module and 𝒪_{S,s} is Noetherian, then

depth ((f_* F)_s) ≥ 2.

Restriction Hom(𝒪_{S,s}, (f_*F)_s) → Hom(𝔪_s, (f_*F)_s) is bijective, which is the criterion Module.two_le_depth_of_bijective_restrict_maximalIdeal; its two halves are eq_zero_of_germ_smul_eq_zero and exists_germ_smul_eq, both fed by the covering exists_nbhd_mem_basicOpen that replaces the source's base change to Spec 𝒪_{S,s}.

public theorem two_le_depth_stalk_pushforward_of_notMem_range [QuasiCompact f] [QuasiSeparated f]
    [F.IsQuasicoherent] (s : S) (hs : s ∉ Set.range f)
    (hnoeth : IsNoetherianRing (S.presheaf.stalk s))
    (hfinite : Module.Finite (S.presheaf.stalk s) (TopCat.Presheaf.stalk (C := Ab.{u})
      ((Scheme.Modules.pushforward f).obj F).val.presheaf s)) :
    (2 : ℕ∞) ≤ Module.depth (S.presheaf.stalk s)
      (IsLocalRing.maximalIdeal (S.presheaf.stalk s))
      (TopCat.Presheaf.stalk (C := Ab.{u})
        ((Scheme.Modules.pushforward f).obj F).val.presheaf s)

Declarations registered for the tag:

Stacks.AlgebraicGeometry.PushforwardRegularity.isSMulRegular_stalk_pushforward, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/Depth.lean, line 64 (StacksFrontier): “pushforward_nonzerodivisor”.
WeakAssPushforward.not_isWeaklyAssociatedPoint_pushforward_of_not_mem_range registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/PushforwardRegularity/OutsideImageDepthGeneral.lean, line 107 (StacksFrontier): “part (1)”.

Sources

LeanAlgebraicGeometry.weaklyAssociatedPoints_pushforward_subset_image · AlgebraicGeometry.image_associatedPoints_eq_associatedPoints_pushforward · AlgebraicGeometry.associatedPoints_pushforward_eq_weaklyAssociatedPoints_pushforward · AlgebraicGeometry.weaklyAssociatedPoints_pushforward_eq_image_of_isAffineHom · AlgebraicGeometry.weaklyAssociatedPoints_pushforward_eq_image_of_isFinite · AlgebraicGeometry.isWeaklyAssociatedPoint_pullback_of_isGenericPoint_fiber · Stacks.Divisors.IsWeaklyAssociatedPoint.pullback_of_isGenericPoint_fiber · AlgebraicGeometry.isWeaklyAssociatedPoint_of_baseChange

Section31.7 Relative assassin #

Section 31.7 of the Stacks Project, Tag 05AS. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05AT, a definition

Tag 05AT in the Stacks Project.

Stacks.Divisors.relativeAssassin, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/WeaklyAssociated.lean, line 176.

Stacks Project, Tag 05AT. The relative assassin Ass_{X/S}(F) of an 𝒪_X-module along f : X ⟶ S is the union over the points of S of the images in X of the associated points of the restriction of F to the scheme-theoretic fibre.

noncomputable def relativeAssassin (f : X ⟶ S) (F : X.Modules) : Set X

Tag 0CU5, a lemma

Tag 0CU5 in the Stacks Project.

AlgebraicGeometry.mem_relativeAssassin_of_mem_relativeAssassin_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassinTwo/AffineOpen.lean, line 568. The attribute's comment: “forward implication”.

Stacks Project, Tag 0CU5. A relative associated prime of the sections on an affine open gives a relative associated point of the sheaf.

public theorem mem_relativeAssassin_of_mem_relativeAssassin_sections
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) (V : S.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
    (hUV : U ≤ f ⁻¹ᵁ V) {x : X} (hx : x ∈ U) :
    letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
    letI : Module Γ(S, V) Γ(F, U) :=
      Module.compHom Γ(F, U) (f.appLE V U hUV).hom
    letI : IsScalarTower Γ(S, V) Γ(X, U) Γ(F, U) :=
      IsScalarTower.of_compHom Γ(S, V) Γ(X, U) Γ(F, U)
    (hU.primeIdealOf ⟨x, hx⟩) ∈
      Module.relativeAssassin Γ(S, V) Γ(X, U) Γ(F, U) →
      x ∈ Stacks.Divisors.relativeAssassin f F

AlgebraicGeometry.mem_relativeAssassin_sections_iff_of_locallyNoetherian_fibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassinTwo/AffineOpen.lean, line 605. The attribute's comment: “locally Noetherian equivalence”.

Stacks Project, Tag 0CU5. With locally Noetherian fibres, the relative associated primes of affine sections are exactly the relative associated points of the sheaf.

public theorem mem_relativeAssassin_sections_iff_of_locallyNoetherian_fibers
    {X S : Scheme.{u}} (f : X ⟶ S) (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) (V : S.Opens) (hU : IsAffineOpen U) (hV : IsAffineOpen V)
    (hUV : U ≤ f ⁻¹ᵁ V) (hf : ∀ s : S, IsLocallyNoetherian (f.fiber s))
    {x : X} (hx : x ∈ U) :
    letI : Algebra Γ(S, V) Γ(X, U) := (f.appLE V U hUV).hom.toAlgebra
    letI : Module Γ(S, V) Γ(F, U) :=
      Module.compHom Γ(F, U) (f.appLE V U hUV).hom
    letI : IsScalarTower Γ(S, V) Γ(X, U) Γ(F, U) :=
      IsScalarTower.of_compHom Γ(S, V) Γ(X, U) Γ(F, U)
    (hU.primeIdealOf ⟨x, hx⟩) ∈
      Module.relativeAssassin Γ(S, V) Γ(X, U) Γ(F, U) ↔
      x ∈ Stacks.Divisors.relativeAssassin f F

Tag 05DC, a lemma

Tag 05DC in the Stacks Project.

AlgebraicGeometry.mem_relativeAssassin_pullback_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/MorphismAssociatedPoints/BaseChange.lean, line 552.

Stacks Project, Tag 05DC. Under arbitrary base change, a point is in the relative assassin of the pulled-back quasi-coherent module exactly when its image is in the original relative assassin and its residue-field tensor product point is generic in an irreducible component.

theorem mem_relativeAssassin_pullback_iff
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (F : X.Modules)
    [F.IsQuasicoherent] [LocallyOfFiniteType f]
    (x' : pullback (C := Scheme.{u}) f g) :
    x' ∈ Stacks.Divisors.relativeAssassin (pullback.snd (C := Scheme.{u}) f g)
        ((Scheme.Modules.pullback (pullback.fst (C := Scheme.{u}) f g)).obj F) ↔
      (pullback.fst (C := Scheme.{u}) f g x' ∈ Stacks.Divisors.relativeAssassin f F ∧
        ∃ Z ∈ irreducibleComponents
            (Spec (Scheme.Pullback.Triplet.ofPoint x').tensor),
          IsGenericPoint (Scheme.Pullback.SpecOfPoint x') Z)

Tag 05KL, a remark

Tag 05KL in the Stacks Project.

AlgebraicGeometry.relativeAssassin_pullback_subset_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassinTwo/BaseChange.lean, line 194. The attribute's comment: “unconditional containment”.

Stacks Project, Tag 05KL. After arbitrary base change, the relative assassin of the pulled-back module is contained in the inverse image of the original relative assassin.

public theorem relativeAssassin_pullback_subset_preimage
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (F : X.Modules)
    [F.IsQuasicoherent] [LocallyOfFiniteType f] :
    Stacks.Divisors.relativeAssassin (pullback.snd (C := Scheme.{u}) f g)
        ((Scheme.Modules.pullback (pullback.fst (C := Scheme.{u}) f g)).obj F) ⊆
      (pullback.fst (C := Scheme.{u}) f g) ⁻¹'
        Stacks.Divisors.relativeAssassin f F

AlgebraicGeometry.preimage_relativeAssassin_eq_pullback_of_locallyQuasiFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassinTwo/BaseChange.lean, line 206. The attribute's comment: “equality for locally quasi-finite base change”.

Stacks Project, Tag 05KL. A locally quasi-finite base change pulls the relative assassin back exactly.

public theorem preimage_relativeAssassin_eq_pullback_of_locallyQuasiFinite
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (F : X.Modules)
    [F.IsQuasicoherent] [LocallyOfFiniteType f]
    [LocallyOfFiniteType g] [LocallyQuasiFinite g] :
    (pullback.fst (C := Scheme.{u}) f g) ⁻¹' Stacks.Divisors.relativeAssassin f F =
      Stacks.Divisors.relativeAssassin (pullback.snd (C := Scheme.{u}) f g)
        ((Scheme.Modules.pullback (pullback.fst (C := Scheme.{u}) f g)).obj F)

AlgebraicGeometry.preimage_relativeAssassin_eq_pullback_of_isAlgebraic_residueField, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeAssassinTwo/BaseChange.lean, line 225. The attribute's comment: “equality for algebraic residue-field extensions”.

Stacks Project, Tag 05KL. If every residue-field extension induced by the base-change morphism is algebraic, then it pulls the relative assassin back exactly.

public theorem preimage_relativeAssassin_eq_pullback_of_isAlgebraic_residueField
    {X S S' : Scheme.{u}} (f : X ⟶ S) (g : S' ⟶ S) (F : X.Modules)
    [F.IsQuasicoherent] [LocallyOfFiniteType f]
    (hg : ∀ s' : S',
      letI := (g.residueFieldMap s').hom.toAlgebra
      Algebra.IsAlgebraic (S.residueField (g s')) (S'.residueField s')) :
    (pullback.fst (C := Scheme.{u}) f g) ⁻¹' Stacks.Divisors.relativeAssassin f F =
      Stacks.Divisors.relativeAssassin (pullback.snd (C := Scheme.{u}) f g)
        ((Scheme.Modules.pullback (pullback.fst (C := Scheme.{u}) f g)).obj F)

Sources

LeanStacks.Divisors.relativeAssassin · AlgebraicGeometry.mem_relativeAssassin_of_mem_relativeAssassin_sections · AlgebraicGeometry.mem_relativeAssassin_sections_iff_of_locallyNoetherian_fibers · AlgebraicGeometry.mem_relativeAssassin_pullback_iff · AlgebraicGeometry.relativeAssassin_pullback_subset_preimage · AlgebraicGeometry.preimage_relativeAssassin_eq_pullback_of_locallyQuasiFinite · AlgebraicGeometry.preimage_relativeAssassin_eq_pullback_of_isAlgebraic_residueField

Section31.8 Relative weak assassin #

Section 31.8 of the Stacks Project, Tag 05AU. 3 tags here are carried by 3 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 05AV, a definition

Tag 05AV in the Stacks Project.

AlgebraicGeometry.relativeWeaklyAssociatedPoints, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/RelativeWeakAssassin.lean, line 54.

Stacks Project, Tag 05AV. The relative weak assassin of an 𝒪_X-module F along f : X ⟶ S, viewed as a set of points of X.

noncomputable abbrev relativeWeaklyAssociatedPoints {X S : Scheme.{u}} (f : X ⟶ S)
    (F : X.Modules) : Set X

Tag 05F2, a lemma

Tag 05F2 in the Stacks Project.

AlgebraicGeometry.relativeWeaklyAssociatedPoints_eq_relativeAssassin, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/AssociatedPoints/RelativeWeakAssassin.lean, line 62.

Stacks Project, Tag 05F2. For a morphism locally of finite type the relative weak assassin of a module is its relative assassin.

theorem relativeWeaklyAssociatedPoints_eq_relativeAssassin {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F : X.Modules) :
    relativeWeaklyAssociatedPoints f F = Stacks.Divisors.relativeAssassin f F

Tag 0CUD, a lemma

Tag 0CUD in the Stacks Project.

AlgebraicGeometry.relativeWeaklyAssociatedPoints_pushforward_eq_image, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RelativeWeakAssassin/FinitePushforward.lean, line 111.

Stacks Project, Tag 0CUD. The relative weak assassin of a finite direct image is the image of the relative weak assassin on the source.

theorem relativeWeaklyAssociatedPoints_pushforward_eq_image
    {Z X S : Scheme.{u}} (f : X ⟶ S) (i : Z ⟶ X) [IsFinite i]
    (F : Z.Modules) [F.IsQuasicoherent] :
    relativeWeaklyAssociatedPoints f ((Scheme.Modules.pushforward i).obj F) =
      i '' relativeWeaklyAssociatedPoints (i ≫ f) F

Sources

LeanAlgebraicGeometry.relativeWeaklyAssociatedPoints · AlgebraicGeometry.relativeWeaklyAssociatedPoints_eq_relativeAssassin · AlgebraicGeometry.relativeWeaklyAssociatedPoints_pushforward_eq_image

Section31.9 Fitting ideals #

Section 31.9 of the Stacks Project, Tag 0C3C. 7 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0C3D, a lemma

Tag 0C3D in the Stacks Project.

AlgebraicGeometry.fittingIdeal_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingIdeals.lean, line 199.

Stacks Project, Tag 0C3D. Fitting ideal sheaves of finite type quasi-coherent modules commute with arbitrary base change.

theorem fittingIdeal_comap {X Y : Scheme.{u}} (f : X ⟶ Y)
    (F : Y.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (k : ℤ) :
    (fittingIdeal F k).comap f =
      fittingIdeal ((Scheme.Modules.pullback f).obj F) k

Tag 0C3E, a lemma

Tag 0C3E in the Stacks Project.

AlgebraicGeometry.fittingIdeal_isFiniteType, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingIdeals.lean, line 257.

The Fitting ideals of a finitely presented sheaf of modules are quasi-coherent ideals of finite type.

lemma fittingIdeal_isFiniteType {X : Scheme.{u}} (F : X.Modules)
    [F.IsFinitePresentation] (r : ℕ) :
    Scheme.IdealSheafData.IsFiniteType (fittingIdealOfNat F r)

Tag 0CYX, a lemma

Tag 0CYX in the Stacks Project.

AlgebraicGeometry.fittingIdeal_zero_le_annihilatorIdeal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingSupport.lean, line 70. The attribute's comment: “scheme_theoretic_inclusion”.

Stacks Project, Tag 0CYX, part (1). The scheme-theoretic support of a finite type quasi-coherent module is a closed subscheme of the one cut out by its zeroth Fitting ideal: over every affine open the zeroth Fitting ideal is contained in the annihilator.

theorem fittingIdeal_zero_le_annihilatorIdeal : fittingIdeal F 0 ≤ annihilatorIdeal' F

AlgebraicGeometry.fittingIdeal_zero_support_eq_supp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingSupport.lean, line 105. The attribute's comment: “underlying_support”. References: SGA 7 VI (5.1), “more general”.

Stacks Project, Tag 0CYX, part (2). The closed subscheme cut out by the zeroth Fitting ideal of a finite type quasi-coherent module has the support of the module as its underlying closed set, so it agrees there with the scheme-theoretic support.

theorem fittingIdeal_zero_support_eq_supp :
    (fittingIdeal F 0).support = SheafOfModules.supp F

AlgebraicGeometry.exists_module_on_fittingSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingSupport.lean, line 150. The attribute's comment: “module_on_fitting_subscheme”.

Stacks Project, Tag 0CYX, part (3). A finite type quasi-coherent module is the direct image of a finite type quasi-coherent module on the closed subscheme cut out by its zeroth Fitting ideal, namely of its own pullback there.

theorem exists_module_on_fittingSubscheme :
    ∃ (G : (fittingIdeal F 0).subscheme.Modules)
      (_ : (Scheme.Modules.pushforward (fittingIdeal F 0).subschemeι).obj G ≅ F),
      G.IsFiniteType ∧ G.IsQuasicoherent

Declarations registered for the tag:

AlgebraicGeometry.supp_eq_annihilatorIdeal_support, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingSupport.lean, line 99 (StacksFrontier): “underlying_support”.

Tag 0C3F, a lemma

Tag 0C3F in the Stacks Project.

AlgebraicGeometry.isGeneratedByNear_iff_fittingIdeal_stalk_eq_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/FittingIdeals/Basic.lean, line 526.

A finite type quasicoherent module is generated by r sections near a point if and only if the stalk of its rth Fitting ideal is the unit ideal.

public theorem isGeneratedByNear_iff_fittingIdeal_stalk_eq_top
    {X : Scheme.{u}} (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (r : ℕ) (s : X) :
    IsGeneratedByNear F r s ↔ IdealSheafData.stalk (fittingIdeal F r) s = ⊤

Tag 0C3G, a lemma

Tag 0C3G in the Stacks Project.

AlgebraicGeometry.finiteLocallyFreeOfRank_tfae_fittingIdeal, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FittingRank/Basic.lean, line 589.

Stacks Project, Tag 0C3G. A finite type quasicoherent module is finite locally free of rank r if and only if its Fitting ideals vanish below r and are the unit ideal from r onward.

public lemma finiteLocallyFreeOfRank_tfae_fittingIdeal
    {X : Scheme.{u}} (F : X.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (r : ℕ) :
    List.TFAE [
      AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFreeOfRank F r,
      (r = 0 ∨ AlgebraicGeometry.fittingIdeal F (r - 1) = ⊥) ∧
        AlgebraicGeometry.fittingIdeal F r = ⊤,
      (∀ k < r, AlgebraicGeometry.fittingIdeal F k = ⊥) ∧
        (∀ k, r ≤ k → AlgebraicGeometry.fittingIdeal F k = ⊤)]

Tag 05P8, a lemma

Tag 05P8 in the Stacks Project.

AlgebraicGeometry.fittingClosedSubscheme_antitone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Exhaustion.lean, line 65. The attribute's comment: “the Fitting ideals cut out a descending chain of closed subschemes”.

The closed subschemes cut out by the Fitting ideals of a quasi-coherent module of finite type decrease with the index: for i ≤ j the j-th one admits a morphism over the base scheme to the i-th one, namely the inclusion of closed subschemes coming from the inclusion of Fitting ideals.

theorem fittingClosedSubscheme_antitone {S : Scheme.{u}} (F : S.Modules) [F.IsFiniteType]
    [F.IsQuasicoherent] {i j : ℕ} (hij : i ≤ j) :
    Nonempty (fittingClosedSubscheme F (j : ℤ) ⟶ fittingClosedSubscheme F (i : ℤ))

AlgebraicGeometry.fittingClosedSubscheme_iInter_range_eq_empty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Exhaustion.lean, line 76. The attribute's comment: “property (1): the Fitting closed subschemes have empty intersection”.

The Fitting closed subschemes of a quasi-coherent module of finite type exhaust the base scheme: the images in S of the subschemes indexed by the natural numbers meet in the empty set. Indeed, if x lies in an affine open U whose module of sections is generated by n elements, then the n-th Fitting ideal is the unit ideal on U, so x avoids the n-th member.

theorem fittingClosedSubscheme_iInter_range_eq_empty {S : Scheme.{u}} (F : S.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] :
    (⋂ i : ℕ, Set.range (fittingClosedSubscheme F (i : ℤ)).hom.base) = ∅

AlgebraicGeometry.fittingClosedSubscheme_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/FinitePresentation.lean, line 85. The attribute's comment: “finite presentation of the morphism Z_r to S”.

Stacks Project, Tag 05P8. The closed subscheme of S cut out by the r-th Fitting ideal of a finitely presented sheaf of modules F is of finite presentation over S.

public theorem fittingClosedSubscheme_finitePresentation {S : Scheme.{u}} (F : S.Modules)
    [F.IsFinitePresentation] (r : ℕ) :
    FinitePresentation
      (@fittingClosedSubscheme S F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
        (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) (r : ℤ)).hom

AlgebraicGeometry.fittingGeneratorOpen_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/FinitePresentation.lean, line 100. The attribute's comment: “finite presentation of the morphism S minus Z_r to S”.

Stacks Project, Tag 05P8. The open complement in S of the closed subscheme cut out by the r-th Fitting ideal of a finitely presented sheaf of modules F — the locus where F is generated by r sections — is of finite presentation over S.

public theorem fittingGeneratorOpen_finitePresentation {S : Scheme.{u}} (F : S.Modules)
    [F.IsFinitePresentation] (r : ℕ) :
    FinitePresentation
      (@fittingGeneratorOpen S F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
        (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) r).ι

AlgebraicGeometry.locallyGenerated_iff_factorsThrough_fittingGeneratorOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/GeneratorOpen.lean, line 80. The attribute's comment: “property (2): representability of the functor of generation by <= r sections”.

Stacks Project, Tag 05P8. The pullback of a finite type quasi-coherent module F along f : T ⟶ S is generated by r sections near every point of T if and only if f factors uniquely through the open complement of the r-th Fitting closed subscheme of F.

public theorem locallyGenerated_iff_factorsThrough_fittingGeneratorOpen
    {S T : Scheme.{u}} (F : S.Modules) [F.IsFiniteType] [F.IsQuasicoherent]
    (r : ℕ) (f : T ⟶ S) :
    (∀ t : T, IsGeneratedByNear ((Scheme.Modules.pullback f).obj F) r t) ↔
      ∃! g : T ⟶ (fittingGeneratorOpen F r).toScheme,
        g ≫ (fittingGeneratorOpen F r).ι = f

AlgebraicGeometry.isImmersion_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/RankStratum.lean, line 78. The attribute's comment: “property (3): the rank r stratum is a locally closed subscheme”.

The structural morphism of the rank r Fitting stratum is a locally closed immersion: it is the inclusion of an open subscheme followed by a closed immersion.

public theorem isImmersion_fittingRankStratum {S : Scheme.{u}} (F : S.Modules)
    [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ) :
    IsImmersion (fittingRankStratum F r).hom

AlgebraicGeometry.rankRFunctor_representableBy_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/RankStratum.lean, line 199. The attribute's comment: “property (3): representability of the functor of local freeness of rank r”.

Stacks Project, Tag 05P8. The rank r functor of a finite type quasi-coherent module F on S is represented by the rank r Fitting stratum of F, a locally closed subscheme of S.

public theorem rankRFunctor_representableBy_fittingRankStratum {S : Scheme.{u}}
    (F : S.Modules) [F.IsFiniteType] [F.IsQuasicoherent] (r : ℕ) :
    Nonempty ((rankRFunctor S F r).RepresentableBy (fittingRankStratum F r))

AlgebraicGeometry.finitePresentation_fittingRankStratum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/RankStratumFinitePresentation.lean, line 102. The attribute's comment: “finite presentation of the morphism Z_(r-1) minus Z_r to S”.

Stacks Project, Tag 05P8. The structural morphism of the rank r Fitting stratum of a finitely presented sheaf of modules F on S — the locally closed subscheme of S over which F pulls back to a module finite locally free of rank r — is of finite presentation.

public theorem finitePresentation_fittingRankStratum {S : Scheme.{u}} (F : S.Modules)
    [F.IsFinitePresentation] (r : ℕ) :
    FinitePresentation
      (@fittingRankStratum S F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
        (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) r).hom

Stacks.Fitting.idealSheaf_monotone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Groupoids/FittingIdealSheaf.lean, line 157. The attribute's comment: “decreasing closed subschemes”.

Stacks Project, Tag 05P8. The Fitting ideal sheaves increase, so the closed subschemes they cut out form a decreasing chain.

theorem idealSheaf_monotone {X : Scheme.{u}} (F : X.Modules) : Monotone (idealSheaf F)

Tag 05P9, a lemma

Tag 05P9 in the Stacks Project.

AlgebraicGeometry.rankStratum_isFiniteLocallyFreeOfRank, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Flattening.lean, line 391. The attribute's comment: “rank on each stratum”.

Stacks Project, Tag 05P9. The module restricts to a finite locally free module of rank r on the r-th Fitting rank stratum.

public theorem rankStratum_isFiniteLocallyFreeOfRank (r : ℕ) :
    SheafOfModules.IsFiniteLocallyFreeOfRank.{u, u, u}
      ((Scheme.Modules.pullback
        (@fittingRankStratum S F (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
          (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) r).hom).obj F) r

AlgebraicGeometry.flat_iff_existsUnique_lift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Flattening.lean, line 404. The attribute's comment: “representability”.

Stacks Project, Tag 05P9. A pullback of a finitely presented module is flat exactly when the morphism to the base factors, necessarily uniquely, through the flattening stratification — the disjoint union of the Fitting rank strata.

public theorem flat_iff_existsUnique_lift {T : Scheme.{u}} (g : T ⟶ S) :
    SheafOfModules.IsFlat (C := TopologicalSpace.Opens T.toTopCat)
        (J := Opens.grothendieckTopology T.toTopCat) (O := T.sheaf)
        ((Scheme.Modules.pullback g).obj F) ↔
      ∃! h : T ⟶ @flatnessStratification S F
          (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
          (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F),
        h ≫ @flatnessStratificationHom S F
          (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
          (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F) = g

AlgebraicGeometry.flatnessStratification_finitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Flattening.lean, line 428. The attribute's comment: “finite presentation of the disjoint union”.

Stacks Project, Tag 05P9. The structural morphism of the flattening stratification is of finite presentation: it is locally of finite presentation because each stratum is, quasi-compact because the Fitting generator opens exhaust the base, and quasi-separated because it is injective.

public theorem flatnessStratification_finitePresentation :
    FinitePresentation (@flatnessStratificationHom S F
      (SheafOfModules.instIsFiniteTypeOfIsFinitePresentation F)
      (SheafOfModules.instIsQuasicoherentOfIsFinitePresentation F))

Declarations registered for the tag:

AlgebraicGeometry.finitePresentation_fittingRankStratum, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Flatness/FittingStratification/Flattening.lean, line 453 (StacksFrontier): “finite presentation of each stratum”.

Sources

LeanAlgebraicGeometry.fittingIdeal_comap · AlgebraicGeometry.fittingIdeal_isFiniteType · AlgebraicGeometry.fittingIdeal_zero_le_annihilatorIdeal · AlgebraicGeometry.fittingIdeal_zero_support_eq_supp · AlgebraicGeometry.exists_module_on_fittingSubscheme · AlgebraicGeometry.supp_eq_annihilatorIdeal_support · AlgebraicGeometry.isGeneratedByNear_iff_fittingIdeal_stalk_eq_top · AlgebraicGeometry.finiteLocallyFreeOfRank_tfae_fittingIdeal

Section31.10 The singular locus of a morphism #

Section 31.10 of the Stacks Project, Tag 0C3H. 3 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0C3I, a lemma

Tag 0C3I in the Stacks Project.

AlgebraicGeometry.fittingIdeal_relativeDifferentials_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/FittingIdealsDifferentials.lean, line 44. References: SGA 7 VI (5.3), “(1)”.

For a cartesian square of schemes with right edge f : X ⟶ S locally of finite type, left edge f' : X' ⟶ S' and top edge g' : X' ⟶ X, the inverse image along g' of the r-th Fitting ideal sheaf of Ω_{X/S} is the r-th Fitting ideal sheaf of Ω_{X'/S'}: the closed subschemes cut out by the Fitting ideals of the relative differentials commute with arbitrary base change.

public theorem fittingIdeal_relativeDifferentials_comap {X' X S' S : Scheme.{u}} (g' : X' ⟶ X)
    (f' : X' ⟶ S') (f : X ⟶ S) (g : S' ⟶ S) (h : IsPullback g' f' f g)
    [LocallyOfFiniteType f] (r : ℤ) :
    (fittingIdeal (Scheme.Hom.relativeDifferentials f) r).comap g' =
      fittingIdeal (Scheme.Hom.relativeDifferentials f') r

Tag 0C3J, a lemma

Tag 0C3J in the Stacks Project.

Stacks.Discriminant.range_kaehlerDifferent_subschemeι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Different/KaehlerDifferent/UnramifiedLocus.lean, line 88.

Stacks Project, Tag 0BVY and Stacks Project, Tag 0C3J. For a morphism of schemes f : Y ⟶ X locally of finite type, the closed subscheme R ⊆ Y cut out by the Kähler different of f — equivalently, by the zeroth Fitting ideal of Ω_{Y/X}, which is what the Kähler different is — has as its underlying subset of Y exactly the set of points at which f is not unramified.

theorem range_kaehlerDifferent_subschemeι {Y X : Scheme.{u}} (f : Y ⟶ X)
    [LocallyOfFiniteType f] :
    Set.range (kaehlerDifferent f).subschemeι = {y : Y | ¬ UnramifiedAt f y}

Tag 0C3K, a lemma

Tag 0C3K in the Stacks Project.

AlgebraicGeometry.mem_fittingIdeal_relativeDifferentials_iff_not_smoothAt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/FittingIdeals/SingularLocus.lean, line 551. The attribute's comment: “pointwise characterisation of the nonsmooth locus”.

The nonsmooth locus is cut out by the d-th Fitting ideal of the relative differentials. For f : X ⟶ S flat and locally of finite presentation whose nonempty fibres are all equidimensional of dimension d, a point of X lies in the closed subscheme defined by the d-th Fitting ideal of Ω_{X/S} exactly when f is not smooth at that point.

theorem mem_fittingIdeal_relativeDifferentials_iff_not_smoothAt
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (d : ℕ)
    (hd : ∀ s : S, Nonempty (f.fiber s) →
      (TopologicalSpace.Equidimensional (f.fiber s) ∧
        topologicalKrullDim (f.fiber s) = (d : WithBot ℕ∞)))
    (x : X) :
    x ∈ Set.range
      (fittingIdeal (Scheme.Hom.relativeDifferentials f) (d : ℤ)).subschemeι ↔
      ¬ InfinitesimalLifting.SmoothAt f x

AlgebraicGeometry.range_subschemeι_fittingIdeal_relativeDifferentials, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/FittingIdeals/SingularLocus.lean, line 592.

The closed subscheme cut out by the d-th Fitting ideal of Ω_{X/S} is the nonsmooth locus. For f : X ⟶ S flat and locally of finite presentation whose nonempty fibres are all equidimensional of dimension d, that closed subscheme has as its underlying subset of X exactly the set of points at which f is not smooth.

theorem range_subschemeι_fittingIdeal_relativeDifferentials
    {X S : Scheme.{u}} (f : X ⟶ S) [Flat f]
    [LocallyOfFinitePresentation f] (d : ℕ)
    (hd : ∀ s : S, Nonempty (f.fiber s) →
      (TopologicalSpace.Equidimensional (f.fiber s) ∧
        topologicalKrullDim (f.fiber s) = (d : WithBot ℕ∞))) :
    Set.range (fittingIdeal (Scheme.Hom.relativeDifferentials f) (d : ℤ)).subschemeι =
      {x : X | ¬ InfinitesimalLifting.SmoothAt f x}

Sources

LeanAlgebraicGeometry.fittingIdeal_relativeDifferentials_comap · Stacks.Discriminant.range_kaehlerDifferent_subschemeι · AlgebraicGeometry.mem_fittingIdeal_relativeDifferentials_iff_not_smoothAt · AlgebraicGeometry.range_subschemeι_fittingIdeal_relativeDifferentials

Section31.11 Torsion free modules #

Section 31.11 of the Stacks Project, Tag 0AVQ. 13 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AXR, a lemma

Tag 0AXR in the Stacks Project.

AlgebraicGeometry.torsion_section_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TorsionSections.lean, line 224.

A section of a quasi-coherent module on an integral scheme is torsion at some stalk if and only if it is torsion at every stalk; equivalently, its germ at the generic point and its image in the pushforward from the generic point vanish.

theorem torsion_section_tfae
    (X : Scheme.{u}) [IsIntegral X] (F : X.Modules) [F.IsQuasicoherent]
    (U : X.Opens) [Nonempty U] (s : Γ(F, U)) :
    let η := genericPoint X
    let hη : η ∈ U :=
      ((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr
        (by simpa using (inferInstance : Nonempty U))
    letI : ∀ V : X.Opens, Decidable (η ∈ V) := fun V ↦ Classical.propDecidable _
    let isTorsionAt (x : X) (hx : x ∈ U) : Prop :=
      letI : Module (X.presheaf.stalk x) ↑(F.presheaf.stalk x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) F.val x
      IsTorsionElement (R := X.presheaf.stalk x)
        (M := ↑(F.presheaf.stalk x)) (F.presheaf.germ U x hx s)
    List.TFAE [
      ∃ (x : X) (hx : x ∈ U), isTorsionAt x hx,
      ∀ (x : X) (hx : x ∈ U), isTorsionAt x hx,
      F.presheaf.germ U η hη s = 0,
      ((skyscraperPresheafStalkAdjunction (C := AddCommGrpCat.{u}) η).unit.app
        F.presheaf).app (op U) s = 0]

Tag 0AVR, a definition

Tag 0AVR in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.IsTorsionSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Reflexive/Basic.lean, line 138. The attribute's comment: “part (1)”. References: EGA I (7.4.1), “torsion section”.

A local section of a module on a scheme is torsion if its germ at every point of its domain is a torsion element of the stalk, i.e. is annihilated by a nonzero element of the local ring.

public def IsTorsionSection (F : X.Modules) {U : X.Opens} (s : Γ(F, U)) : Prop

Stacks.AlgebraicGeometry.ReflexiveModules.IsTorsionFree, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Reflexive/Basic.lean, line 144. The attribute's comment: “part (2)”. References: EGA I (7.4.1), “torsion free”; EGA IV (20.1.5), “quasi-coherent case”.

A module on a scheme is torsion free if every torsion local section vanishes.

public def IsTorsionFree (F : X.Modules) : Prop

Tag 0AXS, a lemma

Tag 0AXS in the Stacks Project.

AlgebraicGeometry.isTorsionFree_iff_forall_isAffineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TorsionFree.lean, line 170.

A quasi-coherent module on an integral scheme is torsion free if and only if its sections on every affine open are torsion free over the ring of functions there.

theorem isTorsionFree_iff_forall_isAffineOpen
    {X : Scheme.{u}} [IsIntegral X] (F : X.Modules) [F.IsQuasicoherent] :
    IsTorsionFree F ↔
      ∀ U : X.Opens, IsAffineOpen U → Module.IsTorsionFree Γ(X, U) Γ(F, U)

Tag 0AXT, a lemma

Tag 0AXT in the Stacks Project.

Stacks.AlgebraicGeometry.TorsionQuasicoherent.torsionSubmodule_isQuasicoherent, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TorsionQuasicoherent/Basic.lean, line 316. The attribute's comment: “torsion_subsheaf_quasi_coherent”. References: EGA I (7.4.1), “quasi-coherence of T”.

The first assertion of [Stacks, Tag 0AXT]. The torsion submodule sheaf of a quasi-coherent module on an integral scheme is quasi-coherent.

instance torsionSubmodule_isQuasicoherent :
    (torsionSubmodule F).toSheafOfModules.IsQuasicoherent

Stacks.AlgebraicGeometry.TorsionQuasicoherent.isTorsionFree_torsionQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TorsionQuasicoherent/Quotient.lean, line 165. The attribute's comment: “the quotient F/F_tors is torsion free”. References: EGA I (7.4.1), “special case”.

The second assertion of [Stacks, Tag 0AXT]. The quotient of a quasi-coherent module on an integral scheme by its torsion subsheaf is torsion free.

theorem isTorsionFree_torsionQuotient :
    ReflexiveModules.IsTorsionFree (torsionQuotient F)

Tag 0AXU, a lemma

Tag 0AXU in the Stacks Project.

AlgebraicGeometry.isTorsionFree_of_isFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TorsionFree.lean, line 222.

A flat quasi-coherent module on an integral scheme is torsion free.

theorem isTorsionFree_of_isFlat {X : Scheme.{u}} [IsIntegral X]
    (F : X.Modules) [F.IsQuasicoherent]
    (hF : SheafOfModules.IsFlat.{u, u, u, u} (O := X.sheaf) F) :
    IsTorsionFree F

Tag 0AXV, a lemma

Tag 0AXV in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.isTorsionFree_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/TorsionFree/FlatPullback.lean, line 89. References: EGA IV (9.4.9), “partial”.

Stacks Project, Tag 0AXV. The flat pullback of a torsion-free quasi-coherent module on an integral scheme is torsion free.

theorem isTorsionFree_modulePullback {X Y : Scheme.{u}}
    [IsIntegral X] [IsIntegral Y] (f : X ⟶ Y) [Flat f]
    (G : Y.Modules) [G.IsQuasicoherent] (hG : IsTorsionFree G) :
    letI : ((Scheme.Modules.pullback f).obj G).IsQuasicoherent :=
      @AlgebraicGeometry.SheafOfModules.modulePullback_isQuasicoherent X.toRingedSpace
        Y.toRingedSpace f.toLRSHom.toShHom G ‹G.IsQuasicoherent›
    IsTorsionFree ((Scheme.Modules.pullback f).obj G)

Tag 0BCM, a lemma

Tag 0BCM in the Stacks Project.

AlgebraicGeometry.isIntegral_of_flat_of_isIntegral_genericFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/GenericFibre.lean, line 78.

Stacks Project, Tag 0BCM. If a flat morphism has integral target and integral generic fibre, then its source is integral.

theorem isIntegral_of_flat_of_isIntegral_genericFiber
    {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsIntegral Y]
    [IsIntegral (f.fiber (genericPoint Y))] : IsIntegral X

Tag 0AXW, a lemma

Tag 0AXW in the Stacks Project.

AlgebraicGeometry.isTorsionFree_iff_forall_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TorsionFree.lean, line 106.

A quasi-coherent module on an integral scheme is torsion free precisely when its stalk at every point is torsion free over the local ring at that point.

theorem isTorsionFree_iff_forall_stalk
    {X : Scheme.{u}} [IsIntegral X] (F : X.Modules) [F.IsQuasicoherent] :
    IsTorsionFree F ↔
      ∀ x : X,
        letI : Module (X.presheaf.stalk x) ↑(F.presheaf.stalk x) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) F.val x
        Module.IsTorsionFree (X.presheaf.stalk x) ↑(F.presheaf.stalk x)

Tag 0AXX, a lemma

Tag 0AXX in the Stacks Project.

AlgebraicGeometry.isTorsionFree_middle_of_shortExact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/TorsionFree.lean, line 201.

A short exact extension of torsion-free quasi-coherent modules on an integral scheme is torsion free.

lemma isTorsionFree_middle_of_shortExact {X : Scheme.{u}} [IsIntegral X]
    (S : ShortComplex X.Modules) (hS : S.ShortExact)
    [S.X₁.IsQuasicoherent] [S.X₂.IsQuasicoherent] [S.X₃.IsQuasicoherent]
    (h₁ : IsTorsionFree S.X₁)
    (h₃ : IsTorsionFree S.X₃) :
    IsTorsionFree S.X₂

Tag 0AXY, a lemma

Tag 0AXY in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.isTorsionFree_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/TorsionFree/IntegralNoetherian.lean, line 269. References: EGA IV (5.10.14), “integral case, (i)”.

Stacks Project, Tag 0AXY. The characterizations of a nonzero torsion-free coherent module on a locally Noetherian integral scheme: torsion freeness, uniqueness of the generic point as associated point, Serre's condition (S₁) with support at the generic point, and absence of embedded associated points with support at the generic point.

theorem isTorsionFree_tfae
    (X : Scheme.{u}) [IsLocallyNoetherian X] [IsIntegral X]
    (F : X.Modules) [F.IsCoherent] (hF : (SheafOfModules.supp F).Nonempty) :
    letI : F.IsQuasicoherent := isQuasicoherent_of_isCoherent F
    List.TFAE [
      IsTorsionFree F,
      Stacks.Divisors.associatedPoints F = {genericPoint X},
      genericPoint X ∈ SheafOfModules.supp F ∧ AlgebraicGeometry.SheafHasPropertySk X F 1,
      genericPoint X ∈ SheafOfModules.supp F ∧
        AlgebraicGeometry.HasNoEmbeddedAssociatedPoints F]

Tag 0CC4, a lemma

Tag 0CC4 in the Stacks Project.

AlgebraicGeometry.isTorsionFree_iff_isFiniteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/TorsionFreeDimensionOne.lean, line 68.

On an integral regular scheme of dimension at most one a coherent module is torsion free if and only if it is finite locally free.

theorem isTorsionFree_iff_isFiniteLocallyFree {X : Scheme.{u}} [IsIntegral X]
    (hregular : IsRegular X) (hdim : topologicalKrullDim X ≤ 1)
    (F : X.Modules) [_root_.SheafOfModules.IsCoherent F] :
    (let : F.IsQuasicoherent := _root_.isQuasicoherent_of_isCoherent F
     IsTorsionFree F) ↔ SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) F

Tag 0AXZ, a lemma

Tag 0AXZ in the Stacks Project.

AlgebraicGeometry.isTorsionFree_sheafHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/TorsionFree/SheafHom.lean, line 64. The attribute's comment: “torsion freeness”.

The torsion freeness clause of [Stacks, Tag 0AXZ]. On an integral scheme, the sheaf-hom SheafHom(F, G) from a module of finite presentation into a quasi-coherent torsion free module is torsion free.

The proof is the one of the source: torsion freeness of a quasi-coherent module on an integral scheme is a condition on the stalks, the stalk of SheafHom(F, G) at x is Hom_{𝒪_{X,x}}(F_x, G_x) by [Stacks, Tag 01CP], and a module of linear maps into a torsion free module is torsion free.

theorem isTorsionFree_sheafHom {X : Scheme.{u}} [IsIntegral X] (F G : X.Modules)
    [F.IsFinitePresentation] [G.IsQuasicoherent] (hG : IsTorsionFree G) :
    IsTorsionFree (sheafInternalHom (spaceRingedSite X.sheaf) F G)

AlgebraicGeometry.sheafHom_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomCoherent/Quasicoherent.lean, line 135. The attribute's comment: “quasi-coherence”.

The quasi-coherence clause of [Stacks, Tag 0AXZ]. On a scheme, the sheaf-hom SheafHom(F, G) from a module of finite presentation into a quasi-coherent module is quasi-coherent.

This is the assertion of Schemes, [Stacks, Tag 01LA] which makes the statement of Tag 0AXZ meaningful: torsion freeness is a notion for quasi-coherent modules. It is deduced from the first clause of [Stacks, Tag 01CQ], Stacks.SheafOfModules.InternalHom.exists_locally_isoKernel_sheafInternalHom.

theorem sheafHom_isQuasicoherent (F G : X.Modules)
    [F.IsFinitePresentation] [G.IsQuasicoherent] :
    SheafOfModules.IsQuasicoherent (R := X.ringCatSheaf)
      (sheafInternalHom (spaceRingedSite X.sheaf) F G)

Tag 0AVS, a lemma

Tag 0AVS in the Stacks Project.

AlgebraicGeometry.isIso_of_stalk_isIso_or_depth_two_and_not_associated_of_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/Reflexive.lean, line 180. The attribute's comment: “alternative (2) in the form Tag 0AV8 gives it, namely depth at least two at a point not associated to the target, which is the form the source's proof of this statement reduces to through Tag 0AV9, and asked for only at the generic point, the one point of an integral base at which a torsion-free target can have an associated point”.

Stacks Project, Tag 0AVS. Let X be an integral locally Noetherian scheme and f : F ⟶ G a map of quasi-coherent modules with F coherent and G torsion free. If at every point the map on stalks is an isomorphism, or the stalk of F has depth at least two and, at the generic point, that point is not associated to G, then f is an isomorphism.

Alternative (2) is the one of Tag 0AV8, the lemma the source's proof of this statement reduces to: Tag 0AVS is proved there as a translation of Tag 0AV9 into the language of schemes, Tag 0AV9 as a special case of Tag 0AV8, and the alternative (2) of Tag 0AV8 reads depth(M_p) ≥ 2 together with p ∉ Ass(N). Over an integral base with G torsion free the clause on associated points holds of itself at every point other than the generic one, by eq_genericPoint_of_isAssociatedPoint_of_isTorsionFree, which is why it is asked for here only at the generic point; that single point is where it does its work, by exists_counterexample_to_displayed_statement_of_tag_0AVS, which exhibits a map satisfying alternative (2) of Tag 0AVS as displayed at every point and failing to be an isomorphism.

theorem isIso_of_stalk_isIso_or_depth_two_and_not_associated_of_isTorsionFree
    {X : Scheme.{u}} [IsIntegral X] [IsLocallyNoetherian X]
    {F G : X.Modules} [F.IsQuasicoherent] [G.IsQuasicoherent] [F.IsCoherent]
    (f : F ⟶ G) (hG : Stacks.AlgebraicGeometry.ReflexiveModules.IsTorsionFree G)
    (hf : ∀ x : X,
      let : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) F.val x
      IsIso ((TopCat.Presheaf.stalkFunctor AddCommGrpCat.{u} x).map
        ((PresheafOfModules.toPresheaf X.ringCatSheaf.obj).map f.val)) ∨
      ((2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
          (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x) ∧
        (x = genericPoint X → x ∉ Stacks.Divisors.associatedPoints G))) :
    IsIso f

Sources

LeanAlgebraicGeometry.torsion_section_tfae · Stacks.AlgebraicGeometry.ReflexiveModules.IsTorsionSection · Stacks.AlgebraicGeometry.ReflexiveModules.IsTorsionFree · AlgebraicGeometry.isTorsionFree_iff_forall_isAffineOpen · Stacks.AlgebraicGeometry.TorsionQuasicoherent.torsionSubmodule_isQuasicoherent · Stacks.AlgebraicGeometry.TorsionQuasicoherent.isTorsionFree_torsionQuotient · AlgebraicGeometry.isTorsionFree_of_isFlat · Stacks.AlgebraicGeometry.ReflexiveModules.isTorsionFree_modulePullback

Section31.13 Reflexive modules #

Section 31.13 of the Stacks Project, Tag 0AVT. 14 tags here are carried by 36 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0AVU, a definition

Tag 0AVU in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.reflexiveHull, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveHull/Hull.lean, line 64. The attribute's comment: “reflexive hull”. References: SGA 3 VIB (13.1).

The reflexive hull F⁎⁎ of a module on a scheme: the dual of its dual.

public noncomputable abbrev reflexiveHull (F : X.Modules) : X.Modules

Stacks.AlgebraicGeometry.ReflexiveModules.toReflexiveHull, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveHull/Hull.lean, line 71. The attribute's comment: “canonical map to the reflexive hull”.

The canonical map F ⟶ F⁎⁎ to the reflexive hull, bundled with the formula that characterizes it: over an open U it sends a local section f to the functional on F^∨|_U whose component at the terminal object of the slice site over U is evaluation at f.

public noncomputable def toReflexiveHull (F : X.Modules) :
    { j : F ⟶ reflexiveHull F //
      ∀ (U : X.Opens) (f : Γ(F, U)) (lam : Γ(dualSheaf F, U)),
        (((j.val.app (op U)).hom f).app (op (Over.mk (𝟙 U)))).hom lam =
          (lam.app (op (Over.mk (𝟙 U)))).hom f }

Stacks.AlgebraicGeometry.ReflexiveModules.isReflexive_iff_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveHull/Hull.lean, line 124. The attribute's comment: “reflexive predicate”.

Reflexivity of F is invertibility of any morphism F ⟶ F⁎⁎ satisfying the defining formula of the canonical map.

public theorem isReflexive_iff_isIso (F : X.Modules) (j : F ⟶ reflexiveHull F)
    (hj : ∀ (U : X.Opens) (f : Γ(F, U)) (lam : Γ(dualSheaf F, U)),
      (((j.val.app (op U)).hom f).app (op (Over.mk (𝟙 U)))).hom lam =
        (lam.app (op (Over.mk (𝟙 U)))).hom f) :
    IsReflexive F ↔ IsIso j

Tag 0AY0, a lemma

Tag 0AY0 in the Stacks Project.

AlgebraicGeometry.isReflexive_iff_sections_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/AffineLocalCriterion.lean, line 131.

A coherent module on an integral locally Noetherian scheme is reflexive if and only if its module of sections over every affine open is reflexive.

theorem isReflexive_iff_sections_isReflexive (X : Scheme.{u}) [IsIntegral X]
    [IsLocallyNoetherian X] (F : X.Modules) [_root_.SheafOfModules.IsCoherent F] :
    IsReflexive F ↔ ∀ (U : X.Opens), IsAffineOpen U → Module.IsReflexive Γ(X, U) Γ(F, U)

Tag 0AY2, a lemma

Tag 0AY2 in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.isTorsionFree_of_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Reflexive/DoubleDual.lean, line 212. The attribute's comment: “part (1)”.

A reflexive module on an integral scheme is torsion free.

public theorem isTorsionFree_of_isReflexive [IsIntegral X] (F : X.Modules)
    (hF : IsReflexive F) : IsTorsionFree F

Stacks.AlgebraicGeometry.ReflexiveModules.mono_toDoubleDual_iff_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveTorsionFree/Converse.lean, line 135. The attribute's comment: “part (2)”.

On an integral scheme, the canonical map of a coherent module to its double dual is a monomorphism if and only if the module is torsion free.

public theorem mono_toDoubleDual_iff_isTorsionFree [IsIntegral X] (F : X.Modules)
    [F.IsCoherent] : Mono (toDoubleDual F) ↔ IsTorsionFree F

Tag 0AY3, a lemma

Tag 0AY3 in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.isReflexive_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveStalk/ClosedPoints.lean, line 238.

Stacks Project, Tag 0AY3. For a coherent module F on a locally Noetherian scheme X, the following are equivalent:

F is reflexive, that is, the canonical map F ⟶ F^∨∨ is an isomorphism;

for every point x of X the stalk F_x is a reflexive 𝒪_{X,x}-module;

the same for every closed point x of X.

Integrality of X is not needed: reflexivity of a module of finite presentation is detected on stalks over an arbitrary commutative local ring.

public theorem isReflexive_tfae (X : Scheme.{u}) [IsLocallyNoetherian X] (F : X.Modules)
    [F.IsCoherent] :
    [IsReflexive F,
      ∀ x : X, Module.IsReflexive (ringStalk X.sheaf x) (modStalk F x),
      ∀ x : X, x ∈ closedPoints X →
        Module.IsReflexive (ringStalk X.sheaf x) (modStalk F x)].TFAE

Tag 0EBF, a lemma

Tag 0EBF in the Stacks Project.

AlgebraicGeometry.isCoherent_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentPullback/Basic.lean, line 48. The attribute's comment: “coherence of the pullback”.

Stacks Project, Tag 0EBF. The pullback of a coherent module along a morphism of schemes with locally Noetherian source is coherent.

public theorem isCoherent_pullback
    {X Y : Scheme.{u}} [IsLocallyNoetherian X]
    (f : X ⟶ Y) (G : Y.Modules) [G.IsCoherent] :
    ((Scheme.Modules.pullback f).obj G).IsCoherent

Stacks.AlgebraicGeometry.ReflexiveModules.isReflexive_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CoherentPullback/Reflexive.lean, line 114. The attribute's comment: “reflexivity of the pullback”.

The reflexivity clause of Stacks, Tag 0EBF: the pullback of a coherent reflexive module along a flat morphism of integral locally Noetherian schemes is reflexive.

Reflexivity is checked on stalks by Tag 0AY3, on the target to read off reflexivity of the stalks of G and on the source to put reflexivity of the stalks of f^*G back together; coherence of f^*G, which the source half needs, is AlgebraicGeometry.isCoherent_pullback, and that declaration carries the coherence clause of the tag.

public theorem isReflexive_pullback {X Y : Scheme.{u}}
    [IsIntegral X] [IsIntegral Y] [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [Flat f] (G : Y.Modules) [G.IsCoherent] (hG : IsReflexive G) :
    IsReflexive ((Scheme.Modules.pullback f).obj G)

Tag 0EBG, a lemma

Tag 0EBG in the Stacks Project.

AlgebraicGeometry.isReflexive_of_exact_of_isReflexive_of_isTorsionFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/ExactSequence.lean, line 54.

In an exact sequence 0 → ℱ → ℱ' → ℱ'' of coherent modules on an integral locally Noetherian scheme, if ℱ' is reflexive and ℱ'' is torsion free then ℱ is reflexive.

theorem isReflexive_of_exact_of_isReflexive_of_isTorsionFree {X : Scheme.{u}} [IsIntegral X]
    [IsLocallyNoetherian X] {F F' F'' : X.Modules} [_root_.SheafOfModules.IsCoherent F]
    [_root_.SheafOfModules.IsCoherent F'] [_root_.SheafOfModules.IsCoherent F'']
    (f : F ⟶ F') (g : F' ⟶ F'') [Mono f] (hfg : f ≫ g = 0)
    (hexact : (ShortComplex.mk f g hfg).Exact) (hF' : IsReflexive F')
    (hF'' : (letI : F''.IsQuasicoherent := _root_.isQuasicoherent_of_isCoherent F'';
      IsTorsionFree F'')) :
    IsReflexive F

Tag 0AY4, a lemma

Tag 0AY4 in the Stacks Project.

AlgebraicGeometry.sheafHom_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/SheafHomReflexive.lean, line 39.

On an integral locally Noetherian scheme, the internal Hom SheafHom(ℱ, 𝒢) of coherent modules is reflexive as soon as 𝒢 is.

theorem sheafHom_isReflexive (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
    (F G : X.Modules) [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (hG : IsReflexive G) :
    IsReflexive (sheafInternalHom (spaceRingedSite X.sheaf) F G)

Tag 0EBH, a remark

Tag 0EBH in the Stacks Project.

AlgebraicGeometry.hullReflectionAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentCategory.lean, line 82. The attribute's comment: “adjunction”.

On an integral locally Noetherian scheme, taking reflexive hulls is a left adjoint of the inclusion of the coherent reflexive modules into the coherent modules.

noncomputable def hullReflectionAdjunction : hullReflection X ⊣ inclusion X

AlgebraicGeometry.coherentReflexiveModules_hasFiniteBiproducts, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentCategory.lean, line 122. The attribute's comment: “additive”.

The coherent reflexive modules on an integral locally Noetherian scheme form an additive category: they have finite direct sums.

noncomputable instance coherentReflexiveModules_hasFiniteBiproducts :
    HasFiniteBiproducts (CoherentReflexiveModules X)

AlgebraicGeometry.CoherentReflexive.internalHomObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentInternalHom.lean, line 80. The attribute's comment: “internal_hom”.

Stacks Project, Tag 0EBH. The sheaf Hom of two coherent reflexive modules, as a coherent reflexive module: it is coherent by [Stacks, Tag 01Y2] and reflexive by [Stacks, Tag 0AY4].

noncomputable def internalHomObj (G H : CoherentReflexiveModules X) :
    CoherentReflexiveModules X

AlgebraicGeometry.CoherentReflexive.dualObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentInternalHom.lean, line 99. The attribute's comment: “dual”.

Stacks Project, Tag 0EBH. Every coherent reflexive module has a dual object in the category of coherent reflexive modules, namely ℋom_{𝒪_X}(ℱ, 𝒪_X).

noncomputable def dualObj (F : CoherentReflexiveModules X) : CoherentReflexiveModules X

AlgebraicGeometry.CoherentReflexive.isReflexive_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentKernels.lean, line 92. The attribute's comment: “kernels”.

Stacks Project, Tag 0EBH. The ordinary kernel of a morphism of coherent reflexive modules is reflexive: it is the kernel of a map into the reflexive, hence torsion-free, module 𝒢.

theorem isReflexive_kernel (f : F ⟶ G) : IsReflexive (kernel f.hom.hom)

AlgebraicGeometry.CoherentReflexive.kernelIsKernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentKernels.lean, line 123. The attribute's comment: “kernels”.

Stacks Project, Tag 0EBH. The ordinary kernel, with its ordinary inclusion, is a kernel in the category of coherent reflexive modules.

noncomputable def kernelIsKernel (f : F ⟶ G) :
    IsLimit (KernelFork.ofι (f := f) (kernelι f) (kernelι_comp f))

AlgebraicGeometry.CoherentReflexive.cokernelIsCokernel, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentKernels.lean, line 179. The attribute's comment: “cokernels”.

Stacks Project, Tag 0EBH. The reflexive hull of the ordinary cokernel, with the ordinary projection followed by the canonical map to the double dual, is a cokernel in the category of coherent reflexive modules.

noncomputable def cokernelIsCokernel (f : F ⟶ G) :
    IsColimit (CokernelCofork.ofπ (f := f) (cokernelπ f) (comp_cokernelπ f))

AlgebraicGeometry.CoherentReflexive.tensorObj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentTensor.lean, line 139. The attribute's comment: “tensor”.

Stacks Project, Tag 0EBH. The tensor product of the category of coherent reflexive modules: the reflexive hull of the ordinary tensor product.

noncomputable def tensorObj (F G : CoherentReflexiveModules X) : CoherentReflexiveModules X

AlgebraicGeometry.CoherentReflexive.tensorObjComm, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentTensor.lean, line 154. The attribute's comment: “symmetry”.

Stacks Project, Tag 0EBH. The tensor product of the category of coherent reflexive modules is symmetric: the hull of the braiding of the ordinary tensor product.

noncomputable def tensorObjComm (F G : CoherentReflexiveModules X) :
    tensorObj F G ≅ tensorObj G F

AlgebraicGeometry.CoherentReflexive.tensorHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentTensor.lean, line 187. The attribute's comment: “internal_hom”.

Stacks Project, Tag 0EBH. The internal-Hom adjunction of the category of coherent reflexive modules: morphisms out of the hull tensor product ℱ ⊗_𝒞 𝒢 are morphisms of ℱ into the internal Hom ℋom_{𝒪_X}(𝒢, ℋ).

noncomputable def tensorHomEquiv (F G H : CoherentReflexiveModules X) :
    (tensorObj F G ⟶ H) ≃ (F ⟶ internalHomObj G H)

AlgebraicGeometry.CoherentReflexive.tensorHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentTensor.lean, line 198. The attribute's comment: “internal_hom”.

Stacks Project, Tag 0EBH. The adjunction bijection is the currying map of [Stacks, Tag 01CN], applied after restricting along the canonical map from the ordinary tensor product to its double dual. This pins the bijection down.

theorem tensorHomEquiv_apply (F G H : CoherentReflexiveModules X)
    (f : tensorObj F G ⟶ H) :
    (tensorHomEquiv F G H f).hom.hom =
      Stacks.SheafOfModules.tensorHomEquiv X.toRingedSpace F.obj.obj G.obj.obj H.obj.obj
        (toDoubleDual ((((Stacks.SheafOfModules.Tensor.sheafTensor.{u, u, u, u, u}
          ⟨((X.toRingedSpace)).presheaf, ((X.toRingedSpace)).IsSheaf⟩).obj (F.obj.obj)).obj
            (G.obj.obj))) ≫ f.hom.hom)

AlgebraicGeometry.CoherentReflexive.tensorObjAssoc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/CoherentTensorAssoc.lean, line 211. The attribute's comment: “associativity”.

Stacks Project, Tag 0EBH. The tensor product of the category of coherent reflexive modules is associative.

noncomputable def tensorObjAssoc (F G K : CoherentReflexiveModules X) :
    tensorObj (tensorObj F G) K ≅ tensorObj F (tensorObj G K)

AlgebraicGeometry.isReflexive_reflexiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/HullCoherentReflexive.lean, line 48. The attribute's comment: “hull”.

The reflexive hull F^∨∨ of a coherent module on an integral locally Noetherian scheme is reflexive: it is the dual of the coherent module F^∨, and duals of coherent modules are reflexive.

theorem isReflexive_reflexiveHull (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
    (F : X.Modules) [_root_.SheafOfModules.IsCoherent F] : IsReflexive (reflexiveHull F)

AlgebraicGeometry.not_forall_fiberRank_one_tensorObj_dualObj_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneNotInvertible.lean, line 209. The attribute's comment: “unit_failure”.

On an integral locally Noetherian scheme a coherent reflexive module of rank one at the generic point need not have its dual as a tensor inverse for the hull tensor product.

theorem not_forall_fiberRank_one_tensorObj_dualObj_iso_unit :
    ¬ ∀ (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
        (F : CoherentReflexiveModules X),
        Scheme.Modules.fiberRank (F.obj.obj : X.Modules) (genericPoint X) = 1 →
        Nonempty ((tensorObj F (dualObj F)).obj.obj ≅ unitModule X)

AlgebraicGeometry.not_forall_rank_one_sheafHom_iso_dualObj_tensorObj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RankOneNotInvertible.lean, line 224. The attribute's comment: “hom_failure”.

On an integral locally Noetherian scheme the sheaf Hom of two coherent reflexive modules of rank one at every point need not be the hull tensor product of the dual of the first with the second.

theorem not_forall_rank_one_sheafHom_iso_dualObj_tensorObj :
    ¬ ∀ (X : Scheme.{u}) [IsIntegral X] [IsLocallyNoetherian X]
        (F G : CoherentReflexiveModules X),
        (∀ x : X, Module.rank (X.presheaf.stalk x)
          ((show X.Modules from F.obj.obj).presheaf.stalk x) = 1) →
        (∀ x : X, Module.rank (X.presheaf.stalk x)
          ((show X.Modules from G.obj.obj).presheaf.stalk x) = 1) →
        Nonempty (Stacks.SheafOfModules.sheafHomSpace X.toRingedSpace F.obj.obj G.obj.obj ≅
          (tensorObj (dualObj F) G).obj.obj)

Stacks.AlgebraicGeometry.ReflexiveEquivalence.isCoherent_doubleDual, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ReflexiveEquivalence/StalkDescent.lean, line 154. The attribute's comment: “hull”.

[Stacks, Tag 01Y2] for the double dual. The reflexive hull F^∨∨ of a coherent module on a locally Noetherian scheme is coherent. This is the coherence half of the hull assertion of [Stacks, Tag 0EBH].

public lemma isCoherent_doubleDual [IsLocallyNoetherian X] (F : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] :
    _root_.SheafOfModules.IsCoherent (dualSheaf (dualSheaf F))

Stacks.AlgebraicGeometry.InternalHomLocalKernel.reflexiveHullAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomLocalKernel/Basic.lean, line 453. The attribute's comment: “adjunction”.

Stacks Tag 0EBH. On an integral locally Noetherian scheme the double-dual functor is left adjoint to the inclusion of coherent reflexive modules into coherent modules, with the canonical bidual map as its unit.

This is reflexiveHullAdjunction_of_isLocallyStructureKernel with its standing hypothesis discharged by isLocallyStructureKernel_dualSheaf_of_isCoherent.

noncomputable def reflexiveHullAdjunction (X : Scheme.{u})
    [IsIntegral X] [IsLocallyNoetherian X] :
    { p : (Σ L : ReflexiveHull.CoherentModules X ⥤ ReflexiveHull.CoherentReflexiveModules X,
        L ⊣ ReflexiveHull.inclusion X) //
      ∀ F : ReflexiveHull.CoherentModules X,
        ∃ e : (p.1.obj F).obj.obj = ReflexiveModules.reflexiveHull F.obj,
          (p.2.unit.app F).hom ≫ eqToHom e =
            (ReflexiveModules.toReflexiveHull F.obj).1 }

Tag 0AY5, a lemma

Tag 0AY5 in the Stacks Project.

AlgebraicGeometry.isReflexive_iff_stalk_isReflexive_or_depth_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/StalkDepthCriterion.lean, line 122.

Stacks Project, Tag 0AY5. A coherent module on an integral locally Noetherian scheme is reflexive if and only if at every point its stalk is either a reflexive module over the local ring there or has depth at least two.

theorem isReflexive_iff_stalk_isReflexive_or_depth_two (X : Scheme.{u}) [IsIntegral X]
    [IsLocallyNoetherian X] (F : X.Modules) [_root_.SheafOfModules.IsCoherent F] :
    IsReflexive F ↔
      ∀ x : X, Module.IsReflexive (X.presheaf.stalk x) (F.presheaf.stalk x) ∨
        (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (F.presheaf.stalk x)

Tag 0EBI, a lemma

Tag 0EBI in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.depth_stalk_ge_two_of_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Reflexive/ExtensionChain/Depth.lean, line 169. The attribute's comment: “part (1)”.

[Stacks, Tag 0EBI], part (1). A coherent reflexive module on a locally Noetherian scheme has depth at least two at every point where the local ring does.

public theorem depth_stalk_ge_two_of_isReflexive [IsLocallyNoetherian X] (F : X.Modules)
    [_root_.SheafOfModules.IsCoherent F]
    (hF : IsReflexive F) (x : X)
    (hx : (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (F.presheaf.stalk x)

Stacks.AlgebraicGeometry.ReflexiveModules.sheafHasPropertySk_two_of_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Reflexive/ExtensionChain/Depth.lean, line 240. The attribute's comment: “part (2)”.

[Stacks, Tag 0EBI], part (2). On a locally Noetherian scheme satisfying Serre's condition (S₂), every coherent reflexive module satisfies (S₂).

public theorem sheafHasPropertySk_two_of_isReflexive [IsLocallyNoetherian X] (F : X.Modules)
    [_root_.SheafOfModules.IsCoherent F]
    (hF : IsReflexive F) (hX : HasPropertySk X 2) :
    SheafHasPropertySk X F 2

Stacks.AlgebraicGeometry.ReflexiveStalkDepthTwo.two_le_depth_stalk_of_isCoherent_of_isReflexive, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveStalkDepthTwo/Basic.lean, line 57. The attribute's comment: “part (1)”.

On a locally Noetherian scheme, a coherent reflexive module has depth at least two at every point at which the structure sheaf has depth at least two.

theorem two_le_depth_stalk_of_isCoherent_of_isReflexive [IsLocallyNoetherian X]
    (G : X.Modules) (hc : G.IsCoherent) (hr : IsReflexive G) (x : X)
    (hx : (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
      (TopCat.Presheaf.stalk (C := Ab.{u}) G.val.presheaf x)

Tag 0EBJ, a lemma

Tag 0EBJ in the Stacks Project.

Stacks.AlgebraicGeometry.ReflexiveModules.reflexiveCoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ReflexiveOpenEquivalence/Pushforward.lean, line 158.

Stacks Project, Tag 0EBJ. Restriction to an open subscheme whose complement has structure-sheaf depth at least two is an equivalence on coherent reflexive modules; its inverse is direct image. Both identifications are natural.

This is reflexiveCoherentEquivalenceOfPushforward with its one hypothesis discharged by isCoherent_and_isReflexive_pushforward.

public noncomputable def reflexiveCoherentEquivalence (X : Scheme.{u})
    [AlgebraicGeometry.IsIntegral X] [IsLocallyNoetherian X] (U : X.Opens)
    (hdepth : ∀ x : X, x ∉ (U : Set X) →
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (X.presheaf.stalk x)) :
    Σ e : ReflexiveCoherentModules X ≌ ReflexiveCoherentModules U.toScheme,
      (e.functor ⋙ ObjectProperty.ι
          (fun F : U.toScheme.Modules =>
            F.IsCoherent ∧ IsReflexive F) ≅
        ObjectProperty.ι
          (fun F : X.Modules => F.IsCoherent ∧ IsReflexive F) ⋙
          Scheme.Modules.pullback U.ι) ×
      (e.inverse ⋙ ObjectProperty.ι
          (fun F : X.Modules => F.IsCoherent ∧ IsReflexive F) ≅
        ObjectProperty.ι
          (fun F : U.toScheme.Modules =>
            F.IsCoherent ∧ IsReflexive F) ⋙
          Scheme.Modules.pushforward U.ι)

Tag 0AY6, a lemma

Tag 0AY6 in the Stacks Project.

AlgebraicGeometry.isReflexive_isTorsionFree_propertyS2_extension_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/NormalCriterion.lean, line 345.

Let X be an integral locally Noetherian normal scheme and let F be a coherent 𝒪_X-module. The following are equivalent:

F is reflexive;

F is torsion free and satisfies Serre's condition (S₂);

there is an open subscheme j : U → X whose complement has codimension at least two at every point, such that j^*F is finite locally free and the canonical map F → j_*j^*F is an isomorphism.

theorem isReflexive_isTorsionFree_propertyS2_extension_tfae (X : Scheme.{u}) [IsIntegral X]
    [IsLocallyNoetherian X] [IsNormal X] (F : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] :
    List.TFAE [
      IsReflexive F,
      IsTorsionFree F ∧ SheafHasPropertySk X F 2,
      ∃ U : X.Opens,
        (∀ x : X, x ∉ U →
          (2 : ℕ∞) ≤ codimension (IrreducibleCloseds.closureSingleton x)) ∧
        SheafOfModules.IsFiniteLocallyFree (F.restrict U.ι) ∧
        IsIso ((Scheme.Modules.pullbackPushforwardAdjunction U.ι).unit.app F)]

Tag 0AY7, a lemma

Tag 0AY7 in the Stacks Project.

AlgebraicGeometry.exists_lift_toReflexiveHull_iff_codimension_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/HullExtension.lean, line 414.

On an integral locally Noetherian normal scheme, a linear map of generic stalks extends to a map into the reflexive hull of its target if and only if, at every point whose local ring has dimension one, it carries the image of the source stalk into the image of the target stalk.

theorem exists_lift_toReflexiveHull_iff_codimension_one (X : Scheme.{u}) [IsIntegral X]
    [IsLocallyNoetherian X] [IsNormal X] (F G : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] [_root_.SheafOfModules.IsCoherent G]
    (T : (G.presheaf.stalk (genericPoint X)) →ₗ[X.functionField]
      (F.presheaf.stalk (genericPoint X))) :
    (∃ e : G ⟶ reflexiveHull F,
      ∀ m : G.presheaf.stalk (genericPoint X),
        ((TopCat.Presheaf.stalkFunctor Ab (genericPoint X)).map
          (Scheme.Modules.Hom.mapPresheaf (X := X) e)) m =
          ((TopCat.Presheaf.stalkFunctor Ab (genericPoint X)).map
            (Scheme.Modules.Hom.mapPresheaf (X := X)
              (toReflexiveHull F).1)) (T m)) ↔
      ∀ x : X, ringKrullDim (X.presheaf.stalk x) = 1 →
        let h : genericPoint X ⤳ x := (genericPoint_spec X).specializes trivial
        Set.MapsTo T (Set.range (G.presheaf.stalkSpecializes h))
          (Set.range (F.presheaf.stalkSpecializes h))

Tag 0B3N, a lemma

Tag 0B3N in the Stacks Project.

AlgebraicGeometry.isReflexive_iff_isFiniteLocallyFree_of_isRegular_of_dim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Reflexive/RegularDimensionTwo.lean, line 155.

Stacks Project, Tag 0B3N. A coherent module on a regular scheme of dimension at most two is reflexive precisely when it is finite locally free.

theorem isReflexive_iff_isFiniteLocallyFree_of_isRegular_of_dim_le_two (X : Scheme.{u})
    (hX : IsRegular X) (hXdim : topologicalKrullDim X ≤ 2) (F : X.Modules)
    [_root_.SheafOfModules.IsCoherent F] :
    IsReflexive F ↔ SheafOfModules.IsFiniteLocallyFree (R := X.ringCatSheaf) F

Sources

LeanStacks.AlgebraicGeometry.ReflexiveModules.reflexiveHull · Stacks.AlgebraicGeometry.ReflexiveModules.toReflexiveHull · Stacks.AlgebraicGeometry.ReflexiveModules.isReflexive_iff_isIso · AlgebraicGeometry.isReflexive_iff_sections_isReflexive · Stacks.AlgebraicGeometry.ReflexiveModules.isTorsionFree_of_isReflexive · Stacks.AlgebraicGeometry.ReflexiveModules.mono_toDoubleDual_iff_isTorsionFree · Stacks.AlgebraicGeometry.ReflexiveModules.isReflexive_tfae · AlgebraicGeometry.isCoherent_pullback

Section31.14 Effective Cartier divisors #

Section 31.14 of the Stacks Project, Tag 01WQ. 14 tags here are carried by 26 declarations of the repository (all in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01WR, a definition

Tag 01WR in the Stacks Project.

Stacks.Divisors.IsLocallyPrincipal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier.lean, line 73. The attribute's comment: “locally_principal_closed_subscheme”.

Stacks Project, Tag 01WR (1). A closed subscheme of S is locally principal when its sheaf of ideals is locally generated by a single element: every point of S has an affine open neighbourhood on which the defining ideal is principal.

abbrev IsLocallyPrincipal {X : Scheme.{u}} (I : X.IdealSheafData) : Prop

Stacks.Divisors.IsEffectiveCartierDivisor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier.lean, line 79. The attribute's comment: “effective_cartier_divisor”. References: EGA II (8.9.4), “Setup hypothesis”.

Stacks Project, Tag 01WR (2). An effective Cartier divisor on S is a closed subscheme D ⊆ S whose ideal sheaf ℐ_D ⊆ 𝒪_S is an invertible 𝒪_S-module.

abbrev IsEffectiveCartierDivisor {X : Scheme.{u}} (I : X.IdealSheafData) : Prop

Tag 01WS, a lemma

Tag 01WS in the Stacks Project.

Stacks.CartierAffineLocalConverse.isEffectiveCartierDivisor_iff_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CartierAffineLocalConverse/Basic.lean, line 546. References: EGA IV (21.2.12), “partial”; EGA IV (21.6.5), “partial”.

Stacks Project, Tag 01WS. A closed subscheme D ⊆ X is an effective Cartier divisor if and only if every point of D has an affine open neighbourhood U in X on which D is cut out by a nonzerodivisor f ∈ Γ(X, U).

The forward direction is Stacks.CartierAffineLocal.exists_affineOpen_isRegular, which proves the stronger statement with the quantifier over all of X; the reverse direction is isEffectiveCartierDivisor_of_affineLocal.

The right-hand side renders the source's D ∩ U = Spec(A/fA) as the equation I.ideal U = Ideal.span {f} between ideals of A = Γ(X, U): I.ideal U is the ideal cutting D out on U, so the two say the same thing. The scheme-level packaging as an isomorphism D ×_X U ≅ Spec (A ⧸ (f)) compatible with the closed immersions is not produced here; see the module docstring.

theorem isEffectiveCartierDivisor_iff_isRegular (I : X.IdealSheafData) :
    Stacks.Divisors.IsEffectiveCartierDivisor I ↔
      ∀ x ∈ I.supportSet, ∃ V : X.affineOpens, x ∈ (V : Set X) ∧
        ∃ f : Γ(X, V.1), IsRegular f ∧ I.ideal V = Ideal.span {f}

Stacks.Divisors.isEffectiveCartierDivisor_iff_affineLocal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierAffineLocal.lean, line 524.

A closed subscheme is an effective Cartier divisor if and only if it is locally, on affine neighbourhoods of its support, the zero scheme of a nonzerodivisor.

theorem isEffectiveCartierDivisor_iff_affineLocal :
    IsEffectiveCartierDivisor I ↔
      ∀ x ∈ I.supportSet,
        ∃ (U : X.Opens) (hU : IsAffineOpen U),
          x ∈ (U : Set X) ∧
            ∃ f : Γ(X, U), IsRegular f ∧
              ∃ e : pullback I.subschemeι U.ι ≅
                  Spec (.of (Γ(X, U) ⧸ Ideal.span {f})),
                pullback.snd I.subschemeι U.ι ≫ hU.isoSpec.hom =
                  e.hom ≫ Spec.map
                    (CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {f})))

Stacks.Divisors.isEffectiveCartierDivisor_of_forall_mem_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/IdealSheafSections.lean, line 374. The attribute's comment: “(2) implies (1)”. References: EGA IV (21.2.12), “partial”.

Stacks Project, Tag 01WS, the direction (2) ⇒ (1). A closed subscheme which near every point of its support is cut out, on an affine open, by a single nonzerodivisor is an effective Cartier divisor.

The hypothesis is clause (2) of the tag: the points of I.support are the points of D, by AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι, and I.ideal U = (f) says that U ∩ D = Spec(Γ(X, U)/(f)), by AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app.

Near such a point the generator gives a rank-one dual basis of the ideal sheaf (Stacks.Divisors.dualBasisOneOfPrincipal), and off the support the ideal is the unit ideal, generated by the nonzerodivisor 1; the resulting dual bases cover X, so Stacks.Divisors.isEffectiveCartierDivisor_of_forall_exists_dualBasisOne applies.

The converse direction (1) ⇒ (2) is not proved: it needs that an invertible sheaf of modules is locally free of rank one, which is the descent step StacksFrontier.Algebra.Category.ModuleCat.Sheaf.Invertible records as missing.

theorem isEffectiveCartierDivisor_of_forall_mem_support (I : X.IdealSheafData)
    (h : ∀ x ∈ I.support, ∃ (U : X.affineOpens) (f : Γ(X, (U : X.Opens))),
      x ∈ (U : Set X) ∧ I.ideal U = Ideal.span {f} ∧
        f ∈ nonZeroDivisors Γ(X, (U : X.Opens))) :
    IsEffectiveCartierDivisor I

Tag 07ZT, a lemma

Tag 07ZT in the Stacks Project.

Stacks.Divisors.isAffineHom_ι_of_forall_support_inter_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/LocallyPrincipalAffineComplement.lean, line 108. The attribute's comment: “the complement is affine over the base already when the support is locally a zero locus of one section”.

Stacks Project, Tag 07ZT. Support-only form: if every point of X has an affine open neighbourhood V on which the support of the ideal sheaf I is the zero locus of a single section a, then the inclusion into X of any open W presenting the complement of that support is an affine morphism. The hypothesis asks nothing about the ideal I.ideal V beyond its radical, so it applies to ideal sheaves that are only locally principal up to radicals.

theorem isAffineHom_ι_of_forall_support_inter_eq
    (hI : ∀ x : X, ∃ (V : X.affineOpens) (_ : x ∈ (V.1 : Set X)) (a : Γ(X, V.1)),
      (I.support : Set X) ∩ (V.1 : Set X) = X.zeroLocus {a} ∩ (V.1 : Set X))
    {W : X.Opens} (hW : (W : Set X) = (I.support : Set X)ᶜ) :
    IsAffineHom (Scheme.Opens.ι W)

Stacks.Divisors.isAffineHom_ι_compl_support_of_isLocallyPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/LocallyPrincipalAffineComplement.lean, line 141.

Stacks Project, Tag 07ZT. Let X be a scheme and let Z ⊆ X be a locally principal closed subscheme, cut out by the ideal sheaf I. Then the inclusion of the open complement X \ Z into X is an affine morphism.

theorem isAffineHom_ι_compl_support_of_isLocallyPrincipal (hI : IsLocallyPrincipal I) :
    IsAffineHom (Scheme.Opens.ι I.support.compl)

Stacks.Divisors.isAffineHom_compl_of_isLocallyPrincipal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/LocallyPrincipalComplementAffine.lean, line 55.

Stacks Project, Tag 07ZT. The open complement of a locally principal closed subscheme is affine over the ambient scheme.

theorem isAffineHom_compl_of_isLocallyPrincipal (hI : IsLocallyPrincipal I) :
    IsAffineHom (Scheme.Opens.ι I.support.compl)

Tag 07ZU, a lemma

Tag 07ZU in the Stacks Project.

Stacks.Divisors.isSchemeTheoreticallyDense_compl_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierComplement.lean, line 196. The attribute's comment: “scheme-theoretic density”.

Stacks Project, Tag 07ZU (scheme-theoretic density). The complement of an effective Cartier divisor is scheme-theoretically dense in the ambient scheme.

theorem isSchemeTheoreticallyDense_compl_of_isEffectiveCartierDivisor
    (hI : IsEffectiveCartierDivisor I) :
    Scheme.Opens.IsSchemeTheoreticallyDense I.support.compl

Stacks.Divisors.isAffineHom_compl_of_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/LocallyPrincipalComplementAffine.lean, line 63. The attribute's comment: “affineness”.

Stacks Project, Tag 07ZU (affineness). The complement of an effective Cartier divisor is affine over the ambient scheme: an effective Cartier divisor is locally principal, so Tag 07ZT applies.

theorem isAffineHom_compl_of_isEffectiveCartierDivisor (hI : IsEffectiveCartierDivisor I) :
    IsAffineHom (Scheme.Opens.ι I.support.compl)

Tag 056N, a lemma

Tag 056N in the Stacks Project.

AlgebraicGeometry.topologicalKrullDimAt_subscheme_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/DimensionDrop.lean, line 88.

An effective Cartier divisor has smaller local dimension at every point where the ambient local dimension is finite.

theorem topologicalKrullDimAt_subscheme_lt {X : Scheme.{u}}
    (I : X.IdealSheafData) (hI : IsEffectiveCartierDivisor I)
    (x : I.subscheme)
    (hfin : topologicalKrullDimAt X (I.subschemeι x) < ⊤) :
    topologicalKrullDimAt I.subscheme x <
      topologicalKrullDimAt X (I.subschemeι x)

Tag 01WT, a definition

Tag 01WT in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Scheme.IdealSheafData.instMul registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierStalk/Operations.lean, line 42 (StacksFrontier): “product ideal sheaf”.
AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierStalk/Operations.lean, line 43 (StacksFrontier): “ideal of the sum”.
AlgebraicGeometry.Scheme.IdealSheafData.instMul registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DivisorSum/Basic.lean, line 98 (StacksFrontier): “the sum of two effective Cartier divisors, as the product of their sheaves of ideals”.
AlgebraicGeometry.Scheme.IdealSheafData.instPowNat registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DivisorSum/Basic.lean, line 101 (StacksFrontier): “the n-fold sum nD of the remark following the definition; the general sum ∑ nᵢ Dᵢ is the Finset product of these”. References: SGA 1 III (7.1), “partial”.
AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/DivisorSum/Basic.lean, line 105 (StacksFrontier): “the defining ideal of the sum on an affine open is the product of the two defining ideals, so the construction computes what the definition says”.

Tag 01WU, a lemma

Tag 01WU in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Sum.lean, line 69.

Stacks Project, Tag 01WU. The sum of two effective Cartier divisors on a scheme, that is, the closed subscheme cut out by the product of their ideal sheaves, is again an effective Cartier divisor.

theorem isEffectiveCartierDivisor_mul (I J : X.IdealSheafData)
    (hI : IsEffectiveCartierDivisor I) (hJ : IsEffectiveCartierDivisor J) :
    IsEffectiveCartierDivisor (I * J)

Tag 02ON, a lemma

Tag 02ON in the Stacks Project.

AlgebraicGeometry.exists_isEffectiveCartierDivisor_mul_eq_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Difference.lean, line 141.

Let D and D' be effective Cartier divisors on a scheme X with D ⊆ D' as closed subschemes, that is, with ℐ_{D'} ⊆ ℐ_D. Then there is an effective Cartier divisor E with D' = D + E, in the ideal-sheaf presentation ℐ_{D'} = ℐ_D · ℐ_E.

The divisor E is the quotient of ideal sheaves ℐ_{D'} : ℐ_D.

theorem exists_isEffectiveCartierDivisor_mul_eq_of_le (D D' : X.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) (hD' : IsEffectiveCartierDivisor D') (h : D' ≤ D) :
    ∃ E : X.IdealSheafData, IsEffectiveCartierDivisor E ∧ D' = D * E

Tag 07ZV, a lemma

Tag 07ZV in the Stacks Project.

AlgebraicGeometry.isEffectiveCartierDivisor_left_of_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Summands.lean, line 116. The attribute's comment: “effectivity of the first summand”.

Stacks Project, Tag 07ZV. If the product of the ideal sheaves of two closed subschemes of a scheme cuts out an effective Cartier divisor, then the first subscheme is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_left_of_mul (I J : X.IdealSheafData)
    (hIJ : IsEffectiveCartierDivisor (I * J)) : IsEffectiveCartierDivisor I

AlgebraicGeometry.isEffectiveCartierDivisor_right_of_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Summands.lean, line 148. The attribute's comment: “effectivity of the second summand”.

Stacks Project, Tag 07ZV. If the product of the ideal sheaves of two closed subschemes of a scheme cuts out an effective Cartier divisor, then the second subscheme is an effective Cartier divisor.

theorem isEffectiveCartierDivisor_right_of_mul (I J : X.IdealSheafData)
    (hIJ : IsEffectiveCartierDivisor (I * J)) : IsEffectiveCartierDivisor J

Tag 0C4R, a lemma

Tag 0C4R in the Stacks Project.

AlgebraicGeometry.mul_eq_inf_of_comap_isEffectiveCartierDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/Intersection.lean, line 198.

Stacks Project, Tag 0C4R. Let D, D' ⊆ X be effective Cartier divisors such that the scheme-theoretic intersection D ∩ D' is an effective Cartier divisor on D'. Then D + D' is the scheme-theoretic union of D and D'.

theorem mul_eq_inf_of_comap_isEffectiveCartierDivisor (D D' : X.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) (hD' : IsEffectiveCartierDivisor D')
    (hinter : IsEffectiveCartierDivisor (D.comap D'.subschemeι)) :
    D * D' = D ⊓ D'

Tag 053P, a lemma

Tag 053P in the Stacks Project.

Stacks.Divisors.isLocallyPrincipal_comap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocallyPrincipalPullback/Basic.lean, line 76.

Stacks Project, Tag 053P. The inverse image of a locally principal closed subscheme is locally principal.

theorem isLocallyPrincipal_comap {X Y : Scheme.{u}} (f : X ⟶ Y)
    (I : Y.IdealSheafData)
    (hI : IsLocallyPrincipal I) :
    IsLocallyPrincipal (I.comap f)

Tag 01WV, a definition

Tag 01WV in the Stacks Project.

Stacks.Divisors.IsPullbackDefined, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DivisorFlatPullback/Basic.lean, line 113. References: EGA IV (21.4.2), “effective Cartier div.”.

Stacks Project, Tag 01WV. The pullback of an effective Cartier divisor is defined exactly when its scheme-theoretic inverse image is an effective Cartier divisor.

abbrev IsPullbackDefined
    {X Y : Scheme.{u}} (f : X ⟶ Y) (D : Y.IdealSheafData) : Prop

Tag 02OO, a lemma

Tag 02OO in the Stacks Project.

Stacks.Divisors.isPullbackDefined_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/DivisorFlatPullback/Basic.lean, line 123. The attribute's comment: “flat_morphism”. References: EGA IV (21.4.5), “(i), eff. Cartier div”; EGA IV (21.10.6), “(D), special case”; EGA IV (21.5.6), “(D)”.

Stacks Project, Tag 02OO (6). The pullback of an effective Cartier divisor along a flat morphism is defined.

theorem isPullbackDefined_of_flat {X Y : Scheme.{u}} (f : X ⟶ Y)
    (D : Y.IdealSheafData) [Flat f]
    (hD : IsEffectiveCartierDivisor D) :
    IsPullbackDefined f D

Stacks.Divisors.isPullbackDefined_of_isReduced, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierPullbackCorollaries.lean, line 61. The attribute's comment: “part (3): a reduced source whose generic points avoid the support”. References: EGA IV (21.10.1), “special case”; EGA IV (21.4.5), “special case”.

Stacks 02OO (3). The pullback of an effective Cartier divisor D ⊆ Y along a morphism f : X ⟶ Y out of a reduced scheme is defined as soon as f carries no generic point of an irreducible component of X into the support of D: on a reduced scheme those generic points are exactly the weakly associated points.

theorem isPullbackDefined_of_isReduced {X Y : Scheme.{u}} (f : X ⟶ Y) [IsReduced X]
    (D : Y.IdealSheafData) (hD : IsEffectiveCartierDivisor D)
    (hf : ∀ ξ ∈ genericPoints X, f ξ ∉ D.supportSet) :
    IsPullbackDefined f D

Stacks.Divisors.isPullbackDefined_of_isDominant, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierPullbackCorollaries.lean, line 75. The attribute's comment: “part (2): a dominant morphism of integral schemes”. References: EGA IV (21.10.1), “special case”; EGA IV (21.4.5), “special case”.

Stacks 02OO (2). The pullback of an effective Cartier divisor is defined along a dominant morphism of integral schemes: the generic point of the source is its only weakly associated point, and dominance sends it to the generic point of the target, which an effective Cartier divisor misses.

theorem isPullbackDefined_of_isDominant {X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegral X]
    [IsIntegral Y] [IsDominant f] (D : Y.IdealSheafData) (hD : IsEffectiveCartierDivisor D) :
    IsPullbackDefined f D

Stacks.Divisors.isPullbackDefined_of_notMem_support_of_associated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierPullbackCorollaries.lean, line 93. The attribute's comment: “part (4): a locally Noetherian source whose associated points avoid the support”. References: EGA IV (21.4.5), “special case”.

Stacks 02OO (4). The pullback of an effective Cartier divisor D ⊆ Y along a morphism f : X ⟶ Y out of a locally Noetherian scheme is defined as soon as f carries no associated point of X into the support of D: on a locally Noetherian scheme the associated points are exactly the weakly associated points.

theorem isPullbackDefined_of_notMem_support_of_associated {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian X] (D : Y.IdealSheafData) (hD : IsEffectiveCartierDivisor D)
    (hf : ∀ x ∈ schemeAssociatedPoints X, f x ∉ D.supportSet) :
    IsPullbackDefined f D

Stacks.Divisors.isPullbackDefined_of_hasNoEmbeddedPoints, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartierPullbackCorollaries.lean, line 109. The attribute's comment: “part (5): no embedded points, generic points avoiding the support”. References: EGA IV (21.10.1), “partial”; EGA IV (21.4.5), “special case”.

Stacks 02OO (5). The pullback of an effective Cartier divisor D ⊆ Y along a morphism f : X ⟶ Y out of a locally Noetherian scheme without embedded points is defined as soon as f carries no generic point of an irreducible component of X into the support of D: without embedded points those generic points are exactly the weakly associated points.

theorem isPullbackDefined_of_hasNoEmbeddedPoints {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian X] (hX : HasNoEmbeddedPoints X) (D : Y.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) (hf : ∀ ξ ∈ genericPoints X, f ξ ∉ D.supportSet) :
    IsPullbackDefined f D

Stacks.Divisors.isPullbackDefined_of_notMem_support_of_weaklyAssociated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/EffectiveCartierPullbackCriteria.lean, line 76. The attribute's comment: “part (1): a morphism carrying no weakly associated point into the support”. References: EGA IV (21.4.5), “special case”.

Stacks 02OO (1), the scheme case. The pullback of an effective Cartier divisor D ⊆ Y along a morphism of schemes f : X ⟶ Y is defined as soon as f carries no weakly associated point of X into the support of D.

The question is affine-local: near a point x of the support of the inverse image, D is cut out on an affine open V ∋ f x by a nonzerodivisor t, and on an affine open U ∋ x inside f⁻¹(V) the inverse image is cut out by the image φ t of t. Were φ t a zerodivisor, a minimal prime q over the annihilator of a witness would be a weakly associated prime of Γ(X, U) containing φ t, hence by Stacks 056M a weakly associated point x₀ of X with t in the prime of f x₀; so f x₀ would lie in the support of D.

theorem isPullbackDefined_of_notMem_support_of_weaklyAssociated {X Y : Scheme.{u}} (f : X ⟶ Y)
    (D : Y.IdealSheafData) (hD : IsEffectiveCartierDivisor D)
    (hf : ∀ x ∈ schemeWeaklyAssociatedPoints X, f x ∉ D.supportSet) :
    IsPullbackDefined f D

Tag 01WW, a lemma

Tag 01WW in the Stacks Project.

AlgebraicGeometry.comap_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SumPullback.lean, line 40. The attribute's comment: “pullback of the sum”.

Scheme-theoretic inverse image commutes with products of ideal sheaves. For a morphism of schemes f : X ⟶ Y and quasi-coherent ideal sheaves I, J on Y, the inverse image of I * J is the product of the inverse images. In divisor language: the pullback of a sum of effective Cartier divisors is the sum of their pullbacks.

theorem comap_mul {X Y : Scheme.{u}} (f : X ⟶ Y) (I J : Y.IdealSheafData) :
    (I * J).comap f = I.comap f * J.comap f

AlgebraicGeometry.isPullbackDefined_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SumPullback.lean, line 60. The attribute's comment: “definedness of the pullback”.

If the pullbacks of two effective Cartier divisors along a morphism of schemes are defined, then so is the pullback of their sum.

theorem isPullbackDefined_mul {X Y : Scheme.{u}} (f : X ⟶ Y) (I J : Y.IdealSheafData)
    (hI : IsPullbackDefined f I) (hJ : IsPullbackDefined f J) :
    IsPullbackDefined f (I * J)

Sources

LeanStacks.Divisors.IsLocallyPrincipal · Stacks.Divisors.IsEffectiveCartierDivisor · Stacks.CartierAffineLocalConverse.isEffectiveCartierDivisor_iff_isRegular · Stacks.Divisors.isEffectiveCartierDivisor_iff_affineLocal · Stacks.Divisors.isEffectiveCartierDivisor_of_forall_mem_support · Stacks.Divisors.isAffineHom_ι_of_forall_support_inter_eq · Stacks.Divisors.isAffineHom_ι_compl_support_of_isLocallyPrincipal · Stacks.Divisors.isAffineHom_compl_of_isLocallyPrincipal

Section31.15 Effective Cartier divisors and invertible sheaves #

Section 31.15 of the Stacks Project, Tag 0C4S. 11 tags here are carried by 55 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 01WX, a definition

Tag 01WX in the Stacks Project.

Stacks.Divisors.negativeTwist', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 100. The attribute's comment: “part (3): negative twist”.

Stacks Project, Tag 01WX (3). The sheaf 𝒪_X(-D) = ℐ_D of a closed subscheme D ⊆ X: its sheaf of ideals.

noncomputable abbrev negativeTwist' : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.invertibleSheaf', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 107. The attribute's comment: “part (1): associated sheaf”.

Stacks Project, Tag 01WX (1). The sheaf 𝒪_X(D) = SheafHom_{𝒪_X}(ℐ_D, 𝒪_X) associated to a closed subscheme D ⊆ X. It is invertible as soon as D is an effective Cartier divisor; see Stacks.Divisors.invertibleSheaf_isInvertible.

noncomputable abbrev invertibleSheaf' : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.invertibleSheaf_isInvertible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 143. The attribute's comment: “part (1): invertibility”.

Stacks Project, Tag 01WX (1). The sheaf 𝒪_X(D) of an effective Cartier divisor is invertible: the evaluation pairing 𝒪_X(D) ⊗ ℐ_D ⟶ 𝒪_X trivializes it.

theorem invertibleSheaf_isInvertible [IsEffectiveCartierDivisor D] :
    AlgebraicGeometry.SheafOfModules.IsInvertible X.presheaf
      (structureSheafRing X.toRingedSpace).property (invertibleSheaf' D)

Stacks.Divisors.canonicalSection', a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 168. The attribute's comment: “part (2): canonical section”.

Stacks Project, Tag 01WX (2). The canonical section 1_D of 𝒪_X(D): the global section corresponding to the inclusion of the ideal sheaf ℐ_D into 𝒪_X.

noncomputable def canonicalSection' : (invertibleSheaf' D).sections

Stacks.Divisors.invertibleSheafIsoInverseIdeal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 182. The attribute's comment: “part (1): inverse tensor power”.

Stacks Project, Tag 01WX (1). The sheaf 𝒪_X(D) of an effective Cartier divisor is the inverse tensor power ℐ_D^{⊗ -1} of its ideal sheaf: both are tensor inverses of ℐ_D, and a tensor inverse is unique up to a canonical isomorphism.

noncomputable def invertibleSheafIsoInverseIdeal [IsEffectiveCartierDivisor D] :
    Stacks.SheafOfModules.Invertible.tensorPower X.presheaf
        (structureSheafRing X.toRingedSpace).property (negativeTwist' D) (-1) ≅
      invertibleSheaf' D

Stacks.Divisors.negativeTwistIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 197. The attribute's comment: “part (3): inverse tensor power”.

Stacks Project, Tag 01WX (3). The sheaf 𝒪_X(-D) = ℐ_D is the inverse tensor power 𝒪_X(D)^{⊗ -1}, which is the sense in which 𝒪_X(-D) is the inverse of 𝒪_X(D).

noncomputable def negativeTwistIso [IsEffectiveCartierDivisor D] :
    Stacks.SheafOfModules.Invertible.tensorPower X.presheaf
        (structureSheafRing X.toRingedSpace).property (invertibleSheaf' D) (-1) ≅
      negativeTwist' D

Stacks.Divisors.differenceTwist', an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorInvertibleSheaf.lean, line 214. The attribute's comment: “part (4): difference twist”.

Stacks Project, Tag 01WX (4). The sheaf 𝒪_X(D - D') = 𝒪_X(D) ⊗_{𝒪_X} 𝒪_X(-D') attached to a pair of closed subschemes.

noncomputable abbrev differenceTwist' : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.negativeTwist, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 123. The attribute's comment: “(3): O_S(-D) = I_D”.

Stacks Project, Tag 01WX (3). The sheaf 𝒪_S(-D) is the ideal sheaf ℐ_D of the closed subscheme D ⊆ S.

noncomputable abbrev negativeTwist : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.invertibleSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 136. The attribute's comment: “(1): O_S(D) = SheafHom(I_D, O_S)”.

Stacks Project, Tag 01WX (1). The sheaf 𝒪_S(D) = SheafHom_{𝒪_S}(ℐ_D, 𝒪_S) associated to a closed subscheme D ⊆ S: the dual of its ideal sheaf.

noncomputable abbrev invertibleSheaf : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.differenceTwist, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 144. The attribute's comment: “(4): O_S(D - D') = O_S(D) tensor O_S(-D')”.

Stacks Project, Tag 01WX (4). The difference twist 𝒪_S(D - D') = 𝒪_S(D) ⊗_{𝒪_S} 𝒪_S(-D'). The expression D - D' has no geometric meaning on its own; this is the definition of the sheaf it names.

noncomputable abbrev differenceTwist : SheafOfModules.{u} (structureSheafRing X.toRingedSpace)

Stacks.Divisors.isInvertible_invertibleSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 197. The attribute's comment: “(1): O_S(D) is invertible”.

Stacks Project, Tag 01WX (1). The sheaf 𝒪_S(D) of an effective Cartier divisor is invertible, which is what the tag's wording "the invertible sheaf 𝒪_S(D)" asserts.

This is Tag 0B8K (2) ⟹ (1) applied to the evaluation pairing: no trivializing cover is constructed, and no rank-one dual basis is assumed.

instance isInvertible_invertibleSheaf :
    AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj
      (structureSheafRing X.toRingedSpace).property (invertibleSheaf D)

Stacks.Divisors.invertibleSheafIsoNegativeTensorPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 216. The attribute's comment: “(1): O_S(D) = I_D^{tensor -1}”.

Stacks Project, Tag 01WX (1): 𝒪_S(D) = ℐ_D^{⊗ -1}. The dual of the ideal sheaf is its negative first tensor power, by uniqueness of tensor inverses; the identification is the one normalized by invertibleSheafPairing, not an arbitrary isomorphism. That normalization needs no restatement here: this is Stacks.SheafOfModules.Invertible.isoTensorPowerNegOne at that pairing, so Stacks.SheafOfModules.Invertible.isoTensorPowerNegOne_hom_tensor applies to it directly and says that tensoring this isomorphism with ℐ_D carries the canonical trivialization of ℐ_D^{⊗ -1} ⊗ ℐ_D back to invertibleSheafPairing.

noncomputable def invertibleSheafIsoNegativeTensorPower :
    invertibleSheaf D ≅ Stacks.SheafOfModules.Invertible.tensorPower X.sheaf.obj
      (structureSheafRing X.toRingedSpace).property (negativeTwist D) (-1)

Stacks.Divisors.negativeTwistIsoNegativeTensorPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 228. The attribute's comment: “(3): O_S(-D) = O_S(D)^{tensor -1}”.

Stacks Project, Tag 01WX (3): 𝒪_S(-D) = 𝒪_S(D)^{⊗ -1}. Together with the definition of negativeTwist this is the tag's full chain 𝒪_S(-D) = 𝒪_S(D)^{⊗ -1} = ℐ_D. The identification is normalized by invertibleSheafPairing', through the same Stacks.SheafOfModules.Invertible.isoTensorPowerNegOne_hom_tensor.

noncomputable def negativeTwistIsoNegativeTensorPower :
    negativeTwist D ≅ Stacks.SheafOfModules.Invertible.tensorPower X.sheaf.obj
      (structureSheafRing X.toRingedSpace).property (invertibleSheaf D) (-1)

Stacks.Divisors.canonicalSection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheaf.lean, line 244. The attribute's comment: “(2): the canonical section”.

Stacks Project, Tag 01WX (2). The canonical section 1 = 1_D: the global section of 𝒪_S(D) corresponding to the inclusion mapping ℐ_D ⟶ 𝒪_S.

A section of SheafHom(ℐ_D, 𝒪_S) over an open U is a morphism ℐ_D|_U ⟶ 𝒪_S|_U of presheaves of modules on the slice site over U (Tag 03EM), so the global section in question is the restriction of idealInclusion to the slice site over ⊤.

noncomputable def canonicalSection : (invertibleSheaf D).val.obj (op (⊤ : Opens X))

Tag 0B3P, a lemma

Tag 0B3P in the Stacks Project.

Stacks.CartierConormal.conormalSheafIsoNegativeTwist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CartierConormal/Basic.lean, line 57. The attribute's comment: “conormal sheaf”. References: EGA II (8.9.4), “partial”.

For an ideal sheaf datum D on a scheme X, the conormal sheaf of the closed immersion D.subschemeι is the restriction to the subscheme of the ideal sheaf ℐ_D, that is, of 𝒪_X(-D).

noncomputable def conormalSheafIsoNegativeTwist {X : Scheme.{u}} (D : X.IdealSheafData) :
    Stacks.Conormal.conormalSheaf D.subschemeι ≅
      (modulePullback D.subschemeι.toLRSHom.toShHom).obj
        (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom)

Stacks.Divisors.conormalSheafIsoNegativeTwist_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ConormalAlgebra/AffineGenerators.lean, line 578. The attribute's comment: “canonical ideal quotient”.

Stacks Project, Tag 0B3P, the canonical-ideal-quotient clause: on an affine open U of X carrying an affine model D ∩ U = Spec (Γ(X, U) ⧸ I) of the closed subscheme D, the affine computation of the conormal sheaf of D sends the image of a section x of ℐ_D over U — pulled back to D by the unit of the adjunction and read on the conormal sheaf through Stacks.Divisors.conormalSheafIsoNegativeTwist — to the class of x modulo I².

The sheaf 𝒪_X(-D) of Tag 01WX is the ideal sheaf ℐ_D itself, so this is the normalisation of both of Tag 0B3P's descriptions of the conormal sheaf at once.

theorem conormalSheafIsoNegativeTwist_apply {X : Scheme.{u}} (D : X.IdealSheafData)
    (U : X.Opens) (hU : IsAffineOpen U) (I : Ideal Γ(X, U))
    (e : Limits.pullback D.subschemeι U.ι ≅ Spec (.of (Γ(X, U) ⧸ I)))
    (he : Limits.pullback.snd D.subschemeι U.ι ≫ hU.isoSpec.hom =
      e.hom ≫ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
    (x : (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom).val.obj (op U))
    (hx : (kernel.ι (SheafOfModules.unitToPushforwardObjUnit
      (structureSheafHom D.subschemeι.toLRSHom.toShHom))).val.app (op U) x ∈ I) :
    (Stacks.Conormal.affineConormalIsoCotangent D.subschemeι U hU I e he).hom.hom
        ((conormalSheafIsoNegativeTwist D).inv.val.app
          (op ((opensMap D.subschemeι.toLRSHom.toShHom).obj U))
          (((modulePullbackPushforwardAdjunction D.subschemeι.toLRSHom.toShHom).unit.app
            (Stacks.ClosedImmersion.idealSheaf
              D.subschemeι.toLRSHom.toShHom)).val.app (op U) x))
      = I.toCotangent ⟨(kernel.ι (SheafOfModules.unitToPushforwardObjUnit
          (structureSheafHom D.subschemeι.toLRSHom.toShHom))).val.app (op U) x, hx⟩

Stacks.Divisors.conormalSheafIsoNegativeTwist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalSheaf.lean, line 280. The attribute's comment: “conormal sheaf”.

Stacks Project, Tag 0B3P, the conormal-sheaf clause: the conormal sheaf of a closed subscheme D ⊆ X is the restriction ℐ_D|_D = 𝒪_X(-D)|_D of its ideal sheaf.

The conormal sheaf of Tag 01R2 is computed through the liftCoborder factorization of the immersion; for a closed immersion the open through which it factors is the whole target (coborderRange_eq_top) and its open immersion is an isomorphism (isIso_coborderRange_ι), so Stacks.ClosedImmersion.pullbackIdealSheafIso identifies the two pullbacks. The sheaf 𝒪_X(-D) of Tag 01WX is the ideal sheaf itself, so the right-hand side is both descriptions at once.

noncomputable def conormalSheafIsoNegativeTwist {X : Scheme.{u}} (D : X.IdealSheafData) :
    (modulePullback D.subschemeι.liftCoborder.toLRSHom.toShHom).obj
        (Stacks.ClosedImmersion.idealSheaf
          D.subschemeι.liftCoborder.toLRSHom.toShHom) ≅
      (modulePullback D.subschemeι.toLRSHom.toShHom).obj
        (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom)

Stacks.Divisors.normalSheafIsoInvertibleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalSheaf.lean, line 301. The attribute's comment: “normal sheaf”.

Stacks Project, Tag 0B3P, the normal-sheaf clause: the normal sheaf of an effective Cartier divisor D ⊆ X is the restriction 𝒪_X(D)|_D of its associated invertible sheaf 𝒪_X(D) = SheafHom(ℐ_D, 𝒪_X).

There is no hypothesis beyond the divisor. The stalk formula of Tag 0098 for modulePullback along the closed immersion of D, which used to be carried here as Stacks.RingedSpace.PullbackStalkFormula, is a theorem (Stacks.RingedSpace.pullbackStalkFormula), so Tag 01CD is available outright as Stacks.RingedSpace.isIso_comparison.

noncomputable def normalSheafIsoInvertibleSheaf {X : Scheme.{u}} (D : X.IdealSheafData)
    [IsEffectiveCartierDivisor D] :
    normalSheaf D.subschemeι ≅
      (modulePullback D.subschemeι.toLRSHom.toShHom).obj
        (Stacks.SheafOfModules.dualSheaf X.sheaf.obj (structureSheafRing X.toRingedSpace).property
          (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom))

Stacks.Divisors.normalSheafIsoInvertibleSheaf_eval, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/NormalSheafEvaluation.lean, line 494. The attribute's comment: “canonical evaluation”.

Let φ be a section of 𝒪_X(D) = ℐ_D^∨ over U and x a section of 𝒪_X(-D) = ℐ_D over U, both carried to D by the unit of f^* ⊣ f_* for the closed immersion f of D. The functional which Stacks.Divisors.normalSheafIsoInvertibleSheaf produces from φ on the conormal sheaf takes the image of x to the restriction of φ(x).

theorem normalSheafIsoInvertibleSheaf_eval {X : Scheme.{u}} (D : X.IdealSheafData)
    [IsEffectiveCartierDivisor D] (U : Opens X)
    (φ : (dualSheaf X.sheaf.obj (structureSheafRing X.toRingedSpace).property
      (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom)).val.obj (op U))
    (x : (Stacks.ClosedImmersion.idealSheaf
      D.subschemeι.toLRSHom.toShHom).val.obj (op U)) :
    evalSection D.subscheme.sheaf.obj
        ((modulePullback D.subschemeι.liftCoborder.toLRSHom.toShHom).obj
          (Stacks.ClosedImmersion.idealSheaf
            D.subschemeι.liftCoborder.toLRSHom.toShHom)).val
        (_root_.SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf
          D.subscheme.sheaf.obj
          (structureSheafRing D.subscheme.toRingedSpace).property)).val
        (op ((opensMap D.subschemeι.toLRSHom.toShHom).obj U))
        ((normalSheafIsoInvertibleSheaf D).inv.val.app
          (op ((opensMap D.subschemeι.toLRSHom.toShHom).obj U))
          (((modulePullbackPushforwardAdjunction
              D.subschemeι.toLRSHom.toShHom).unit.app
            (dualSheaf X.sheaf.obj (structureSheafRing X.toRingedSpace).property
              (Stacks.ClosedImmersion.idealSheaf
                D.subschemeι.toLRSHom.toShHom))).val.app (op U) φ))
        ((conormalSheafIsoNegativeTwist D).inv.val.app
          (op ((opensMap D.subschemeι.toLRSHom.toShHom).obj U))
          (((modulePullbackPushforwardAdjunction
              D.subschemeι.toLRSHom.toShHom).unit.app
            (Stacks.ClosedImmersion.idealSheaf
              D.subschemeι.toLRSHom.toShHom)).val.app (op U) x)) =
      ((structureSheafHom D.subschemeι.toLRSHom.toShHom).hom.app (op U)).hom
        (evalSection X.sheaf.obj
          (Stacks.ClosedImmersion.idealSheaf D.subschemeι.toLRSHom.toShHom).val
          (_root_.SheafOfModules.unit (Stacks.SheafOfModules.TensorSheafification.structureSheaf
            X.sheaf.obj
            (structureSheafRing X.toRingedSpace).property)).val (op U) φ x)

Tag 0C4T, a lemma

Tag 0C4T in the Stacks Project.

Stacks.Divisors.shortExact_sumKernelMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SumKernelMap.lean, line 298. The attribute's comment: “with the kernel inclusion named, rather than existentially bound”. References: SGA 7 X (1.13), “more general”.

[Stacks, Tag 0C4T] with its kernel inclusion named. For D ⊆ D' effective Cartier divisors on a scheme X and C an effective Cartier divisor with D' = D + C, the sequence 0 ⟶ 𝒪_X(-D)|_C ⟶ 𝒪_{D'} ⟶ 𝒪_D ⟶ 0 is short exact, with first map Stacks.Divisors.sumKernelMap and second map the canonical restriction.

Stacks.Divisors.addEffectiveCartierDivisor_shortExact is the same assertion with the first map bound by an existential; this version is the one a consumer needs in order to state an equation about that map, and Stacks.Divisors.eq_sumKernelMap shows the two are about the same morphism. The sum is written C * D rather than D * C because the named morphism's type mentions it, so no mul_comm can be absorbed into a proof.

public theorem shortExact_sumKernelMap (D C : X.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) (hsub : C * D ≤ D) :
    (ShortComplex.mk (sumKernelMap D C hD)
      (Scheme.IdealSheafData.closedSubschemeRestriction hsub)
      (sumKernelMap_comp_closedSubschemeRestriction D C hD hsub)).ShortExact

Stacks.Divisors.addEffectiveCartierDivisor_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/EffectiveCartier/SumSequence.lean, line 1071.

Stacks Project, Tag 0C4T. Let D ⊆ D' be effective Cartier divisors on a scheme X and let C be an effective Cartier divisor with D' = D + C, which exists by [Stacks, Tag 02ON]. Then there is a short exact sequence 0 ⟶ 𝒪_X(-D)|_C ⟶ 𝒪_{D'} ⟶ 𝒪_D ⟶ 0 of 𝒪_X-modules.

theorem addEffectiveCartierDivisor_shortExact (D D' C : X.IdealSheafData)
    (hD : IsEffectiveCartierDivisor D) (hD' : IsEffectiveCartierDivisor D')
    (hC : IsEffectiveCartierDivisor C) (hsub : D' ≤ D) (hsum : D' = D * C) :
    ∃ f : (Scheme.Modules.pushforward C.subschemeι).obj
          ((Scheme.Modules.pullback C.subschemeι).obj (negativeTwist D)) ⟶
        Scheme.IdealSheafData.closedSubschemeStructureSheaf D',
      ∃ zero : f ≫ Scheme.IdealSheafData.closedSubschemeRestriction hsub = 0,
        (ShortComplex.mk f (Scheme.IdealSheafData.closedSubschemeRestriction hsub)
          zero).ShortExact

Tag 02OP, a lemma

Tag 02OP in the Stacks Project.

Stacks.Divisors.invertibleSheafSumIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafSum.lean, line 323. The attribute's comment: “existence and distinguished-section compatibility”. References: EGA IV (21.2.8), “(21.2.8.3), special case”.

The canonical identification 𝒪_X(D) ⊗_{𝒪_X} 𝒪_X(D') ≅ 𝒪_X(D + D') of the tensor product of the invertible sheaves of two effective Cartier divisors with the invertible sheaf of their sum, carrying the pure tensor 1_D ⊗ 1_{D'} of the canonical sections to the canonical section 1_{D + D'}.

def invertibleSheafSumIso [IsEffectiveCartierDivisor D] [IsEffectiveCartierDivisor D'] :
    sumSheaf D D' ≅ invertibleSheaf' (D * D')

Stacks.Divisors.invertibleSheafSumIso_canonicalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafSum.lean, line 330. The attribute's comment: “existence and distinguished-section compatibility”.

Under Stacks.Divisors.invertibleSheafSumIso the pure tensor 1_D ⊗ 1_{D'} of the canonical sections of 𝒪_X(D) and 𝒪_X(D') is the canonical section 1_{D + D'} of 𝒪_X(D + D').

theorem invertibleSheafSumIso_canonicalSection
    [IsEffectiveCartierDivisor D] [IsEffectiveCartierDivisor D'] :
    Scheme.Modules.Hom.app (invertibleSheafSumIso D D').hom ⊤ (canonicalSectionTensor D D') =
      (canonicalSection' (D * D')).val (op ⊤)

Stacks.Divisors.invertibleSheafSumIso_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafSum.lean, line 339. The attribute's comment: “uniqueness”.

An isomorphism 𝒪_X(D) ⊗ 𝒪_X(D') ≅ 𝒪_X(D + D') carrying 1_D ⊗ 1_{D'} to 1_{D + D'} is Stacks.Divisors.invertibleSheafSumIso.

theorem invertibleSheafSumIso_unique
    [IsEffectiveCartierDivisor D] [IsEffectiveCartierDivisor D']
    (e : sumSheaf D D' ≅ invertibleSheaf' (D * D'))
    (he : Scheme.Modules.Hom.app e.hom ⊤ (canonicalSectionTensor D D') =
      (canonicalSection' (D * D')).val (op ⊤)) :
    e = invertibleSheafSumIso D D'

Tag 0C4U, a lemma

Tag 0C4U in the Stacks Project.

Stacks.Divisors.invertibleSheafPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafPullback.lean, line 194. The attribute's comment: “associated sheaf”.

Stacks Project, Tag 0C4U. The canonical identification f^* 𝒪_Y(D) ≅ 𝒪_X(f^{-1}D) of the invertible sheaf of an effective Cartier divisor whose pullback is defined with the invertible sheaf of its inverse image.

def invertibleSheafPullbackIso :
    (Scheme.Modules.pullback f).obj (invertibleSheaf' D) ≅ invertibleSheaf' (D.comap f)

Stacks.Divisors.invertibleSheafPullbackIso_canonicalSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/InvertibleSheafPullback.lean, line 202. The attribute's comment: “canonical section”.

Stacks Project, Tag 0C4U. Under the identification Stacks.Divisors.invertibleSheafPullbackIso the pullback of the canonical section 1_D is the canonical section 1_{f^{-1}D}.

theorem invertibleSheafPullbackIso_canonicalSection :
    Scheme.Modules.Hom.app (invertibleSheafPullbackIso f D).hom ⊤
        (pullbackCanonicalSection f D) =
      (canonicalSection' (D.comap f)).val (op ⊤)

Tag 01WY, a definition

Tag 01WY in the Stacks Project.

AlgebraicGeometry.IsRegularSection, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSections.lean, line 107.

A global section is regular when multiplication by it gives a monomorphism from the structure sheaf to its module sheaf.

noncomputable abbrev IsRegularSection
    {L : SheafOfModules.{w}
      (Stacks.SheafOfModules.TensorSheafification.structureSheaf O hO)}
    (s : L.sections) : Prop

Tag 01WZ, a lemma

Tag 01WZ in the Stacks Project.

AlgebraicGeometry.isRegularSection_iff_stalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSections.lean, line 257. The attribute's comment: “conditions (1) and (2)”.

A section of the structure sheaf is regular if and only if its germ at every point is a nonzerodivisor.

theorem isRegularSection_iff_stalk
    (X : LocallyRingedSpace.{u})
    (f : (SheafOfModules.unit
      ((sheafCompose (Opens.grothendieckTopology X)
        (forget₂ CommRingCat.{u} RingCat.{u})).obj X.sheaf)).sections) :
    IsRegularSection X.presheaf
        ((Presheaf.isSheaf_iff_isSheaf_comp _ X.presheaf
          (forget₂ CommRingCat.{u} RingCat.{u})).mp X.IsSheaf) f ↔
      ∀ x : X, IsSMulRegular (X.presheaf.stalk x)
        (X.presheaf.germ ⊤ x trivial (f.val (.op ⊤)))

AlgebraicGeometry.isRegularSection_iff_affineOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSections.lean, line 300. The attribute's comment: “conditions (1) and (3)”.

On a scheme, a section of the structure sheaf is regular if and only if its restriction to every affine open is a nonzerodivisor.

theorem isRegularSection_iff_affineOpen
    (X : Scheme.{u})
    (f : (SheafOfModules.unit
      ((sheafCompose (Opens.grothendieckTopology X)
        (forget₂ CommRingCat.{u} RingCat.{u})).obj X.sheaf)).sections) :
    IsRegularSection X.presheaf
        ((Presheaf.isSheaf_iff_isSheaf_comp _ X.presheaf
          (forget₂ CommRingCat.{u} RingCat.{u})).mp X.IsSheaf) f ↔
      ∀ U : X.Opens, IsAffineOpen U →
        IsSMulRegular Γ(X, U) (show Γ(X, U) from f.val (.op U))

AlgebraicGeometry.isRegularSection_iff_exists_affineOpenCover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/Meromorphic/RegularSections.lean, line 319. The attribute's comment: “conditions (1) and (4)”.

On a scheme, a section of the structure sheaf is regular if and only if its restrictions are nonzerodivisors on the members of some affine open covering.

theorem isRegularSection_iff_exists_affineOpenCover
    (X : Scheme.{u})
    (f : (SheafOfModules.unit
      ((sheafCompose (Opens.grothendieckTopology X)
        (forget₂ CommRingCat.{u} RingCat.{u})).obj X.sheaf)).sections) :
    IsRegularSection X.presheaf
        ((Presheaf.isSheaf_iff_isSheaf_comp _ X.presheaf
          (forget₂ CommRingCat.{u} RingCat.{u})).mp X.IsSheaf) f ↔
      ∃ (I : Type u) (U : I → X.Opens), IsOpenCover U ∧
        (∀ i, IsAffineOpen (U i) ∧
          IsSMulRegular Γ(X, U i) (show Γ(X, U i) from f.val (.op (U i))))

Tag 02OQ, a definition

Tag 02OQ in the Stacks Project.

Stacks.Divisors.zeroScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/GysinConstruction/ZeroScheme.lean, line 56. The attribute's comment: “the closed subscheme construction”.

Stacks 02OQ. The quasi-coherent ideal sheaf cutting out the zero scheme of a global section s of an invertible module L on X: on an affine open U it is generated by the values φ (s|_U) of the Γ(X, U)-linear functionals φ on Γ(L, U). The closed subscheme itself is (zeroScheme X L s).subscheme, with closed immersion (zeroScheme X L s).subschemeι.

noncomputable abbrev zeroScheme (X : Scheme.{u}) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) : X.IdealSheafData

Stacks.Divisors.zeroScheme_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/ZeroSchemeIdeal.lean, line 189. The attribute's comment: “the defining ideal”.

Stacks 02OQ, the defining ideal. The ideal of the zero scheme of a global section s of an invertible module L on an affine open U is generated by the values φ (s|_U) of the Γ(X, U)-linear functionals on Γ(L, U): the prescribed affine-local family is already an ideal sheaf, so Scheme.IdealSheafData.ofIdeals leaves it untouched.

theorem zeroScheme_ideal (X : Scheme.{u}) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (U : X.affineOpens) :
    (zeroScheme X L s).ideal U =
      Ideal.span {a : Γ(X, U.1) | ∃ φ : Γ(L, U.1) →ₗ[Γ(X, U.1)] Γ(X, U.1),
        a = φ (L.presheaf.map (homOfLE le_top).op s)}

AlgebraicGeometry.zeroScheme, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeData.lean, line 198. The attribute's comment: “the closed subscheme construction”.

The zero scheme of a global section s of an invertible module L, as a quasi-coherent sheaf of ideals: on an affine open it is the image of the dual map s : L^{⊗ -1} ⟶ 𝒪_X, i.e. the ideal generated by the values of s under the linear functionals on the sections of L.

noncomputable abbrev zeroScheme (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) : X.IdealSheafData

AlgebraicGeometry.zeroScheme_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeData.lean, line 208. The attribute's comment: “the defining ideal”.

The defining ideal of the zero scheme on an affine open is the ideal generated by the values of the restricted section under the local linear functionals.

theorem zeroScheme_ideal (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) (U : X.affineOpens) :
    (zeroScheme X L s).ideal U =
      Ideal.span {a : Γ(X, U.1) | ∃ φ : Γ(L, U.1) →ₗ[Γ(X, U.1)] Γ(X, U.1),
        a = φ (L.presheaf.map (homOfLE le_top).op s)}

Stacks.Tag02OQSectionIdeal.zeroScheme_ideal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionIdeal/Qcoh.lean, line 204. The attribute's comment: “the defining ideal”.

Stacks Tag 02OQ, the defining ideal of the zero scheme. On every affine open the ideal of the zero scheme of a global section of an invertible module is the ideal generated by the values of the restricted section under all linear functionals there.

Scheme.IdealSheafData.ofIdeals is a supremum and in general shrinks the family it is applied to; it does not here, because that family is already compatible with passage to a basic open and hence is itself an ideal sheaf.

theorem zeroScheme_ideal (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (t : Γ(L, ⊤)) (U : X.affineOpens) :
    (Stacks.RegularSectionSequence.zeroScheme X L t).ideal U =
      Ideal.span {a : Γ(X, U.1) | ∃ φ : Γ(L, U.1) →ₗ[Γ(X, U.1)] Γ(X, U.1),
        a = φ (L.presheaf.map (homOfLE le_top).op t)}

Tag 02OR, a lemma

Tag 02OR in the Stacks Project.

Stacks.Divisors.pullbackSection_eq_zero_iff_factorsThrough_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Chow/ZeroSchemePullback/Factorization.lean, line 378. The attribute's comment: “factorization”.

A global section s of an invertible module L on X vanishes after pullback along f : Y ⟶ X if and only if f factors through the zero scheme of s.

theorem pullbackSection_eq_zero_iff_factorsThrough_zeroScheme
    (X : Scheme.{u}) (L : X.Modules)
    [AlgebraicGeometry.SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) {Y : Scheme.{u}} (f : Y ⟶ X) :
    pullbackGlobalSections f L s = 0 ↔
      ∃ g : Y ⟶ (_root_.Stacks.Divisors.zeroScheme X L s).subscheme,
        g ≫ (_root_.Stacks.Divisors.zeroScheme X L s).subschemeι = f

AlgebraicGeometry.pullbackSection_eq_zero_iff_factorsThrough_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeFactorization.lean, line 210. The attribute's comment: “factorization”.

Stacks Tag 02OR (2). A global section of an invertible module vanishes after pullback along f if and only if f factors through its zero scheme.

theorem pullbackSection_eq_zero_iff_factorsThrough_zeroScheme (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : Γ(L, ⊤))
    {Y : Scheme.{u}} (f : Y ⟶ X) :
    pullbackGlobalSections f L s = 0 ↔
      ∃ g : Y ⟶ (zeroScheme X L s).subscheme,
        g ≫ (zeroScheme X L s).subschemeι = f

AlgebraicGeometry.zeroScheme_isGreatest_vanishingClosedSubscheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeFactorization.lean, line 275. The attribute's comment: “maximal”.

Stacks Tag 02OR (1). Among the closed subschemes on which the section pulls back to zero, the zero scheme is the largest. Closed subschemes are ordered by their ideal sheaves, and geometric inclusion is the reverse of that order, which is why the statement is about the order dual.

theorem zeroScheme_isGreatest_vanishingClosedSubscheme (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : Γ(L, ⊤)) :
    IsGreatest
      {I : (X.IdealSheafData)ᵒᵈ |
        pullbackGlobalSections (OrderDual.ofDual I).subschemeι L s = 0}
      (OrderDual.toDual (zeroScheme X L s))

AlgebraicGeometry.isLocallyPrincipal_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeProperties.lean, line 81. The attribute's comment: “locally_principal”.

Stacks Tag 02OR (3). The zero scheme of a global section of an invertible module is a locally principal closed subscheme: on the trivializing opens its ideal is generated by the one function representing the section.

theorem isLocallyPrincipal_zeroScheme (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
    (s : Γ(L, ⊤)) : Stacks.Divisors.IsLocallyPrincipal (zeroScheme X L s)

AlgebraicGeometry.isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeRegular.lean, line 221. The attribute's comment: “cartier_iff_regular”.

Stacks Project, Tag 02OR (4). The zero scheme of a global section s of an invertible module is an effective Cartier divisor if and only if s is a nonzerodivisor.

theorem isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection (s : L.sections) :
    Stacks.Divisors.IsEffectiveCartierDivisor (zeroScheme X L (s.eval (op ⊤))) ↔
      IsRegularSection X.sheaf.obj X.ringCatSheaf.property s

Tag 01X0, a lemma

Tag 01X0 in the Stacks Project.

Stacks.Divisors.canonicalSection_isRegular, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/CanonicalSectionRegular.lean, line 180. The attribute's comment: “canonical_section_regular”.

The first clause of [Stacks, Tag 01X0]. For D ⊆ X an effective Cartier divisor on a scheme, the canonical section 1_D of 𝒪_X(D) is a regular section.

Tensoring with ℐ_D is an autoequivalence of the category of 𝒪_X-modules, since ℐ_D is invertible, so it is faithful and therefore reflects monomorphisms; and Stacks.Divisors.evaluation_canonicalHom identifies the image of 1_D under it, up to the left unitor and the evaluation isomorphism, with the inclusion ℐ_D ⟶ 𝒪_X, which is a kernel morphism and hence a monomorphism.

theorem canonicalSection_isRegular [IsEffectiveCartierDivisor D] :
    AlgebraicGeometry.IsRegularSection X.presheaf
      (structureSheafRing X.toRingedSpace).property (canonicalSection' D)

AlgebraicGeometry.existsUnique_invertibleSheafIso_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionCorrespondence.lean, line 250. The attribute's comment: “regular_section_divisor”.

There is a unique isomorphism from the invertible sheaf of the zero scheme of a regular section to the original invertible sheaf that sends its canonical section to that section. This is [Stacks, Tag 01X0] (2): for s a regular section of an invertible 𝒪_X-module L the zero scheme D = Z(s) is an effective Cartier divisor (AlgebraicGeometry.isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection) and 𝒪_X(D) ≅ L by a unique isomorphism matching 1_D with s.

Existence is AlgebraicGeometry.invertibleSheafIsoZeroSchemeOfIsRegularSection and its section identity; uniqueness is AlgebraicGeometry.eq_id_of_sectionsMap_eq, applied to the endomorphism of L built from two such isomorphisms.

theorem existsUnique_invertibleSheafIso_zeroScheme (X : Scheme.{u}) (L : X.Modules)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    (hs : IsRegularSection X.sheaf.obj X.ringCatSheaf.property s) :
    ∃! e : Stacks.Divisors.invertibleSheaf' (zeroScheme X L (s.eval (op ⊤))) ≅ L,
      Scheme.Modules.Hom.app e.hom ⊤
          ((Stacks.Divisors.canonicalSection'
            (zeroScheme X L (s.eval (op ⊤)))).eval (op ⊤)) = s.eval (op ⊤)

AlgebraicGeometry.effectiveCartierDivisor_equiv_regularSectionClass, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionCorrespondence.lean, line 398. The attribute's comment: “divisor_regular_section_equiv”. References: EGA IV (21.3.3), “(ii)”.

The canonical bijection between the effective Cartier divisors on a scheme and the isomorphism classes of invertible modules with a regular global section ([Stacks, Tag 01X0]).

Forwards a divisor D goes to the class of (𝒪_X(D), 1_D); backwards a pair (L, s) goes to the zero scheme Z(s), which is well defined on classes by AlgebraicGeometry.RegularSectionPair.zeroScheme_eq_of_isIsomorphic. The two round trips are Z(1_D) = D (Stacks.Divisors.zeroScheme_canonicalSection) and (𝒪_X(Z(s)), 1_{Z(s)}) ≅ (L, s) (AlgebraicGeometry.invertibleSheafIsoZeroSchemeOfIsRegularSection).

def effectiveCartierDivisor_equiv_regularSectionClass (X : Scheme.{u}) :
    EffectiveCartierDivisor X ≃ RegularSectionClass X

AlgebraicGeometry.effectiveCartierDivisor_equiv_regularSectionClass_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionCorrespondence.lean, line 413. The attribute's comment: “divisor_regular_section_equiv”.

The forward map of the bijection of [Stacks, Tag 01X0] sends an effective Cartier divisor to the isomorphism class of its invertible sheaf with its canonical section, which is a regular section.

theorem effectiveCartierDivisor_equiv_regularSectionClass_apply (D : EffectiveCartierDivisor X) :
    ∃ h : IsRegularSection X.sheaf.obj X.ringCatSheaf.property
        (Stacks.Divisors.canonicalSection' D.1),
      effectiveCartierDivisor_equiv_regularSectionClass X D =
        RegularSectionPair.classOf
          ⟨Stacks.Divisors.invertibleSheaf' D.1,
            @Stacks.Divisors.isInvertible_divisorSheaf X D.1 D.2,
            Stacks.Divisors.canonicalSection' D.1, h⟩

AlgebraicGeometry.effectiveCartierDivisor_equiv_regularSectionClass_symm_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionCorrespondence.lean, line 427. The attribute's comment: “divisor_regular_section_equiv”.

The inverse map of the bijection of [Stacks, Tag 01X0] sends the class of a regular-section pair to the effective Cartier divisor cut out by its zero scheme. The equation holds for every representative of the class.

theorem effectiveCartierDivisor_equiv_regularSectionClass_symm_apply (P : RegularSectionPair X) :
    ∃ h : Stacks.Divisors.IsEffectiveCartierDivisor P.zeroScheme,
      (effectiveCartierDivisor_equiv_regularSectionClass X).symm P.classOf = ⟨P.zeroScheme, h⟩

Stacks.Divisors.zeroScheme_canonicalSection', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeCanonicalSection.lean, line 196. The attribute's comment: “zeroScheme_canonicalSection”.

Z(1_D) = D. The zero scheme of the canonical section of 𝒪_X(D) is D itself: the composite D ↦ (𝒪_X(D), 1_D) ↦ Z(1_D) is the identity.

theorem zeroScheme_canonicalSection' :
    zeroScheme X (modulesInvertibleSheaf D) (canonicalSection D) = D

Stacks.Divisors.isRegularSection_canonicalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeCanonicalSection.lean, line 210. The attribute's comment: “canonical_section_regular”.

The canonical section 1_D of 𝒪_X(D) is a regular section, i.e. a nonzerodivisor ([Stacks, Tag 01WY]).

theorem isRegularSection_canonicalSections :
    IsRegularSection X.sheaf.obj X.ringCatSheaf.property (canonicalSections D)

Declarations registered for the tag:

AlgebraicGeometry.isEffectiveCartierDivisor_zeroScheme_iff_isRegularSection, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionCorrespondence.lean, line 236 (StacksFrontier): “regular_section_divisor”.

Tag 0C6K, a remark

Tag 0C6K in the Stacks Project.

Stacks.Divisors.shortExact_divisor_normal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DivisorNormalSequence.lean, line 92. The attribute's comment: “divisor_normal_sequence”.

Stacks Tag 0C6K, the label divisor_normal_sequence. For an effective Cartier divisor D ⊆ X with inclusion i, the normal sheaf 𝒩_{D/X} is the restriction i^* 𝒪_X(D), and

0 ⟶ 𝒪_X ⟶ 𝒪_X(D) ⟶ i_* 𝒩_{D/X} ⟶ 0

is short exact, the first map being multiplication by the canonical section 1_D and the second the unit of i^* ⊣ i_* followed by the pushforward of that identification.

theorem shortExact_divisor_normal :
    let i := D.subschemeι
    let L : X.Modules := invertibleSheaf D
    let N : D.subscheme.Modules := normalSheaf i
    ∃ e : (Scheme.Modules.pullback i).obj L ≅ N,
      let O : X.Modules := SheafOfModules.unit X.ringCatSheaf
      let f : O ⟶ L := L.unitHomEquiv.symm (canonicalSections D)
      let g : L ⟶ (Scheme.Modules.pushforward i).obj N :=
        (Scheme.Modules.pullbackPushforwardAdjunction i).unit.app L ≫
          (Scheme.Modules.pushforward i).map e.hom
      ∃ h : f ≫ g = 0, (ShortComplex.mk f g h).ShortExact

AlgebraicGeometry.shortExact_zeroScheme_ideal_of_isRegularSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionIdealSequence.lean, line 204. The attribute's comment: “regular_section_ideal_sequence”.

Stacks Tag 0C6K, the label regular_section_ideal_sequence. For an invertible module L on a scheme X and a regular global section s of L ([Stacks, Tag 01WY]), the sequence

0 ⟶ L^{⊗ -1} ⟶ 𝒪_X ⟶ i_* 𝒪_{Z(s)} ⟶ 0

is short exact, where i is the inclusion of the zero scheme of s, the first map is multiplication by s through the canonical trivialization L^{⊗ -1} ⊗ L ≅ 𝒪_X and the second is restriction to the zero scheme.

theorem shortExact_zeroScheme_ideal_of_isRegularSection (s : L.sections)
    (hs : IsRegularSection X.sheaf.obj X.ringCatSheaf.property s) :
    let i := (zeroScheme X L (s.eval (op ⊤))).subschemeι
    let Linv : X.Modules := inverseTensorPower X L
    let u : Linv ⟶ SheafOfModules.unit X.ringCatSheaf :=
      ((ρ_ Linv).inv ≫ Linv ◁ L.unitHomEquiv.symm s) ≫ (inverseTensorPowerIsoUnit X L).hom
    let q : SheafOfModules.unit X.ringCatSheaf ⟶
        (Scheme.Modules.pushforward i).obj
          (SheafOfModules.unit (zeroScheme X L (s.eval (op ⊤))).subscheme.ringCatSheaf) :=
      SheafOfModules.unitToPushforwardObjUnit i.toRingCatSheafHom
    ∃ h : u ≫ q = 0, (ShortComplex.mk u q h).ShortExact

AlgebraicGeometry.isEffectiveCartierDivisor_zeroScheme_and_shortExact_sequences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/RegularSectionRemark.lean, line 68.

Stacks Tag 0C6K. Let X be a scheme.

For an invertible 𝒪_X-module L and a regular section s of L ([Stacks, Tag 01WY]), with i the inclusion of the zero scheme Z(s): Z(s) is an effective Cartier divisor on X, the sequence 0 ⟶ 𝒪_X ⟶ L ⟶ i_* i^* L ⟶ 0 is short exact (first map multiplication by s, second the unit of i^* ⊣ i_*), and the sequence 0 ⟶ L^{⊗ -1} ⟶ 𝒪_X ⟶ i_* 𝒪_{Z(s)} ⟶ 0 is short exact (first map multiplication by s read through L^{⊗ -1} ⊗ L ≅ 𝒪_X, second restriction to the zero scheme).

For an effective Cartier divisor D ⊆ X with inclusion i: the normal sheaf 𝒩_{D/X} is i^* 𝒪_X(D) and 0 ⟶ 𝒪_X ⟶ 𝒪_X(D) ⟶ i_* 𝒩_{D/X} ⟶ 0 is short exact (first map multiplication by the canonical section 1_D), and 0 ⟶ ℐ_D ⟶ 𝒪_X ⟶ i_* 𝒪_D ⟶ 0 is short exact.

theorem isEffectiveCartierDivisor_zeroScheme_and_shortExact_sequences (X : Scheme.{u}) :
    (∀ (L : X.Modules) [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L]
        (s : L.sections), IsRegularSection X.sheaf.obj X.ringCatSheaf.property s →
      Stacks.Divisors.IsEffectiveCartierDivisor (zeroScheme X L (s.eval (op ⊤))) ∧
      (let i := (zeroScheme X L (s.eval (op ⊤))).subschemeι
        let O : X.Modules := SheafOfModules.unit X.ringCatSheaf
        let f : O ⟶ L := L.unitHomEquiv.symm s
        let g : L ⟶ (Scheme.Modules.pushforward i).obj ((Scheme.Modules.pullback i).obj L) :=
          (Scheme.Modules.pullbackPushforwardAdjunction i).unit.app L
        ∃ h : f ≫ g = 0, (ShortComplex.mk f g h).ShortExact) ∧
      (let i := (zeroScheme X L (s.eval (op ⊤))).subschemeι
        let Linv : X.Modules := inverseTensorPower X L
        let u : Linv ⟶ SheafOfModules.unit X.ringCatSheaf :=
          ((ρ_ Linv).inv ≫ Linv ◁ L.unitHomEquiv.symm s) ≫ (inverseTensorPowerIsoUnit X L).hom
        let q : SheafOfModules.unit X.ringCatSheaf ⟶
            (Scheme.Modules.pushforward i).obj
              (SheafOfModules.unit (zeroScheme X L (s.eval (op ⊤))).subscheme.ringCatSheaf) :=
          SheafOfModules.unitToPushforwardObjUnit i.toRingCatSheafHom
        ∃ h : u ≫ q = 0, (ShortComplex.mk u q h).ShortExact)) ∧
    (∀ (D : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor D],
      (let i := D.subschemeι
        let L : X.Modules := Stacks.Divisors.invertibleSheaf D
        let N : D.subscheme.Modules := Stacks.Divisors.normalSheaf i
        ∃ e : (Scheme.Modules.pullback i).obj L ≅ N,
          let O : X.Modules := SheafOfModules.unit X.ringCatSheaf
          let f : O ⟶ L := L.unitHomEquiv.symm (Stacks.Divisors.canonicalSections D)
          let g : L ⟶ (Scheme.Modules.pushforward i).obj N :=
            (Scheme.Modules.pullbackPushforwardAdjunction i).unit.app L ≫
              (Scheme.Modules.pushforward i).map e.hom
          ∃ h : f ≫ g = 0, (ShortComplex.mk f g h).ShortExact) ∧
      ∃ hz : Stacks.IdealSheafSequence.divisorIdealMap D ≫
          Stacks.IdealSheafSequence.divisorQuotientMap D = 0,
        (ShortComplex.mk (Stacks.IdealSheafSequence.divisorIdealMap D)
          (Stacks.IdealSheafSequence.divisorQuotientMap D) hz).ShortExact)

AlgebraicGeometry.exists_cokernelIso_unit_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeExactSequence.lean, line 234. The attribute's comment: “regular_section_sequence”.

For an invertible module L on a scheme X and a global section s, the unit of the pullback–pushforward adjunction along the inclusion i of the zero scheme Z(s) realizes i_* i^* L as the cokernel of multiplication by s.

No regularity hypothesis on s is needed.

theorem exists_cokernelIso_unit_zeroScheme (s : L.sections) :
    let i := (zeroScheme X L (s.eval (op ⊤))).subschemeι
    ∃ e : cokernel (L.unitHomEquiv.symm s) ≅
        (Scheme.Modules.pushforward i).obj ((Scheme.Modules.pullback i).obj L),
      cokernel.π (L.unitHomEquiv.symm s) ≫ e.hom =
        (Scheme.Modules.pullbackPushforwardAdjunction i).unit.app L

AlgebraicGeometry.shortExact_zeroScheme_of_isRegularSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/ZeroSchemeExactSequence.lean, line 269. The attribute's comment: “regular_section_sequence”.

For an invertible module L on a scheme X and a regular global section s ([Stacks, Tag 01WY]), the sequence 0 ⟶ 𝒪_X ⟶ L ⟶ i_* i^* L ⟶ 0 is short exact, where i is the inclusion of the zero scheme of s.

theorem shortExact_zeroScheme_of_isRegularSection (s : L.sections)
    (hs : IsRegularSection X.sheaf.obj X.ringCatSheaf.property s) :
    let i := (zeroScheme X L (s.eval (op ⊤))).subschemeι
    let O : X.Modules := SheafOfModules.unit X.ringCatSheaf
    let f : O ⟶ L := L.unitHomEquiv.symm s
    let g : L ⟶ (Scheme.Modules.pushforward i).obj ((Scheme.Modules.pullback i).obj L) :=
      (Scheme.Modules.pullbackPushforwardAdjunction i).unit.app L
    ∃ h : f ≫ g = 0, (ShortComplex.mk f g h).ShortExact

Stacks.IdealSheafSequence.divisorIdeal_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/IdealSheafSequence/Basic.lean, line 116. The attribute's comment: “divisor_ideal_sequence”. References: SGA 6 X (5.2.2), “more general”.

Stacks Tag 0C6K, the label divisor_ideal_sequence. For a closed subscheme D of a scheme X with inclusion i, the canonical sequence 0 ⟶ ℐ_D ⟶ 𝒪_X ⟶ i_* 𝒪_D ⟶ 0 of sheaves of 𝒪_X-modules is short exact.

The effective-Cartier hypothesis of Tag 0C6K is not used: it is what makes ℐ_D the invertible module 𝒪_X(-D), and the exactness of the sequence does not depend on it.

theorem divisorIdeal_shortExact :
    ∃ hz : divisorIdealMap D ≫ divisorQuotientMap D = 0,
      (ShortComplex.mk (divisorIdealMap D) (divisorQuotientMap D) hz).ShortExact

Stacks.Tag0C6KSectionIdeal.exists_cokernelIso_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionIdeal/Basic.lean, line 204. The attribute's comment: “regular_section_sequence”.

The first assertion of Stacks Tag 0C6K's label regular_section_sequence. For L an invertible 𝒪_X-module and s a global section of L, the restriction map L ⟶ i_* (L|_{Z(s)}) to the zero scheme of s is the cokernel of multiplication by s, compatibly with the cokernel projection. No regularity of s is used, as in the source.

theorem exists_cokernelIso_zeroScheme (L : SheafOfModules.{u} X.ringCatSheaf)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections) :
    ∃ e : cokernel (L.unitHomEquiv.symm s) ≅
        (SheafOfModules.pushforward.{u} (Stacks.RegularSectionSequence.zeroScheme X L
            (s.eval (op ⊤))).subschemeι.toRingCatSheafHom).obj
          ((SheafOfModules.pullback.{u} (Stacks.RegularSectionSequence.zeroScheme X L
            (s.eval (op ⊤))).subschemeι.toRingCatSheafHom).obj L),
      cokernel.π (L.unitHomEquiv.symm s) ≫ e.hom =
        Stacks.RegularSectionSequence.restrictionUnit
          (Stacks.RegularSectionSequence.zeroScheme X L (s.eval (op ⊤))) L

Stacks.Tag0C6KSectionIdeal.shortExact_zeroScheme, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionIdeal/Basic.lean, line 222. The attribute's comment: “regular_section_sequence”.

The second assertion of Stacks Tag 0C6K's label regular_section_sequence. For s a regular global section of an invertible module — regularity being monicity of multiplication by s, which is Stacks Tag 01WY and is literally the hypothesis below — the sequence 0 ⟶ 𝒪_X ⟶ L ⟶ i_* (L|_{Z(s)}) ⟶ 0 is short exact.

theorem shortExact_zeroScheme (L : SheafOfModules.{u} X.ringCatSheaf)
    [SheafOfModules.IsInvertible X.sheaf.obj X.ringCatSheaf.property L] (s : L.sections)
    [Mono (L.unitHomEquiv.symm s)] :
    ∃ h : L.unitHomEquiv.symm s ≫ Stacks.RegularSectionSequence.restrictionUnit
        (Stacks.RegularSectionSequence.zeroScheme X L (s.eval (op ⊤))) L = 0,
      (ShortComplex.mk (L.unitHomEquiv.symm s)
        (Stacks.RegularSectionSequence.restrictionUnit
          (Stacks.RegularSectionSequence.zeroScheme X L (s.eval (op ⊤))) L) h).ShortExact

Sources

LeanStacks.Divisors.negativeTwist' · Stacks.Divisors.invertibleSheaf' · Stacks.Divisors.invertibleSheaf_isInvertible · Stacks.Divisors.canonicalSection' · Stacks.Divisors.invertibleSheafIsoInverseIdeal · Stacks.Divisors.negativeTwistIso · Stacks.Divisors.differenceTwist' · Stacks.Divisors.negativeTwist

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

31.2 Associated points to 31.15 Effective Cartier…

Section31.2 Associated points#

Tag 02OJ, a definition

Tag 02OK, a lemma

Tag 05AD, a lemma

Tag 05AE, a lemma

Tag 05AF, a lemma

Tag 05AG, a lemma

Tag 05AI, an example

Tag 0B3L, a lemma

Tag 05AH, a lemma

Tag 0AVL, a lemma

Tag 0AVM, a lemma

Sources

Section31.3 Morphisms and associated points#

Tag 05DB, a lemma

Sources

Section31.4 Embedded points#

Tag 05AK, a definition

Tag 05AL, a lemma

Tag 0346, a lemma

Tag 0BXG, a lemma

Tag 083P, a lemma

Tag 02OL, a lemma

Tag 02OM, a lemma

Sources

Section31.5 Weakly associated points#

Tag 056L, a definition

Tag 056M, a lemma

Tag 05AM, a lemma

Tag 05AN, a lemma

Tag 05AP, a lemma

Tag 0B3M, a lemma

Tag 05AQ, a lemma

Tag 05AR, a lemma

Tag 0AVN, a lemma

Tag 0AVP, a lemma

Tag 0E9I, a lemma

Tag 0EME, a lemma

Sources

Section31.6 Morphisms and weakly associated points#

Tag 05EX, a lemma

Tag 05EY, a lemma

Tag 05EZ, a lemma

Tag 05F0, a lemma

Tag 0CUC, a lemma

Tag 0EY0, a lemma

Sources

Section31.7 Relative assassin#

Tag 05AT, a definition

Tag 0CU5, a lemma

Tag 05DC, a lemma

Tag 05KL, a remark

Sources

Section31.8 Relative weak assassin#

Tag 05AV, a definition

Tag 05F2, a lemma

Tag 0CUD, a lemma

Sources

Section31.9 Fitting ideals#

Tag 0C3D, a lemma

Tag 0C3E, a lemma

Tag 0CYX, a lemma

Tag 0C3F, a lemma

Tag 0C3G, a lemma

Tag 05P8, a lemma

Tag 05P9, a lemma

Sources

Section31.10 The singular locus of a morphism#

Tag 0C3I, a lemma

Tag 0C3J, a lemma

Tag 0C3K, a lemma

Sources

Section31.11 Torsion free modules#

Tag 0AXR, a lemma

Tag 0AVR, a definition

Tag 0AXS, a lemma

Tag 0AXT, a lemma

Tag 0AXU, a lemma

Tag 0AXV, a lemma

Section31.2 Associated points #

Section31.3 Morphisms and associated points #

Section31.4 Embedded points #

Section31.5 Weakly associated points #

Section31.6 Morphisms and weakly associated points #

Section31.7 Relative assassin #

Section31.8 Relative weak assassin #

Section31.9 Fitting ideals #

Section31.10 The singular locus of a morphism #

Section31.11 Torsion free modules #

Section31.13 Reflexive modules #

Section31.14 Effective Cartier divisors #

Section31.15 Effective Cartier divisors and invertible sheaves #