CartierSupport.lean`

49 declarations, 0 contain sorry, 0 declared as axioms

Cartier support and elementary transformations

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

theorem OAI.kernelMono line 20
Also declared: OAI/AlgebraicGeometry/SurfaceCones/CartierPullback.lean:10 (same declaration text).
lemma OAI.ActualCartier.exists_idealMultiple_isZero_of_complement line 50
Source documentation
A coherent sheaf supported on the Cartier divisor is killed by an ideal power. Its support is specified only by vanishing on the geometric complement of the closed immersion.
```
lemma exists_idealMultiple_isZero_of_complement (M : Coh Y)
    (hM : IsZero (M.obj.over (ActualOpenSupport.complement g))) :
    ∃ n : ℕ, IsZero (idealMultiple g d n M) := by
…
```
Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.idealMultiple

lemma OAI.ActualCartier.lattice_complement_identity line 60

Source documentation

Divisor support, a short exact sequence and the Cartier line give the divisor-side Grothendieck identity.

lemma lattice_complement_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 : IsZero (S.X₃.obj.over (ActualOpenSupport.complement 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.ActualOpenSupport.complement, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor

structure OAI.ActualSheafTensor.FiniteAffineLineCover line 79
Source documentation
Finite affine trivializations, with their ordinary ring schemes, covering maps and module-sheaf isomorphisms.
```
structure FiniteAffineLineCover {Y : Scheme.{0}} (L : Y.Modules) where
…
```
abbrev OAI.ActualSheafTensor.ChartIndex line 92
abbrev OAI.ActualSheafTensor.chartRing line 93
def OAI.ActualSheafTensor.chartMap line 95
instance OAI.ActualSheafTensor.(instance at line 97) line 97
def OAI.ActualSheafTensor.chartIso line 101
lemma OAI.ActualSheafTensor.chartCover line 109
def OAI.ActualSheafTensor.LineTrivialization.finiteAffineCover line 123
Source documentation
Quasi-compactness gives a finite affine refinement of a line-bundle trivializing cover.
```
def LineTrivialization.finiteAffineCover [CompactSpace Y] : FiniteAffineLineCover L := Classical.choice <| by
…
```
Mentions: OAI.ActualSheafTensor.FiniteAffineLineCover
structure OAI.CartierConnecting.Boundary line 150
Source documentation
Connecting morphism and exactness on the Cartier divisor.
```
structure Boundary (K Q : ShortComplex D) where
…
```

def OAI.CartierConnecting.boundary line 160

Source documentation

The snake connecting morphism descends through a fully faithful exact closed pushforward to the divisor category.

def boundary
    (J : D ⥤ C) [J.Full] [J.Faithful] [J.PreservesZeroMorphisms]
    [PreservesFiniteLimits J] [PreservesFiniteColimits J]
    (K Q : ShortComplex D) (S₁ S₂ : ShortComplex C)
    (i : K.map J ⟶ S₁) (m : S₁ ⟶ S₂) (p : S₂ ⟶ Q.map J)
    (wi : i ≫ m = 0) (wp : m ≫ p = 0)
    (hi : IsLimit (KernelFork.ofι i wi))
    (hp : IsColimit (CokernelCofork.ofπ p wp))
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) : Boundary K Q := by
…

Mentions: OAI.CartierConnecting.Boundary

lemma OAI.CartierConnecting.Boundary.mono_of_middle_isZero line 208
def OAI.CartierConnecting.Boundary.toQuotientKernel line 212
Source documentation
The right-hand morphism in the elementary modification sequence.
```
def toQuotientKernel (_b : Boundary K Q) : Q.X₁ ⟶ kernel Q.g := kernel.lift Q.g Q.f Q.zero
```
Mentions: OAI.CartierConnecting.Boundary
instance OAI.CartierConnecting.Boundary.epi_toQuotientKernel line 214
lemma OAI.CartierConnecting.Boundary.δ_toQuotientKernel line 217
def OAI.CartierConnecting.Boundary.modificationComplex line 223
Source documentation
The sequence firstTor(layer) → restriction(modification) → kernel(restriction(E) → layer), before suppressing the harmless zero terms.
```
def modificationComplex : ShortComplex D :=
…
```
lemma OAI.CartierConnecting.Boundary.modification_shortExact line 228
Source documentation
Once the middle lattice is Cartier-regular, this is a short exact elementary-modification sequence on the divisor.
```
lemma modification_shortExact (hz : IsZero K.X₂) :
    b.modificationComplex.ShortExact := by
