CartierPullback.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Cartier pullback and coherent lattice filtrations

This development accompanies A Complete Local Domain without a Small Cohen–Macaulay Module (OpenAI, 2026).

theorem OAI.kernelMono line 10
Also declared: OAI/AlgebraicGeometry/SurfaceCones/CartierSupport.lean:20 (same declaration text).
theorem OAI.counitIsIso line 15
def OAI.ActualCartier.restrictionUnit line 35
lemma OAI.ActualCartier.restrictionUnit_zero line 38

def OAI.ActualCartier.restrictionUnitIsColimit line 43

Source documentation

This is the cokernel fork in all sheaves of modules after forgetting coherence.

def restrictionUnitIsColimit (M : Coh Y) :
    IsColimit (CokernelCofork.ofπ ((restrictionUnit f d).app M).hom
      (show ((action f d).app M).hom ≫ ((restrictionUnit f d).app M).hom = 0 from
        congrArg (fun z => z.hom) (NatTrans.congr_app (restrictionUnit_zero f d) M))) := by
…

Mentions: OAI.ActualCartier.restrictionUnit, OAI.ActualCartier.action, OAI.ActualCartier.restrictionUnit_zero

def OAI.ActualCartier.restrictionPullbackIso line 56
Source documentation
The descended ordinary restriction is the geometric pullback. This spells out its universal property, rather than using the desired identification as an extra hypothesis.
```
def restrictionPullbackIso (M : Coh Y) :
    (Scheme.Modules.pullback f).obj M.obj ≅ ((restriction f d).obj M).obj := by
…
```
Mentions: OAI.ActualCartier.restriction
lemma OAI.ActualCartier.coherent_pullback line 76
lemma OAI.ActualCartier.firstTor_isZero line 94
Source documentation
The first Cartier Tor vanishes for a sectionwise torsion-free coherent sheaf: this is proved from the invertible ideal action.
```
lemma firstTor_isZero (M : Coh Y)
    (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.obj.val.obj U)) :
    IsZero ((firstTor f d).obj M) := by
…
```
Mentions: OAI.ActualCartier.firstTor
lemma OAI.ActualCartier.derivedRestriction_cls_torsionFree line 111
lemma OAI.ActualCartier.action_pushforward_zero line 118
Source documentation
A coherent sheaf pushed forward from the divisor has zero Cartier action.
```
lemma action_pushforward_zero (N : Coh X) :
    (action f d).app ((cohPushforward f).obj N) = 0 := by
…
```
Mentions: OAI.ActualCartier.action
def OAI.ActualCartier.firstTor_supported_pushforwardIso line 125
Source documentation
The first Tor of a supported layer is the ambient ideal line tensor after closed pushforward. Full faithfulness descends this identification to the divisor.
```
def firstTor_supported_pushforwardIso (N : Coh X) :
    (cohPushforward f).obj ((firstTor f d).obj ((cohPushforward f).obj N)) ≅
      (coherentTensorLine (idealSheaf f) d).obj ((cohPushforward f).obj N) :=
…
```
Mentions: OAI.ActualCartier.firstTor, OAI.ActualCartier.idealSheaf
def OAI.ActualCartier.restriction_supported_iso line 135
Source documentation
Ordinary restriction of a closed pushforward is the original coherent sheaf on the divisor.
```
def restriction_supported_iso (N : Coh X) :
    (restriction f d).obj ((cohPushforward f).obj N) ≅ N :=
…
```
Mentions: OAI.ActualCartier.restriction
lemma OAI.ActualCartier.derivedRestriction_supported line 141

lemma OAI.ActualSheafTensor.tensorSchemeRestrictIso_inv_pure line 158

Source documentation

The inverse restriction comparison is the identity on pure sections, with the scalar action transported by the open immersion's ring isomorphism.

