Effective Cartier divisors

An effective Cartier divisor on an integral scheme is presented by a Cartier divisor, a closed subscheme, and an identification of O_X(-D) with the ideal sheaf of that subscheme. This file constructs the fundamental sequence

0 → O_X(-D) → O_X → i_* O_D → 0,

proves its exactness in X.Modules, and lifts it to Coh X under explicit coherence hypotheses. Exact tensoring by an invertible sheaf is supplied by the neutral Modules.Tensor layer; this gives the normalized twisted sequence

0 → O_X(E-D) → O_X(E) → O_X(E) ⊗ i_* O_D → 0.

The closed subscheme comes from Mathlib's Scheme.IdealSheafData.subscheme. Surjectivity of the quotient map is checked locally on the affine-open basis, where Mathlib supplies the corresponding surjectivity theorem.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.quotientMap {X : Scheme} (I : X.IdealSheafData) : Modules.Hom (SheafOfModules.unit X.ringCatSheaf) ((Modules.pushforward I.subschemeι).obj (SheafOfModules.unit I.subscheme.ringCatSheaf))

The quotient from the structure sheaf to the pushed-forward structure sheaf of the closed subscheme defined by an ideal sheaf.

Equations

• I.quotientMap = SheafOfModules.unitToPushforwardObjUnit (AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom I.subschemeι)

