AffineNaturalPower.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Principal equations and restriction of tensor powers

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

lemma OAI.AffineNaturalScalar.power_eq line 18

Source documentation

The scalar formula for powers of a natural action on an associated sheaf.

lemma power_eq (M : ModuleCat R) (n : ℕ) :
    (End.of (b.app (tilde M)) ^ n).asHom = (tilde.functor R).map
      (ModuleCat.ofHom (scalar R b ^ n • (LinearMap.id : M →ₗ[R] M))) := by
…

Mentions: OAI.AffineNaturalScalar.scalar

def OAI.CartierImageFiltration.trivialPowerIso line 62
Source documentation
The iterated tensor power trivialization, derived from the given line trivialization, retaining its compatibility with the ideal action.
```
def trivialPowerIso (n : ℕ) (M : C) : (power T n).obj M ≅ M :=
…
```
Mentions: OAI.CartierImageFiltration.power
lemma OAI.CartierImageFiltration.trivialPowerIso_action line 67
lemma OAI.CartierAffineLattice.natural_power_intertwine line 87
lemma OAI.CartierAffineLattice.natural_coherent_power line 99
Source documentation
The natural scalar power on every quasi-coherent affine sheaf, transported via its canonical affine presentation.
```
lemma natural_coherent_power (b : 𝟭 (Spec R).Modules ⟶ 𝟭 (Spec R).Modules)
    (M : (Spec R).Modules) [M.IsQuasicoherent] (n : ℕ) :
    (End.of (b.app M) ^ n).asHom = affineScalar (AffineNaturalScalar.scalar R b ^ n) M := by
…
```
Mentions: OAI.CartierAffineLattice.affineScalar, OAI.AffineNaturalScalar.scalar

lemma OAI.CartierAffineLattice.trivial_power_scalar line 112

Source documentation

Exact comparison between the ideal tensor power and its principal equation on a trivializing affine Cartier chart.

lemma trivial_power_scalar (L : (Spec R).Modules)
    (eL : L ≅ SheafOfModules.unit (Spec R).ringCatSheaf)
    (i : L ⟶ SheafOfModules.unit (Spec R).ringCatSheaf)
    (M : (Spec R).Modules) [M.IsQuasicoherent] (n : ℕ) :
    (trivialPowerIso (tensorLeft (Spec R).sheaf L)
      (trivialTensorIso (Spec R).sheaf eL) n M).hom ≫
      affineScalar (AffineCartierNilpotence.equation L eL i ^ n) M =
      (powerAction (tensorLeft (Spec R).sheaf L) (idealAction (Spec R).sheaf i) n).app M := by
…

Mentions: OAI.CartierAffineLattice.affineScalar, OAI.AffineCartierNilpotence.equation

lemma OAI.CartierAffineLattice.exists_twisted_coherent_sandwich line 144

Source documentation

The affine Cartier lattice extension uses iterated tensor powers of the ideal. Its two injections restrict to the prescribed identification times the Cartier action.

lemma exists_twisted_coherent_sandwich [IsNoetherianRing R]
    (L : (Spec R).Modules) (eL : L ≅ SheafOfModules.unit (Spec R).ringCatSheaf)
    (i : L ⟶ SheafOfModules.unit (Spec R).ringCatSheaf) [Mono i]
    (M N : (Spec R).Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ U, Module.IsTorsionFree ((Spec R).sheaf.obj.obj U) (M.val.obj U))
    (hN : ∀ U, Module.IsTorsionFree ((Spec R).sheaf.obj.obj U) (N.val.obj U))
    (e : M.over (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i)) ≅
      N.over (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i))) :
    let U := PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i)
…

Mentions: OAI.AffineCartierNilpotence.equation

instance OAI.CartierImageFiltration.power_preservesMonos line 197

lemma OAI.CartierImageFiltration.exists_extension_of_le line 206

Source documentation

Once a pole is cleared, every larger ideal twist is cleared. The extending maps remain monomorphisms and retain their prescribed restriction; this is the uniform-exponent step in finite-cover gluing.