lemma tensorSchemeRestrictIso_inv_pure (M N : X.Modules) (V : U.toScheme.Opens)
    (x : ((restrictFunctor U.ι).obj M).val.obj (op V))
    (y : ((restrictFunctor U.ι).obj N).val.obj (op V)) :
    (tensorSchemeRestrictIso X U M N).inv.val.app (op V)
      (pure U.toScheme.sheaf ((restrictFunctor U.ι).obj M)
        ((restrictFunctor U.ι).obj N) (op V) x y) =
    pure X.sheaf M N (op (U.ι ''ᵁ V)) x y := by
…

Mentions: OAI.ActualSheafTensor.tensorSchemeRestrictIso, OAI.ActualSheafTensor.pure

lemma OAI.ActualSheafTensor.tensorLeft_map_pure line 207
lemma OAI.ActualSheafTensor.pure_naturality line 216
def OAI.ActualSheafTensor.projectionRestrictLeft line 234
def OAI.ActualSheafTensor.projectionRestrictRight line 244
lemma OAI.ActualSheafTensor.projectionRestrictLeft_pure line 261
lemma OAI.ActualSheafTensor.projectionRestrictRight_pure line 287
lemma OAI.ActualSheafTensor.tensorProjection_restrict line 324
Source documentation
The tensor projection morphism commutes with open restriction through the pullback comparison induced by the adjunction.
```
lemma tensorProjection_restrict :
    projectionRestrictLeft f U L N = projectionRestrictRight f U L N := by
…
```
Mentions: OAI.ActualSheafTensor.projectionRestrictLeft, OAI.ActualSheafTensor.projectionRestrictRight
lemma OAI.ActualSheafTensor.projectionRestrictRight_isIso line 346
lemma OAI.ActualSheafTensor.projectionRestrict_isIso line 374
lemma OAI.ActualSheafTensor.tensorProjection_isIso_of_line line 394
Source documentation
Projection formula for the tensor sheaf and any line bundle, proved locally from its pure-section projection morphism.
```
lemma tensorProjection_isIso_of_line (d : LineTrivialization Y.sheaf L) (N : X.Modules) :
    IsIso (tensorProjection f L N) := by
…
```
Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensorProjection

def OAI.ActualSheafTensor.tensorProjectionIso line 401

Source documentation

The canonical projection-formula isomorphism for any line bundle.

def tensorProjectionIso (d : LineTrivialization Y.sheaf L) (N : X.Modules) :
    tensor Y.sheaf L ((pushforward f).obj N) ≅
      (pushforward f).obj (tensor X.sheaf ((Scheme.Modules.pullback f).obj L) N) := by
…

Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensor

lemma OAI.ActualCartier.coherent_conormal_tensor line 422
Source documentation
Tensor by the conormal line preserves coherence on the divisor by the projection formula and coherent Cartier pullback.
```
lemma coherent_conormal_tensor (N : Coh X) :
    (tensor X.sheaf ((Scheme.Modules.pullback f).obj (idealSheaf f)) N.obj).IsFinitePresentation := by
…
```
Mentions: OAI.ActualCartier.idealSheaf
def OAI.ActualCartier.conormalTensor line 435
Source documentation
The conormal twist, as a coherent sheaf ON the Cartier divisor.
```
def conormalTensor (N : Coh X) : Coh X :=
…
```
def OAI.ActualCartier.conormalProjectionIso line 439
def OAI.ActualCartier.firstTor_supported_iso line 445
Source documentation
The first Tor of a supported layer is its tensor by the conormal sheaf on the divisor.
```
def firstTor_supported_iso (N : Coh X) :
    (firstTor f d).obj ((cohPushforward f).obj N) ≅ conormalTensor f d N :=
…
```
Mentions: OAI.ActualCartier.firstTor, OAI.ActualCartier.conormalTensor
lemma OAI.ActualCartier.derivedRestriction_conormal line 451
Source documentation
The precise class formula used for each supported layer in the Cartier restriction formula.
```
lemma derivedRestriction_conormal (N : Coh X) :
    derivedRestriction f d (cls ((cohPushforward f).obj N)) =
      cls N - cls (conormalTensor f d N) := by
…
```
Mentions: OAI.ActualCartier.derivedRestriction, OAI.ActualCartier.conormalTensor

