CMReflexivity.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Depth localization and reflexivity of finite maximal Cohen–Macaulay modules.

lemma OAI.SmallCM.LocalizationDepth.subsingleton_ext_of_subsingleton_left line 20
lemma OAI.SmallCM.LocalizationDepth.subsingleton_of_smul_surjective line 29
lemma OAI.SmallCM.LocalizationDepth.ext_subsingleton_of_regular_quotient line 42
lemma OAI.SmallCM.LocalizationDepth.ext_subsingleton_of_supportDim_le_zero line 61
lemma OAI.SmallCM.LocalizationDepth.ext_subsingleton_of_shortExact line 81

lemma OAI.SmallCM.LocalizationDepth.ext_vanishing_of_supportDim_le line 103

Source documentation

A regular sequence of length n forces Ext against every finite module of support dimension at most d to vanish below n-d. The proof uses prime filtrations, the regular-element dimension drop, the long exact Ext sequence, and Nakayama; it does not assume a depth-localization theorem.

lemma ext_vanishing_of_supportDim_le (M : ModuleCat.{u} R)
    [Module.Finite R M] (rs : List R)
    (hm : ∀ x ∈ rs, x ∈ maximalIdeal R) (hr : IsRegular M rs)
    (d : ℕ) (N : Type u) [AddCommGroup N] [Module R N] [Module.Finite R N] :
    Module.supportDim R N ≤ d → ∀ i : ℕ, i + d < rs.length →
      Subsingleton (Ext (ModuleCat.of R N) M i) := by
…

lemma OAI.SmallCM.LocalizationDepth.exists_regular_in_prime line 152

Source documentation

A global regular sequence gives a sufficiently long regular sequence inside any prime, with the loss controlled by the dimension of the quotient.

lemma exists_regular_in_prime (M : Type u) [AddCommGroup M] [Module R M]
    [Module.Finite R M] (rs : List R)
    (hm : ∀ x ∈ rs, x ∈ maximalIdeal R) (hr : IsRegular M rs)
    (p : Ideal R) [p.IsPrime] (d : ℕ) (hdim : ringKrullDim (R ⧸ p) ≤ d) :
    ∃ ts : List R, ts.length = rs.length - d ∧ (∀ x ∈ ts, x ∈ p) ∧ IsRegular M ts := by
…

lemma OAI.SmallCM.LocalizationDepth.localDepth_le_localized_add line 174

Source documentation

The regular-sequence definition of depth obeys the localization inequality. The localized module is not assumed to be graded, free, or Cohen–Macaulay.

lemma localDepth_le_localized_add
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (p : Ideal R) [p.IsPrime] (d : ℕ) (hdim : ringKrullDim (R ⧸ p) ≤ d)
    (S N : Type u) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p]
    [IsLocalRing S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [Nontrivial N] [Module.Finite S N]
    (f : M →ₗ[R] N) [IsLocalizedModule.AtPrime p f] :
    localDepth R M ≤ localDepth S N + d := by
…

Mentions: OAI.SmallCM.localDepth

lemma OAI.SmallCM.LocalizationDepth.localization_quotient_dim_le line 199
Source documentation
A chain through p is obtained by concatenating chains below and above it. This is the dimension budget needed to pass full depth to a localization.
```
lemma localization_quotient_dim_le (p : Ideal R) [p.IsPrime]
    (S : Type*) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p] :
    ringKrullDim S + ringKrullDim (R ⧸ p) ≤ ringKrullDim R := by
…
```

lemma OAI.SmallCM.LocalizationDepth.localized_full_depth line 216

Source documentation

Maximal depth, expressed using the regular-sequence convention, localizes at every point of the module's support. No equidimensionality or catenarity is assumed, and the module is completely arbitrary (not graded).

lemma localized_full_depth
    (M : Type u) [AddCommGroup M] [Module R M] [Module.Finite R M]
    (hdepth : ringKrullDim R ≤ (localDepth R M : WithBot ℕ∞))
    (p : Ideal R) [p.IsPrime]
    (S N : Type u) [CommRing S] [Algebra R S] [IsLocalization.AtPrime S p]
    [IsLocalRing S] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N]
    [Nontrivial N] [Module.Finite S N]
    (f : M →ₗ[R] N) [IsLocalizedModule.AtPrime p f] :
    ringKrullDim S ≤ (localDepth S N : WithBot ℕ∞) := by
…

Mentions: OAI.SmallCM.localDepth

def OAI.CMBidualBaseChange.dualIso line 255
lemma OAI.CMBidualBaseChange.dualIso_tmul line 260
def OAI.CMBidualBaseChange.bidualIso line 267
lemma OAI.CMBidualBaseChange.bidualIso_eval line 271
lemma OAI.CMBidualBaseChange.eval_baseChange line 282
lemma OAI.CMBidualBaseChange.surjective_eval_baseChange line 289
lemma OAI.CMCodimension.coheight_le_one line 307
lemma OAI.CMCodimension.supportDim_le_one line 324
lemma OAI.CMCodimension.atPrime_pid line 336
lemma OAI.CMCokernel.eval_injective line 361
abbrev OAI.CMCokernel.cokernel line 372
lemma OAI.CMCokernel.eval_exact line 376
lemma OAI.CMCokernel.notMem_support line 380
lemma OAI.CMCokernel.supportDim_le_one line 404
lemma OAI.CMReflexivity.eval_surjective_of_regular_three line 424
lemma OAI.CMReflexivity.reflexive_of_regular_three line 465
def OAI.CMReflexiveSheaf.identityEIso line 482
def OAI.CMReflexiveSheaf.openEIso line 490
theorem OAI.CMReflexiveSheaf.openImmersion_over_open line 495
def OAI.CMReflexiveSheaf.punctureEIso line 501