GeometricChartSandwich.lean`

48 declarations, 0 contain sorry, 0 declared as axioms

Cartier twists on affine charts and derived restriction

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

lemma OAI.ActualCartier.exists_chart_sandwich_on_geometric_puncture line 28

Source documentation

Uniform affine Cartier lattice embeddings retain the fixed isomorphism on the entire geometric puncture of the chart.

lemma exists_chart_sandwich_on_geometric_puncture (M N : Y.Modules)
    [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (M.val.obj V))
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ≅
      N.over (ActualOpenSupport.complement g)) :
    let L := (restrictFunctor f).obj (idealSheaf g)
…

Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.idealSheaf

lemma OAI.ActualCartier.exists_chart_global_power_sandwich line 73

Source documentation

Affine denominator clearing for restrictions of global Cartier twists. The embeddings agree with the fixed puncture identification, and the tensor comparison intertwines their iterated actions.

lemma exists_chart_global_power_sandwich (M N : Y.Modules)
    [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (M.val.obj V))
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (e : M.over (ActualOpenSupport.complement g) ≅
      N.over (ActualOpenSupport.complement g)) :
    let T := tensorLeft Y.sheaf (idealSheaf g)
…

Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.idealSheaf

def OAI.ActualSheafTensor.pullbackUnitSemilinear line 143
def OAI.ActualSheafTensor.pushforwardSemilinear line 150
def OAI.ActualSheafTensor.tensorProjectionApp line 157
def OAI.ActualSheafTensor.tensorProjectionPresheaf line 211
def OAI.ActualSheafTensor.tensorProjection line 249
Source documentation
The canonical projection morphism for the tensor sheaves.
```
def tensorProjection : tensor Y.sheaf L ((pushforward f).obj N) ⟶
    (pushforward f).obj (tensor X.sheaf ((Scheme.Modules.pullback f).obj L) N) :=
…
```
Mentions: OAI.ActualSheafTensor.tensor
lemma OAI.ActualSheafTensor.tensorProjection_pure line 254
lemma OAI.ActualSheafTensor.tensorProjection_pure' line 282
lemma OAI.ActualSheafTensor.tensorProjection_naturality_left line 291
lemma OAI.ActualSheafTensor.opensMap_final line 329

def OAI.ActualSheafTensor.sheafPullbackUnitIso line 338

Source documentation

Canonical identification of the pullback of the unit sheaf.

def sheafPullbackUnitIso : (Scheme.Modules.pullback f).obj (SheafOfModules.unit _) ≅
    SheafOfModules.unit X.ringCatSheaf := by
…

lemma OAI.ActualSheafTensor.sheafPullbackUnitIso_unit line 353

def OAI.ActualSheafTensor.tensorProjectionUnitTargetIso line 365

Source documentation

Target trivialization for the projection formula with unit coefficients.

def tensorProjectionUnitTargetIso (N : X.Modules) :
    (pushforward f).obj (tensor X.sheaf
      ((Scheme.Modules.pullback f).obj (SheafOfModules.unit _)) N) ≅
      (pushforward f).obj N :=
…

Mentions: OAI.ActualSheafTensor.tensor

lemma OAI.ActualSheafTensor.tensorProjection_unit line 372
instance OAI.ActualSheafTensor.tensorProjection_unit_isIso line 396
lemma OAI.ActualSheafTensor.tensorProjection_isIso_of_trivial line 406
Source documentation
For a trivial line, the projection morphism is an isomorphism.
```
lemma tensorProjection_isIso_of_trivial {L : Y.Modules}
    (e : L ≅ SheafOfModules.unit _) (N : X.Modules) : IsIso (tensorProjection f L N) := by
…
```
Mentions: OAI.ActualSheafTensor.tensorProjection

def OAI.ActualSheafTensor.sliceUnitIso line 431

Source documentation

Convert an open-subscheme unit trivialization to the exact slice-site unit trivialization used by the tensor construction.

def sliceUnitIso {X : Scheme.{0}} (L : X.Modules) (U : X.Opens)
    (e : (restrictFunctor U.ι).obj L ≅ SheafOfModules.unit U.toScheme.ringCatSheaf) :
    L.over U ≅ SheafOfModules.unit (X.ringCatSheaf.over U) :=
…

def OAI.ActualSheafTensor.LineTrivialization.pullback line 440
Source documentation
The pullback of a line bundle is a line bundle, via inverse-image trivializing opens and the pullback of the unit.
```
def LineTrivialization.pullback {X Y : Scheme.{0}} (f : X ⟶ Y)
    (L : Y.Modules) (d : LineTrivialization Y.sheaf L) :
    LineTrivialization X.sheaf ((Scheme.Modules.pullback f).obj L) where