lemma OAI.ActualCartier.lattice_firstTor_identity line 469

Source documentation

The coherent Grothendieck identity for an inclusion of torsion-free lattices whose quotient has a finite filtration by divisor sheaves.

lemma lattice_firstTor_identity {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (h₁ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₁.obj.val.obj U))
    (h₂ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U))
    (layers : List (Coh X))
    (hlayers : FilteredBy S.X₃ (layers.map (cohPushforward f).obj)) :
    cls ((restriction f d).obj S.X₁) = cls ((restriction f d).obj S.X₂) +
      (layers.map fun Q =>
        cls ((firstTor f d).obj ((cohPushforward f).obj Q)) - cls Q).sum := by
…

Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.firstTor

def OAI.ActualCartier.restrictionCokernelIso line 508
Source documentation
Ordinary restriction is the cokernel of the ideal action.
```
def restrictionCokernelIso (M : Coh Y) :
    (cohPushforward f).obj ((restriction f d).obj M) ≅ cokernel ((action f d).app M) :=
…
```
Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.action
abbrev OAI.ActualCartier.idealMultiple line 514
Source documentation
Repeated images of the Cartier ideal action on a coherent sheaf.
```
abbrev idealMultiple (n : ℕ) (M : Coh Y) : Coh Y :=
…
```
abbrev OAI.ActualCartier.idealLayers line 518
Source documentation
The coherent layers of the ideal-adic image filtration.
```
abbrev idealLayers (n : ℕ) (M : Coh Y) : List (Coh X) :=
…
```
lemma OAI.ActualCartier.filteredBy_idealLayers line 523

lemma OAI.ActualCartier.lattice_conormal_identity line 530

Source documentation

Coherent K₀ identity of the Cartier restriction formula, with each supported term identified ON the divisor as its conormal tensor.

lemma lattice_conormal_identity {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (h₁ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₁.obj.val.obj U))
    (h₂ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U))
    (layers : List (Coh X))
    (hlayers : FilteredBy S.X₃ (layers.map (cohPushforward f).obj)) :
    cls ((restriction f d).obj S.X₁) = cls ((restriction f d).obj S.X₂) +
      (layers.map fun Q => cls (conormalTensor f d Q) - cls Q).sum := by
…

Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.conormalTensor

lemma OAI.ActualCartier.lattice_nilpotent_identity line 542

Source documentation

A nilpotent ideal quotient gives a finite coherent filtration for the Cartier lattice identity.

lemma lattice_nilpotent_identity {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (h₁ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₁.obj.val.obj U))
    (h₂ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U))
    (n : ℕ) (hn : IsZero (idealMultiple f d n S.X₃)) :
    cls ((restriction f d).obj S.X₁) = cls ((restriction f d).obj S.X₂) +
      ((idealLayers f d n S.X₃).map fun Q => cls (conormalTensor f d Q) - cls Q).sum :=
…

Mentions: OAI.ActualCartier.idealMultiple, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor

lemma OAI.CartierImageFiltration.map_powerAction_zero_of_le line 564
Source documentation
A locally vanishing ideal power remains vanishing at every larger exponent, by naturality of the iterated action.
```
lemma map_powerAction_zero_of_le (M : C) {n m : ℕ} (hnm : n ≤ m)
    (hn : F.map ((powerAction T a n).app M) = 0) :
    F.map ((powerAction T a m).app M) = 0 := by
…
```
Mentions: OAI.CartierImageFiltration.powerAction

lemma OAI.ActualCartier.idealMultiple_isZero_of_finite_cover line 585

Source documentation