instance AlgebraicGeometry.Scheme.IdealSheafData.quotientMap_epi {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.Epi I.quotientMap

The structure-sheaf quotient defining a closed subscheme is an epimorphism.

The affine opens are a basis, so every point of an open U sits in an affine V ≤ U, and subschemeι_app_surjective produces a preimage there. That is exactly the pointwise hypothesis of Modules.epi_of_pointwise_preimages, which runs the local-surjectivity chain.

structure AlgebraicGeometry.Scheme.EffectiveCartierDivisor {X : Scheme} [IsIntegral X] : Type u

An effective Cartier divisor is a Cartier divisor whose inverse associated sheaf is the ideal sheaf of a closed subscheme.

• divisor : ↥X.CartierDivisor
• idealSheaf : X.IdealSheafData
• idealIso : CartierDivisor.associatedSheaf (-self.divisor) ≅ CategoryTheory.Limits.kernel self.idealSheaf.quotientMap

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.structureSheaf {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : X.Modules

The pushed-forward structure sheaf of the divisor's closed subscheme.

Equations

• D.structureSheaf = (AlgebraicGeometry.Scheme.Modules.pushforward D.idealSheaf.subschemeι).obj (SheafOfModules.unit D.idealSheaf.subscheme.ringCatSheaf)

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.quotient {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : Modules.Hom (SheafOfModules.unit X.ringCatSheaf) D.structureSheaf

The quotient O_X → i_* O_D.

Equations

• D.quotient = D.idealSheaf.quotientMap

instance AlgebraicGeometry.Scheme.EffectiveCartierDivisor.quotient_epi {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : CategoryTheory.Epi D.quotient

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.idealInclusion {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : (CartierDivisor.associatedSheaf (-D.divisor)).Hom (SheafOfModules.unit X.ringCatSheaf)

The canonical inclusion O_X(-D) → O_X.

Equations

• D.idealInclusion = CategoryTheory.CategoryStruct.comp D.idealIso.hom (CategoryTheory.Limits.kernel.ι D.quotient)

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.fundamentalSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : CategoryTheory.ShortComplex X.Modules

The fundamental complex O_X(-D) → O_X → i_* O_D.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.fundamentalSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : D.fundamentalSequence.ShortExact

The fundamental sequence of an effective Cartier divisor is short exact.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cokernelIsoStructureSheaf {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) : CategoryTheory.Limits.cokernel D.idealInclusion ≅ D.structureSheaf

The divisor structure sheaf is the cokernel of O_X(-D) → O_X.

Equations

• D.cokernelIsoStructureSheaf = (CategoryTheory.Limits.cokernelIsCokernel D.idealInclusion).coconePointUniqueUpToIso ⋯.gIsCokernel

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistedStructureSheaf {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : X.Modules

The structure sheaf of the divisor, twisted by O_X(E).

Equations

• D.twistedStructureSheaf E = (AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf E).tensorObj D.structureSheaf

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.tensorTwistSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : CategoryTheory.ShortComplex X.Modules

Tensor form of the fundamental sequence twisted by O_X(E).

Equations

• D.tensorTwistSequence E = D.fundamentalSequence.map (AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf E).tensorLeftFunctor

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistSourceIso {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : (D.tensorTwistSequence E).X₁ ≅ CartierDivisor.associatedSheaf (E - D.divisor)

The source of the tensor-twisted sequence is O_X(E - D).

Equations

• D.twistSourceIso E = AlgebraicGeometry.Scheme.CartierDivisor.associatedTensorAddIso E (-D.divisor) ≪≫ CategoryTheory.eqToIso ⋯

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistMiddleIso {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : (D.tensorTwistSequence E).X₂ ≅ CartierDivisor.associatedSheaf E

The middle of the tensor-twisted sequence is O_X(E).

Equations

• D.twistMiddleIso E = (AlgebraicGeometry.Scheme.CartierDivisor.associatedSheaf E).tensorUnitRightIso

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistedIdealInclusion {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : CartierDivisor.associatedSheaf (E - D.divisor) ⟶ CartierDivisor.associatedSheaf E

The inclusion O_X(E - D) → O_X(E).

Equations

• D.twistedIdealInclusion E = CategoryTheory.CategoryStruct.comp (D.twistSourceIso E).inv (CategoryTheory.CategoryStruct.comp (D.tensorTwistSequence E).f (D.twistMiddleIso E).hom)

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistedQuotient {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : CartierDivisor.associatedSheaf E ⟶ D.twistedStructureSheaf E

The quotient O_X(E) → O_X(E) ⊗ i_* O_D.

Equations

• D.twistedQuotient E = CategoryTheory.CategoryStruct.comp (D.twistMiddleIso E).inv (D.tensorTwistSequence E).g

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : CategoryTheory.ShortComplex X.Modules

The normalized twisted fundamental sequence O_X(E-D) → O_X(E) → O_X(E) ⊗ i_* O_D.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : (D.twistSequence E).ShortExact

Twisting the fundamental sequence by any Cartier divisor remains short exact.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistCokernelIso {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) (E : ↥X.CartierDivisor) : CategoryTheory.Limits.cokernel (D.twistedIdealInclusion E) ≅ D.twistedStructureSheaf E

The final term of the twisted sequence is the cokernel of its inclusion.

Equations

• D.twistCokernelIso E = (CategoryTheory.Limits.cokernelIsCokernel (D.twistedIdealInclusion E)).coconePointUniqueUpToIso ⋯.gIsCokernel

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.structureSheaf_isCoherent {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (hIdeal : X.coherent (CartierDivisor.associatedSheaf (-D.divisor))) (hUnit : X.coherent (SheafOfModules.unit X.ringCatSheaf)) : X.coherent D.structureSheaf

The divisor structure sheaf is coherent when O_X(-D) and O_X are coherent.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohFundamentalSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (hIdeal : X.coherent (CartierDivisor.associatedSheaf (-D.divisor))) (hUnit : X.coherent (SheafOfModules.unit X.ringCatSheaf)) : CategoryTheory.ShortComplex (Coh X)

The coherent-sheaf form of the fundamental sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohFundamentalSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (hIdeal : X.coherent (CartierDivisor.associatedSheaf (-D.divisor))) (hUnit : X.coherent (SheafOfModules.unit X.ringCatSheaf)) : (D.cohFundamentalSequence hIdeal hUnit).ShortExact

The coherent fundamental sequence is short exact.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.twistedStructureSheaf_isCoherent {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) : X.coherent (D.twistedStructureSheaf E)

The twisted divisor sheaf is coherent when the two line-bundle terms are coherent.

noncomputable def AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistSequence {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) : CategoryTheory.ShortComplex (Coh X)

The coherent-sheaf form of the twisted fundamental sequence.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.EffectiveCartierDivisor.cohTwistSequence_shortExact {X : Scheme} [IsIntegral X] (D : EffectiveCartierDivisor) [IsLocallyNoetherian X] (E : ↥X.CartierDivisor) (hSource : X.coherent (CartierDivisor.associatedSheaf (E - D.divisor))) (hMiddle : X.coherent (CartierDivisor.associatedSheaf E)) : (D.cohTwistSequence E hSource hMiddle).ShortExact

The coherent twisted fundamental sequence is short exact.