Documentation

Mathlib.RingTheory.LocalRing.Quotient

We gather results about the quotients of local rings.

source
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
Instances For
    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
    @[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
    Instances For
      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.