…
```

def OAI.CartierConnecting.from_resolution line 261

Source documentation

The divisor-valued boundary obtained from an invertible-ideal resolution, retaining its morphisms and exactness rather than just Euler classes.

def from_resolution
    (J : D ⥤ C) [J.Full] [J.Faithful] [J.PreservesZeroMorphisms]
    [PreservesFiniteLimits J] [PreservesFiniteColimits J]
    (T : C ⥤ C) [T.PreservesZeroMorphisms]
    [PreservesFiniteLimits T] [PreservesFiniteColimits T]
    (K Q : C ⥤ D) [K.PreservesZeroMorphisms] [Q.PreservesZeroMorphisms]
    (κ : K ⋙ J ⟶ T) (ε : T ⟶ 𝟭 C) (π : 𝟭 C ⟶ Q ⋙ J)
    (zK : κ ≫ ε = 0) (zQ : ε ≫ π = 0)
    (hK : ∀ X, IsLimit (KernelFork.ofι (κ.app X) (NatTrans.congr_app zK X)))
    (hQ : ∀ X, IsColimit (CokernelCofork.ofπ (π.app X) (NatTrans.congr_app zQ X)))
    {S : ShortComplex C} (hS : S.ShortExact) : Boundary (S.map K) (S.map Q) := by
…

Mentions: OAI.CartierConnecting.Boundary

def OAI.CartierConnecting.from_kernels line 300

Source documentation

The kernel and cokernel functors supply the universal properties used in from_resolution.

def from_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) [K.Additive] [Q.Additive]
    (eK : K ⋙ J ≅ kernel a) (eQ : Q ⋙ J ≅ cokernel a)
    {S : ShortComplex C} (hS : S.ShortExact) : Boundary (S.map K) (S.map Q) := by
…

Mentions: OAI.CartierConnecting.Boundary

def OAI.ActualCartier.connecting line 340
Source documentation
The ideal action constructs the connecting morphism and exact sequences of coherent sheaves on the Cartier divisor.
```
def connecting {S : ShortComplex (Coh Y)} (hS : S.ShortExact) :
    CartierConnecting.Boundary (S.map (firstTor f d)) (S.map (restriction f d)) := by
…
```
Mentions: OAI.CartierConnecting.Boundary, OAI.ActualCartier.firstTor, OAI.ActualCartier.restriction
lemma OAI.ActualCartier.modification_shortExact line 351
Source documentation
The elementary modification sequence underlying the elementary transformation formula, with first Tor retained as the divisor sheaf.
```
lemma modification_shortExact {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (S.X₂.obj.val.obj U)) :
    (connecting f d hS).modificationComplex.ShortExact :=
…
```
Mentions: OAI.ActualCartier.connecting
instance OAI.ActualCartier.restrictionUnit_supported_isIso line 367
def OAI.ActualCartier.supportedCounitIso line 378
Source documentation
The canonical coherent counit, inverse to ordinary restriction's unit on a supported sheaf.
```
def supportedCounitIso (N : Coh X) : (restriction f d).obj ((cohPushforward f).obj N) ≅ N :=
…
```
Mentions: OAI.ActualCartier.restriction
lemma OAI.ActualCartier.unit_supported_counit line 382
def OAI.ActualCartier.modificationMap line 388
Source documentation
The ambient quotient map for an elementary transform.
```
def modificationMap {E : Coh Y} {G : Coh X} (q : (restriction f d).obj E ⟶ G) :
    E ⟶ (cohPushforward f).obj G :=
…
```
Mentions: OAI.ActualCartier.restriction
instance OAI.ActualCartier.modificationMap_epi line 392
def OAI.ActualCartier.modificationSequence line 398
Source documentation
A coherent elementary modification is the kernel along the divisor.
```
def modificationSequence {E : Coh Y} {G : Coh X} (q : (restriction f d).obj E ⟶ G) :
    ShortComplex (Coh Y) :=
…
```
Mentions: OAI.ActualCartier.restriction
lemma OAI.ActualCartier.modificationSequence_shortExact line 403
lemma OAI.ActualCartier.modificationMap_restrict line 410
def OAI.ActualCartier.modificationKernelIso line 424
Source documentation
The right-hand kernel after restriction is the kernel of the last-factor quotient.
```
def modificationKernelIso {E : Coh Y} {G : Coh X}
    (q : (restriction f d).obj E ⟶ G) :
    kernel ((restriction f d).map (modificationMap f d q)) ≅ kernel q :=
…
```
Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.modificationMap
def OAI.ActualCartier.transformSequence line 431
Source documentation
Sequence G⊗J|X → E'|X → ker(P→G) of the elementary transformation formula.
```
def transformSequence {E : Coh Y} {G : Coh X}
    (q : (restriction f d).obj E ⟶ G) [Epi q] : ShortComplex (Coh X) := by
