Documentation

TauCeti.RingTheory.Ideal.Quotient.Pi

Componentwise quotient maps of products #

For families of two-sided ideals I j ≤ J j of an R₁-algebra A, the quotient maps A ⧸ I j → A ⧸ J j assemble into an R₁-algebra map ∏ j, A ⧸ I j → ∏ j, A ⧸ J j, which is surjective. This is the product version of Mathlib's Ideal.Quotient.factorₐ.

For ideals I i of a commutative ring and exponents n i, the factors of ∏ i, A ⧸ I i ^ n i with n i = 0 are zero, so restricting to the factors with n i ≠ 0 is a linear bijection.

Main declarations #

source
def TauCeti.Ideal.Quotient.piFactorₐ (R₁ : Type u_1) {A : Type u_2} [CommSemiring R₁] [Ring A] [Algebra R₁ A] {ι : Type u_3} {I J : ι → Ideal A} [∀ (j : ι), (I j).IsTwoSided] [∀ (j : ι), (J j).IsTwoSided] (hle : ∀ (j : ι), I j ≤ J j) :
((j : ι) → A ⧸ I j) →ₐ[R₁] (j : ι) → A ⧸ J j

The componentwise quotient map ∏ j, A ⧸ I j → ∏ j, A ⧸ J j for ideals I j ≤ J j.

Instances For
    source
    @[simp]
    theorem TauCeti.Ideal.Quotient.piFactorₐ_apply (R₁ : Type u_1) {A : Type u_2} [CommSemiring R₁] [Ring A] [Algebra R₁ A] {ι : Type u_3} {I J : ι → Ideal A} [∀ (j : ι), (I j).IsTwoSided] [∀ (j : ι), (J j).IsTwoSided] (hle : ∀ (j : ι), I j ≤ J j) (x : (j : ι) → A ⧸ I j) (j : ι) :
    (piFactorₐ R₁ hle) x j = (Ideal.Quotient.factor ⋯) (x j)

    Each component of piFactorₐ is the quotient map A ⧸ I j → A ⧸ J j.

    source
    theorem TauCeti.Ideal.Quotient.piFactorₐ_surjective (R₁ : Type u_1) {A : Type u_2} [CommSemiring R₁] [Ring A] [Algebra R₁ A] {ι : Type u_3} {I J : ι → Ideal A} [∀ (j : ι), (I j).IsTwoSided] [∀ (j : ι), (J j).IsTwoSided] (hle : ∀ (j : ι), I j ≤ J j) :
    Function.Surjective ⇑(piFactorₐ R₁ hle)

    The componentwise quotient map is surjective.

    source
    theorem TauCeti.Ideal.Quotient.bijective_pi_restrict_pow {A : Type u_1} [CommRing A] {ι : Type u_2} (I : ι → Ideal A) (n : ι → ℕ) :
    Function.Bijective ⇑(LinearMap.pi fun (y : { i : ι // n i ≠ 0 }) => LinearMap.proj ↑y)

    Dropping the factors with exponent zero from ∏ᵢ A ⧸ Iᵢ ^ nᵢ is bijective, as those factors are A ⧸ A = 0.