We gather results about the quotients of local rings.
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]
[LocalRing R]
[Module.Finite R S]
(s : Set S)
:
Submodule.span (R ⧸ LocalRing.maximalIdeal R)
(⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) '' s) = ⊤ ↔ Submodule.span R s = ⊤
theorem
LocalRing.finrank_quotient_map
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[LocalRing R]
[Module.Finite R S]
[Module.Free R S]
:
Module.finrank (R ⧸ LocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R)) = Module.finrank R S
noncomputable def
LocalRing.basisQuotient
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[LocalRing R]
[Module.Finite R S]
[Module.Free R S]
{ι : Type u_3}
[Fintype ι]
(b : Basis ι R S)
:
Basis ι (R ⧸ LocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))
Given a basis of S, the induced basis of S / Ideal.map (algebraMap R S) p.
Equations
- LocalRing.basisQuotient b = basisOfTopLeSpanOfCardEqFinrank (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) ∘ ⇑b) ⋯ ⋯
Instances For
theorem
LocalRing.basisQuotient_apply
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[LocalRing R]
[Module.Finite R S]
[Module.Free R S]
{ι : Type u_3}
[Fintype ι]
(b : Basis ι R S)
(i : ι)
:
(LocalRing.basisQuotient b) i = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) (b i)
theorem
LocalRing.basisQuotient_repr
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[CommRing S]
[Algebra R S]
[LocalRing R]
[Module.Finite R S]
[Module.Free R S]
{ι : Type u_4}
[Fintype ι]
(b : Basis ι R S)
(x : S)
(i : ι)
:
((LocalRing.basisQuotient b).repr ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (LocalRing.maximalIdeal R))) x)) i = (Ideal.Quotient.mk (LocalRing.maximalIdeal R)) ((b.repr x) i)