lemma exists_extension_of_le [T.PreservesMonomorphisms]
    (F : C ⥤ D) (M N : C) [Mono (a.app M)]
    (e : F.obj M ⟶ F.obj N) {n m : ℕ} (hnm : n ≤ m)
    (z : (power T n).obj M ⟶ N) [Mono z]
    (hz : F.map z = F.map ((powerAction T a n).app M) ≫ e) :
    ∃ w : (power T m).obj M ⟶ N, Mono w ∧
      F.map w = F.map ((powerAction T a m).app M) ≫ e := by
…

Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.powerAction

lemma OAI.CartierAffineLattice.exists_uniform_twisted_sandwich line 242

Source documentation

A coherent lattice identification on an affine Cartier puncture extends injectively after every sufficiently large ideal twist, in both directions with one common lower bound. This is exactly the uniform local extension needed to choose one exponent on a finite trivializing cover.

lemma exists_uniform_twisted_sandwich [IsNoetherianRing R]
    (L : (Spec R).Modules) (eL : L ≅ SheafOfModules.unit (Spec R).ringCatSheaf)
    (i : L ⟶ SheafOfModules.unit (Spec R).ringCatSheaf) [Mono i]
    (M N : (Spec R).Modules) [M.IsFinitePresentation] [N.IsFinitePresentation]
    (hM : ∀ U, Module.IsTorsionFree ((Spec R).sheaf.obj.obj U) (M.val.obj U))
    (hN : ∀ U, Module.IsTorsionFree ((Spec R).sheaf.obj.obj U) (N.val.obj U))
    (e : M.over (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i)) ≅
      N.over (PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i))) :
    let U := PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation L eL i)
…

Mentions: OAI.AffineCartierNilpotence.equation

lemma OAI.ActualCartier.equation_basicOpen_disjoint line 283
Source documentation
The nonvanishing locus of the equation of a Cartier ideal avoids the closed divisor.
```
lemma equation_basicOpen_disjoint :
    f ⁻¹ᵁ Y.basicOpen (equation f U e) = ⊥ := by
…
```
Mentions: OAI.ActualCartier.equation
lemma OAI.ActualCartier.equation_affineChart_disjoint line 291
Source documentation
The same statement on the canonical affine chart, with precisely the ordinary principal open used by associated-module localization.
```
lemma equation_affineChart_disjoint (hU : IsAffineOpen U) :
    f ⁻¹ᵁ (hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen (equation f U e)) = ⊥ := by
…
```
Mentions: OAI.ActualCartier.equation
lemma OAI.AffineCartierNilpotence.equation_section line 308
Source documentation
The equation from the fully faithful affine functor is the trivialized ideal section under the structure-section isomorphism.
```
lemma equation_section :
    (Scheme.ΓSpecIso R).inv (equation L e i) =
      i.val.app (op ⊤) (e.inv.val.app (op ⊤) (1 : Γ(Spec R, ⊤))) := by
…
```
Mentions: OAI.AffineCartierNilpotence.equation

def OAI.ActualSheafTensor.openRingRestrictHom line 336

Source documentation

The coefficient-ring map for open-scheme restriction.

def openRingRestrictHom : X.ringCatSheaf ⟶
    (f.opensFunctor.sheafPushforwardContinuous RingCat
      (Opens.grothendieckTopology X) (Opens.grothendieckTopology Y)).obj
      Y.ringCatSheaf :=
…

def OAI.ActualSheafTensor.openPresheafRestrict line 346
Source documentation
The concrete presheaf restriction underlying open-scheme restriction.
```
def openPresheafRestrict : PresheafOfModules.{0} Y.ringCatSheaf.obj ⥤
    PresheafOfModules.{0} X.ringCatSheaf.obj :=
…
```

def OAI.ActualSheafTensor.openSheafifyRestrictMap line 351

Source documentation

Canonical open restriction comparison for module sheafification.

def openSheafifyRestrictMap (P : PresheafOfModules.{0} Y.ringCatSheaf.obj) :
    (PresheafOfModules.sheafification (𝟙 X.ringCatSheaf.obj)).obj
        ((openPresheafRestrict f).obj P) ⟶
      (restrictFunctor f).obj
        ((PresheafOfModules.sheafification (𝟙 Y.ringCatSheaf.obj)).obj P) :=
…

Mentions: OAI.ActualSheafTensor.openPresheafRestrict

instance OAI.ActualSheafTensor.openSheafifyRestrictMap_isIso line 358

def OAI.ActualSheafTensor.openPresheafTensorRestrictIso line 363

Source documentation