…
```
Mentions: OAI.ActualCartier.restriction
lemma OAI.ActualCartier.transformSequence_shortExact line 441
Source documentation
The elementary transform has the exact divisor restriction claimed by the manuscript, with the conormal tensor.
```
lemma transformSequence_shortExact {E : Coh Y} {G : Coh X}
    (q : (restriction f d).obj E ⟶ G) [Epi q]
    (hE : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (E.obj.val.obj U)) :
    (transformSequence f d q).ShortExact := by
…
```
Mentions: OAI.ActualCartier.restriction, OAI.ActualCartier.transformSequence

lemma OAI.ActualCartier.pushforward_restrict_isZero line 467

Source documentation

A sheaf supported on the closed divisor vanishes on every open whose inverse image is empty. This uses its section modules.

lemma pushforward_restrict_isZero {X Y : Scheme.{0}} (f : X ⟶ Y)
    (G : X.Modules) (U : Y.Opens) (hU : f ⁻¹ᵁ U = ⊥) :
    IsZero ((restrictFunctor U.ι).obj ((pushforward f).obj G)) := by
…

lemma OAI.ActualCartier.modification_puncture_isIso line 489

Source documentation

An elementary modification is canonically unchanged off the divisor.

lemma modification_puncture_isIso {X Y : Scheme.{0}}
    [IsLocallyNoetherian X] [IsLocallyNoetherian Y]
    (f : X ⟶ Y) [IsClosedImmersion f]
    (d : ActualSheafTensor.LineTrivialization Y.sheaf (idealSheaf f))
    {E : Coh Y} {G : Coh X} (q : (restriction f d).obj E ⟶ G) [Epi q]
    (U : Y.Opens) (hU : f ⁻¹ᵁ U = ⊥) :
    IsIso ((restrictFunctor U.ι).map
      ((cohInclusion Y).map (kernel.ι (modificationMap f d q)))) := by
…

Mentions: OAI.ActualSheafTensor.LineTrivialization, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.restriction, OAI.ActualCartier.modificationMap

lemma OAI.ActualCartier.exists_idealMultiple_isZero line 517
Source documentation
Quasi-compact coherent support on the Cartier divisor implies a vanishing ideal multiple. The affine cover and exponent are constructed.
```
lemma exists_idealMultiple_isZero (M : Coh Y)
    (hM : IsZero (M.obj.over (ActualOpenSupport.complement g))) :
    ∃ n : ℕ, IsZero (idealMultiple g d n M) := by
…
```
Mentions: OAI.ActualOpenSupport.complement, OAI.ActualCartier.idealMultiple

lemma OAI.ActualCartier.quotient_supported_of_puncture_iso line 526

Source documentation

Cokernels of a lattice embedding are supported on the divisor when that embedding is an isomorphism on its open complement.

lemma quotient_supported_of_puncture_iso {S : ShortComplex (Coh Y)} (hS : S.ShortExact)
    [IsIso ((restrictFunctor (ActualOpenSupport.complement g).ι).map
      ((cohInclusion Y).map S.f))] :
    IsZero (S.X₃.obj.over (ActualOpenSupport.complement g)) := by
…

Mentions: OAI.ActualOpenSupport.complement

lemma OAI.ActualCartier.lattice_puncture_identity line 540

Source documentation

The Cartier restriction identity follows from Cartier data and a puncture isomorphism.

lemma lattice_puncture_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))
    [IsIso ((restrictFunctor (ActualOpenSupport.complement g).ι).map
      ((cohInclusion Y).map S.f))] :
    ∃ 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.ActualOpenSupport.complement, OAI.ActualCartier.restriction, OAI.ActualCartier.idealLayers, OAI.ActualCartier.conormalTensor

lemma OAI.ActualSheafTensor.isZero_of_tensor_line line 564
Source documentation
Tensor by a line bundle reflects the zero object by its local unit trivializations.
```
lemma isZero_of_tensor_line (L M : SheafOfModules.{u} (ringSheaf R))
    (d : LineTrivialization R L) (h : IsZero ((tensorLeft R L).obj M)) : IsZero M := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.tensorLeft
lemma OAI.ActualSheafTensor.coherent_isZero_of_tensor_line line 580

lemma OAI.ActualCartier.isZero_of_idealMultiple_isZero line 604

Source documentation

A torsion-free coherent sheaf annihilated by a Cartier ideal power is zero.

lemma isZero_of_idealMultiple_isZero (n : ℕ) (M : Coh Y)
    (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.obj.val.obj U))
    (hn : IsZero (idealMultiple g d n M)) : IsZero M := by
…

Mentions: OAI.ActualCartier.idealMultiple

lemma OAI.ActualCartier.isZero_of_supported_torsionFree line 633
Source documentation
A coherent torsion-free sheaf supported on an effective Cartier divisor vanishes. Support here means restriction to its geometric complement.
```
lemma isZero_of_supported_torsionFree [CompactSpace Y] (M : Coh Y)
    (hM : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (M.obj.val.obj U))
    (hs : IsZero (M.obj.over (ActualOpenSupport.complement g))) : IsZero M := by
…
```
Mentions: OAI.ActualOpenSupport.complement