Finitely many locally vanishing Cartier powers give a global nilpotence exponent and a finite supported filtration.

lemma idealMultiple_isZero_of_finite_cover
    {ι : Type} [Fintype ι] (U : ι → Y.Opens)
    (hU : (Opens.grothendieckTopology Y).CoversTop U) (M : Coh Y)
    (h : ∀ i, ∃ n : ℕ,
      (((cohInclusion Y).map
        ((powerAction (coherentTensorLine (idealSheaf f) d) (action f d) n).app M)).over
          (U i)) = 0) :
    ∃ n : ℕ, IsZero (idealMultiple f d n M) := by
…

Mentions: OAI.ActualCartier.idealSheaf, OAI.ActualCartier.action, OAI.ActualCartier.idealMultiple

lemma OAI.CartierAffineCoverNilpotence.exists_powerAction_zero line 627

Source documentation

Support on finitely many principal Cartier charts gives a vanishing tensor-ideal power.

lemma exists_powerAction_zero (M : Y.Modules) [M.IsFinitePresentation]
    (hM : ∀ j, IsZero (((restrictFunctor (f j)).obj M).over
      (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
        ((restrictFunctor (f j)).obj L) (e j) (restrictedIdeal (f j) i))))) :
    ∃ n : ℕ, (powerAction (tensorLeft Y.sheaf L) (idealAction Y.sheaf i) n).app M = 0 := by
…

Mentions: OAI.AffineCartierNilpotence.equation

instance OAI.ActualCartier.firstTor_additive line 664
instance OAI.ActualCartier.restriction_additive line 671
instance OAI.ActualCartier.restrictionUnit_epi line 689
instance OAI.ActualCartier.restriction_preservesEpis line 693
abbrev OAI.ActualCartier.layer line 704
Source documentation
The jth supported quotient of the ideal-image filtration.
```
abbrev layer (j : ℕ) (M : Coh Y) : Coh X :=
…
```
def OAI.ActualCartier.layerCover line 709
Source documentation
An ambient ideal power of the original lattice surjects onto each corresponding layer of its quotient.
```
def layerCover {L Q : Coh Y} (q : L ⟶ Q) (j : ℕ) :
    (CartierImageFiltration.power (coherentTensorLine (idealSheaf f) d) j).obj L ⟶
      (cohPushforward f).obj (layer f d j Q) :=
…
```
Mentions: OAI.CartierImageFiltration.power, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.layer
instance OAI.ActualCartier.layerCover_epi line 716
def OAI.ActualCartier.layerQuotient line 722
Source documentation
The quotient morphism on the Cartier divisor.
```
def layerQuotient {L Q : Coh Y} (q : L ⟶ Q) (j : ℕ) :
    (restriction f d).obj
      ((CartierImageFiltration.power (coherentTensorLine (idealSheaf f) d) j).obj L) ⟶
      layer f d j Q :=
…
```
Mentions: OAI.ActualCartier.restriction, OAI.CartierImageFiltration.power, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.layer
instance OAI.ActualCartier.layerQuotient_epi line 729

lemma OAI.ActualCartier.lattice_sandwich_identity line 736

Source documentation

An ideal-power containment in a lattice inclusion gives nilpotence and coherent layers in the conormal Grothendieck identity.

lemma lattice_sandwich_identity {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (h₁ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₁.obj.val.obj U))
    (h₂ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U))
    (n : ℕ)
    (b : (CartierImageFiltration.power (coherentTensorLine (idealSheaf f) d) n).obj S.X₂ ⟶ S.X₁)
    (hb : b ≫ S.f =
      (CartierImageFiltration.powerAction (coherentTensorLine (idealSheaf f) d) (action f d) n).app S.X₂) :
    cls ((restriction f d).obj S.X₁) = cls ((restriction f d).obj S.X₂) +
      ((idealLayers f d n S.X₃).map fun Q => cls (conormalTensor f d Q) - cls Q).sum := by