…
```
Mentions: OAI.ActualSheafTensor.LineTrivialization
def OAI.ActualSheafTensor.LineTrivialization.ofIso line 470
Source documentation
A module-sheaf isomorphism transports a line atlas.
```
def LineTrivialization.ofIso (d : LineTrivialization Y.sheaf L) (e : K ≅ L) :
    LineTrivialization Y.sheaf K where
…
```
Mentions: OAI.ActualSheafTensor.LineTrivialization
def OAI.ActualSheafTensor.LineTrivialization.restrict line 478
Source documentation
Restriction of a line bundle to any open subscheme.
```
def LineTrivialization.restrict (d : LineTrivialization Y.sheaf L) (U : Y.Opens) :
    LineTrivialization U.toScheme.sheaf ((restrictFunctor U.ι).obj L) :=
…
```
Mentions: OAI.ActualSheafTensor.LineTrivialization
def OAI.ActualCartier.restrictedLine line 489
Source documentation
The restricted ideal line atlas is induced by the kernel restriction isomorphism.
```
def restrictedLine : LineTrivialization U.toScheme.sheaf (idealSheaf (g ∣_ U)) :=
…
```
Mentions: OAI.ActualCartier.idealSheaf
lemma OAI.ActualOpenSupport.complement_restrict line 502
Source documentation
The geometric complement of the restricted closed immersion is precisely the inverse image of its original geometric complement.
```
lemma complement_restrict (U : Y.Opens) :
    complement (g ∣_ U) = U.ι ⁻¹ᵁ complement g := by
…
```
Mentions: OAI.ActualOpenSupport.complement

lemma OAI.SheafLocality.module_hom_ext_of_coversTop line 534

Source documentation

Equality of module-sheaf morphisms descends from any covering family.

lemma module_hom_ext_of_coversTop (hX : J.CoversTop X)
    {F G : SheafOfModules.{u} R} {f g : F ⟶ G}
    (h : ∀ i, (SheafOfModules.overFunctor R (X i)).map f =
      (SheafOfModules.overFunctor R (X i)).map g) : f = g := by
…

lemma OAI.SheafLocality.module_epi_of_coversTop line 544

Source documentation

Epimorphisms, as well as monomorphisms, descend from restriction.

lemma module_epi_of_coversTop (hX : J.CoversTop X)
    {F G : SheafOfModules.{u} R} (f : F ⟶ G)
    (h : ∀ i, Epi ((SheafOfModules.overFunctor R (X i)).map f)) : Epi f := by
…

lemma OAI.SheafLocality.module_isIso_of_coversTop line 557

Source documentation

The global isomorphism test on a covering family, for modules.

lemma module_isIso_of_coversTop [Balanced (SheafOfModules.{u} R)]
    (hX : J.CoversTop X) {F G : SheafOfModules.{u} R} (f : F ⟶ G)
    (h : ∀ i, IsIso ((SheafOfModules.overFunctor R (X i)).map f)) : IsIso f := by
…

lemma OAI.CoherentGlobal.isIso_of_restrict_cover line 568

Source documentation

Isomorphism of scheme-module morphisms is local on any open cover.

lemma isIso_of_restrict_cover {Y : Scheme.{0}} {ι : Type*} (U : ι → Y.Opens)
    (hU : (Opens.grothendieckTopology Y).CoversTop U)
    {M N : Y.Modules} (f : M ⟶ N)
    (h : ∀ i, IsIso ((restrictFunctor (U i).ι).map f)) : IsIso f := by
…

lemma OAI.SheafLocality.module_zero_of_openCover line 596
Source documentation
Restrictions along an open immersion cover are jointly faithful, including their non-definitional coefficient-ring changes.
```
lemma module_zero_of_openCover
    (h : (⨆ i, (f i).opensRange) = ⊤)
    {M N : Y.Modules} (a : M ⟶ N)
    (ha : ∀ i, (restrictFunctor (f i)).map a = 0) : a = 0 := by
