Local Ring

Results named in Tau Ceti's TauCeti.RingTheory.LocalRing modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCohen structure theorem with the minimal number of variables#

A complete local ring containing a field whose maximal ideal 𝔪 is finitely generated has a coefficient field s and is a quotient of the power series ring over its residue field in spanFinrank 𝔪 variables, by a surjection which is s on constants and sends the variables to generators of 𝔪.

TauCeti.exists_surjective_mvPowerSeries_spanFinrank.{u_1, u_2} (k : Type u_1) (R : Type u_2)
  [Field k] [CommRing R] [IsLocalRing R] [Algebra k R]
  [IsAdicComplete (IsLocalRing.maximalIdeal R) R] (hfg : (IsLocalRing.maximalIdeal R).FG) :
  ∃ s,
    (∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a) ∧
      ∃ φ,
        Function.Surjective ⇑φ ∧
          φ.comp MvPowerSeries.C = s ∧
            Ideal.span (Set.range fun i => φ (MvPowerSeries.X i)) = IsLocalRing.maximalIdeal R
Lean

Formalized in Tau Ceti as TauCeti.exists_surjective_mvPowerSeries_spanFinrank.

Other forms

Cohen structure theorem for complete local rings containing a field. Formalized in Tau Ceti as TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal.

TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal.{u_1, u_2, u_3} (k : Type u_1)
  (R : Type u_2) [Field k] [CommRing R] [IsLocalRing R] [Algebra k R]
  [IsAdicComplete (IsLocalRing.maximalIdeal R) R] {σ : Type u_3} [Finite σ] (x : σ → R)
  (hx : Ideal.span (Set.range x) = IsLocalRing.maximalIdeal R) :
  ∃ s,
    (∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a) ∧
      ∃ φ,
        Function.Surjective ⇑φ ∧ φ.comp MvPowerSeries.C = s ∧ ∀ (i : σ), φ (MvPowerSeries.X i) = x i
Sources
LeanTauCeti.exists_surjective_mvPowerSeries_spanFinrank · TauCeti.exists_surjective_mvPowerSeries_of_span_eq_maximalIdeal
Uses 1
Proof usesCohen's theorem: a complete local ring containing a field has a coefficient field

TheoremCohen's theorem: a complete local ring containing a field has a coefficient field#

If the complete local ring R is an algebra over some field k, then reduction R → ResidueField R has a ring homomorphism section. When k is perfect, TauCeti.residueFieldSection k R is even a k-algebra section. In general a k-linear section need not exist.

TauCeti.exists_residueFieldSection.{u_1, u_2} (k : Type u_1) (R : Type u_2) [Field k] [CommRing R]
  [IsLocalRing R] [Algebra k R] [IsAdicComplete (IsLocalRing.maximalIdeal R) R] :
  ∃ s, ∀ (a : IsLocalRing.ResidueField R), (IsLocalRing.residue R) (s a) = a
Lean

Formalized in Tau Ceti as TauCeti.exists_residueFieldSection.

Sources
LeanTauCeti.exists_residueFieldSection
Used by 2
Used byAt every place the completion is F_P((T)), separable residue field or not · Cohen structure theorem with the minimal number of variables

TheoremHilbert's counting identity#

Let a finite group G act faithfully on a discrete valuation ring S generated over a base R fixed by G by a single element ξ. Then the sum over the nontrivial σ ∈ G of the valuations v (σ • ξ - ξ) is ∑_{i ≥ 0} (#G_i - 1), where G_i is the i-th ramification group: each σ ≠ 1 lies in exactly v (σ • ξ - ξ) of the groups G_0, G_1, …, and the sum is finite because the filtration is eventually trivial.

TauCeti.IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one.{u_1, u_2, u_3}
  {G : Type u_1} [Group G] {S : Type u_2} [CommRing S] [IsDomain S] [IsDiscreteValuationRing S]
  [MulSemiringAction G S] {R : Type u_3} [CommSemiring R] [Algebra R S] [SMulCommClass G R S]
  [Fintype G] [DecidableEq G] [FaithfulSMul G S] {ξ : S} (hξ : R[ξ] = ⊤) :
  ∑ σ ∈ Finset.univ.erase 1, (IsDiscreteValuationRing.addVal S) (σ • ξ - ξ) =
    ↑(∑ᶠ (i : ℕ), (Nat.card ↥(TauCeti.IsLocalRing.ramificationGroup G S ↑i) - 1))
Lean

Formalized in Tau Ceti as TauCeti.IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one.

Sources
LeanTauCeti.IsLocalRing.sum_addVal_smul_sub_eq_finsum_card_ramificationGroup_sub_one
Uses 1 · Used by 2
Proof usesSerre's criterion
Used byHilbert's different formula · Hilbert's formula, truncated

TheoremNakayama's lemma in coordinates#

Elements of 𝔪 whose gradients span κⁿ generate 𝔪.

TauCeti.maximalIdeal_eq_span_range_of_span_eq_top.{u_1, u_2, u_3, u_4} {R : Type u_1} {Q : Type u_2}
  {ι : Type u_3} {κ : Type u_4} [CommSemiring R] [CommRing Q] [Algebra R Q] [IsLocalRing Q]
  [DecidableEq ι] {x : ι → Q} {D : ι → Derivation R Q Q} [Finite ι] [Finite κ]
  (hx : IsLocalRing.maximalIdeal Q = Ideal.span (Set.range x))
  (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {w : κ → Q}
  (hw : ∀ (k : κ), w k ∈ IsLocalRing.maximalIdeal Q)
  (h :
    Submodule.span (IsLocalRing.ResidueField Q)
        (Set.range fun k i => (IsLocalRing.residue Q) ((D i) (w k))) =
      ⊤) :
  IsLocalRing.maximalIdeal Q = Ideal.span (Set.range w)
Lean

Formalized in Tau Ceti as TauCeti.maximalIdeal_eq_span_range_of_span_eq_top.

Sources
LeanTauCeti.maximalIdeal_eq_span_range_of_span_eq_top

TheoremSerre's criterion for the ramification filtration#

when S is generated over R by a set s and G acts by R-algebra automorphisms, membership in G_i is decided on s alone. This is TauCeti.Ideal.mem_inertia_iff_of_adjoin_eq_top at a power of the maximal ideal.

TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_eq_top.{u_1, u_2, u_3} {G : Type u_1}
  [Group G] {S : Type u_2} [CommRing S] [IsLocalRing S] [MulSemiringAction G S] {R : Type u_3}
  [CommSemiring R] [Algebra R S] [SMulCommClass G R S] {s : Set S} (hs : Algebra.adjoin R s = ⊤)
  {i : ℤ} {σ : G} :
  σ ∈ TauCeti.IsLocalRing.ramificationGroup G S i ↔
    ∀ x ∈ s, σ • x - x ∈ IsLocalRing.maximalIdeal S ^ (i + 1).toNat
Lean

Formalized in Tau Ceti as TauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_eq_top.

Sources
LeanTauCeti.IsLocalRing.mem_ramificationGroup_iff_of_adjoin_eq_top
Uses 1
Proof usesSerre's criterion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.