ModuleDepth.lean`

29 declarations, 0 contain sorry, 0 declared as axioms

Finite depth is attained by a regular sequence and cannot exceed dimension.

def OAI.SmallCM.localDepth line 11
def OAI.SmallCM.MainClaim line 18
Source documentation
Existence of a complete normal local domain over ℂ with no small Cohen–Macaulay module.
```
def MainClaim : Prop :=
…
```
lemma OAI.SmallCM.regular_length_le_localDepth line 36

lemma OAI.SmallCM.exists_regularSequence_of_localDepth_eq line 43

Source documentation

Finite positive depth is attained, not merely approached by sequence lengths.

lemma exists_regularSequence_of_localDepth_eq {n : ℕ}
    (hdepth : localDepth R M = (n + 1 : ℕ)) :
    ∃ rs : List R, (∀ x ∈ rs, x ∈ IsLocalRing.maximalIdeal R) ∧
      RingTheory.Sequence.IsRegular M rs ∧ rs.length = n + 1 := by
…

Mentions: OAI.SmallCM.localDepth

lemma OAI.SmallCM.regular_length_le_dimension line 57

Source documentation

A regular sequence in a finite module over a Noetherian local ring has length at most the ring dimension.

lemma regular_length_le_dimension [IsNoetherianRing R] [Module.Finite R M]
    (rs : List R) (hr : RingTheory.Sequence.IsRegular M rs) :
    (rs.length : WithBot ℕ∞) ≤ ringKrullDim R := by
…

lemma OAI.SmallCM.localDepth_le_of_dimension_eq line 75

lemma OAI.SmallCM.localDepth_eq_three_iff line 85

Source documentation

In dimension three, excluding depth three is equivalent to excluding regular sequences of length three.

lemma localDepth_eq_three_iff [IsNoetherianRing R] [Module.Finite R M]
    (hdim : ringKrullDim R = 3) :
    localDepth R M = 3 ↔ ∃ rs : List R,
      (∀ x ∈ rs, x ∈ IsLocalRing.maximalIdeal R) ∧
      RingTheory.Sequence.IsRegular M rs ∧ rs.length = 3 := by
…

Mentions: OAI.SmallCM.localDepth

lemma OAI.SmallCM.exists_regular_outside_maximalSquare line 102
lemma OAI.SmallCM.ext_vanishing_after_regular_quotient line 149

lemma OAI.SmallCM.regular_sequence_after_quotient line 163

Source documentation

Quotienting by any regular element in the maximal ideal loses at most one in regular-sequence depth. This is the bridge needed when replacing a parameter by one outside the square of the maximal ideal.

lemma regular_sequence_after_quotient
    {R M : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M]
    (rs : List R) (hmem : ∀ r ∈ rs, r ∈ maximalIdeal R)
    (hreg : IsRegular M rs) (n : ℕ) (hlen : n + 1 ≤ rs.length)
    (x : R) (hxm : x ∈ maximalIdeal R) (hx : IsSMulRegular M x) :
    ∃ ts : List R, ts.length = n ∧ (∀ t ∈ ts, t ∈ maximalIdeal R) ∧
      IsRegular (QuotSMulTop x M) ts := by
…

lemma OAI.SmallCM.quotient_generators_drop line 197

lemma OAI.SmallCM.free_of_regular_length_le_generators line 258

Source documentation

A finite module whose regular-sequence depth is at least the number of specified generators of the maximal ideal is free.

lemma free_of_regular_length_le_generators
    (n : ℕ) {R M : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M]
    (v : Fin n → R) (hv : Ideal.span (Set.range v) = maximalIdeal R)
    (rs : List R) (hmem : ∀ r ∈ rs, r ∈ maximalIdeal R)
    (hreg : IsRegular M rs) (hlen : n ≤ rs.length) : Module.Free R M := by
…

lemma OAI.SmallCM.exists_regular_from_mapped_radical line 307
lemma OAI.SmallCM.regular_sequence_change_scalars line 342
lemma OAI.SmallCM.regular_sequence_change_scalars_source line 374

theorem OAI.SmallCM.free_over_finite_local_base line 388

Source documentation

A sufficiently deep finite module is free over a local base whose maximal ideal is generated by the given number of parameters.

theorem free_over_finite_local_base
    {A R M : Type u} [CommRing A] [CommRing R] [IsLocalRing A] [IsLocalRing R]
    [Algebra A R] [IsNoetherianRing A] [IsNoetherianRing R] [Module.Finite A R]
    [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower A R M]
    [Module.Finite R M] [Nontrivial M]
    (hrad : (Ideal.map (algebraMap A R) (maximalIdeal A)).radical = maximalIdeal R)
    (n : ℕ) (v : Fin n → A) (hv : Ideal.span (Set.range v) = maximalIdeal A)
    (rs : List R) (hmem : ∀ r ∈ rs, r ∈ maximalIdeal R)
    (hreg : IsRegular M rs) (hlen : n ≤ rs.length) : Module.Free A M := by
…

lemma OAI.SmallCM.radical_map_maximalIdeal_of_integral line 405

theorem OAI.SmallCM.free_over_powerSeries_of_depth_three line 434

Source documentation

The completed-cone module is free over the actual three-dimensional power-series base, once the finite algebra structure has been constructed. No grading of the module, and no prescribed regular parameter sequence, is assumed. This closes the local-algebra step in the manuscript, lines 303–309.

theorem free_over_powerSeries_of_depth_three
    {R M : Type} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [Algebra (MvPowerSeries (Fin 3) ℂ) R] [Module.Finite (MvPowerSeries (Fin 3) ℂ) R]
    [AddCommGroup M] [Module R M] [Module (MvPowerSeries (Fin 3) ℂ) M]
    [IsScalarTower (MvPowerSeries (Fin 3) ℂ) R M]
    [Module.Finite R M] [Nontrivial M] (hdepth : localDepth R M = 3) :
    Module.Free (MvPowerSeries (Fin 3) ℂ) M := by
…

Mentions: OAI.SmallCM.localDepth

def OAI.ExplicitCone.parameterHom line 448
lemma OAI.ExplicitCone.parameterHom_injective line 451
lemma OAI.ExplicitCone.parameterHom_finite line 454
instance OAI.ExplicitCone.completedRing_parameterAlgebra line 457
instance OAI.ExplicitCone.completedRing_parameterFinite line 460
instance OAI.ExplicitCone.completedRing_parameterTower line 463
instance OAI.ExplicitCone.completedRing_parameterFaithful line 467

theorem OAI.ExplicitCone.module_free_from_depth_three line 473

Source documentation

No extra structure or condition on M is assumed: scalar restriction is canonical, through the actual finite injective normalization map.

theorem module_free_from_depth_three (M : Type) [AddCommGroup M]
    [Module completedRing M] [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    letI := Module.restrictScalars (MvPowerSeries (Fin 3) ℂ) completedRing M
…

Mentions: OAI.ExplicitCone.completedRing, OAI.SmallCM.localDepth

lemma OAI.SmallCM.torsionFree_of_algebraic line 490
lemma OAI.SmallCM.support_eq_univ_of_torsionFree line 504

theorem OAI.ExplicitCone.module_properties_from_depth_three line 519

Source documentation

Every hypothetical small CM module for the actual ring has full support and positive generic rank. This uses no grading or algebra structure on M.

theorem module_properties_from_depth_three (M : Type) [AddCommGroup M]
    [Module completedRing M] [Module.Finite completedRing M] [Nontrivial M]
    (hdepth : SmallCM.localDepth completedRing M = 3) :
    Module.IsTorsionFree completedRing M ∧
      0 < Module.finrank completedRing M ∧ Module.support completedRing M = Set.univ := by
…

Mentions: OAI.ExplicitCone.completedRing, OAI.SmallCM.localDepth