…
```
abbrev OAI.ActualCartier.action line 634
Source documentation
The ideal resolution in the coherent category. A Cartier hypothesis here is only local triviality of the closed ideal.
```
abbrev action : coherentTensorLine (idealSheaf f) d ⟶ 𝟭 (Coh Y) :=
…
```
Mentions: OAI.ActualCartier.idealSheaf
lemma OAI.ActualCartier.kernel_app_essImage line 637
lemma OAI.ActualCartier.cokernel_app_essImage line 646
lemma OAI.ActualCartier.kernel_functor_essImage line 655
lemma OAI.ActualCartier.cokernel_functor_essImage line 661
def OAI.ActualCartier.firstTor line 668
Source documentation
First Cartier Tor, as a functor to coherent sheaves ON the divisor.
```
def firstTor : Coh Y ⥤ Coh X :=
…
```
def OAI.ActualCartier.restriction line 672
Source documentation
Ordinary Cartier restriction on coherent sheaves.
```
def restriction : Coh Y ⥤ Coh X :=
…
```
def OAI.ActualCartier.firstTorPushforwardIso line 676
def OAI.ActualCartier.restrictionPushforwardIso line 679
lemma OAI.CoherentK0.kernel_functor_additive line 694
Source documentation
Pointwise kernels of transformations of additive functors are additive.
```
lemma kernel_functor_additive (F G : C ⥤ D) [F.Additive] [G.Additive] (a : F ⟶ G) :
    (kernel a).Additive where
…
```

lemma OAI.CoherentK0.cokernel_functor_additive line 702

Source documentation

The corresponding cokernel statement.

lemma cokernel_functor_additive (F G : C ⥤ D) [F.Additive] [G.Additive] (a : F ⟶ G) :
    (cokernel a).Additive where
…

lemma OAI.CoherentK0.cartier_from_functor_kernels line 718

Source documentation

Once kernel and cokernel functors have been descended along a fully faithful exact inclusion, their universal properties imply Cartier additivity in the target's Grothendieck group.

lemma cartier_from_functor_kernels
    (J : D ⥤ C) [J.Full] [J.Faithful] [J.Additive]
    [PreservesFiniteLimits J] [PreservesFiniteColimits J]
    (T : C ⥤ C) [T.Additive]
    [PreservesFiniteLimits T] [PreservesFiniteColimits T]
    (a : T ⟶ 𝟭 C) (K Q : C ⥤ D)
    (eK : K ⋙ J ≅ kernel a) (eQ : Q ⋙ J ≅ cokernel a)
    {S : ShortComplex C} (hS : S.ShortExact) :
    cls (Q.obj S.X₂) - cls (K.obj S.X₂) =
      (cls (Q.obj S.X₁) - cls (K.obj S.X₁)) +
      (cls (Q.obj S.X₃) - cls (K.obj S.X₃)) := by
…

Mentions: OAI.CoherentK0.cls

lemma OAI.ActualCartier.derivedRestriction_additive line 768

Source documentation

Cartier restriction minus first Tor is additive on coherent sheaves, with values in the coherent Grothendieck group ON the divisor.

lemma derivedRestriction_additive {S : ShortComplex (Coh Y)} (hS : S.ShortExact) :
    cls ((restriction f d).obj S.X₂) - cls ((firstTor f d).obj S.X₂) =
      (cls ((restriction f d).obj S.X₁) - cls ((firstTor f d).obj S.X₁)) +
      (cls ((restriction f d).obj S.X₃) - cls ((firstTor f d).obj S.X₃)) := by
…

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

def OAI.ActualCartier.derivedRestriction line 780
Source documentation
The derived restriction homomorphism on the coherent Grothendieck group.
```
def derivedRestriction : CoherentK0.Group (Coh Y) →+ CoherentK0.Group (Coh X) :=
…
```
Mentions: OAI.CoherentK0.Group
lemma OAI.ActualCartier.derivedRestriction_cls line 787
lemma OAI.ActualCartier.derivedRestriction_filtered line 798
Source documentation
The finite coherent-filtration identity used for the nilpotent quotient in the Cartier restriction formula, before identifying the individual supported first-Tor terms with the conormal twist.
```
lemma derivedRestriction_filtered {M : Coh Y} {qs : List (Coh Y)}
    (h : FilteredBy M qs) :
    cls ((restriction f d).obj M) - cls ((firstTor f d).obj M) =
      (qs.map fun Q => cls ((restriction f d).obj Q) - cls ((firstTor f d).obj Q)).sum := by
…
```
Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.firstTor
lemma OAI.ActualSheafTensor.idealAction_zero_of_sections line 823
lemma OAI.ActualCartier.ideal_section_killed line 852
lemma OAI.ActualCartier.idealAction_pushforward_zero line 860
Source documentation
The closed ideal acts by zero on every sheaf pushed forward from that subscheme. This is a direct calculation with the scheme comorphism.
```
lemma idealAction_pushforward_zero (N : X.Modules) :
    (ActualSheafTensor.idealAction Y.sheaf (idealι f)).app
      ((Scheme.Modules.pushforward f).obj N) = 0 := by
…
```
Mentions: OAI.ActualSheafTensor.idealAction, OAI.ActualCartier.idealι
def OAI.CartierUniversal.pullbackIso line 885
Source documentation
The reflection unit identifies the descended cokernel with geometric pullback.
```
def pullbackIso : L.obj M ≅ Q := by
…
```