lemma OAI.ActualCartier.hom_zero_of_puncture line 653

Source documentation

Restriction off an effective Cartier divisor is faithful on morphisms into coherent torsion-free sheaves.

lemma hom_zero_of_puncture {M N : Coh Y} (a : M ⟶ N)
    (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.obj.val.obj U))
    (ha : (restrictFunctor (ActualOpenSupport.complement g).ι).map
      ((cohInclusion Y).map a) = 0) : a = 0 := by
…

Mentions: OAI.ActualOpenSupport.complement

lemma OAI.ActualCartier.hom_ext_of_puncture line 678

Source documentation

The uniqueness assertion needed for gluing cleared lattice denominators.

lemma hom_ext_of_puncture {M N : Coh Y} (a b : M ⟶ N)
    (hN : ∀ U, Module.IsTorsionFree (Y.sheaf.obj.obj U) (N.obj.val.obj U))
    (hab : (restrictFunctor (ActualOpenSupport.complement g).ι).map
      ((cohInclusion Y).map a) =
      (restrictFunctor (ActualOpenSupport.complement g).ι).map ((cohInclusion Y).map b)) :
    a = b := by
…

Mentions: OAI.ActualOpenSupport.complement

lemma OAI.ActualCartier.over_hom_ext_of_puncture line 702

Source documentation

Faithfulness on a local chart, stated on the slice site's section maps. It is the uniqueness needed when denominator-cleared maps from distinct charts are glued; agreement is required only off the divisor.

lemma over_hom_ext_of_puncture (U : Y.Opens) [CompactSpace U.toScheme]
    (M N : Y.Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hN : ∀ V, Module.IsTorsionFree (Y.sheaf.obj.obj V) (N.val.obj V))
    (a b : M.over U ⟶ N.over U)
    (hab : ∀ (V : Y.Opens) (hV : V ≤ U) (_hW : V ≤ ActualOpenSupport.complement g)
      (x : M.val.obj (op V)),
      a.val.app (op (Over.mk (homOfLE hV))) x =
        b.val.app (op (Over.mk (homOfLE hV))) x) : a = b := by
…

Mentions: OAI.ActualOpenSupport.complement

lemma OAI.SheafHomGluing.exists_gluing line 755

Source documentation

Compatible restricted module morphisms glue by the sheaf of linear Hom.

lemma exists_gluing {ι : Type*} (U : ι → X.Opens) (hU : (⨆ i, U i) = ⊤)
    (a : ∀ i, M.over (U i) ⟶ N.over (U i))
    (ha : ∀ i j (V : X.Opens) (hi : V ≤ U i) (hj : V ≤ U j)
      (x : M.val.obj (op V)),
      (a i).val.app (op (Over.mk (homOfLE hi))) x =
        (a j).val.app (op (Over.mk (homOfLE hj))) x) :
    ∃ f : M ⟶ N, ∀ i (V : X.Opens) (hi : V ≤ U i) (x : M.val.obj (op V)),
      f.val.app (op V) x = (a i).val.app (op (Over.mk (homOfLE hi))) x := by
…

lemma OAI.SheafHomGluing.exists_gluing_hom line 782

Source documentation

In categorical form, the glued morphism restricts to every given local morphism. All compatibility is tested on the section maps.

lemma exists_gluing_hom {ι : Type*} (U : ι → X.Opens) (hU : (⨆ i, U i) = ⊤)
    (a : ∀ i, M.over (U i) ⟶ N.over (U i))
    (ha : ∀ i j (V : X.Opens) (hi : V ≤ U i) (hj : V ≤ U j)
      (x : M.val.obj (op V)),
      (a i).val.app (op (Over.mk (homOfLE hi))) x =
        (a j).val.app (op (Over.mk (homOfLE hj))) x) :
    ∃ f : M ⟶ N, ∀ i, f.over (U i) = a i := by
…

lemma OAI.SheafHomGluing.over_eq_of_local_values line 806

Source documentation

The glued global morphism retains the prescribed morphism on the open where its local extensions were constructed, by sheaf separatedness.

lemma over_eq_of_local_values {ι : Type*} (U : ι → Y.Opens)
    (hU : (⨆ i, U i) = ⊤) (M N : Y.Modules) (W : Y.Opens)
    (e : M.over W ⟶ N.over W) (f : M ⟶ N)
    (hf : ∀ i (V : Y.Opens) (_hi : V ≤ U i) (hV : V ≤ W)
      (x : M.val.obj (op V)),
      f.val.app (op V) x = e.val.app (op (Over.mk (homOfLE hV))) x) :
    f.over W = e := by
…