Documentation

TauCeti.RingTheory.GradedAlgebra.Quotient

Submodule families in an ideal quotient #

TauCeti.GradedAlgebra.quotientPiece 𝒜 I i is the image of the submodule 𝒜 i under Ideal.Quotient.mkₐ R I. The family can be arbitrary: multiplicative families descend to multiplicative families, and spanning families descend to spanning families. These results apply to overlapping families such as polynomial degree filtrations, without asserting a direct-sum grading of the quotient.

The scalar base is a commutative semiring, and I is a two-sided ideal of the ambient ring. When 𝒜 is a grading and I is homogeneous, the additional direct-sum construction is in TauCeti.RingTheory.GradedAlgebra.Homogeneous.Quotient.

The quotient-piece construction follows Antoine Chambert-Loir's Mathlib PR #36501.

Main results #

source
noncomputable def TauCeti.GradedAlgebra.quotientPiece {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] (i : ι) :
Submodule R (A ⧸ I)

The image of 𝒜 i in the quotient by a two-sided ideal I. The family 𝒜 need not be a grading. When it is a grading and I is homogeneous, these images grade the quotient.

Equations
Instances For
    source
    theorem TauCeti.GradedAlgebra.quotientPiece_def {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] (i : ι) :
    quotientPiece 𝒜 I i = Submodule.map (Ideal.Quotient.mkₐ R I).toLinearMap (𝒜 i)

    A quotient piece is the image of its original submodule under the quotient map.

    source
    @[simp]
    theorem TauCeti.GradedAlgebra.mem_quotientPiece_iff {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] {i : ι} {x : A ⧸ I} :
    x ∈ quotientPiece 𝒜 I i ↔ ∃ y ∈ 𝒜 i, (Ideal.Quotient.mk I) y = x

    Membership in the descended piece is being the class of an element of the original piece.

    source
    theorem TauCeti.GradedAlgebra.mk_mem_quotientPiece {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] {i : ι} {y : A} (hy : y ∈ 𝒜 i) :
    (Ideal.Quotient.mk I) y ∈ quotientPiece 𝒜 I i

    An element of 𝒜 i lands in the corresponding piece of the quotient.

    source
    theorem TauCeti.GradedAlgebra.quotientPiece_eq_span_image {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] {i : ι} {s : Set A} (hs : 𝒜 i = Submodule.span R s) :
    quotientPiece 𝒜 I i = Submodule.span R (⇑(Ideal.Quotient.mk I) '' s)

    The descended piece is the span of the images of any spanning family of the original piece: descending commutes with spanning.

    source
    theorem TauCeti.GradedAlgebra.mem_span_of_mem_quotientPiece {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] {i : ι} {s : Set A} (hs : 𝒜 i = Submodule.span R s) {t : Set (A ⧸ I)} (hmem : ∀ z ∈ s, (Ideal.Quotient.mk I) z ∈ Submodule.span R t) {w : A ⧸ I} (hw : w ∈ quotientPiece 𝒜 I i) :
    w ∈ Submodule.span R t

    A member of a descended piece lies in the span of t if the images of a spanning family of the original piece lie in that span.

    source
    theorem TauCeti.GradedAlgebra.quotientPiece_eq_bot_of_le {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] {i : ι} (hle : ∀ y ∈ 𝒜 i, y ∈ I) :
    quotientPiece 𝒜 I i = ⊥

    A piece contained in I vanishes in the quotient.

    source
    theorem TauCeti.GradedAlgebra.quotientPiece_mul_quotientPiece_le {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] [Add ι] [SetLike.GradedMul 𝒜] (m n : ι) :
    quotientPiece 𝒜 I m * quotientPiece 𝒜 I n ≤ quotientPiece 𝒜 I (m + n)

    Multiplication adds degrees, as an inclusion of products of pieces.

    source
    theorem TauCeti.GradedAlgebra.mul_mem_quotientPiece {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] [Add ι] [SetLike.GradedMul 𝒜] {m n : ι} {x y : A ⧸ I} (hx : x ∈ quotientPiece 𝒜 I m) (hy : y ∈ quotientPiece 𝒜 I n) :
    x * y ∈ quotientPiece 𝒜 I (m + n)

    Multiplication adds degrees in the quotient: the product of a degree-m class and a degree-n class lies in degree m + n.

    source
    instance TauCeti.GradedAlgebra.instGradedMonoidQuotientIdealSubmoduleQuotientPiece {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] [AddMonoid ι] [SetLike.GradedMonoid 𝒜] :
    SetLike.GradedMonoid (quotientPiece 𝒜 I)

    The multiplicative structure of the descended pieces: the unit lies in degree 0 and multiplication adds degrees. This supplies the instance data for downstream GradedAlgebra constructions; neither independence of the pieces nor homogeneity of I is required. Since SetLike.GradedMonoid is a Prop-valued class, this can be registered globally without attaching data to unrelated quotients.

    source
    theorem TauCeti.GradedAlgebra.iSup_quotientPiece_eq_top {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [Ring A] [Algebra R A] (𝒜 : ι → Submodule R A) (I : Ideal A) [I.IsTwoSided] (h𝒜 : ⨆ (i : ι), 𝒜 i = ⊤) :
    ⨆ (i : ι), quotientPiece 𝒜 I i = ⊤

    If the original pieces span A, their images span the quotient. The pieces may overlap.