…

Mentions: OAI.CartierImageFiltration.power, OAI.ActualCartier.idealSheaf, OAI.CartierImageFiltration.powerAction, OAI.ActualCartier.action, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor

def OAI.ActualCartier.conormalFunctor line 761
Source documentation
Tensor by the conormal line, on coherent sheaves of the divisor.
```
def conormalFunctor : Coh X ⥤ Coh X :=
…
```
lemma OAI.ActualCartier.action_central line 767
def OAI.ActualCartier.restriction_tensorLine_iso line 775
Source documentation
Cartier restriction sends an ideal twist to the conormal twist by preservation of cokernels and centrality of multiplication.
```
def restriction_tensorLine_iso (M : Coh Y) :
    (restriction f d).obj ((coherentTensorLine (idealSheaf f) d).obj M) ≅
      (conormalFunctor f d).obj ((restriction f d).obj M) := by
…
```
Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.conormalFunctor

def OAI.ActualCartier.restriction_powerIso line 789

Source documentation

Restricting each ambient ideal power gives the corresponding conormal tensor power on the divisor.

def restriction_powerIso : (j : ℕ) → (M : Coh Y) →
    (restriction f d).obj ((power (coherentTensorLine (idealSheaf f) d) j).obj M) ≅
      (power (conormalFunctor f d) j).obj ((restriction f d).obj M)
  | 0, _ => Iso.refl _
  | j + 1, M => restriction_powerIso j ((coherentTensorLine (idealSheaf f) d).obj M) ≪≫
      (power (conormalFunctor f d) j).mapIso (restriction_tensorLine_iso f d M)

/-- The surjection from the jth conormal twist of the original
restricted lattice onto its jth supported quotient (the ideal-image filtration). -/

Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.conormalFunctor, OAI.ActualCartier.restriction_tensorLine_iso

def OAI.ActualCartier.twistedLayerQuotient line 798
Source documentation
The surjection from the jth conormal twist of the original restricted lattice onto its jth supported quotient (the ideal-image filtration).
```
def twistedLayerQuotient {L Q : Coh Y} (q : L ⟶ Q) (j : ℕ) :
    (power (conormalFunctor f d) j).obj ((restriction f d).obj L) ⟶ layer f d j Q :=
…
```
Mentions: OAI.ActualCartier.conormalFunctor, OAI.ActualCartier.restriction, OAI.ActualCartier.layer
instance OAI.ActualCartier.twistedLayerQuotient_epi line 802

lemma OAI.ActualCartier.exists_idealMultiple_isZero_of_support line 828

Source documentation

Support on the finite principal-chart complement yields a finite filtration by the Cartier ideal images in the coherent category.

lemma exists_idealMultiple_isZero_of_support (M : Coh Y)
    (hM : ∀ j, IsZero (((restrictFunctor (f j)).obj M.obj).over
      (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
        ((restrictFunctor (f j)).obj (idealSheaf g)) (e j)
        (restrictedIdeal (f j) (idealι g)))))) :
    ∃ n : ℕ, IsZero (idealMultiple g d n M) := by
…

Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualCartier.idealMultiple

lemma OAI.ActualCartier.lattice_support_identity line 848

Source documentation

The divisor-side Grothendieck lattice identity follows from local support.

lemma lattice_support_identity {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (h₁ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₁.obj.val.obj U))
    (h₂ : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U))
    (hQ : ∀ j, IsZero (((restrictFunctor (f j)).obj S.X₃.obj).over
      (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
        ((restrictFunctor (f j)).obj (idealSheaf g)) (e j)
        (restrictedIdeal (f j) (idealι g)))))) :
    ∃ n : ℕ, cls ((restriction g d).obj S.X₁) = cls ((restriction g d).obj S.X₂) +
      ((idealLayers g d n S.X₃).map fun Q => cls (conormalTensor g d Q) - cls Q).sum := by
…

Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor