CartierImageFiltration.lean`

50 declarations, 0 contain sorry, 0 declared as axioms

Powers and image filtrations of Cartier ideal actions

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

def OAI.CartierImageFiltration.multiple line 21
Source documentation
The ideal multiple, defined as the image of the ideal action.
```
def multiple (M : C) : C := Abelian.image (a.app M)
```

def OAI.CartierImageFiltration.iterated line 24

Source documentation

Repeated images of the ideal action.

def iterated : ℕ → C → C
  | 0, M => M
  | n + 1, M => iterated n (multiple T a M)

/-- Canonical image/cokernel sequence of the ideal action. -/

Mentions: OAI.CartierImageFiltration.multiple

def OAI.CartierImageFiltration.layerSequence line 29
Source documentation
Canonical image/cokernel sequence of the ideal action.
```
def layerSequence (M : C) : ShortComplex C :=
…
```
lemma OAI.CartierImageFiltration.layerSequence_shortExact line 33
def OAI.CartierImageFiltration.supportedSequence line 40
Source documentation
The same sequence, identified with its supported quotient.
```
def supportedSequence (M : C) : ShortComplex C :=
…
```
lemma OAI.CartierImageFiltration.supportedSequence_shortExact line 44
def OAI.CartierImageFiltration.layers line 53
Source documentation
Successive quotients selected by images of the ideal action.
```
def layers : ℕ → C → List D
  | 0, _ => []
  | n + 1, M => Q M :: layers n (multiple T a M)

include e in
/-- A nilpotent iterated image gives a finite filtration by supported layers. -/
```
Mentions: OAI.CartierImageFiltration.multiple, OAI.CartierImageFiltration.iterated
lemma OAI.CartierImageFiltration.filteredBy_iterated_zero line 59
Source documentation
A nilpotent iterated image gives a finite filtration by supported layers.
```
lemma filteredBy_iterated_zero (n : ℕ) (M : C) (h : IsZero (iterated T a n M)) :
    CoherentK0.FilteredBy M ((layers T a Q n M).map J.obj) := by
…
```
Mentions: OAI.CartierImageFiltration.iterated, OAI.CoherentK0.FilteredBy, OAI.CartierImageFiltration.layers
def OAI.CartierImageFiltration.power line 78
Source documentation
Iterated tensor functors.
```
def power : ℕ → C ⥤ C
  | 0 => 𝟭 C
  | n + 1 => T ⋙ power n
```
instance OAI.CartierImageFiltration.power_preservesEpis line 82

def OAI.CartierImageFiltration.powerAction line 89

Source documentation

The n-fold ideal action, as a natural transformation.

def powerAction : (n : ℕ) → power T n ⟶ 𝟭 C
  | 0 => 𝟙 _
  | n + 1 => Functor.whiskerLeft T (powerAction n) ≫ a

/-- The canonical inclusion of the iterated ideal image in the original object. -/

Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.iterated

def OAI.CartierImageFiltration.iteratedInclusion line 94

Source documentation

The canonical inclusion of the iterated ideal image in the original object.

def iteratedInclusion : (n : ℕ) → (M : C) → iterated T a n M ⟶ M
  | 0, M => 𝟙 M
  | n + 1, M => iteratedInclusion n (multiple T a M) ≫ Abelian.image.ι (a.app M)

/-- Powers surject onto the corresponding iterated image. -/

Mentions: OAI.CartierImageFiltration.iterated, OAI.CartierImageFiltration.multiple

def OAI.CartierImageFiltration.powerToImage line 99
Source documentation
Powers surject onto the corresponding iterated image.
```
def powerToImage : (n : ℕ) → (M : C) → (power T n).obj M ⟶ iterated T a n M
  | 0, M => 𝟙 M
  | n + 1, M => (power T n).map (Abelian.factorThruImage (a.app M)) ≫
      powerToImage n (multiple T a M)
```
Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.iterated, OAI.CartierImageFiltration.multiple
instance OAI.CartierImageFiltration.powerToImage_epi line 104
instance OAI.CartierImageFiltration.iteratedInclusion_mono line 114
lemma OAI.CartierImageFiltration.powerToImage_fac line 123
lemma OAI.CartierImageFiltration.iterated_isZero_of_powerAction_zero line 157
Source documentation
Vanishing of the n-fold ideal action forces the iterated image to vanish.
```
lemma iterated_isZero_of_powerAction_zero [T.PreservesEpimorphisms]
    (n : ℕ) (M : C) (h : (powerAction T a n).app M = 0) :
    IsZero (iterated T a n M) := by
…
```
Mentions: OAI.CartierImageFiltration.powerAction, OAI.CartierImageFiltration.iterated
lemma OAI.CartierImageFiltration.powerAction_quotient_zero line 167
Source documentation
If an ideal power on L factors through a subobject, its quotient is annihilated by that power. This is the categorical lattice sandwich.
```
lemma powerAction_quotient_zero [T.PreservesEpimorphisms]
    {S : ShortComplex C} (hS : S.ShortExact) (n : ℕ)
    (b : (power T n).obj S.X₂ ⟶ S.X₁)
    (hb : b ≫ S.f = (powerAction T a n).app S.X₂) :
    (powerAction T a n).app S.X₃ = 0 := by
…
```
Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.powerAction

def OAI.CartierImageFiltration.powerComparison line 188

Source documentation

Iterated tensor actions commute with restriction through the restriction comparison.

def powerComparison : (n : ℕ) → (M : C) →
    F.obj ((power T n).obj M) ≅ (power S n).obj (F.obj M)
  | 0, _ => Iso.refl _
  | n + 1, M => powerComparison n (T.obj M) ≪≫ (power S n).mapIso (e.app M)

variable (a : T ⟶ 𝟭 C) (b : S ⟶ 𝟭 D)
    (he : ∀ M, (e.app M).hom ≫ b.app (F.obj M) = F.map (a.app M))

include he

/-- The same restriction comparison intertwines every Cartier
power. This lifts the local principal-equation calculation to the iterated tensor functor used in the coherent filtration. -/

Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.iterated

lemma OAI.CartierImageFiltration.powerComparison_action line 200
Source documentation
The same restriction comparison intertwines every Cartier power. This lifts the local principal-equation calculation to the iterated tensor functor used in the coherent filtration.
```
lemma powerComparison_action (n : ℕ) (M : C) :
    (powerComparison T S F e n M).hom ≫ (powerAction S b n).app (F.obj M) =
      F.map ((powerAction T a n).app M) := by
…
```
Mentions: OAI.CartierImageFiltration.powerComparison, OAI.CartierImageFiltration.powerAction
lemma OAI.CartierImageFiltration.map_powerAction_zero_of_comparison line 217
Source documentation
Vanishing of a local power implies vanishing of the restricted global action.
```
lemma map_powerAction_zero_of_comparison (n : ℕ) (M : C)
    (h : (powerAction S b n).app (F.obj M) = 0) :
    F.map ((powerAction T a n).app M) = 0 := by
…
```
Mentions: OAI.CartierImageFiltration.powerAction

def OAI.CartierImageFiltration.identityPowerIso line 232

Source documentation

The recursively iterated identity functor is canonically the identity.

def identityPowerIso : (n : ℕ) → (M : C) → (power (𝟭 C) n).obj M ≅ M
  | 0, M => Iso.refl M
  | n + 1, M => identityPowerIso n M

/-- For the identity tensor functor, an iterated action is the power
of its endomorphism component, with its canonical source identification. -/

Mentions: OAI.CartierImageFiltration.power, OAI.CartierImageFiltration.iterated

lemma OAI.CartierImageFiltration.powerAction_id line 238
Source documentation
For the identity tensor functor, an iterated action is the power of its endomorphism component, with its canonical source identification.
```
lemma powerAction_id (b : 𝟭 C ⟶ 𝟭 C) (n : ℕ) (M : C) :
    (powerAction (𝟭 C) b n).app M =
      (identityPowerIso n M).hom ≫ (End.of (b.app M) ^ n).asHom := by
…
```
Mentions: OAI.CartierImageFiltration.powerAction, OAI.CartierImageFiltration.identityPowerIso
lemma OAI.CartierImageFiltration.powerAction_zero_of_trivialization line 253
Source documentation
A trivialization turns nilpotence of the normalized scalar endomorphism into nilpotence of the tensor-power action.
```
lemma powerAction_zero_of_trivialization (T : C ⥤ C) (a : T ⟶ 𝟭 C)
    (e : T ≅ 𝟭 C) (n : ℕ) (M : C)
    (h : (End.of ((e.inv ≫ a).app M) ^ n).asHom = 0) :
    (powerAction T a n).app M = 0 := by
…
```
Mentions: OAI.CartierImageFiltration.powerAction
lemma OAI.CartierAffineLattice.exists_uniform_power line 277
Source documentation
Finite generation makes the elementwise power killing condition uniform. This is the local Noetherian support step in the divisor lattice filtration.
```
lemma exists_uniform_power [Module.Finite R M] (t : R)
    (h : ∀ m : M, ∃ k : ℕ, t ^ k • m = 0) :
    ∃ k : ℕ, ∀ m : M, t ^ k • m = 0 := by
…
```

lemma OAI.CartierAffineLattice.exists_annihilator_power_of_localization_zero line 299

Source documentation

Vanishing of principal localization gives a uniform nilpotence exponent.

lemma exists_annihilator_power_of_localization_zero [Module.Finite R M]
    (t : R) (f : M →ₗ[R] L) [IsLocalizedModule.Away t f] [Subsingleton L] :
    ∃ k : ℕ, ∀ m : M, t ^ k • m = 0 := by
…

lemma OAI.CartierAffineLattice.exists_annihilator_power_of_puncture_zero line 315
Source documentation
The local support assertion: a coherent associated sheaf that vanishes on the complement of the principal divisor is killed by one power of its equation. This uses restriction, evaluation and localization.
```
lemma exists_annihilator_power_of_puncture_zero {R : CommRingCat.{0}}
    (M : ModuleCat R) [Module.Finite R M] (t : R)
    (h : IsZero ((tilde M).over (PrimeSpectrum.basicOpen t))) :
    ∃ k : ℕ, ∀ m : M, t ^ k • m = 0 := by
…
```
def OAI.AffineCartierNilpotence.equation line 341
Source documentation
Principal equation obtained from the trivialized ideal inclusion by the fully faithful associated-sheaf functor.
```
def equation : R :=
…
```
lemma OAI.AffineCartierNilpotence.normalized_scalar line 345

lemma OAI.AffineCartierNilpotence.powerAction_zero_of_puncture_zero line 356

Source documentation

Support on the Cartier divisor implies tensor-ideal nilpotence on an affine trivializing chart. The equation comes from the ideal inclusion.

lemma powerAction_zero_of_puncture_zero (M : ModuleCat R) [Module.Finite R M]
    (h : IsZero ((tilde M).over (PrimeSpectrum.basicOpen (equation L e i)))) :
    ∃ n : ℕ, (powerAction (tensorLeft (Spec R).sheaf L)
      (idealAction (Spec R).sheaf i) n).app (tilde M) = 0 := by
…

Mentions: OAI.AffineCartierNilpotence.equation

lemma OAI.AffineCartierNilpotence.coherent_powerAction_zero_of_puncture_zero line 370

Source documentation

Coherent affine sheaves satisfy uniform ideal nilpotence. The finite module of global sections is transferred through the affine counit.

lemma coherent_powerAction_zero_of_puncture_zero (M : (Spec R).Modules)
    [M.IsFinitePresentation]
    (h : IsZero (M.over (PrimeSpectrum.basicOpen (equation L e i)))) :
    ∃ n : ℕ, (powerAction (tensorLeft (Spec R).sheaf L)
      (idealAction (Spec R).sheaf i) n).app M = 0 := by
…

Mentions: OAI.AffineCartierNilpotence.equation

lemma OAI.CartierTorsion.line_map_formula line 407
lemma OAI.CartierTorsion.line_map_regular line 411

lemma OAI.CartierTorsion.tensor_action_injective line 421

Source documentation

Tensoring an invertible ideal with a torsion-free module is injective.

lemma tensor_action_injective [Module.IsTorsionFree R M] (hi : Function.Injective i) :
    Function.Injective
      ((TensorProduct.lid R M).toLinearMap.comp (TensorProduct.map i LinearMap.id)) := by
…

lemma OAI.ActualSheafTensor.idealAction_mono_of_unitIso line 459
lemma OAI.ActualSheafTensor.idealAction_mono_of_line line 493
Source documentation
An invertible ideal acts injectively on sectionwise torsion-free module sheaves. In particular its first Cartier Tor vanishes.
```
lemma idealAction_mono_of_line {L : SheafOfModules.{u} (ringSheaf R)}
    (d : LineTrivialization R L) (i : L ⟶ SheafOfModules.unit _) [Mono i]
    (M : SheafOfModules.{u} (ringSheaf R))
    (hM : ∀ U, Module.IsTorsionFree (R.obj.obj U) (M.val.obj U)) :
    Mono ((idealAction R i).app M) := by
…
```
Mentions: OAI.ActualSheafTensor.ringSheaf, OAI.ActualSheafTensor.LineTrivialization, OAI.ActualSheafTensor.idealAction

lemma OAI.CartierAffineLattice.hom_ext_affine line 555

Source documentation

Global sections detect maps from quasi-coherent affine sheaves.

lemma hom_ext_affine {M N : (Spec R).Modules} [M.IsQuasicoherent]
    (a b : M ⟶ N) (h : moduleSpecΓFunctor.map a = moduleSpecΓFunctor.map b) : a = b := by
…

lemma OAI.CartierAffineLattice.scalar_regular_on_Gamma line 569
Source documentation
Injectivity of a natural affine sheaf endomorphism is equivalent to injectivity of its scalar action on the module of global sections.
```
lemma scalar_regular_on_Gamma (b : 𝟭 (Spec R).Modules ⟶ 𝟭 (Spec R).Modules)
    (M : (Spec R).Modules) [M.IsQuasicoherent] [Mono (b.app M)] :
    IsSMulRegular (moduleSpecΓFunctor.obj M) (AffineNaturalScalar.scalar R b) := by
…
```
Mentions: OAI.AffineNaturalScalar.scalar
def OAI.CartierAffineLattice.affineCounitIso line 592
Source documentation
The canonical affine quasi-coherent counit isomorphism.
```
def affineCounitIso (M : (Spec R).Modules) [M.IsQuasicoherent] :
    tilde (moduleSpecΓFunctor.obj M) ≅ M := by
…
```

def OAI.CartierAffineLattice.affinePunctureSectionsIso line 598

Source documentation

The precise puncture identification on the associated section modules.

def affinePunctureSectionsIso (M N : (Spec R).Modules)
    [M.IsQuasicoherent] [N.IsQuasicoherent] (U : (Spec R).Opens)
    (e : M.over U ≅ N.over U) :
    Γ(tilde (moduleSpecΓFunctor.obj M), U) ≃ₗ[R]
      Γ(tilde (moduleSpecΓFunctor.obj N), U) :=
…

lemma OAI.CartierAffineLattice.coherent_compatible_sandwich line 615

Source documentation

For coherent sheaves on an affine Cartier chart, clearing both directions of a prescribed puncture isomorphism gives injective maps between their section modules, with a shared constructed exponent. The regularity of the equation is proved from the ideal action.

lemma coherent_compatible_sandwich (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 P := moduleSpecΓFunctor.obj M
…

Mentions: OAI.AffineCartierNilpotence.equation

lemma OAI.CartierAffineLattice.hom_ext_tilde_over line 688

Source documentation

A morphism from an associated affine sheaf, even over an arbitrary open, is determined by the images of the original module's sections. This is proved by localization on basic opens and sheaf separation.

lemma hom_ext_tilde_over (P : ModuleCat R) (N : (Spec R).Modules)
    (U : (Spec R).Opens) (a b : (tilde P).over U ⟶ N.over U)
    (h : ∀ x : P,
      (a.val.app (op (Over.mk (𝟙 U)))) ((tilde.toOpen P U).hom x) =
        (b.val.app (op (Over.mk (𝟙 U)))) ((tilde.toOpen P U).hom x)) : a = b := by
…

lemma OAI.CartierAffineLattice.tilde_cleared_map_over line 755

Source documentation

Denominator-cleared sheaf maps retain the prescribed puncture morphism.

lemma tilde_cleared_map_over (P Q : ModuleCat R) (t : R) (n : ℕ)
    (e : (tilde P).over (PrimeSpectrum.basicOpen t) ≅
      (tilde Q).over (PrimeSpectrum.basicOpen t)) (a : P →ₗ[R] Q)
    (ha : ∀ x, (tilde.toOpen Q (PrimeSpectrum.basicOpen t)).hom (a x) =
      t ^ n • punctureSectionsIso (PrimeSpectrum.basicOpen t) e
        ((tilde.toOpen P (PrimeSpectrum.basicOpen t)).hom x)) :
    ((tilde.functor R).map (ModuleCat.ofHom a)).over (PrimeSpectrum.basicOpen t) =
      ((tilde.functor R).map
        (ModuleCat.ofHom (t ^ n • (LinearMap.id : P →ₗ[R] P)))).over
          (PrimeSpectrum.basicOpen t) ≫ e.hom := by
…

Mentions: OAI.CartierAffineLattice.punctureSectionsIso

lemma OAI.CartierAffineLattice.exists_tilde_compatible_sandwich line 785

Source documentation

On every affine chart, a puncture isomorphism provides a pair of coherent-sheaf monomorphisms with one common denominator and exact compatibility on the whole puncture.

lemma exists_tilde_compatible_sandwich
    (P Q : ModuleCat R) [Module.FinitePresentation R P] [Module.FinitePresentation R Q]
    (t : R) (htP : IsSMulRegular P t) (htQ : IsSMulRegular Q t)
    (e : (tilde P).over (PrimeSpectrum.basicOpen t) ≅
      (tilde Q).over (PrimeSpectrum.basicOpen t)) :
    ∃ (n : ℕ) (a : tilde P ⟶ tilde Q) (b : tilde Q ⟶ tilde P),
      Mono a ∧ Mono b ∧
      a.over (PrimeSpectrum.basicOpen t) =
        ((tilde.functor R).map
          (ModuleCat.ofHom (t ^ n • (LinearMap.id : P →ₗ[R] P)))).over
            (PrimeSpectrum.basicOpen t) ≫ e.hom ∧
      b.over (PrimeSpectrum.basicOpen t) =
…

def OAI.CartierAffineLattice.tildeScalar line 840
Source documentation
Scalar map on an associated sheaf.
```
def tildeScalar (r : R) (P : ModuleCat R) : tilde P ⟶ tilde P :=
…
```
def OAI.CartierAffineLattice.affineScalar line 845
Source documentation
Scalar action on a quasi-coherent affine sheaf via its canonical section-module presentation, rather than an unspecified endomorphism.
```
def affineScalar (r : R) (M : (Spec R).Modules) [M.IsQuasicoherent] : M ⟶ M :=
…
```
lemma OAI.CartierAffineLattice.conjugate_compat line 849
lemma OAI.CartierAffineLattice.transport_all line 858
lemma OAI.CartierAffineLattice.sheaf_sandwich_of_linear line 879

lemma OAI.CartierAffineLattice.exists_coherent_sheaf_sandwich line 926

Source documentation

The affine coherent-sheaf sandwich on a trivializing Cartier chart. The equation and its regularity come from the ideal inclusion; the puncture compatibility is an equality of sheaf morphisms on all opens.

lemma exists_coherent_sheaf_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 t := AffineCartierNilpotence.equation L eL i
…

Mentions: OAI.AffineCartierNilpotence.equation