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 = ⊤

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

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 : Module.Basis ι R S) : Module.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) ⋯ ⋯

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 : Module.Basis ι R S) (i : ι) : (basisQuotient b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (maximalIdeal R))) (b i)

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 : Module.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)

theorem IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient {R : Type u_1} [CommRing R] [IsLocalRing R] (I : Ideal R) [IsArtinianRing (R ⧸ I)] : ∃ (n : ℕ), maximalIdeal R ^ n ≤ I

instance IsLocalRing.instFiniteQuotientIdealHPowNatMaximalIdealOfIsNoetherianRingOfResidueField {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Finite (ResidueField R)] (n : ℕ) : Finite (R ⧸ maximalIdeal R ^ n)

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