Mathlib.RingTheory.LocalRing.Quotient

We gather results about the quotients of local rings.

theorem IsLocalRing.quotient_span_eq_top_iff_span_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] (s : Set S) :

Submodule.span (R ⧸ maximalIdeal R) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) '' s) = ⊤ ↔ Submodule.span R s = ⊤

source

theorem IsLocalRing.finrank_quotient_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] :

Module.finrank (R ⧸ maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) = Module.finrank R S

source

noncomputable def IsLocalRing.basisQuotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) :

Basis ι (R ⧸ maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Given a basis of S, the induced basis of S / Ideal.map (algebraMap R S) p.

Equations

IsLocalRing.basisQuotient b = basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) ∘ ⇑b) ⋯ ⋯

source

theorem IsLocalRing.basisQuotient_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) (i : ι) :

(basisQuotient b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) (b i)

source

theorem IsLocalRing.basisQuotient_repr {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_4} [Fintype ι] (b : Basis ι R S) (x : S) (i : ι) :

((basisQuotient b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) x)) i = (Ideal.Quotient.mk (maximalIdeal R)) ((b.repr x) i)

source

theorem IsLocalRing.exists_maximalIdeal_pow_le_of_finite_quotient {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [Finite (R ⧸ I)] :

∃ (n : ℕ), maximalIdeal R ^ n ≤ I

source

theorem IsLocalRing.finite_quotient_iff {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Finite (ResidueField R)] {I : Ideal R} :

Finite (R ⧸ I) ↔ ∃ (n : ℕ), maximalIdeal R ^ n ≤ I

source

@[deprecated IsLocalRing.quotient_span_eq_top_iff_span_eq_top (since := "2024-11-11")]

theorem LocalRing.quotient_span_eq_top_iff_span_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] (s : Set S) :

Submodule.span (R ⧸ IsLocalRing.maximalIdeal R) (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) '' s) = ⊤ ↔ Submodule.span R s = ⊤

Alias of IsLocalRing.quotient_span_eq_top_iff_span_eq_top.

source

@[deprecated IsLocalRing.finrank_quotient_map (since := "2024-11-11")]

theorem LocalRing.finrank_quotient_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] :

Module.finrank (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) = Module.finrank R S

Alias of IsLocalRing.finrank_quotient_map.

source

@[deprecated IsLocalRing.basisQuotient (since := "2024-11-11")]

def LocalRing.basisQuotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) :

Basis ι (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))

Alias of IsLocalRing.basisQuotient.

Given a basis of S, the induced basis of S / Ideal.map (algebraMap R S) p.

Equations

@LocalRing.basisQuotient = @IsLocalRing.basisQuotient

source

@[deprecated IsLocalRing.basisQuotient_apply (since := "2024-11-11")]

theorem LocalRing.basisQuotient_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_3} [Fintype ι] (b : Basis ι R S) (i : ι) :

(IsLocalRing.basisQuotient b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) (b i)

Alias of IsLocalRing.basisQuotient_apply.

source

@[deprecated IsLocalRing.basisQuotient_repr (since := "2024-11-11")]

theorem LocalRing.basisQuotient_repr {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsLocalRing R] [Module.Finite R S] [Module.Free R S] {ι : Type u_4} [Fintype ι] (b : Basis ι R S) (x : S) (i : ι) :

((IsLocalRing.basisQuotient b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) x)) i = (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ((b.repr x) i)

Alias of IsLocalRing.basisQuotient_repr.