Tensor presheaves commute with restriction to an open subscheme.

def openPresheafTensorRestrictIso (M N : PresheafOfModules.{0} Y.ringCatSheaf.obj) :
    (openPresheafRestrict f).obj
      (PresheafOfModulesOfCommRing.Monoidal.tensorObj (R := Y.sheaf.obj) M N) ≅
…

Mentions: OAI.ActualSheafTensor.openPresheafRestrict

def OAI.ActualSheafTensor.tensorOpenRestrictIso line 398

Source documentation

The tensor sheaf commutes with open-scheme restriction.

def tensorOpenRestrictIso (M N : Y.Modules) :
    (restrictFunctor f).obj (tensor Y.sheaf M N) ≅
      tensor X.sheaf ((restrictFunctor f).obj M) ((restrictFunctor f).obj N) :=
…

Mentions: OAI.ActualSheafTensor.tensor

lemma OAI.ActualSheafTensor.tensorOpenRestrictIso_inv_pure line 408

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 tensorOpenRestrictIso_inv_pure (M N : Y.Modules) (V : X.Opens)
    (x : ((restrictFunctor f).obj M).val.obj (op V))
    (y : ((restrictFunctor f).obj N).val.obj (op V)) :
    (tensorOpenRestrictIso f M N).inv.val.app (op V)
      (pure X.sheaf ((restrictFunctor f).obj M)
        ((restrictFunctor f).obj N) (op V) x y) =
    pure Y.sheaf M N (op (f ''ᵁ V)) x y := by
…

Mentions: OAI.ActualSheafTensor.tensorOpenRestrictIso, OAI.ActualSheafTensor.pure

lemma OAI.ActualSheafTensor.tensorLeft_pure line 451
lemma OAI.ActualSheafTensor.tensorOpenRestrict_naturality line 469
def OAI.ActualSheafTensor.tensorOpenRestrictNatIso line 509
Source documentation
Restriction of tensoring is natural, with the coefficient changes.
```
def tensorOpenRestrictNatIso (L : Y.Modules) :
    tensorLeft Y.sheaf L ⋙ restrictFunctor f ≅
      restrictFunctor f ⋙ tensorLeft X.sheaf ((restrictFunctor f).obj L) :=
…
```
Mentions: OAI.ActualSheafTensor.tensorLeft

def OAI.ActualSheafTensor.restrictedIdeal line 516

Source documentation

Restriction of the ideal inclusion.

def restrictedIdeal {L : Y.Modules} (i : L ⟶ SheafOfModules.unit Y.ringCatSheaf) :
    (restrictFunctor f).obj L ⟶ SheafOfModules.unit X.ringCatSheaf :=
…

lemma OAI.ActualSheafTensor.tensorOpenRestrict_action line 520
lemma OAI.ActualCartier.chart_equation_disjoint line 569
Source documentation
On an affine trivializing chart, the principal equation extracted by full faithfulness has nonvanishing open disjoint from the divisor.
```
lemma chart_equation_disjoint :
    g ⁻¹ᵁ (f ''ᵁ PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
      ((restrictFunctor f).obj (idealSheaf g)) e (restrictedIdeal f (idealι g)))) = ⊥ := by
…
```
Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι
lemma OAI.ActualOpenSupport.isZero_over_of_le line 602
Source documentation
Vanishing of a sheaf on an open persists on every smaller open.
```
lemma isZero_over_of_le (M : Y.Modules) {U V : Y.Opens} (hUV : U ≤ V)
    (hM : IsZero (M.over V)) : IsZero (M.over U) := by
…
```

lemma OAI.ActualOpenSupport.isZero_restrict_over_of_image line 619

Source documentation

Restriction along an open immersion preserves vanishing on the image open.

lemma isZero_restrict_over_of_image (f : X ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules) (V : X.Opens) (hM : IsZero (M.over (f ''ᵁ V))) :
    IsZero (((restrictFunctor f).obj M).over V) := by
…

lemma OAI.ActualOpenSupport.isZero_over_of_restrict line 641
Source documentation
Vanishing on the open subscheme is equivalent to vanishing on the slice site; this direction is needed for an exact quotient's support.
```
lemma isZero_over_of_restrict (M : Y.Modules) (U : Y.Opens)
    (hM : IsZero ((restrictFunctor U.ι).obj M)) : IsZero (M.over U) := by
…
```
def OAI.ActualOpenSupport.complement line 649
Source documentation
The open complement of a closed immersion.
```
def complement (g : X ⟶ Y) [IsClosedImmersion g] : Y.Opens :=
…
```
lemma OAI.ActualOpenSupport.le_complement line 652

lemma OAI.ActualOpenSupport.isZero_restrict_of_disjoint line 663

Source documentation

Geometric support on the divisor implies vanishing on every restricted open whose image is disjoint from it.

lemma isZero_restrict_of_disjoint (g : X ⟶ Y) [IsClosedImmersion g]
    {Z : Scheme.{0}} (f : Z ⟶ Y) [IsOpenImmersion f]
    (M : Y.Modules) (hM : IsZero (M.over (complement g)))
    (V : Z.Opens) (hV : g ⁻¹ᵁ (f ''ᵁ V) = ⊥) :
    IsZero (((restrictFunctor f).obj M).over V) :=
…

Mentions: OAI.ActualOpenSupport.complement

def OAI.ActualCartier.chartPunctureIso line 686
Source documentation
The geometric puncture lies above the affine Cartier nonvanishing open, so its fixed isomorphism restricts to the affine principal puncture.
```
def chartPunctureIso (M N : Y.Modules)
    (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_uniform_sandwich line 701

Source documentation

Each affine trivializing chart admits a uniform bound in both directions for ideal-twisted embeddings of torsion-free lattices identified off the divisor.

lemma exists_chart_uniform_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 L := (restrictFunctor f).obj (idealSheaf g)
…

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

lemma OAI.ActualCartier.equation_basicOpen_eq_puncture line 747
Source documentation
The Cartier principal open equals the geometric puncture of the affine chart.
```
lemma equation_basicOpen_eq_puncture :
    Y.basicOpen (equation f U e) = U ⊓ ActualOpenSupport.complement f := by
…
```
Mentions: OAI.ActualCartier.equation, OAI.ActualOpenSupport.complement
def OAI.ActualCartier.chartSectionTrivialization line 785
Source documentation
An affine-scheme line trivialization gives the section trivialization on its image open, accounting for the coefficient-ring iso.
```
def chartSectionTrivialization : SectionTrivialization g (f ''ᵁ (⊤ : (Spec R).Opens)) where
…
```
Mentions: OAI.ActualCartier.SectionTrivialization
lemma OAI.ActualCartier.chart_equation_section line 814
Source documentation
The abstract affine equation used for denominator clearing is the actual-ideal generator under the scheme's section-ring iso.
```
lemma chart_equation_section :
    (f.appIso ⊤).inv ((Scheme.ΓSpecIso R).inv
      (AffineCartierNilpotence.equation ((restrictFunctor f).obj (idealSheaf g))
        e (restrictedIdeal f (idealι g)))) =
      equation g (f ''ᵁ (⊤ : (Spec R).Opens)) (chartSectionTrivialization g f e) := by
…
```
Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualCartier.equation, OAI.ActualCartier.chartSectionTrivialization
lemma OAI.ActualCartier.chart_equation_image_eq_puncture line 827
Source documentation
Exact agreement of the affine principal open and the geometric Cartier puncture, including its image in the ambient scheme.
```
lemma chart_equation_image_eq_puncture [IsClosedImmersion g] :
    f ''ᵁ PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
      ((restrictFunctor f).obj (idealSheaf g)) e (restrictedIdeal f (idealι g))) =
        f.opensRange ⊓ ActualOpenSupport.complement g := by
…
```
Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualOpenSupport.complement
lemma OAI.ActualCartier.chart_equation_puncture_eq_preimage line 838
Source documentation
The local principal puncture on the chart is precisely the inverse image of the open complement of the closed divisor.
```
lemma chart_equation_puncture_eq_preimage [IsClosedImmersion g] :
    PrimeSpectrum.basicOpen (AffineCartierNilpotence.equation
      ((restrictFunctor f).obj (idealSheaf g)) e (restrictedIdeal f (idealι g))) =
        f ⁻¹ᵁ ActualOpenSupport.complement g := by
…
```
Mentions: OAI.AffineCartierNilpotence.equation, OAI.ActualCartier.idealSheaf, OAI.ActualCartier.idealι, OAI.ActualOpenSupport.complement