Mathlib.RingTheory.Ideal.Quotient.Operations

RingHom.kerLift definition

: R ⧸ ker f →+* S

Full source

/-- The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotientKerEquivOfRightInverse`) /
is surjective (`quotientKerEquivOfSurjective`).
-/
def kerLift : R ⧸ ker fR ⧸ ker f →+* S :=
  Ideal.Quotient.lift _ f fun _ => mem_ker.mp

Induced homomorphism from quotient by kernel

Informal description

Given a ring homomorphism $f \colon R \to S$, the induced map $\ker f \colon R/\ker f \to S$ is defined by sending each equivalence class $[r] \in R/\ker f$ to $f(r) \in S$. This map is well-defined since $f$ is constant on each coset of $\ker f$.

RingHom.kerLift_mk theorem

(r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r

Full source

@[simp]
theorem kerLift_mk (r : R) : kerLift f (Ideal.Quotient.mk (ker f) r) = f r :=
  Ideal.Quotient.lift_mk _ _ _

Evaluation of Induced Homomorphism on Quotient Elements

Informal description

For any ring homomorphism $f \colon R \to S$ and any element $r \in R$, the induced homomorphism $\ker f \colon R/\ker f \to S$ satisfies $\ker f([r]) = f(r)$, where $[r]$ denotes the equivalence class of $r$ in the quotient ring $R/\ker f$.

RingHom.lift_injective_of_ker_le_ideal theorem

 (I : Ideal R) [I.IsTwoSided] {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0) (hI : ker f ≤ I) :
  Function.Injective (Ideal.Quotient.lift I f H)

Full source

theorem lift_injective_of_ker_le_ideal (I : Ideal R) [I.IsTwoSided]
    {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
    (hI : ker f ≤ I) : Function.Injective (Ideal.Quotient.lift I f H) := by
  rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
  intro u hu
  obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
  rw [Ideal.Quotient.lift_mk] at hu
  rw [Ideal.Quotient.eq_zero_iff_mem]
  exact hI (RingHom.mem_ker.mpr hu)

Injectivity of Lifted Homomorphism when Kernel is Contained in Ideal

Informal description

Let $R$ and $S$ be commutative rings, $I$ a two-sided ideal of $R$, and $f \colon R \to S$ a ring homomorphism such that $f(a) = 0$ for all $a \in I$. If the kernel of $f$ is contained in $I$, then the induced homomorphism $\text{lift}(I, f, H) \colon R/I \to S$ is injective.

RingHom.kerLift_injective theorem

: Function.Injective (kerLift f)

Full source

/-- The induced map from the quotient by the kernel is injective. -/
theorem kerLift_injective : Function.Injective (kerLift f) :=
  lift_injective_of_ker_le_ideal (ker f) (fun a => by simp only [mem_ker, imp_self]) le_rfl

Injectivity of the Induced Homomorphism from Quotient by Kernel

Informal description

Given a ring homomorphism $f \colon R \to S$, the induced map $\ker f \colon R/\ker f \to S$ defined by $[r] \mapsto f(r)$ is injective.

RingHom.quotientKerEquivOfRightInverse definition

{g : S → R} (hf : Function.RightInverse g f) : R ⧸ ker f ≃+* S

Full source

/-- The **first isomorphism theorem for commutative rings**, computable version. -/
def quotientKerEquivOfRightInverse {g : S → R} (hf : Function.RightInverse g f) :
    R ⧸ ker fR ⧸ ker f ≃+* S :=
  { kerLift f with
    toFun := kerLift f
    invFun := Ideal.Quotient.mkIdeal.Quotient.mk (ker f) ∘ g
    left_inv := by
      rintro ⟨x⟩
      apply kerLift_injective
      simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk,
        Function.comp_apply, hf (f x)]
    right_inv := hf }

First Isomorphism Theorem for Rings with Right Inverse

Informal description

Given a ring homomorphism $ f \colon R \to S $ and a right inverse $ g \colon S \to R $ of $ f $ (i.e., $ f \circ g = \text{id}_S $), the quotient ring $ R / \ker f $ is isomorphic to $ S $ as a ring. The isomorphism is given by the induced homomorphism $ \ker f \colon R / \ker f \to S $ and its inverse $ [g] \colon S \to R / \ker f $, where $ [g] $ maps $ y \in S $ to the equivalence class of $ g(y) $ in $ R / \ker f $.

RingHom.quotientKerEquivOfRightInverse.apply theorem

{g : S → R} (hf : Function.RightInverse g f) (x : R ⧸ ker f) : quotientKerEquivOfRightInverse hf x = kerLift f x

Full source

@[simp]
theorem quotientKerEquivOfRightInverse.apply {g : S → R} (hf : Function.RightInverse g f)
    (x : R ⧸ ker f) : quotientKerEquivOfRightInverse hf x = kerLift f x :=
  rfl

First Isomorphism Theorem: Application of Quotient by Kernel Equivalence with Right Inverse

Informal description

Given a ring homomorphism $f \colon R \to S$ and a right inverse $g \colon S \to R$ of $f$ (i.e., $f \circ g = \text{id}_S$), for any element $x \in R / \ker f$, the isomorphism $\text{quotientKerEquivOfRightInverse}\ hf$ maps $x$ to $\ker f\ x$.

RingHom.quotientKerEquivOfRightInverse.Symm.apply theorem

 {g : S → R} (hf : Function.RightInverse g f) (x : S) :
  (quotientKerEquivOfRightInverse hf).symm x = Ideal.Quotient.mk (ker f) (g x)

Full source

@[simp]
theorem quotientKerEquivOfRightInverse.Symm.apply {g : S → R} (hf : Function.RightInverse g f)
    (x : S) : (quotientKerEquivOfRightInverse hf).symm x = Ideal.Quotient.mk (ker f) (g x) :=
  rfl

Inverse of First Isomorphism Theorem for Rings with Right Inverse

Informal description

Given a ring homomorphism $f \colon R \to S$ with a right inverse $g \colon S \to R$ (i.e., $f \circ g = \text{id}_S$), for any $x \in S$, the inverse of the isomorphism $R / \ker f \cong S$ maps $x$ to the equivalence class of $g(x)$ in $R / \ker f$. That is, $$(\text{quotientKerEquivOfRightInverse}\ hf)^{-1}(x) = [g(x)] \in R / \ker f.$$

RingHom.quotientKerEquivOfSurjective definition

(hf : Function.Surjective f) : R ⧸ (ker f) ≃+* S

Full source

/-- The **first isomorphism theorem** for commutative rings, surjective case. -/
noncomputable def quotientKerEquivOfSurjective (hf : Function.Surjective f) : R ⧸ (ker f)R ⧸ (ker f) ≃+* S :=
  quotientKerEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)

First Isomorphism Theorem for Surjective Ring Homomorphisms

Informal description

Given a surjective ring homomorphism $ f \colon R \to S $, the quotient ring $ R / \ker f $ is isomorphic to $ S $ as a ring. This is the **first isomorphism theorem** for commutative rings in the surjective case.

RingHom.quotientKerEquivRangeS definition

(f : R →+* S) : R ⧸ ker f ≃+* f.rangeS

Full source

/-- The **first isomorphism theorem** for commutative rings (`RingHom.rangeS` version). -/
noncomputable def quotientKerEquivRangeS (f : R →+* S) : R ⧸ ker fR ⧸ ker f ≃+* f.rangeS :=
  (Ideal.quotEquivOfEq f.ker_rangeSRestrict.symm).trans <|
  quotientKerEquivOfSurjective f.rangeSRestrict_surjective

First Isomorphism Theorem for Ring Homomorphisms (Subsemiring Version)

Informal description

Given a ring homomorphism $ f \colon R \to S $, the quotient ring $ R / \ker f $ is isomorphic to the subsemiring $ f.rangeS $ of $ S $ via the first isomorphism theorem for commutative rings. Here, $ f.rangeS $ denotes the image of $ f $ as a subsemiring of $ S $.

RingHom.quotientKerEquivRange definition

(f : R →+* S) : R ⧸ ker f ≃+* f.range

Full source

/-- The **first isomorphism theorem** for commutative rings (`RingHom.range` version). -/
noncomputable def quotientKerEquivRange (f : R →+* S) : R ⧸ ker fR ⧸ ker f ≃+* f.range :=
  (Ideal.quotEquivOfEq f.ker_rangeRestrict.symm).trans <|
    quotientKerEquivOfSurjective f.rangeRestrict_surjective

First Isomorphism Theorem for Ring Homomorphisms

Informal description

Given a ring homomorphism $ f \colon R \to S $, the quotient ring $ R / \ker f $ is isomorphic to the range of $ f $ as a ring. This is the **first isomorphism theorem** for commutative rings.

Ideal.map_quotient_self theorem

(I : Ideal R) [I.IsTwoSided] : map (Quotient.mk I) I = ⊥

Full source

@[simp]
theorem map_quotient_self (I : Ideal R) [I.IsTwoSided] : map (Quotient.mk I) I = ⊥ :=
  eq_bot_iff.2 <|
    Ideal.map_le_iff_le_comap.2 fun _ hx =>
      (Submodule.mem_bot (R ⧸ I)).2 <| Ideal.Quotient.eq_zero_iff_mem.2 hx

Image of Ideal Under Quotient Map is Zero

Informal description

For any two-sided ideal $I$ of a ring $R$, the image of $I$ under the quotient map $R \to R/I$ is the zero ideal in $R/I$, i.e., $I \mapsto 0$ under the quotient map.

Ideal.mk_ker theorem

{I : Ideal R} [I.IsTwoSided] : ker (Quotient.mk I) = I

Full source

@[simp]
theorem mk_ker {I : Ideal R} [I.IsTwoSided] : ker (Quotient.mk I) = I := by
  ext
  rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]

Kernel of Quotient Map Equals Ideal

Informal description

For any two-sided ideal $I$ of a ring $R$, the kernel of the quotient map $\pi : R \to R/I$ is equal to $I$ itself. That is, $\ker(\pi) = I$.

Ideal.map_mk_eq_bot_of_le theorem

{I J : Ideal R} [J.IsTwoSided] (h : I ≤ J) : I.map (Quotient.mk J) = ⊥

Full source

theorem map_mk_eq_bot_of_le {I J : Ideal R} [J.IsTwoSided] (h : I ≤ J) :
    I.map (Quotient.mk J) = ⊥ := by
  rw [map_eq_bot_iff_le_ker, mk_ker]
  exact h

Image of Contained Ideal Vanishes Under Quotient

Informal description

For any two-sided ideal $J$ of a commutative ring $R$ and any ideal $I$ of $R$ such that $I \subseteq J$, the image of $I$ under the quotient map $R \to R/J$ is the zero ideal, i.e., $I \mapsto 0$ in $R/J$.

Ideal.ker_quotient_lift theorem

 {I : Ideal R} [I.IsTwoSided] (f : R →+* S) (H : I ≤ ker f) :
  ker (Ideal.Quotient.lift I f H) = (RingHom.ker f).map (Quotient.mk I)

Full source

theorem ker_quotient_lift {I : Ideal R} [I.IsTwoSided] (f : R →+* S)
    (H : I ≤ ker f) :
    ker (Ideal.Quotient.lift I f H) = (RingHom.ker f).map (Quotient.mk I) := by
  apply Ideal.ext
  intro x
  constructor
  · intro hx
    obtain ⟨y, hy⟩ := Quotient.mk_surjective x
    rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
    rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
    exact ⟨y, hx, rfl⟩
  · intro hx
    rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
    obtain ⟨y, hy⟩ := hx
    rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
    exact hy.left

Kernel of Lifted Homomorphism Equals Quotient of Original Kernel

Informal description

Let $R$ and $S$ be commutative rings, $I$ a two-sided ideal of $R$, and $f \colon R \to S$ a ring homomorphism such that $I$ is contained in the kernel of $f$. Then the kernel of the lifted homomorphism $\text{lift}(I, f, H) \colon R/I \to S$ is equal to the image of the kernel of $f$ under the quotient map $\pi \colon R \to R/I$.

Ideal.injective_lift_iff theorem

 {I : Ideal R} [I.IsTwoSided] {f : R →+* S} (H : ∀ (a : R), a ∈ I → f a = 0) :
  Injective (Quotient.lift I f H) ↔ ker f = I

Full source

lemma injective_lift_iff {I : Ideal R} [I.IsTwoSided]
    {f : R →+* S} (H : ∀ (a : R), a ∈ I → f a = 0) :
    InjectiveInjective (Quotient.lift I f H) ↔ ker f = I := by
  rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]
  constructor
  · exact fun h ↦ le_antisymm h H
  · rintro rfl; rfl

Injectivity Criterion for Lifted Ring Homomorphism: $\ker f = I$

Informal description

Let $R$ and $S$ be commutative rings, $I$ a two-sided ideal of $R$, and $f \colon R \to S$ a ring homomorphism such that $f(a) = 0$ for all $a \in I$. Then the lifted homomorphism $\overline{f} \colon R/I \to S$ is injective if and only if the kernel of $f$ equals $I$.

Ideal.ker_Pi_Quotient_mk theorem

 {ι : Type*} (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] : ker (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) = ⨅ i, I i

Full source

lemma ker_Pi_Quotient_mk {ι : Type*} (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    ker (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) = ⨅ i, I i := by
  simp [Pi.ker_ringHom, mk_ker]

Kernel of Product of Quotient Maps Equals Infimum of Ideals

Informal description

For a commutative ring $R$ and a family of two-sided ideals $I_i$ indexed by $ι$, the kernel of the ring homomorphism from $R$ to the product of quotient rings $\prod_i (R/I_i)$ (where each component is the canonical quotient map $R \to R/I_i$) is equal to the infimum of the ideals $I_i$, i.e., \[ \ker\left(\prod_{i \in \iota} (R \to R/I_i)\right) = \bigsqcap_{i \in \iota} I_i. \]

Ideal.bot_quotient_isMaximal_iff theorem

(I : Ideal R) [I.IsTwoSided] : (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal

Full source

@[simp]
theorem bot_quotient_isMaximal_iff (I : Ideal R) [I.IsTwoSided] :
    (⊥ : Ideal (R ⧸ I)).IsMaximal ↔ I.IsMaximal :=
  ⟨fun hI =>
    mk_ker (I := I) ▸
      comap_isMaximal_of_surjective (Quotient.mk I) Quotient.mk_surjective (K := ⊥) (H := hI),
    fun hI => by
    letI := Quotient.divisionRing I
    exact bot_isMaximal⟩

Maximality of Zero Ideal in Quotient Ring Corresponds to Maximality of Ideal

Informal description

For any two-sided ideal $I$ of a ring $R$, the zero ideal in the quotient ring $R/I$ is maximal if and only if $I$ is a maximal ideal of $R$.

Ideal.mem_quotient_iff_mem_sup theorem

{I J : Ideal R} [I.IsTwoSided] {x : R} : Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J ⊔ I

Full source

/-- See also `Ideal.mem_quotient_iff_mem` in case `I ≤ J`. -/
@[simp]
theorem mem_quotient_iff_mem_sup {I J : Ideal R} [I.IsTwoSided] {x : R} :
    Quotient.mkQuotient.mk I x ∈ J.map (Quotient.mk I)Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J ⊔ I := by
  rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]

Membership in Quotient Ideal Image via Ideal Sum

Informal description

Let $R$ be a commutative ring with two-sided ideals $I$ and $J$. For any element $x \in R$, the image of $x$ under the quotient map $\pi_I : R \to R/I$ belongs to the image of $J$ under $\pi_I$ if and only if $x$ belongs to the ideal sum $J + I$.

Ideal.mem_quotient_iff_mem theorem

{I J : Ideal R} [I.IsTwoSided] (hIJ : I ≤ J) {x : R} : Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J

Full source

/-- See also `Ideal.mem_quotient_iff_mem_sup` if the assumption `I ≤ J` is not available. -/
theorem mem_quotient_iff_mem {I J : Ideal R} [I.IsTwoSided] (hIJ : I ≤ J) {x : R} :
    Quotient.mkQuotient.mk I x ∈ J.map (Quotient.mk I)Quotient.mk I x ∈ J.map (Quotient.mk I) ↔ x ∈ J := by
  rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]

Membership in Quotient Ideal Image under Ideal Inclusion

Informal description

Let $R$ be a commutative ring with two-sided ideals $I$ and $J$ such that $I \subseteq J$. For any element $x \in R$, the image of $x$ under the quotient map $\pi_I : R \to R/I$ belongs to the image of $J$ under $\pi_I$ if and only if $x \in J$.

Ideal.quotientInfToPiQuotient definition

(I : ι → Ideal R) [∀ i, (I i).IsTwoSided] : (R ⧸ ⨅ i, I i) →+* ∀ i, R ⧸ I i

Full source

/-- The homomorphism from `R/(⋂ i, f i)` to `∏ i, (R / f i)` featured in the Chinese
  Remainder Theorem. It is bijective if the ideals `f i` are coprime. -/
def quotientInfToPiQuotient (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    (R ⧸ ⨅ i, I i) →+* ∀ i, R ⧸ I i :=
  Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Quotient.mk (I i))
    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])

Chinese Remainder Theorem homomorphism from quotient by intersection to product of quotients

Informal description

The ring homomorphism from the quotient ring $ R / (\bigcap_i I_i) $ to the product ring $\prod_i (R / I_i)$, where $I_i$ is a family of two-sided ideals of a commutative ring $R$. This homomorphism is featured in the Chinese Remainder Theorem and is defined by lifting the canonical projection maps $R \to R/I_i$ to the quotient $R / (\bigcap_i I_i)$.

Ideal.quotientInfToPiQuotient_mk theorem

 (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] (x : R) :
  quotientInfToPiQuotient I (Quotient.mk _ x) = fun i : ι ↦ Quotient.mk (I i) x

Full source

lemma quotientInfToPiQuotient_mk (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] (x : R) :
    quotientInfToPiQuotient I (Quotient.mk _ x) = fun i : ι ↦ Quotient.mk (I i) x :=
  rfl

Commutativity of Chinese Remainder Theorem Homomorphism with Quotient Maps

Informal description

For a commutative ring $R$ and a family of two-sided ideals $I_i$ indexed by $\iota$, the homomorphism $\mathrm{quotientInfToPiQuotient}\, I$ from the quotient ring $R / (\bigcap_i I_i)$ to the product ring $\prod_i (R / I_i)$ satisfies the following property: for any element $x \in R$, the image of the equivalence class $[x] \in R / (\bigcap_i I_i)$ under this homomorphism is the family of equivalence classes $([x]_{I_i})_{i \in \iota}$ in $\prod_i (R / I_i)$. In other words, the following diagram commutes: $$ \begin{CD} R @>{\mathrm{Quotient.mk}\, (\bigcap_i I_i)}>> R / (\bigcap_i I_i) \\ @V{\mathrm{Quotient.mk}\, I_i}VV @VV{\mathrm{quotientInfToPiQuotient}\, I}V \\ R / I_i @<{\mathrm{proj}_i}<< \prod_i (R / I_i) \end{CD} $$ where $\mathrm{proj}_i$ is the projection onto the $i$-th component.

Ideal.quotientInfToPiQuotient_mk' theorem

 (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] (x : R) (i : ι) :
  quotientInfToPiQuotient I (Quotient.mk _ x) i = Quotient.mk (I i) x

Full source

lemma quotientInfToPiQuotient_mk' (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] (x : R) (i : ι) :
    quotientInfToPiQuotient I (Quotient.mk _ x) i = Quotient.mk (I i) x :=
  rfl

Component-wise evaluation of the Chinese Remainder Theorem homomorphism

Informal description

For a commutative ring $R$ with a family of two-sided ideals $I_i$ indexed by $\iota$, and for any element $x \in R$, the $i$-th component of the image of the equivalence class $[x]$ under the homomorphism from $R / (\bigcap_i I_i)$ to $\prod_i (R / I_i)$ is equal to the equivalence class $[x]$ in $R / I_i$.

Ideal.quotientInfToPiQuotient_inj theorem

(I : ι → Ideal R) [∀ i, (I i).IsTwoSided] : Injective (quotientInfToPiQuotient I)

Full source

lemma quotientInfToPiQuotient_inj (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    Injective (quotientInfToPiQuotient I) := by
  rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]

Injectivity of the Chinese Remainder Theorem Homomorphism

Informal description

For a commutative ring $R$ and a family of two-sided ideals $I_i$ indexed by $\iota$, the canonical ring homomorphism \[ R / \bigcap_i I_i \to \prod_i (R / I_i) \] is injective.

Ideal.quotientInfToPiQuotient_surj theorem

{I : ι → Ideal R} (hI : Pairwise (IsCoprime on I)) : Surjective (quotientInfToPiQuotient I)

Full source

lemma quotientInfToPiQuotient_surj {I : ι → Ideal R}
    (hI : Pairwise (IsCoprimeIsCoprime on I)) : Surjective (quotientInfToPiQuotient I) := by
  classical
  cases nonempty_fintype ι
  intro g
  choose f hf using fun i ↦ mk_surjective (g i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      intros j hj
      exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
    rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩
    replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
    refine ⟨e, ?_, ?_⟩
    · simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
    · exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
  choose e he using key
  use mk _ (∑ i, f i*e i)
  ext i
  rw [quotientInfToPiQuotient_mk', map_sum, Fintype.sum_eq_single i]
  · simp [(he i).1, hf]
  · intros j hj
    simp [(he j).2 i hj.symm]

Surjectivity of the Chinese Remainder Theorem homomorphism for pairwise coprime ideals

Informal description

Let $R$ be a commutative ring and $(I_i)_{i \in \iota}$ be a family of ideals of $R$ that are pairwise coprime (i.e., for any distinct $i,j \in \iota$, the ideals $I_i$ and $I_j$ are coprime). Then the canonical ring homomorphism \[ R / \bigcap_{i} I_i \to \prod_{i} (R / I_i) \] is surjective.

Ideal.quotientInfRingEquivPiQuotient definition

(f : ι → Ideal R) (hf : Pairwise (IsCoprime on f)) : (R ⧸ ⨅ i, f i) ≃+* ∀ i, R ⧸ f i

Full source

/-- **Chinese Remainder Theorem**. Eisenbud Ex.2.6.
Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/
noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R)
    (hf : Pairwise (IsCoprimeIsCoprime on f)) : (R ⧸ ⨅ i, f i) ≃+* ∀ i, R ⧸ f i :=
  { Equiv.ofBijective _ ⟨quotientInfToPiQuotient_inj f, quotientInfToPiQuotient_surj hf⟩,
    quotientInfToPiQuotient f with }

Chinese Remainder Theorem for Commutative Rings (Isomorphism Version)

Informal description

Given a commutative ring $ R $ and a family of pairwise coprime ideals $ (I_i)_{i \in \iota} $ of $ R $, the quotient ring $ R / (\bigcap_i I_i) $ is isomorphic to the product ring $ \prod_i (R / I_i) $ via the canonical map. This is the Chinese Remainder Theorem for commutative rings.

Ideal.pi_quotient_surjective theorem

 {I : ι → Ideal R} (hf : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : (i : ι) → R ⧸ I i) : ∃ r : R, ∀ i, r = x i

Full source

/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then the canonical map `R → ∏ (R ⧸ Iᵢ)` is surjective. -/
lemma pi_quotient_surjective {I : ι → Ideal R}
    (hf : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : (i : ι) → R ⧸ I i) :
    ∃ r : R, ∀ i, r = x i := by
  obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y
  exact ⟨r, fun i ↦ rfl⟩

Surjectivity of the Chinese Remainder Theorem map for pairwise coprime ideals

Informal description

Let $R$ be a commutative ring and $(I_i)_{i \in \iota}$ be a family of pairwise coprime ideals in $R$. For any family $(x_i)_{i \in \iota}$ where each $x_i \in R/I_i$, there exists an element $r \in R$ such that for all $i \in \iota$, the image of $r$ in $R/I_i$ equals $x_i$.

Ideal.exists_forall_sub_mem_ideal theorem

 {I : ι → Ideal R} (hI : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : ι → R) : ∃ r : R, ∀ i, r - x i ∈ I i

Full source

/-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
commutative ring then given elements `xᵢ` you can find `r` with `r - xᵢ ∈ Iᵢ` for all `i`. -/
lemma exists_forall_sub_mem_ideal
    {I : ι → Ideal R} (hI : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : ι → R) :
    ∃ r : R, ∀ i, r - x i ∈ I i := by
  obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)
  exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Chinese Remainder Theorem: Existence of Solution for Pairwise Coprime Ideals

Informal description

Let $R$ be a commutative ring, $(I_i)_{i \in \iota}$ a finite family of pairwise coprime ideals in $R$, and $(x_i)_{i \in \iota}$ a family of elements in $R$. Then there exists an element $r \in R$ such that for all $i \in \iota$, the difference $r - x_i$ belongs to $I_i$.

Ideal.quotientInfEquivQuotientProd definition

(I J : Ideal R) (coprime : IsCoprime I J) : R ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J

Full source

/-- **Chinese remainder theorem**, specialized to two ideals. -/
noncomputable def quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    R ⧸ I ⊓ JR ⧸ I ⊓ J ≃+* (R ⧸ I) × R ⧸ J :=
  let f : Fin 2 → Ideal R := ![I, J]
  have hf : Pairwise (IsCoprimeIsCoprime on f) := by
    intro i j h
    fin_cases i <;> fin_cases j <;> try contradiction
    · assumption
    · exact coprime.symm
  (Ideal.quotEquivOfEq (by simp [f, iInf, inf_comm])).trans <|
            (Ideal.quotientInfRingEquivPiQuotient f hf).trans <| RingEquiv.piFinTwo fun i => R ⧸ f i

Chinese Remainder Theorem for Two Coprime Ideals (Isomorphism Version)

Informal description

Given a commutative ring $ R $ and two coprime ideals $ I $ and $ J $ of $ R $, the quotient ring $ R / (I \cap J) $ is isomorphic to the product ring $ (R / I) \times (R / J) $ via the canonical map. This is a special case of the Chinese Remainder Theorem for two ideals.

Ideal.quotientInfEquivQuotientProd_fst theorem

 (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) :
  (quotientInfEquivQuotientProd I J coprime x).fst = Ideal.Quotient.factor inf_le_left x

Full source

@[simp]
theorem quotientInfEquivQuotientProd_fst (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) :
    (quotientInfEquivQuotientProd I J coprime x).fst =
      Ideal.Quotient.factor inf_le_left x :=
  Quot.inductionOn x fun _ => rfl

First Projection of Chinese Remainder Theorem Isomorphism Equals Canonical Quotient Map

Informal description

Let $R$ be a commutative ring, and let $I$ and $J$ be two coprime ideals of $R$. For any element $x$ in the quotient ring $R/(I \cap J)$, the first projection of the isomorphism $\text{quotientInfEquivQuotientProd}(I, J, \text{coprime})(x)$ equals the image of $x$ under the canonical ring homomorphism induced by the inclusion $I \cap J \subseteq I$.

Ideal.quotientInfEquivQuotientProd_snd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) :
  (quotientInfEquivQuotientProd I J coprime x).snd = Ideal.Quotient.factor inf_le_right x

Full source

@[simp]
theorem quotientInfEquivQuotientProd_snd (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) :
    (quotientInfEquivQuotientProd I J coprime x).snd =
      Ideal.Quotient.factor inf_le_right x :=
  Quot.inductionOn x fun _ => rfl

Second Component of Chinese Remainder Theorem Isomorphism for Coprime Ideals

Informal description

For any commutative ring $R$, two coprime ideals $I$ and $J$ of $R$, and any element $x$ in the quotient ring $R/(I \cap J)$, the second component of the isomorphism $\text{quotientInfEquivQuotientProd}(I, J, \text{coprime})(x)$ equals the image of $x$ under the canonical ring homomorphism from $R/(I \cap J)$ to $R/J$ induced by the inclusion $I \cap J \subseteq J$.

Ideal.fst_comp_quotientInfEquivQuotientProd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) :
  (RingHom.fst _ _).comp (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
    Ideal.Quotient.factor inf_le_left

Full source

@[simp]
theorem fst_comp_quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.fst _ _).comp
        (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ JR ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor inf_le_left := by
  apply Quotient.ringHom_ext; ext; rfl

First Projection of Chinese Remainder Isomorphism Equals Quotient Map

Informal description

Let $R$ be a commutative ring with ideals $I$ and $J$ such that $I$ and $J$ are coprime. The composition of the first projection homomorphism $(R/I) \times (R/J) \to R/I$ with the isomorphism $R/(I \cap J) \cong (R/I) \times (R/J)$ from the Chinese Remainder Theorem equals the canonical quotient homomorphism $R/(I \cap J) \to R/I$ induced by the inclusion $I \cap J \subseteq I$.

Ideal.snd_comp_quotientInfEquivQuotientProd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) :
  (RingHom.snd _ _).comp (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
    Ideal.Quotient.factor inf_le_right

Full source

@[simp]
theorem snd_comp_quotientInfEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.snd _ _).comp
        (quotientInfEquivQuotientProd I J coprime : R ⧸ I ⊓ JR ⧸ I ⊓ J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor inf_le_right := by
  apply Quotient.ringHom_ext; ext; rfl

Second Projection of Chinese Remainder Isomorphism Equals Quotient Map

Informal description

Let $R$ be a commutative ring with ideals $I$ and $J$ such that $I$ and $J$ are coprime. The composition of the second projection homomorphism $(R/I) \times (R/J) \to R/J$ with the isomorphism $R/(I \cap J) \cong (R/I) \times (R/J)$ equals the canonical quotient homomorphism $R/(I \cap J) \to R/J$ induced by the inclusion $I \cap J \subseteq J$.

Ideal.quotientMulEquivQuotientProd definition

(I J : Ideal R) (coprime : IsCoprime I J) : R ⧸ I * J ≃+* (R ⧸ I) × R ⧸ J

Full source

/-- **Chinese remainder theorem**, specialized to two ideals. -/
noncomputable def quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    R ⧸ I * JR ⧸ I * J ≃+* (R ⧸ I) × R ⧸ J :=
  Ideal.quotEquivOfEq (inf_eq_mul_of_isCoprime coprime).symm |>.trans <|
    Ideal.quotientInfEquivQuotientProd I J coprime

Chinese Remainder Theorem for Two Coprime Ideals (Product Version)

Informal description

Given a commutative ring $ R $ and two coprime ideals $ I $ and $ J $ of $ R $, the quotient ring $ R / (I \cdot J) $ is isomorphic to the product ring $ (R / I) \times (R / J) $ via the canonical map. This is a special case of the Chinese Remainder Theorem for two ideals, where the intersection $ I \cap J $ is replaced by the product $ I \cdot J $ due to the coprimality condition.

Ideal.quotientMulEquivQuotientProd_fst theorem

 (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) :
  (quotientMulEquivQuotientProd I J coprime x).fst = Ideal.Quotient.factor mul_le_right x

Full source

@[simp]
theorem quotientMulEquivQuotientProd_fst (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) :
    (quotientMulEquivQuotientProd I J coprime x).fst =
      Ideal.Quotient.factor mul_le_right x :=
  Quot.inductionOn x fun _ => rfl

First Projection of Chinese Remainder Isomorphism Equals Quotient Map

Informal description

Let $R$ be a commutative ring with coprime ideals $I$ and $J$. For any element $x$ in the quotient ring $R/(I \cdot J)$, the first projection of the isomorphism $\text{quotientMulEquivQuotientProd}(I, J, \text{coprime})(x)$ equals the image of $x$ under the canonical quotient map induced by the inclusion $I \cdot J \subseteq I$.

Ideal.quotientMulEquivQuotientProd_snd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) :
  (quotientMulEquivQuotientProd I J coprime x).snd = Ideal.Quotient.factor mul_le_left x

Full source

@[simp]
theorem quotientMulEquivQuotientProd_snd (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) :
    (quotientMulEquivQuotientProd I J coprime x).snd =
      Ideal.Quotient.factor mul_le_left x :=
  Quot.inductionOn x fun _ => rfl

Second Component of Chinese Remainder Theorem Isomorphism Equals Quotient Map to $R/J$

Informal description

Let $R$ be a commutative ring, and let $I$ and $J$ be two coprime ideals of $R$. For any element $x$ in the quotient ring $R/(I \cdot J)$, the second component of the image of $x$ under the isomorphism $R/(I \cdot J) \cong (R/I) \times (R/J)$ is equal to the image of $x$ under the canonical quotient map $R/(I \cdot J) \to R/J$ induced by the inclusion $I \cdot J \subseteq J$.

Ideal.fst_comp_quotientMulEquivQuotientProd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) :
  (RingHom.fst _ _).comp (quotientMulEquivQuotientProd I J coprime : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
    Ideal.Quotient.factor mul_le_right

Full source

@[simp]
theorem fst_comp_quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.fst _ _).comp
        (quotientMulEquivQuotientProd I J coprime : R ⧸ I * JR ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor mul_le_right := by
  apply Quotient.ringHom_ext; ext; rfl

First Projection of Chinese Remainder Isomorphism Equals Canonical Quotient Map

Informal description

Let $R$ be a commutative ring with two coprime ideals $I$ and $J$. The composition of the first projection ring homomorphism $(R/I) \times (R/J) \to R/I$ with the isomorphism $R/(I \cdot J) \cong (R/I) \times (R/J)$ equals the canonical quotient map $R/(I \cdot J) \to R/I$ induced by the inclusion $I \cdot J \subseteq I$.

Ideal.snd_comp_quotientMulEquivQuotientProd theorem

 (I J : Ideal R) (coprime : IsCoprime I J) :
  (RingHom.snd _ _).comp (quotientMulEquivQuotientProd I J coprime : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
    Ideal.Quotient.factor mul_le_left

Full source

@[simp]
theorem snd_comp_quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.snd _ _).comp
        (quotientMulEquivQuotientProd I J coprime : R ⧸ I * JR ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor mul_le_left := by
  apply Quotient.ringHom_ext; ext; rfl

Compatibility of Second Projection with Chinese Remainder Theorem Isomorphism

Informal description

Let $R$ be a commutative ring and $I, J$ be coprime ideals of $R$. The composition of the second projection homomorphism $(R/I) \times (R/J) \to R/J$ with the Chinese Remainder Theorem isomorphism $R/(I \cdot J) \simeq (R/I) \times (R/J)$ equals the canonical quotient map $R/(I \cdot J) \to R/J$ induced by the inclusion $I \cdot J \subseteq J$.

Ideal.Quotient.algebra instance

{I : Ideal A} [I.IsTwoSided] : Algebra R₁ (A ⧸ I)

Full source

/-- The `R₁`-algebra structure on `A/I` for an `R₁`-algebra `A` -/
instance Quotient.algebra {I : Ideal A} [I.IsTwoSided] : Algebra R₁ (A ⧸ I) where
  algebraMap := (Ideal.Quotient.mk I).comp (algebraMap R₁ A)
  smul_def' := fun _ x =>
    Quotient.inductionOn' x fun _ =>
      ((Quotient.mk I).congr_arg <| Algebra.smul_def _ _).trans (RingHom.map_mul _ _ _)
  commutes' := by rintro r ⟨x⟩; exact congr_arg (⟦·⟧) (Algebra.commutes r x)

Algebra Structure on Quotient Rings

Informal description

For any commutative semiring $R₁$ and any $R₁$-algebra $A$ with a two-sided ideal $I$, the quotient ring $A ⧸ I$ inherits an $R₁$-algebra structure from $A$.

Ideal.instAlgebraQuotient instance

{A} [CommRing A] [Algebra R₁ A] (I : Ideal A) : Algebra R₁ (A ⧸ I)

Full source

instance {A} [CommRing A] [Algebra R₁ A] (I : Ideal A) : Algebra R₁ (A ⧸ I) := inferInstance

Algebra Structure on Quotient Rings by Ideals

Informal description

For any commutative ring $A$ with an algebra structure over a commutative semiring $R₁$, and any ideal $I$ of $A$, the quotient ring $A ⧸ I$ inherits an $R₁$-algebra structure from $A$.

Ideal.Quotient.isScalarTower instance

[SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A) : IsScalarTower R₁ R₂ (A ⧸ I)

Full source

instance Quotient.isScalarTower [SMul R₁ R₂] [IsScalarTower R₁ R₂ A] (I : Ideal A) :
    IsScalarTower R₁ R₂ (A ⧸ I) := inferInstance

Scalar Tower Structure on Quotient Algebras

Informal description

For any commutative ring $A$ with an algebra structure over $R₁$, and any ideal $I$ of $A$, if there is a scalar multiplication action of $R₁$ on $R₂$ and a scalar tower structure $R₁ \to R₂ \to A$, then the quotient algebra $A ⧸ I$ inherits a scalar tower structure from $R₁$ to $R₂$.

Ideal.Quotient.mkₐ definition

(I : Ideal A) [I.IsTwoSided] : A →ₐ[R₁] A ⧸ I

Full source

/-- The canonical morphism `A →ₐ[R₁] A ⧸ I` as morphism of `R₁`-algebras, for `I` an ideal of
`A`, where `A` is an `R₁`-algebra. -/
def Quotient.mkₐ (I : Ideal A) [I.IsTwoSided] : A →ₐ[R₁] A ⧸ I :=
  ⟨⟨⟨⟨fun a => Submodule.Quotient.mk a, rfl⟩, fun _ _ => rfl⟩, rfl, fun _ _ => rfl⟩, fun _ => rfl⟩

Canonical quotient algebra homomorphism

Informal description

The canonical algebra homomorphism from an $R₁$-algebra $A$ to its quotient $A ⧸ I$ by a two-sided ideal $I$, where the homomorphism maps each element $a \in A$ to its equivalence class $[a] \in A ⧸ I$. This homomorphism preserves both the ring and $R₁$-algebra structures.

Ideal.Quotient.algHom_ext theorem

 {I : Ideal A} [I.IsTwoSided] {S} [Semiring S] [Algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄
  (h : f.comp (Quotient.mkₐ R₁ I) = g.comp (Quotient.mkₐ R₁ I)) : f = g

Full source

theorem Quotient.algHom_ext {I : Ideal A} [I.IsTwoSided]
    {S} [Semiring S] [Algebra R₁ S] ⦃f g : A ⧸ IA ⧸ I →ₐ[R₁] S⦄
    (h : f.comp (Quotient.mkₐ R₁ I) = g.comp (Quotient.mkₐ R₁ I)) : f = g :=
  AlgHom.ext fun x => Quotient.inductionOn' x <| AlgHom.congr_fun h

Uniqueness of Algebra Homomorphisms from Quotient Algebras via Composition with Canonical Quotient Map

Informal description

Let $A$ be an $R₁$-algebra, $I$ a two-sided ideal of $A$, and $S$ a semiring with an $R₁$-algebra structure. For any two $R₁$-algebra homomorphisms $f, g: A ⧸ I \to S$, if their compositions with the canonical quotient homomorphism $\text{Quotient.mkₐ}\, R₁\, I$ are equal, then $f = g$.

Ideal.Quotient.alg_map_eq theorem

 {A} [CommRing A] [Algebra R₁ A] (I : Ideal A) : algebraMap R₁ (A ⧸ I) = (algebraMap A (A ⧸ I)).comp (algebraMap R₁ A)

Full source

theorem Quotient.alg_map_eq {A} [CommRing A] [Algebra R₁ A] (I : Ideal A) :
    algebraMap R₁ (A ⧸ I) = (algebraMap A (A ⧸ I)).comp (algebraMap R₁ A) :=
  rfl

Compatibility of Algebra Maps with Quotient Ring Construction

Informal description

For a commutative ring $A$ with an $R₁$-algebra structure and an ideal $I$ of $A$, the algebra map from $R₁$ to the quotient ring $A ⧸ I$ is equal to the composition of the algebra map from $A$ to $A ⧸ I$ with the algebra map from $R₁$ to $A$.

Ideal.Quotient.mkₐ_toRingHom theorem

(I : Ideal A) [I.IsTwoSided] : (Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I

Full source

theorem Quotient.mkₐ_toRingHom (I : Ideal A) [I.IsTwoSided] :
    (Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I :=
  rfl

Equality of Underlying Ring Homomorphisms in Quotient Algebra Construction

Informal description

For any commutative semiring $R₁$, any $R₁$-algebra $A$, and any two-sided ideal $I$ of $A$, the underlying ring homomorphism of the canonical quotient algebra homomorphism $\text{Quotient.mkₐ}_{R₁} I$ is equal to the canonical quotient ring homomorphism $\text{Quotient.mk} I$.

Ideal.Quotient.mkₐ_eq_mk theorem

(I : Ideal A) [I.IsTwoSided] : ⇑(Quotient.mkₐ R₁ I) = Quotient.mk I

Full source

@[simp]
theorem Quotient.mkₐ_eq_mk (I : Ideal A) [I.IsTwoSided] : ⇑(Quotient.mkₐ R₁ I) = Quotient.mk I :=
  rfl

Equality of Quotient Algebra and Ring Homomorphisms on Underlying Functions

Informal description

For any commutative semiring $R₁$, any $R₁$-algebra $A$, and any two-sided ideal $I$ of $A$, the underlying function of the canonical quotient algebra homomorphism $\text{Quotient.mkₐ} : A \to A ⧸ I$ coincides with the canonical quotient ring homomorphism $\text{Quotient.mk} : A \to A ⧸ I$.

Ideal.Quotient.algebraMap_eq theorem

{R} [CommRing R] (I : Ideal R) : algebraMap R (R ⧸ I) = Quotient.mk I

Full source

@[simp]
theorem Quotient.algebraMap_eq {R} [CommRing R] (I : Ideal R) :
    algebraMap R (R ⧸ I) = Quotient.mk I :=
  rfl

Equality of Algebra Map and Quotient Map in Quotient Ring Construction

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the algebra map from $R$ to the quotient ring $R ⧸ I$ coincides with the canonical quotient ring homomorphism $\text{Quotient.mk} : R \to R ⧸ I$. In other words, the following equality holds: \[ \text{algebraMap}_R (R ⧸ I) = \text{Quotient.mk } I \]

Ideal.Quotient.mk_comp_algebraMap theorem

(I : Ideal A) [I.IsTwoSided] : (Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I)

Full source

@[simp]
theorem Quotient.mk_comp_algebraMap (I : Ideal A) [I.IsTwoSided] :
    (Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I) :=
  rfl

Compatibility of Quotient Map with Algebra Map

Informal description

Let $R₁$ be a commutative semiring and $A$ an $R₁$-algebra with a two-sided ideal $I$. The composition of the quotient map $\text{Quotient.mk} : A \to A ⧸ I$ with the algebra map $\text{algebraMap} : R₁ \to A$ is equal to the algebra map $\text{algebraMap} : R₁ \to A ⧸ I$. In other words, the following diagram commutes: \[ R₁ \xrightarrow{\text{algebraMap}} A \xrightarrow{\text{Quotient.mk}} A ⧸ I = R₁ \xrightarrow{\text{algebraMap}} A ⧸ I \]

Ideal.Quotient.mk_algebraMap theorem

(I : Ideal A) [I.IsTwoSided] (x : R₁) : Quotient.mk I (algebraMap R₁ A x) = algebraMap R₁ (A ⧸ I) x

Full source

@[simp]
theorem Quotient.mk_algebraMap (I : Ideal A) [I.IsTwoSided] (x : R₁) :
    Quotient.mk I (algebraMap R₁ A x) = algebraMap R₁ (A ⧸ I) x :=
  rfl

Commutativity of Algebra Map with Quotient Map

Informal description

Let $R₁$ be a commutative semiring, $A$ an $R₁$-algebra, and $I$ a two-sided ideal of $A$. For any element $x \in R₁$, the image of $x$ under the algebra map $R₁ \to A$ followed by the quotient map $A \to A/I$ equals the image of $x$ under the algebra map $R₁ \to A/I$. In other words, the following diagram commutes: \[ \begin{CD} R₁ @>{\text{algebraMap}}>> A \\ @V{\text{algebraMap}}VV @VV{\text{Quotient.mk }I}V \\ A/I @= A/I \end{CD} \]

Ideal.Quotient.mkₐ_surjective theorem

(I : Ideal A) [I.IsTwoSided] : Function.Surjective (Quotient.mkₐ R₁ I)

Full source

/-- The canonical morphism `A →ₐ[R₁] I.quotient` is surjective. -/
theorem Quotient.mkₐ_surjective (I : Ideal A) [I.IsTwoSided] :
    Function.Surjective (Quotient.mkₐ R₁ I) :=
  Quot.mk_surjective

Surjectivity of the Canonical Quotient Algebra Homomorphism

Informal description

For any commutative semiring $R₁$, any $R₁$-algebra $A$, and any two-sided ideal $I$ of $A$, the canonical algebra homomorphism $\pi : A \to A/I$ is surjective. That is, for every element $[a] \in A/I$, there exists an element $a' \in A$ such that $\pi(a') = [a]$.

Ideal.Quotient.mkₐ_ker theorem

(I : Ideal A) [I.IsTwoSided] : RingHom.ker (Quotient.mkₐ R₁ I : A →+* A ⧸ I) = I

Full source

/-- The kernel of `A →ₐ[R₁] I.quotient` is `I`. -/
@[simp]
theorem Quotient.mkₐ_ker (I : Ideal A) [I.IsTwoSided] :
    RingHom.ker (Quotient.mkₐ R₁ I : A →+* A ⧸ I) = I :=
  Ideal.mk_ker

Kernel of Quotient Algebra Homomorphism Equals Ideal

Informal description

For any commutative semiring $R₁$, any $R₁$-algebra $A$, and any two-sided ideal $I$ of $A$, the kernel of the canonical quotient algebra homomorphism $\pi : A \to A/I$ is equal to $I$. That is, $\ker(\pi) = I$.

Ideal.Quotient.mk_bijective_iff_eq_bot theorem

(I : Ideal A) [I.IsTwoSided] : Function.Bijective (mk I) ↔ I = ⊥

Full source

lemma Quotient.mk_bijective_iff_eq_bot (I : Ideal A) [I.IsTwoSided] :
    Function.BijectiveFunction.Bijective (mk I) ↔ I = ⊥ := by
  constructor
  · intro h
    rw [← map_eq_bot_iff_of_injective h.1]
    exact (map_eq_bot_iff_le_ker _).mpr <| le_of_eq mk_ker.symm
  · exact fun h => ⟨(injective_iff_ker_eq_bot _).mpr <| by rw [mk_ker, h], mk_surjective⟩

Bijectivity of Quotient Map iff Ideal is Zero

Informal description

For a two-sided ideal $I$ of a ring $A$, the quotient map $\pi : A \to A/I$ is bijective if and only if $I$ is the zero ideal (i.e., $I = \bot$).

Ideal.Quotient.liftₐ definition

(I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) : A ⧸ I →ₐ[R₁] B

Full source

/-- `Ideal.quotient.lift` as an `AlgHom`. -/
def Quotient.liftₐ (I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) :
    A ⧸ IA ⧸ I →ₐ[R₁] B :=
  {-- this is IsScalarTower.algebraMap_apply R₁ A (A ⧸ I) but the file `Algebra.Algebra.Tower`
      -- imports this file.
      Ideal.Quotient.lift
      I (f : A →+* B) hI with
    commutes' := fun r => by
      have : algebraMap R₁ (A ⧸ I) r = Ideal.Quotient.mk I (algebraMap R₁ A r) := rfl
      rw [this, RingHom.toFun_eq_coe, Ideal.Quotient.lift_mk,
        AlgHom.coe_toRingHom, Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one,
        map_smul, map_one] }

Lifting of algebra homomorphism through quotient by ideal

Informal description

Given a commutative semiring $R₁$, an $R₁$-algebra $A$ with a two-sided ideal $I$, and an $R₁$-algebra homomorphism $f \colon A \to B$ that vanishes on $I$, there exists a unique $R₁$-algebra homomorphism from the quotient algebra $A/I$ to $B$ that lifts $f$. More precisely, for any $a \in A$, the homomorphism maps the equivalence class $[a] \in A/I$ to $f(a) \in B$.

Ideal.Quotient.liftₐ_apply theorem

 (I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) (x) :
  Ideal.Quotient.liftₐ I f hI x = Ideal.Quotient.lift I (f : A →+* B) hI x

Full source

@[simp]
theorem Quotient.liftₐ_apply (I : Ideal A) [I.IsTwoSided]
    (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) (x) :
    Ideal.Quotient.liftₐ I f hI x = Ideal.Quotient.lift I (f : A →+* B) hI x :=
  rfl

Equality of Lifted Algebra and Ring Homomorphisms on Quotient Elements

Informal description

Let $R₁$ be a commutative semiring, $A$ an $R₁$-algebra with a two-sided ideal $I$, and $f \colon A \to B$ an $R₁$-algebra homomorphism such that $f(a) = 0$ for all $a \in I$. For any $x \in A$, the lifted algebra homomorphism $\text{lift}_ₐ(I, f, hI)$ applied to the equivalence class $[x] \in A/I$ equals the lifted ring homomorphism $\text{lift}(I, f, hI)$ applied to $[x]$.

Ideal.Quotient.liftₐ_comp theorem

 (I : Ideal A) [I.IsTwoSided] (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) :
  (Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f

Full source

theorem Quotient.liftₐ_comp (I : Ideal A) [I.IsTwoSided]
    (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) :
    (Ideal.Quotient.liftₐ I f hI).comp (Ideal.Quotient.mkₐ R₁ I) = f :=
  AlgHom.ext fun _ => (Ideal.Quotient.lift_mk I (f : A →+* B) hI :)

Composition of Lifted Algebra Homomorphism with Quotient Map Equals Original Homomorphism

Informal description

Let $R₁$ be a commutative semiring, $A$ an $R₁$-algebra with a two-sided ideal $I$, and $f \colon A \to B$ an $R₁$-algebra homomorphism such that $f(a) = 0$ for all $a \in I$. Then the composition of the lifted homomorphism $\text{lift}_ₐ(I, f, hI) \colon A/I \to B$ with the canonical quotient homomorphism $\text{mk}_ₐ(R₁, I) \colon A \to A/I$ equals $f$. In symbols: $$ \text{lift}_ₐ(I, f, hI) \circ \text{mk}_ₐ(R₁, I) = f $$

Ideal.KerLift.map_smul theorem

(f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ (RingHom.ker f)) : f.kerLift (r • x) = r • f.kerLift x

Full source

theorem KerLift.map_smul (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ (RingHom.ker f)) :
    f.kerLift (r • x) = r • f.kerLift x := by
  obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x
  exact _root_.map_smul f _ _

Equivariance of Induced Homomorphism on Quotient Algebra

Informal description

Let $R₁$ be a commutative semiring, $A$ and $B$ be $R₁$-algebras, and $f \colon A \to B$ be an $R₁$-algebra homomorphism. For any scalar $r \in R₁$ and any element $x \in A/\ker f$, the induced homomorphism $\ker f \colon A/\ker f \to B$ satisfies: \[ f_{\text{kerLift}}(r \cdot x) = r \cdot f_{\text{kerLift}}(x) \]

Ideal.kerLiftAlg definition

(f : A →ₐ[R₁] B) : A ⧸ (RingHom.ker f) →ₐ[R₁] B

Full source

/-- The induced algebras morphism from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotientKerAlgEquivOfRightInverse`) /
is surjective (`quotientKerAlgEquivOfSurjective`).
-/
def kerLiftAlg (f : A →ₐ[R₁] B) : A ⧸ (RingHom.ker f)A ⧸ (RingHom.ker f) →ₐ[R₁] B :=
  AlgHom.mk' (RingHom.kerLift (f : A →+* B)) fun _ _ => KerLift.map_smul f _ _

Induced algebra homomorphism from quotient by kernel

Informal description

Given a commutative semiring $ R_1 $ and $ R_1 $-algebras $ A $ and $ B $, for any $ R_1 $-algebra homomorphism $ f \colon A \to B $, the induced algebra homomorphism $ \ker f \colon A / \ker f \to B $ is defined by mapping each equivalence class $[a] \in A / \ker f$ to $ f(a) \in B $. This map is well-defined and preserves the algebra structure.

Ideal.kerLiftAlg_mk theorem

(f : A →ₐ[R₁] B) (a : A) : kerLiftAlg f (Quotient.mk (RingHom.ker f) a) = f a

Full source

@[simp]
theorem kerLiftAlg_mk (f : A →ₐ[R₁] B) (a : A) :
    kerLiftAlg f (Quotient.mk (RingHom.ker f) a) = f a := by
  rfl

Evaluation of Induced Algebra Homomorphism on Quotient Class

Informal description

Let $R_1$ be a commutative semiring, and let $A$ and $B$ be $R_1$-algebras. Given an $R_1$-algebra homomorphism $f \colon A \to B$, the induced algebra homomorphism $\ker f \colon A / \ker f \to B$ satisfies \[ \ker f([a]) = f(a) \] for any $a \in A$, where $[a]$ denotes the equivalence class of $a$ in the quotient algebra $A / \ker f$.

Ideal.kerLiftAlg_toRingHom theorem

(f : A →ₐ[R₁] B) : (kerLiftAlg f : A ⧸ ker f →+* B) = RingHom.kerLift (f : A →+* B)

Full source

@[simp]
theorem kerLiftAlg_toRingHom (f : A →ₐ[R₁] B) :
    (kerLiftAlg f : A ⧸ ker fA ⧸ ker f →+* B) = RingHom.kerLift (f : A →+* B) :=
  rfl

Compatibility of algebra and ring homomorphism lifts through quotient by kernel

Informal description

For any commutative semiring $R₁$ and $R₁$-algebra homomorphism $f \colon A \to B$, the induced ring homomorphism from the quotient algebra $A / \ker f$ to $B$ coincides with the ring homomorphism induced by $f$ when viewed as a ring homomorphism. That is, the following diagram commutes: $$(A / \ker f) \to B = \text{RingHom.kerLift} (f \colon A \to B)$$

Ideal.kerLiftAlg_injective theorem

(f : A →ₐ[R₁] B) : Function.Injective (kerLiftAlg f)

Full source

/-- The induced algebra morphism from the quotient by the kernel is injective. -/
theorem kerLiftAlg_injective (f : A →ₐ[R₁] B) : Function.Injective (kerLiftAlg f) :=
  RingHom.kerLift_injective (R := A) (S := B) f

Injectivity of the Induced Algebra Homomorphism from Quotient by Kernel

Informal description

For any commutative semiring $R_1$ and $R_1$-algebra homomorphism $f \colon A \to B$, the induced algebra homomorphism $\ker f \colon A / \ker f \to B$ is injective.

Ideal.quotientKerAlgEquivOfRightInverse definition

{f : A →ₐ[R₁] B} {g : B → A} (hf : Function.RightInverse g f) : (A ⧸ RingHom.ker f) ≃ₐ[R₁] B

Full source

/-- The **first isomorphism** theorem for algebras, computable version. -/
@[simps!]
def quotientKerAlgEquivOfRightInverse {f : A →ₐ[R₁] B} {g : B → A}
    (hf : Function.RightInverse g f) : (A ⧸ RingHom.ker f) ≃ₐ[R₁] B :=
  { RingHom.quotientKerEquivOfRightInverse hf,
    kerLiftAlg f with }

First Isomorphism Theorem for Algebras with Right Inverse

Informal description

Given a commutative semiring $ R_1 $ and $ R_1 $-algebras $ A $ and $ B $, for any $ R_1 $-algebra homomorphism $ f \colon A \to B $ with a right inverse $ g \colon B \to A $ (i.e., $ f \circ g = \text{id}_B $), the quotient algebra $ A / \ker f $ is isomorphic to $ B $ as $ R_1 $-algebras. The isomorphism is given by the induced homomorphism $ \ker f \colon A / \ker f \to B $ and its inverse $ [g] \colon B \to A / \ker f $, where $ [g] $ maps $ y \in B $ to the equivalence class of $ g(y) $ in $ A / \ker f $.

Ideal.quotientKerAlgEquivOfSurjective definition

{f : A →ₐ[R₁] B} (hf : Function.Surjective f) : (A ⧸ (RingHom.ker f)) ≃ₐ[R₁] B

Full source

/-- The **first isomorphism theorem** for algebras. -/
@[simps!]
noncomputable def quotientKerAlgEquivOfSurjective {f : A →ₐ[R₁] B} (hf : Function.Surjective f) :
    (A ⧸ (RingHom.ker f)) ≃ₐ[R₁] B :=
  quotientKerAlgEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)

First Isomorphism Theorem for Algebras (Surjective Case)

Informal description

Given a commutative semiring $ R_1 $ and $ R_1 $-algebras $ A $ and $ B $, for any surjective $ R_1 $-algebra homomorphism $ f \colon A \to B $, the quotient algebra $ A / \ker f $ is isomorphic to $ B $ as $ R_1 $-algebras. The isomorphism is given by the induced homomorphism $ \ker f \colon A / \ker f \to B $ and its inverse $ [g] \colon B \to A / \ker f $, where $ g $ is any right inverse of $ f $.

Ideal.quotientMap definition

 {I : Ideal R} (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R →+* S) (hIJ : I ≤ J.comap f) : R ⧸ I →+* S ⧸ J

Full source

/-- The ring hom `R/I →+* S/J` induced by a ring hom `f : R →+* S` with `I ≤ f⁻¹(J)` -/
def quotientMap {I : Ideal R} (J : Ideal S) [I.IsTwoSided] [J.IsTwoSided] (f : R →+* S)
    (hIJ : I ≤ J.comap f) : R ⧸ IR ⧸ I →+* S ⧸ J :=
  Quotient.lift I ((Quotient.mk J).comp f) fun _ ha => by
    simpa [Function.comp_apply, RingHom.coe_comp, Quotient.eq_zero_iff_mem] using hIJ ha

Induced ring homomorphism on quotient rings

Informal description

Given a ring homomorphism $ f \colon R \to S $ and ideals $ I $ of $ R $ and $ J $ of $ S $ such that $ I $ is contained in the preimage of $ J $ under $ f $, there exists an induced ring homomorphism from the quotient ring $ R/I $ to $ S/J $. This homomorphism maps the equivalence class of an element $ x \in R $ in $ R/I $ to the equivalence class of $ f(x) $ in $ S/J $.

Ideal.quotientMap_mk theorem

 {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S} {H : J ≤ I.comap f} {x : R} :
  quotientMap I f H (Quotient.mk J x) = Quotient.mk I (f x)

Full source

@[simp]
theorem quotientMap_mk {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} {H : J ≤ I.comap f} {x : R} :
    quotientMap I f H (Quotient.mk J x) = Quotient.mk I (f x) :=
  Quotient.lift_mk J _ _

Quotient Map Evaluates to Image of Class Representative

Informal description

Let $R$ and $S$ be commutative rings with two-sided ideals $J \subseteq R$ and $I \subseteq S$, and let $f \colon R \to S$ be a ring homomorphism such that $J$ is contained in the preimage of $I$ under $f$. Then, for any $x \in R$, the induced quotient map $\text{quotientMap}(I, f, H)$ sends the equivalence class of $x$ in $R/J$ to the equivalence class of $f(x)$ in $S/I$.

Ideal.quotientMap_algebraMap theorem

 {J : Ideal A} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : A →+* S} {H : J ≤ I.comap f} {x : R₁} :
  quotientMap I f H (algebraMap R₁ (A ⧸ J) x) = Quotient.mk I (f (algebraMap _ _ x))

Full source

@[simp]
theorem quotientMap_algebraMap {J : Ideal A} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : A →+* S} {H : J ≤ I.comap f}
    {x : R₁} : quotientMap I f H (algebraMap R₁ (A ⧸ J) x) = Quotient.mk I (f (algebraMap _ _ x)) :=
  Quotient.lift_mk J _ _

Compatibility of Quotient Map with Algebra Structure

Informal description

Let $R₁$ be a commutative semiring, $A$ an $R₁$-algebra, and $S$ a ring. Given two-sided ideals $J$ of $A$ and $I$ of $S$, and a ring homomorphism $f \colon A \to S$ such that $J$ is contained in the preimage of $I$ under $f$, then for any $x \in R₁$, the induced quotient map $\text{quotientMap}(I, f, H)$ satisfies \[ \text{quotientMap}(I, f, H)(\text{algebraMap}_{R₁}(A/J)(x)) = [f(\text{algebraMap}_{R₁} A(x))]_I, \] where $[\cdot]_I$ denotes the equivalence class in $S/I$ and $\text{algebraMap}_{R₁}$ denotes the algebra structure map.

Ideal.quotientMap_comp_mk theorem

 {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S} (H : J ≤ I.comap f) :
  (quotientMap I f H).comp (Quotient.mk J) = (Quotient.mk I).comp f

Full source

theorem quotientMap_comp_mk {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} (H : J ≤ I.comap f) :
    (quotientMap I f H).comp (Quotient.mk J) = (Quotient.mk I).comp f :=
  RingHom.ext fun x => by simp only [Function.comp_apply, RingHom.coe_comp, Ideal.quotientMap_mk]

Commutativity of Quotient Map with Canonical Projections

Informal description

Let $R$ and $S$ be commutative rings with ideals $J \subseteq R$ and $I \subseteq S$ respectively. Given a ring homomorphism $f \colon R \to S$ such that $J$ is contained in the preimage of $I$ under $f$, the composition of the induced quotient map $\text{quotientMap}_I f H \colon R/J \to S/I$ with the canonical projection $\text{Quotient.mk}_J \colon R \to R/J$ is equal to the composition of the canonical projection $\text{Quotient.mk}_I \colon S \to S/I$ with $f$. That is, the following diagram commutes: \[ \begin{CD} R @>{f}>> S \\ @V{\text{Quotient.mk}_J}VV @VV{\text{Quotient.mk}_I}V \\ R/J @>{\text{quotientMap}_I f H}>> S/I \end{CD} \]

Ideal.ker_quotientMap_mk theorem

 {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] :
  RingHom.ker (quotientMap (J.map _) (Quotient.mk I) le_comap_map) = I.map (Quotient.mk J)

Full source

lemma ker_quotientMap_mk {I J : Ideal R} [I.IsTwoSided] [J.IsTwoSided] :
    RingHom.ker (quotientMap (J.map _) (Quotient.mk I) le_comap_map) = I.map (Quotient.mk J) := by
  rw [Ideal.quotientMap, Ideal.ker_quotient_lift, ← RingHom.comap_ker, Ideal.mk_ker,
    Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker, Ideal.map_sup, Ideal.map_quotient_self, bot_sup_eq]

Kernel of Quotient Map Composition Equals Image of Ideal Under Quotient

Informal description

Let $R$ be a commutative ring with two-sided ideals $I$ and $J$. The kernel of the quotient map $\text{quotientMap}(J, \pi_I, \text{le\_comap\_map})$ (where $\pi_I : R \to R/I$ is the canonical projection) is equal to the image of $I$ under the quotient map $\pi_J : R \to R/J$. That is, \[ \ker(\text{quotientMap}(J, \pi_I, \text{le\_comap\_map})) = \pi_J(I). \]

Ideal.quotientEquiv definition

: R ⧸ I ≃+* S ⧸ J

Full source

/-- The ring equiv `R/I ≃+* S/J` induced by a ring equiv `f : R ≃+* S`, where `J = f(I)`. -/
@[simps]
def quotientEquiv : R ⧸ IR ⧸ I ≃+* S ⧸ J where
  __ := quotientMap J f (hIJ ▸ le_comap_map)
  invFun := quotientMap I f.symm (hIJ ▸ (map_comap_of_equiv f).le)
  left_inv := by
    rintro ⟨r⟩
    simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe,
      quotientMap_mk, RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]
  right_inv := by
    rintro ⟨s⟩
    simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe,
      quotientMap_mk, RingEquiv.coe_toRingHom, RingEquiv.apply_symm_apply]

Ring isomorphism between quotient rings induced by a ring isomorphism

Informal description

Given a ring isomorphism $ f \colon R \simeq+* S $ and ideals $ I $ of $ R $ and $ J $ of $ S $ such that $ J = f(I) $, there is a ring isomorphism $ R/I \simeq+* S/J $ induced by $ f $. This isomorphism maps the equivalence class of an element $ x \in R $ in $ R/I $ to the equivalence class of $ f(x) $ in $ S/J $, and its inverse maps the equivalence class of $ y \in S $ in $ S/J $ to the equivalence class of $ f^{-1}(y) $ in $ R/I $.

Ideal.quotientEquiv_mk theorem

(x : R) : quotientEquiv I J f hIJ (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J (f x)

Full source

theorem quotientEquiv_mk (x : R) :
    quotientEquiv I J f hIJ (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J (f x) :=
  rfl

Commutativity of quotient equivalence with class representatives

Informal description

Let $R$ and $S$ be commutative rings, $I$ an ideal of $R$, $J$ an ideal of $S$, and $f : R \simeq+* S$ a ring isomorphism such that $J = f(I)$. For any $x \in R$, the image of the equivalence class $[x]_I$ under the induced isomorphism $R/I \simeq+* S/J$ is equal to the equivalence class $[f(x)]_J$.

Ideal.quotientEquiv_symm_mk theorem

(x : S) : (quotientEquiv I J f hIJ).symm (Ideal.Quotient.mk J x) = Ideal.Quotient.mk I (f.symm x)

Full source

@[simp]
theorem quotientEquiv_symm_mk (x : S) :
    (quotientEquiv I J f hIJ).symm (Ideal.Quotient.mk J x) = Ideal.Quotient.mk I (f.symm x) :=
  rfl

Inverse of Quotient Ring Isomorphism Maps Equivalence Classes via Inverse Isomorphism

Informal description

For any ring isomorphism $f \colon R \simeq+* S$ and ideals $I$ of $R$ and $J$ of $S$ such that $J = f(I)$, the inverse of the induced ring isomorphism $R/I \simeq+* S/J$ maps the equivalence class of any element $x \in S$ in $S/J$ to the equivalence class of $f^{-1}(x)$ in $R/I$.

Ideal.quotientMap_injective' theorem

 {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S} {H : J ≤ I.comap f} (h : I.comap f ≤ J) :
  Function.Injective (quotientMap I f H)

Full source

/-- `H` and `h` are kept as separate hypothesis since H is used in constructing the quotient map. -/
theorem quotientMap_injective' {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} {H : J ≤ I.comap f} (h : I.comap f ≤ J) :
    Function.Injective (quotientMap I f H) := by
  refine (injective_iff_map_eq_zero (quotientMap I f H)).2 fun a ha => ?_
  obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
  rw [quotientMap_mk, Quotient.eq_zero_iff_mem] at ha
  exact Quotient.eq_zero_iff_mem.mpr (h ha)

Injectivity Criterion for Induced Quotient Map

Informal description

Let $R$ and $S$ be commutative rings with two-sided ideals $J \subseteq R$ and $I \subseteq S$, and let $f \colon R \to S$ be a ring homomorphism such that $J \subseteq f^{-1}(I)$. If the preimage of $I$ under $f$ is contained in $J$ (i.e., $f^{-1}(I) \subseteq J$), then the induced quotient map $\overline{f} \colon R/J \to S/I$ is injective.

Ideal.quotientMap_injective theorem

{I : Ideal S} {f : R →+* S} [I.IsTwoSided] : Function.Injective (quotientMap I f le_rfl)

Full source

/-- If we take `J = I.comap f` then `quotientMap` is injective automatically. -/
theorem quotientMap_injective {I : Ideal S} {f : R →+* S} [I.IsTwoSided] :
    Function.Injective (quotientMap I f le_rfl) :=
  quotientMap_injective' le_rfl

Injectivity of Induced Quotient Map via Preimage Condition

Informal description

Let $R$ and $S$ be commutative rings, $I$ be a two-sided ideal of $S$, and $f \colon R \to S$ be a ring homomorphism. Then the induced quotient map $\overline{f} \colon R/f^{-1}(I) \to S/I$ is injective.

Ideal.quotientMap_surjective theorem

 {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided] {f : R →+* S} {H : J ≤ I.comap f}
  (hf : Function.Surjective f) : Function.Surjective (quotientMap I f H)

Full source

theorem quotientMap_surjective {J : Ideal R} {I : Ideal S} [I.IsTwoSided] [J.IsTwoSided]
    {f : R →+* S} {H : J ≤ I.comap f}
    (hf : Function.Surjective f) : Function.Surjective (quotientMap I f H) := fun x =>
  let ⟨x, hx⟩ := Quotient.mk_surjective x
  let ⟨y, hy⟩ := hf x
  ⟨(Quotient.mk J) y, by simp [hx, hy]⟩

Surjectivity of Induced Quotient Map via Surjective Ring Homomorphism

Informal description

Let $R$ and $S$ be commutative rings, $I$ be a two-sided ideal of $S$, $J$ be a two-sided ideal of $R$, and $f \colon R \to S$ be a surjective ring homomorphism such that $J \subseteq f^{-1}(I)$. Then the induced quotient map $\overline{f} \colon R/J \to S/I$ is surjective.

Ideal.comp_quotientMap_eq_of_comp_eq theorem

 {R' S' : Type*} [Ring R'] [Ring S'] {f : R →+* S} {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'}
  (hfg : f'.comp g = g'.comp f) (I : Ideal S') [I.IsTwoSided] :
  -- Porting note: was losing track of Ilet leq :=
    le_of_eq (_root_.trans (comap_comap (I := I) f g') (hfg ▸ comap_comap (I := I) g f'))
  (quotientMap I g' le_rfl).comp (quotientMap (I.comap g') f le_rfl) =
    (quotientMap I f' le_rfl).comp (quotientMap (I.comap f') g leq)

Full source

/-- Commutativity of a square is preserved when taking quotients by an ideal. -/
theorem comp_quotientMap_eq_of_comp_eq {R' S' : Type*} [Ring R'] [Ring S'] {f : R →+* S}
    {f' : R' →+* S'} {g : R →+* R'} {g' : S →+* S'} (hfg : f'.comp g = g'.comp f)
    (I : Ideal S') [I.IsTwoSided] :
    -- Porting note: was losing track of I
    let leq := le_of_eq (_root_.trans (comap_comap (I := I) f g') (hfg ▸ comap_comap (I := I) g f'))
    (quotientMap I g' le_rfl).comp (quotientMap (I.comap g') f le_rfl) =
    (quotientMap I f' le_rfl).comp (quotientMap (I.comap f') g leq) := by
  refine RingHom.ext fun a => ?_
  obtain ⟨r, rfl⟩ := Quotient.mk_surjective a
  simp only [RingHom.comp_apply, quotientMap_mk]
  exact (Ideal.Quotient.mk I).congr_arg (_root_.trans (g'.comp_apply f r).symm
    (hfg ▸ f'.comp_apply g r))

Commutativity of Quotient Maps in a Square of Ring Homomorphisms

Informal description

Let $R, S, R', S'$ be rings with ring homomorphisms $f \colon R \to S$, $f' \colon R' \to S'$, $g \colon R \to R'$, and $g' \colon S \to S'$ such that $f' \circ g = g' \circ f$. Let $I$ be a two-sided ideal of $S'$. Then the following diagram commutes: \[ \begin{CD} R/I.g' @>{f}>> S/I \\ @V{g}VV @VV{g'}V \\ R'/I.f' @>{f'}>> S'/I \end{CD} \] where $I.g'$ denotes the ideal $(g')^{-1}(I)$ and $I.f'$ denotes $(f')^{-1}(I)$. Specifically, the composition of the quotient maps satisfies: \[ (\text{quotientMap } I \ g' \ \text{le\_rfl}) \circ (\text{quotientMap } (I.g') \ f \ \text{le\_rfl}) = (\text{quotientMap } I \ f' \ \text{le\_rfl}) \circ (\text{quotientMap } (I.f') \ g \ \text{leq}) \]

Ideal.quotientMapₐ definition

(f : A →ₐ[R₁] B) (hIJ : I ≤ J.comap f) : A ⧸ I →ₐ[R₁] B ⧸ J

Full source

/-- The algebra hom `A/I →+* B/J` induced by an algebra hom `f : A →ₐ[R₁] B` with `I ≤ f⁻¹(J)`. -/
def quotientMapₐ (f : A →ₐ[R₁] B) (hIJ : I ≤ J.comap f) :
    A ⧸ IA ⧸ I →ₐ[R₁] B ⧸ J :=
  { quotientMap J (f : A →+* B) hIJ with commutes' := fun r => by simp only [RingHom.toFun_eq_coe,
    quotientMap_algebraMap, AlgHom.coe_toRingHom, AlgHom.commutes, Quotient.mk_algebraMap] }

Induced algebra homomorphism on quotient algebras

Informal description

Given an algebra homomorphism $ f \colon A \to B $ over a commutative semiring $ R_1 $, and ideals $ I $ of $ A $ and $ J $ of $ B $ such that $ I $ is contained in the preimage of $ J $ under $ f $, there exists an induced algebra homomorphism from the quotient algebra $ A/I $ to $ B/J $. This homomorphism maps the equivalence class of an element $ x \in A $ in $ A/I $ to the equivalence class of $ f(x) $ in $ B/J $.

Ideal.quotient_map_mkₐ theorem

 (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) {x : A} : quotientMapₐ J f H (Quotient.mk I x) = Quotient.mkₐ R₁ J (f x)

Full source

@[simp]
theorem quotient_map_mkₐ (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) {x : A} :
    quotientMapₐ J f H (Quotient.mk I x) = Quotient.mkₐ R₁ J (f x) :=
  rfl

Commutativity of Quotient Algebra Maps: $\text{quotientMap}_J f H([x]_I) = [f(x)]_J$

Informal description

Let $A$ and $B$ be $R_1$-algebras, $I$ an ideal of $A$, $J$ an ideal of $B$, and $f \colon A \to B$ an algebra homomorphism such that $I \subseteq f^{-1}(J)$. Then for any $x \in A$, the induced quotient map $\text{quotientMap}_J f H$ sends the equivalence class $[x]_I$ in $A/I$ to the equivalence class $[f(x)]_J$ in $B/J$. In other words, the following diagram commutes: \[ \begin{CD} A @>{f}>> B \\ @V{\text{Quotient.mk}_I}VV @VV{\text{Quotient.mk}_J}V \\ A/I @>{\text{quotientMap}_J f H}>> B/J \end{CD} \]

Ideal.quotient_map_comp_mkₐ theorem

 (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) : (quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I) = (Quotient.mkₐ R₁ J).comp f

Full source

theorem quotient_map_comp_mkₐ (f : A →ₐ[R₁] B) (H : I ≤ J.comap f) :
    (quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I) = (Quotient.mkₐ R₁ J).comp f :=
  AlgHom.ext fun x => by simp only [quotient_map_mkₐ, Quotient.mkₐ_eq_mk, AlgHom.comp_apply]

Commutativity of Quotient Algebra Homomorphism Diagram

Informal description

Given an algebra homomorphism $ f \colon A \to B $ over a commutative semiring $ R_1 $, and ideals $ I $ of $ A $ and $ J $ of $ B $ such that $ I \subseteq f^{-1}(J) $, the composition of the induced quotient algebra homomorphism $ A/I \to B/J $ with the canonical quotient map $ A \to A/I $ is equal to the composition of the canonical quotient map $ B \to B/J $ with $ f $. In other words, the following diagram commutes: \[ \begin{CD} A @>{f}>> B \\ @V{\text{Quotient.mk}_I}VV @VV{\text{Quotient.mk}_J}V \\ A/I @>{\text{quotientMap}_J\, f\, H}>> B/J \end{CD} \]

Ideal.quotientEquivAlg definition

(f : A ≃ₐ[R₁] B) (hIJ : J = I.map (f : A →+* B)) : (A ⧸ I) ≃ₐ[R₁] B ⧸ J

Full source

/-- The algebra equiv `A/I ≃ₐ[R] B/J` induced by an algebra equiv `f : A ≃ₐ[R] B`,
where`J = f(I)`. -/
def quotientEquivAlg (f : A ≃ₐ[R₁] B) (hIJ : J = I.map (f : A →+* B)) :
    (A ⧸ I) ≃ₐ[R₁] B ⧸ J :=
  { quotientEquiv I J (f : A ≃+* B) hIJ with
    commutes' := fun r => by
      -- Porting note: Needed to add the below lemma because Equivs coerce weird
      have : ∀ (e : RingEquiv (A ⧸ I) (B ⧸ J)), Equiv.toFun e.toEquiv = DFunLike.coe e :=
        fun _ ↦ rfl
      rw [this]
      simp only [quotientEquiv_apply, RingHom.toFun_eq_coe, quotientMap_algebraMap,
      RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, Quotient.mk_algebraMap]}

Algebra equivalence of quotient rings induced by an algebra equivalence

Informal description

Given an algebra equivalence $ f \colon A \simeq_{\text{Alg}[R₁]} B $ between $ R₁ $-algebras $ A $ and $ B $, and ideals $ I $ of $ A $ and $ J $ of $ B $ such that $ J = f(I) $, there is an induced algebra equivalence $ A/I \simeq_{\text{Alg}[R₁]} B/J $. This equivalence maps the equivalence class of an element $ x \in A $ in $ A/I $ to the equivalence class of $ f(x) $ in $ B/J $, and it preserves the algebra structure over $ R₁ $.

Ideal.Quotient.algebraQuotientOfLEComap abbrev

 {R} [CommRing R] [Algebra R A] {p : Ideal R} {P : Ideal A} [P.IsTwoSided] (h : p ≤ comap (algebraMap R A) P) :
  Algebra (R ⧸ p) (A ⧸ P)

Full source

/-- If `P` lies over `p`, then `R / p` has a canonical map to `A / P`. -/
abbrev Quotient.algebraQuotientOfLEComap {R} [CommRing R] [Algebra R A] {p : Ideal R}
    {P : Ideal A} [P.IsTwoSided] (h : p ≤ comap (algebraMap R A) P) :
    Algebra (R ⧸ p) (A ⧸ P) where
  algebraMap := quotientMap P (algebraMap R A) h
  smul := Quotient.lift₂ (⟦· • ·⟧) fun r₁ a₁ r₂ a₂ hr ha ↦ Quotient.sound <| by
    have := h (p.quotientRel_def.mp hr)
    rw [mem_comap, map_sub] at this
    simpa only [Algebra.smul_def] using P.quotientRel_def.mpr
      (P.mul_sub_mul_mem this <| P.quotientRel_def.mp ha)
  smul_def' := by rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.smul_def _ _)
  commutes' := by rintro ⟨_⟩ ⟨_⟩; exact congr_arg (⟦·⟧) (Algebra.commutes _ _)

Algebra Structure on Quotient Ring Induced by Preimage Condition

Informal description

Given a commutative ring $R$ with an algebra structure over $A$, and ideals $p$ of $R$ and $P$ of $A$ such that $p$ is contained in the preimage of $P$ under the algebra map $\text{algebraMap}\, R\, A$, there exists an algebra structure on the quotient ring $A / P$ over the quotient ring $R / p$.

Ideal.quotientAlgebra instance

{R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] : Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I)

Full source

instance (priority := 100) quotientAlgebra {R} [CommRing R] {I : Ideal A} [I.IsTwoSided]
    [Algebra R A] : Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) :=
  Quotient.algebraQuotientOfLEComap le_rfl

Algebra Structure on Quotient Ring Induced by Preimage Ideal

Informal description

For any commutative ring $R$ and algebra $A$ over $R$, given a two-sided ideal $I$ of $A$, the quotient ring $A / I$ inherits an algebra structure over the quotient ring $R / (I \cap R)$, where $I \cap R$ denotes the preimage of $I$ under the algebra map from $R$ to $A$.

Ideal.instAlgebraQuotientComapRingHomAlgebraMap instance

(R) {A} [CommRing R] [CommRing A] (I : Ideal A) [Algebra R A] : Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I)

Full source

instance (R) {A} [CommRing R] [CommRing A] (I : Ideal A) [Algebra R A] :
    Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) := inferInstance

Algebra Structure on Quotient Ring via Preimage Ideal

Informal description

For any commutative rings $R$ and $A$ with an algebra structure of $A$ over $R$, and any ideal $I$ of $A$, the quotient ring $A / I$ inherits an algebra structure over the quotient ring $R / (I \cap R)$, where $I \cap R$ is the preimage of $I$ under the algebra map from $R$ to $A$.

Ideal.algebraMap_quotient_injective theorem

 {R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] :
  Function.Injective (algebraMap (R ⧸ I.comap (algebraMap R A)) (A ⧸ I))

Full source

theorem algebraMap_quotient_injective {R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] :
    Function.Injective (algebraMap (R ⧸ I.comap (algebraMap R A)) (A ⧸ I)) := by
  rintro ⟨a⟩ ⟨b⟩ hab
  replace hab := Quotient.eq.mp hab
  rw [← RingHom.map_sub] at hab
  exact Quotient.eq.mpr hab

Injectivity of the Induced Algebra Map on Quotients

Informal description

Let $R$ be a commutative ring and $A$ an algebra over $R$ with a two-sided ideal $I$ of $A$. Then the algebra map from the quotient ring $R/(I \cap R)$ to the quotient algebra $A/I$ is injective, where $I \cap R$ denotes the preimage of $I$ under the algebra map from $R$ to $A$.

Ideal.quotientEquivAlgOfEq definition

{I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) : (A ⧸ I) ≃ₐ[R₁] A ⧸ J

Full source

/-- Quotienting by equal ideals gives equivalent algebras. -/
def quotientEquivAlgOfEq {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :
    (A ⧸ I) ≃ₐ[R₁] A ⧸ J :=
  quotientEquivAlg I J AlgEquiv.refl <| h ▸ (map_id I).symm

Algebra equivalence of quotient algebras by equal ideals

Informal description

Given two two-sided ideals $ I $ and $ J $ of an $ R_1 $-algebra $ A $ such that $ I = J $, there is an algebra equivalence between the quotient algebras $ A/I $ and $ A/J $. This equivalence maps the equivalence class of an element $ x \in A $ in $ A/I $ to the equivalence class of $ x $ in $ A/J $, and it preserves the algebra structure over $ R_1 $.

Ideal.quotientEquivAlgOfEq_mk theorem

 {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) (x : A) :
  quotientEquivAlgOfEq R₁ h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x

Full source

@[simp]
theorem quotientEquivAlgOfEq_mk {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) (x : A) :
    quotientEquivAlgOfEq R₁ h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
  rfl

Preservation of Equivalence Classes under Quotient Algebra Equivalence for Equal Ideals

Informal description

Let $A$ be an $R_1$-algebra with two-sided ideals $I$ and $J$ such that $I = J$. For any element $x \in A$, the equivalence class of $x$ in the quotient algebra $A/I$ is mapped by the algebra equivalence $\text{quotientEquivAlgOfEq}_{R_1}(h)$ to the equivalence class of $x$ in $A/J$. In other words, the algebra equivalence between $A/I$ and $A/J$ induced by $I = J$ preserves the equivalence classes of elements from $A$.

Ideal.quotientEquivAlgOfEq_symm theorem

 {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :
  (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ h.symm

Full source

@[simp]
theorem quotientEquivAlgOfEq_symm {I J : Ideal A} [I.IsTwoSided] [J.IsTwoSided] (h : I = J) :
    (quotientEquivAlgOfEq R₁ h).symm = quotientEquivAlgOfEq R₁ h.symm := by
  ext
  rfl

Symmetry of Algebra Equivalence for Quotient Algebras by Equal Ideals

Informal description

Given two two-sided ideals $I$ and $J$ of an $R_1$-algebra $A$ such that $I = J$, the inverse of the algebra equivalence between $A/I$ and $A/J$ is equal to the algebra equivalence between $A/J$ and $A/I$ induced by the equality $J = I$.

Ideal.comap_map_mk theorem

 {I J : Ideal R} [I.IsTwoSided] (h : I ≤ J) : Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J

Full source

lemma comap_map_mk {I J : Ideal R} [I.IsTwoSided] (h : I ≤ J) :
    Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J := by
  ext; rw [← Ideal.mem_quotient_iff_mem h, Ideal.mem_comap]

Preimage of Quotient Map Image Equals Original Ideal

Informal description

Let $R$ be a commutative ring with two-sided ideals $I$ and $J$ such that $I \subseteq J$. Then the preimage under the quotient map $\pi_I : R \to R/I$ of the image of $J$ under $\pi_I$ is equal to $J$ itself, i.e., \[ \pi_I^{-1}(\pi_I(J)) = J. \]

Ideal.quotientKerEquivRange definition

 {R A B : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) :
  (A ⧸ RingHom.ker f) ≃ₐ[R] f.range

Full source

/-- The **first isomorphism theorem** for commutative algebras (`AlgHom.range` version). -/
noncomputable def quotientKerEquivRange
    {R A B : Type*} [CommSemiring R] [Ring A] [Algebra R A] [Semiring B] [Algebra R B]
    (f : A →ₐ[R] B) :
    (A ⧸ RingHom.ker f) ≃ₐ[R] f.range :=
  (Ideal.quotientEquivAlgOfEq R (AlgHom.ker_rangeRestrict f).symm).trans <|
    Ideal.quotientKerAlgEquivOfSurjective f.rangeRestrict_surjective

First Isomorphism Theorem for Algebras (Range Version)

Informal description

Given a commutative semiring $ R $ and $ R $-algebras $ A $ (a ring) and $ B $ (a semiring), for any $ R $-algebra homomorphism $ f \colon A \to B $, the quotient algebra $ A / \ker f $ is isomorphic as an $ R $-algebra to the range of $ f $. This isomorphism is constructed by first identifying $ A / \ker f $ with $ A / \ker (f_{\text{range}}) $ (where $ f_{\text{range}} $ is the restriction of $ f $ to its range), and then using the surjectivity of $ f_{\text{range}} $ to establish the isomorphism with $ \text{range}(f) $.

RingEquiv.quotientBot definition

[Ring R] : R ⧸ (⊥ : Ideal R) ≃+* R

Full source

/-- The quotient of a ring by he zero ideal is isomorphic to the ring itself. -/
def RingEquiv.quotientBot [Ring R] : R ⧸ (⊥ : Ideal R)R ⧸ (⊥ : Ideal R) ≃+* R :=
  (Ideal.quotEquivOfEq (RingHom.ker_coe_equiv <| .refl _).symm).trans <|
    RingHom.quotientKerEquivOfRightInverse (f := .id R) (g := _root_.id) fun _ ↦ rfl

Isomorphism between a ring and its quotient by the zero ideal

Informal description

The quotient ring $ R / \{0\} $ is isomorphic to $ R $ as a ring. This isomorphism maps each equivalence class $[x]$ in $ R / \{0\} $ to the element $ x $ in $ R $.

RingEquiv.quotientBot_mk theorem

[Ring R] (r : R) : RingEquiv.quotientBot R (Ideal.Quotient.mk ⊥ r) = r

Full source

@[simp]
lemma RingEquiv.quotientBot_mk [Ring R] (r : R) :
    RingEquiv.quotientBot R (Ideal.Quotient.mk ⊥ r) = r :=
  rfl

Isomorphism maps equivalence class to element: $R / \{0\} \cong R$

Informal description

For any ring $R$ and any element $r \in R$, the image of the equivalence class $[r]$ under the isomorphism $R / \{0\} \cong R$ is equal to $r$ itself.

RingEquiv.quotientBot_symm_mk theorem

[Ring R] (r : R) : (RingEquiv.quotientBot R).symm r = r

Full source

@[simp]
lemma RingEquiv.quotientBot_symm_mk [Ring R] (r : R) :
    (RingEquiv.quotientBot R).symm r = r :=
  rfl

Inverse of Zero Ideal Quotient Isomorphism Acts as Identity

Informal description

For any ring $R$ and any element $r \in R$, the inverse of the isomorphism between $R$ and $R / \{0\}$ maps $r$ to itself, i.e., $(R / \{0\} \cong R)^{-1}(r) = r$.

AlgEquiv.quotientBot definition

[CommSemiring R] [Ring S] [Algebra R S] : (S ⧸ (⊥ : Ideal S)) ≃ₐ[R] S

Full source

/-- `RingEquiv.quotientBot` as an algebra isomorphism. -/
def AlgEquiv.quotientBot [CommSemiring R] [Ring S] [Algebra R S] :
    (S ⧸ (⊥ : Ideal S)) ≃ₐ[R] S where
  __ := RingEquiv.quotientBot S
  commutes' x := by simp [← Ideal.Quotient.mk_algebraMap]

Algebra isomorphism between a ring and its quotient by the zero ideal

Informal description

The quotient ring $ S / \{0\} $ is isomorphic to $ S $ as an $ R $-algebra. This isomorphism maps each equivalence class $[x]$ in $ S / \{0\} $ to the element $ x $ in $ S $, and it commutes with the algebra structure induced by $ R $.

AlgEquiv.quotientBot_mk theorem

[CommSemiring R] [CommRing S] [Algebra R S] (s : S) : AlgEquiv.quotientBot R S (Ideal.Quotient.mk ⊥ s) = s

Full source

@[simp]
lemma AlgEquiv.quotientBot_mk [CommSemiring R] [CommRing S] [Algebra R S] (s : S) :
    AlgEquiv.quotientBot R S (Ideal.Quotient.mk ⊥ s) = s :=
  rfl

Algebra Isomorphism Maps Quotient Class to Original Element

Informal description

For any commutative semiring $R$, any commutative ring $S$ with an $R$-algebra structure, and any element $s \in S$, the algebra isomorphism between $S / \{0\}$ and $S$ maps the equivalence class $[s]$ in $S / \{0\}$ to $s$ itself.

AlgEquiv.quotientBot_symm_mk theorem

[CommSemiring R] [CommRing S] [Algebra R S] (s : S) : (AlgEquiv.quotientBot R S).symm s = s

Full source

@[simp]
lemma AlgEquiv.quotientBot_symm_mk [CommSemiring R] [CommRing S] [Algebra R S]
    (s : S) : (AlgEquiv.quotientBot R S).symm s = s :=
  rfl

Inverse of Zero Ideal Quotient Isomorphism Acts as Identity

Informal description

For any commutative semiring $R$, commutative ring $S$ with an $R$-algebra structure, and element $s \in S$, the inverse of the algebra isomorphism between $S / \{0\}$ and $S$ maps $s$ to itself, i.e., $(\text{AlgEquiv.quotientBot } R S)^{-1}(s) = s$.

DoubleQuot.quotLeftToQuotSup definition

: R ⧸ I →+* R ⧸ I ⊔ J

Full source

/-- The obvious ring hom `R/I → R/(I ⊔ J)` -/
def quotLeftToQuotSup : R ⧸ IR ⧸ I →+* R ⧸ I ⊔ J :=
  Ideal.Quotient.factor le_sup_left

Canonical homomorphism from $ R/I $ to $ R/(I \sqcup J) $

Informal description

The canonical ring homomorphism from the quotient ring $ R/I $ to the quotient ring $ R/(I \sqcup J) $, where $ I \sqcup J $ denotes the supremum of the ideals $ I $ and $ J $ in the lattice of ideals of $ R $. This homomorphism is induced by the inclusion $ I \subseteq I \sqcup J $.

DoubleQuot.ker_quotLeftToQuotSup theorem

: RingHom.ker (quotLeftToQuotSup I J) = J.map (Ideal.Quotient.mk I)

Full source

/-- The kernel of `quotLeftToQuotSup` -/
theorem ker_quotLeftToQuotSup : RingHom.ker (quotLeftToQuotSup I J) =
    J.map (Ideal.Quotient.mk I) := by
  simp only [mk_ker, sup_idem, sup_comm, quotLeftToQuotSup, Quotient.factor, ker_quotient_lift,
    map_eq_iff_sup_ker_eq_of_surjective (Ideal.Quotient.mk I) Quotient.mk_surjective, ← sup_assoc]

Kernel of Canonical Quotient Homomorphism Equals Quotient of Ideal

Informal description

The kernel of the canonical homomorphism $\text{quotLeftToQuotSup} \colon R/I \to R/(I \sqcup J)$ is equal to the image of the ideal $J$ under the quotient map $\pi \colon R \to R/I$. In other words, $\ker(\text{quotLeftToQuotSup}) = \pi(J)$.

DoubleQuot.quotQuotToQuotSup definition

: (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) →+* R ⧸ I ⊔ J

Full source

/-- The ring homomorphism `(R/I)/J' -> R/(I ⊔ J)` induced by `quotLeftToQuotSup` where `J'`
  is the image of `J` in `R/I` -/
def quotQuotToQuotSup : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)(R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) →+* R ⧸ I ⊔ J :=
  Ideal.Quotient.lift (J.map (Ideal.Quotient.mk I)) (quotLeftToQuotSup I J)
    (ker_quotLeftToQuotSup I J).symm.le

Induced homomorphism from double quotient to single quotient by ideal supremum

Informal description

The ring homomorphism from the double quotient ring $(R/I)/J'$ to the quotient ring $R/(I \sqcup J)$, where $J'$ is the image of the ideal $J$ in $R/I$. This homomorphism is induced by the canonical homomorphism $\text{quotLeftToQuotSup} : R/I \to R/(I \sqcup J)$, which maps an equivalence class $[x]_I$ to $[x]_{I \sqcup J}$.

DoubleQuot.quotQuotMk definition

: R →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)

Full source

/-- The composite of the maps `R → (R/I)` and `(R/I) → (R/I)/J'` -/
def quotQuotMk : R →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) :=
  (Ideal.Quotient.mk (J.map (Ideal.Quotient.mk I))).comp (Ideal.Quotient.mk I)

Composite quotient map to double quotient ring

Informal description

The composite ring homomorphism from a commutative ring $ R $ to the double quotient ring $ (R/I) / (J \text{ mod } I) $, where $ I $ and $ J $ are ideals of $ R $. This map is obtained by first taking the quotient map $ R \to R/I $ and then the quotient map $ R/I \to (R/I) / (J \text{ mod } I) $.

DoubleQuot.ker_quotQuotMk theorem

: RingHom.ker (quotQuotMk I J) = I ⊔ J

Full source

/-- The kernel of `quotQuotMk` -/
theorem ker_quotQuotMk : RingHom.ker (quotQuotMk I J) = I ⊔ J := by
  rw [RingHom.ker_eq_comap_bot, quotQuotMk, ← comap_comap, ← RingHom.ker, mk_ker,
    comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ← RingHom.ker,
    mk_ker, sup_comm]

Kernel of Double Quotient Map Equals Sum of Ideals

Informal description

For any two ideals $I$ and $J$ of a commutative ring $R$, the kernel of the composite quotient map $\text{quotQuotMk}_{I,J} : R \to (R/I)/(J \text{ mod } I)$ is equal to the sum of the ideals $I$ and $J$, i.e., $\ker(\text{quotQuotMk}_{I,J}) = I + J$.

DoubleQuot.liftSupQuotQuotMk definition

(I J : Ideal R) : R ⧸ I ⊔ J →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)

Full source

/-- The ring homomorphism `R/(I ⊔ J) → (R/I)/J' `induced by `quotQuotMk` -/
def liftSupQuotQuotMk (I J : Ideal R) : R ⧸ I ⊔ JR ⧸ I ⊔ J →+* (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) :=
  Ideal.Quotient.lift (I ⊔ J) (quotQuotMk I J) (ker_quotQuotMk I J).symm.le

Induced homomorphism from quotient by supremum of ideals to double quotient

Informal description

Given two ideals $ I $ and $ J $ of a commutative ring $ R $, the ring homomorphism $ R/(I \sqcup J) \to (R/I) / (J \text{ mod } I) $ is induced by the composite quotient map $ \text{quotQuotMk} $. This map is well-defined because the kernel of $ \text{quotQuotMk} $ is contained in $ I \sqcup J $.

DoubleQuot.quotQuotEquivQuotSup definition

: (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* R ⧸ I ⊔ J

Full source

/-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where
`I ≤ J`, this is the Third Isomorphism Theorem (see `quotQuotEquivQuotOfLe`). -/
def quotQuotEquivQuotSup : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)(R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* R ⧸ I ⊔ J :=
  RingEquiv.ofHomInv (quotQuotToQuotSup I J) (liftSupQuotQuotMk I J)
    (by
      repeat apply Ideal.Quotient.ringHom_ext
      rfl)
    (by
      repeat apply Ideal.Quotient.ringHom_ext
      rfl)

Isomorphism between double quotient and quotient by ideal supremum

Informal description

The ring isomorphism between the double quotient ring $(R/I)/J'$ and the quotient ring $R/(I \sqcup J)$, where $J'$ is the image of the ideal $J$ in $R/I$. This isomorphism is constructed from the homomorphisms $\text{quotQuotToQuotSup}$ and $\text{liftSupQuotQuotMk}$, which are mutual inverses. When $I \leq J$, this isomorphism corresponds to the Third Isomorphism Theorem for rings.

DoubleQuot.quotQuotEquivQuotSup_quotQuotMk theorem

(x : R) : quotQuotEquivQuotSup I J (quotQuotMk I J x) = Ideal.Quotient.mk (I ⊔ J) x

Full source

@[simp]
theorem quotQuotEquivQuotSup_quotQuotMk (x : R) :
    quotQuotEquivQuotSup I J (quotQuotMk I J x) = Ideal.Quotient.mk (I ⊔ J) x :=
  rfl

Commutativity of the double quotient isomorphism diagram for ring elements

Informal description

For any commutative ring $R$ with ideals $I$ and $J$, and any element $x \in R$, the image of $x$ under the composite quotient map $\text{quotQuotMk}_{I,J}$ followed by the isomorphism $\text{quotQuotEquivQuotSup}_{I,J}$ equals the image of $x$ under the quotient map from $R$ to $R/(I \sqcup J)$. In other words, the following diagram commutes: $$ \text{quotQuotEquivQuotSup}_{I,J} \circ \text{quotQuotMk}_{I,J}(x) = \text{mk}_{I \sqcup J}(x) $$

DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk theorem

(x : R) : (quotQuotEquivQuotSup I J).symm (Ideal.Quotient.mk (I ⊔ J) x) = quotQuotMk I J x

Full source

@[simp]
theorem quotQuotEquivQuotSup_symm_quotQuotMk (x : R) :
    (quotQuotEquivQuotSup I J).symm (Ideal.Quotient.mk (I ⊔ J) x) = quotQuotMk I J x :=
  rfl

Inverse Isomorphism Property in Third Isomorphism Theorem for Rings

Informal description

For any commutative ring $R$ and ideals $I, J$ of $R$, the inverse of the isomorphism $(R/I)/J' \cong R/(I \sqcup J)$ (where $J'$ is the image of $J$ in $R/I$) maps the equivalence class of $x$ in $R/(I \sqcup J)$ to the double equivalence class of $x$ in $(R/I)/J'$. In other words, given $x \in R$, we have: $$(\phi^{-1})([x]_{I \sqcup J}) = [[x]_I]_{J'}$$ where $\phi$ is the isomorphism from the Third Isomorphism Theorem.

DoubleQuot.quotQuotEquivComm definition

: (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* (R ⧸ J) ⧸ I.map (Ideal.Quotient.mk J)

Full source

/-- The obvious isomorphism `(R/I)/J' → (R/J)/I'` -/
def quotQuotEquivComm : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)(R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+*
    (R ⧸ J) ⧸ I.map (Ideal.Quotient.mk J) :=
  ((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm ..))).trans
    (quotQuotEquivQuotSup J I).symm

Commutative isomorphism of double quotient rings

Informal description

The ring isomorphism between the double quotient rings $(R/I)/J'$ and $(R/J)/I'$, where $J'$ is the image of $J$ in $R/I$ and $I'$ is the image of $I$ in $R/J$. This isomorphism is constructed by composing the following maps: 1. The isomorphism $(R/I)/J' \cong R/(I \sqcup J)$, 2. The isomorphism $R/(I \sqcup J) \cong R/(J \sqcup I)$ (using commutativity of the supremum operation), 3. The inverse of the isomorphism $(R/J)/I' \cong R/(J \sqcup I)$.

DoubleQuot.quotQuotEquivComm_quotQuotMk theorem

(x : R) : quotQuotEquivComm I J (quotQuotMk I J x) = quotQuotMk J I x

Full source

@[simp]
theorem quotQuotEquivComm_quotQuotMk (x : R) :
    quotQuotEquivComm I J (quotQuotMk I J x) = quotQuotMk J I x :=
  rfl

Commutativity of Double Quotient Isomorphism on Equivalence Classes

Informal description

For any element $x$ in a commutative ring $R$ and any two ideals $I$ and $J$ of $R$, the isomorphism $\phi : (R/I)/J' \to (R/J)/I'$ (where $J'$ is the image of $J$ in $R/I$ and $I'$ is the image of $I$ in $R/J$) maps the double equivalence class $[[x]_I]_{J'}$ to the double equivalence class $[[x]_J]_{I'}$. In other words, we have: $$\phi([[x]_I]_{J'}) = [[x]_J]_{I'}$$

DoubleQuot.quotQuotEquivComm_comp_quotQuotMk theorem

: RingHom.comp (↑(quotQuotEquivComm I J)) (quotQuotMk I J) = quotQuotMk J I

Full source

@[simp]
theorem quotQuotEquivComm_comp_quotQuotMk :
    RingHom.comp (↑(quotQuotEquivComm I J)) (quotQuotMk I J) = quotQuotMk J I :=
  RingHom.ext <| quotQuotEquivComm_quotQuotMk I J

Compatibility of Double Quotient Isomorphism with Quotient Maps

Informal description

For any commutative ring $R$ and ideals $I, J$ of $R$, the composition of the ring isomorphism $\phi : (R/I)/J' \to (R/J)/I'$ (where $J'$ is the image of $J$ in $R/I$ and $I'$ is the image of $I$ in $R/J$) with the quotient map $\pi_{I,J} : R \to (R/I)/J'$ equals the quotient map $\pi_{J,I} : R \to (R/J)/I'$. That is, $\phi \circ \pi_{I,J} = \pi_{J,I}$.

DoubleQuot.quotQuotEquivComm_symm theorem

: (quotQuotEquivComm I J).symm = quotQuotEquivComm J I

Full source

@[simp]
theorem quotQuotEquivComm_symm : (quotQuotEquivComm I J).symm = quotQuotEquivComm J I := by
  /-  Porting note: this proof used to just be rfl but currently rfl opens up a bottomless pit
  of processor cycles. Synthesizing instances does not seem to be an issue.
  -/
  change (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm ..))).trans
    (quotQuotEquivQuotSup J I).symm).symm =
      ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq (sup_comm ..))).trans
        (quotQuotEquivQuotSup I J).symm
  ext r
  dsimp
  rfl

Inverse of Commutative Isomorphism of Double Quotient Rings

Informal description

The inverse of the ring isomorphism between the double quotient rings $(R/I)/J'$ and $(R/J)/I'$ (where $J'$ is the image of $J$ in $R/I$ and $I'$ is the image of $I$ in $R/J$) is equal to the ring isomorphism between $(R/J)/I'$ and $(R/I)/J'$.

DoubleQuot.quotQuotEquivQuotOfLE definition

(h : I ≤ J) : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* R ⧸ J

Full source

/-- **The Third Isomorphism theorem** for rings. See `quotQuotEquivQuotSup` for a version
    that does not assume an inclusion of ideals. -/
def quotQuotEquivQuotOfLE (h : I ≤ J) : (R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)(R ⧸ I) ⧸ J.map (Ideal.Quotient.mk I) ≃+* R ⧸ J :=
  (quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq <| sup_eq_right.mpr h)

Third Isomorphism Theorem for Rings (inclusion version)

Informal description

Given a commutative ring $R$ and two ideals $I \leq J$ of $R$, there exists a ring isomorphism between the double quotient ring $(R/I)/(J')$ (where $J'$ is the image of $J$ under the quotient map $R \to R/I$) and the single quotient ring $R/J$. This isomorphism is constructed by composing the isomorphism $(R/I)/J' \cong R/(I \sqcup J)$ with the isomorphism $R/(I \sqcup J) \cong R/J$ induced by the equality $I \sqcup J = J$ (which holds because $I \leq J$).

DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk theorem

(x : R) (h : I ≤ J) : quotQuotEquivQuotOfLE h (quotQuotMk I J x) = (Ideal.Quotient.mk J) x

Full source

@[simp]
theorem quotQuotEquivQuotOfLE_quotQuotMk (x : R) (h : I ≤ J) :
    quotQuotEquivQuotOfLE h (quotQuotMk I J x) = (Ideal.Quotient.mk J) x :=
  rfl

Compatibility of Third Isomorphism Theorem with Quotient Maps

Informal description

For any element $x$ in a commutative ring $R$ and ideals $I \leq J$ of $R$, the isomorphism $\phi : (R/I)/(J \text{ mod } I) \cong R/J$ from the third isomorphism theorem satisfies $\phi([x]_{J \text{ mod } I}) = [x]_J$, where $[x]_{J \text{ mod } I}$ denotes the equivalence class of $x$ in the double quotient $(R/I)/(J \text{ mod } I)$ and $[x]_J$ denotes the equivalence class of $x$ in $R/J$.

DoubleQuot.quotQuotEquivQuotOfLE_symm_mk theorem

(x : R) (h : I ≤ J) : (quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = quotQuotMk I J x

Full source

@[simp]
theorem quotQuotEquivQuotOfLE_symm_mk (x : R) (h : I ≤ J) :
    (quotQuotEquivQuotOfLE h).symm ((Ideal.Quotient.mk J) x) = quotQuotMk I J x :=
  rfl

Inverse of Third Isomorphism Theorem Maps Cosets Correctly

Informal description

Let $R$ be a commutative ring with ideals $I \leq J$. For any element $x \in R$, the inverse of the isomorphism $(R/I)/(J \text{ mod } I) \cong R/J$ maps the equivalence class of $x$ in $R/J$ to the equivalence class of $x$ in $(R/I)/(J \text{ mod } I)$.

DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk theorem

(h : I ≤ J) : RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = (Ideal.Quotient.mk J)

Full source

theorem quotQuotEquivQuotOfLE_comp_quotQuotMk (h : I ≤ J) :
    RingHom.comp (↑(quotQuotEquivQuotOfLE h)) (quotQuotMk I J) = (Ideal.Quotient.mk J) := by
  ext
  rfl

Compatibility of Third Isomorphism Theorem with Quotient Maps

Informal description

Given a commutative ring $R$ and two ideals $I \leq J$ of $R$, the composition of the ring isomorphism $(R/I)/(J \text{ mod } I) \cong R/J$ with the composite quotient map $R \to (R/I)/(J \text{ mod } I)$ equals the quotient map $R \to R/J$.

DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk theorem

(h : I ≤ J) : RingHom.comp (↑(quotQuotEquivQuotOfLE h).symm) (Ideal.Quotient.mk J) = quotQuotMk I J

Full source

theorem quotQuotEquivQuotOfLE_symm_comp_mk (h : I ≤ J) :
    RingHom.comp (↑(quotQuotEquivQuotOfLE h).symm) (Ideal.Quotient.mk J) = quotQuotMk I J := by
  ext
  rfl

Compatibility of Third Isomorphism Theorem with Quotient Maps

Informal description

Given a commutative ring $R$ and two ideals $I \leq J$ of $R$, the composition of the inverse of the isomorphism $(R/I)/(J \text{ mod } I) \cong R/J$ with the quotient map $R \to R/J$ equals the composite quotient map $R \to (R/I)/(J \text{ mod } I)$. In symbols, if $\varphi$ denotes the isomorphism $(R/I)/(J \text{ mod } I) \cong R/J$ and $\pi_J : R \to R/J$ is the quotient map, then: \[ \varphi^{-1} \circ \pi_J = \text{quotQuotMk}_{I,J} \] where $\text{quotQuotMk}_{I,J} : R \to (R/I)/(J \text{ mod } I)$ is the composite quotient map.

DoubleQuot.quotQuotEquivComm_mk_mk theorem

 [CommRing R] (I J : Ideal R) (x : R) :
  quotQuotEquivComm I J (Ideal.Quotient.mk _ (Ideal.Quotient.mk _ x)) = algebraMap R _ x

Full source

@[simp]
theorem quotQuotEquivComm_mk_mk [CommRing R] (I J : Ideal R) (x : R) :
    quotQuotEquivComm I J (Ideal.Quotient.mk _ (Ideal.Quotient.mk _ x)) = algebraMap R _ x :=
  rfl

Compatibility of Double Quotient Isomorphism with Quotient Maps

Informal description

Let $R$ be a commutative ring with ideals $I$ and $J$. For any element $x \in R$, the commutative isomorphism of double quotient rings $\text{quotQuotEquivComm}$ satisfies \[ \text{quotQuotEquivComm}([x]_{J'}) = [x]_{I'}, \] where $J'$ is the image of $J$ in $R/I$, $I'$ is the image of $I$ in $R/J$, and $[x]_{J'}$ and $[x]_{I'}$ denote the equivalence classes of $x$ in $(R/I)/J'$ and $(R/J)/I'$, respectively.

DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap theorem

(x : R) : DoubleQuot.quotQuotEquivQuotSup I J (algebraMap R _ x) = algebraMap _ _ x

Full source

@[simp]
theorem quotQuotEquivQuotSup_quot_quot_algebraMap (x : R) :
    DoubleQuot.quotQuotEquivQuotSup I J (algebraMap R _ x) = algebraMap _ _ x :=
  rfl

Compatibility of Double Quotient Isomorphism with Algebra Maps

Informal description

For any element $x$ in a commutative ring $R$, the isomorphism $\text{quotQuotEquivQuotSup}$ between the double quotient ring $(R/I)/J'$ and the quotient ring $R/(I \sqcup J)$ satisfies \[ \text{quotQuotEquivQuotSup}([x]_{J'}) = [x]_{I \sqcup J}, \] where $J'$ is the image of the ideal $J$ in $R/I$, and $[x]_{J'}$ and $[x]_{I \sqcup J}$ denote the equivalence classes of $x$ in $(R/I)/J'$ and $R/(I \sqcup J)$, respectively.

DoubleQuot.quotQuotEquivComm_algebraMap theorem

(x : R) : quotQuotEquivComm I J (algebraMap R _ x) = algebraMap _ _ x

Full source

@[simp]
theorem quotQuotEquivComm_algebraMap (x : R) :
    quotQuotEquivComm I J (algebraMap R _ x) = algebraMap _ _ x :=
  rfl

Compatibility of Double Quotient Isomorphism with Algebra Maps

Informal description

For any element $x$ in a commutative ring $R$, the commutative isomorphism $\text{quotQuotEquivComm}$ between the double quotient rings $(R/I)/J'$ and $(R/J)/I'$ satisfies \[ \text{quotQuotEquivComm}([x]_{J'}) = [x]_{I'}, \] where $J'$ is the image of the ideal $J$ in $R/I$, $I'$ is the image of the ideal $I$ in $R/J$, and $[x]_{J'}$ and $[x]_{I'}$ denote the equivalence classes of $x$ in $(R/I)/J'$ and $(R/J)/I'$ respectively.

DoubleQuot.quotLeftToQuotSupₐ definition

: A ⧸ I →ₐ[R] A ⧸ I ⊔ J

Full source

/-- The natural algebra homomorphism `A / I → A / (I ⊔ J)`. -/
def quotLeftToQuotSupₐ : A ⧸ IA ⧸ I →ₐ[R] A ⧸ I ⊔ J :=
  AlgHom.mk (quotLeftToQuotSup I J) fun _ => rfl

Algebra homomorphism from $ A/I $ to $ A/(I \sqcup J) $

Informal description

The natural algebra homomorphism from the quotient algebra $ A/I $ to the quotient algebra $ A/(I \sqcup J) $, where $ I \sqcup J $ denotes the supremum of the ideals $ I $ and $ J $ in the lattice of ideals of $ A $. This homomorphism preserves the algebra structure over $ R $.

DoubleQuot.quotLeftToQuotSupₐ_toRingHom theorem

: (quotLeftToQuotSupₐ R I J : _ →+* _) = quotLeftToQuotSup I J

Full source

@[simp]
theorem quotLeftToQuotSupₐ_toRingHom :
    (quotLeftToQuotSupₐ R I J : _ →+* _) = quotLeftToQuotSup I J :=
  rfl

Equality of Underlying Ring Homomorphisms in Quotient Algebra Construction

Informal description

The underlying ring homomorphism of the algebra homomorphism $\text{quotLeftToQuotSupₐ} R I J$ from $A/I$ to $A/(I \sqcup J)$ is equal to the ring homomorphism $\text{quotLeftToQuotSup} I J$.

DoubleQuot.coe_quotLeftToQuotSupₐ theorem

: ⇑(quotLeftToQuotSupₐ R I J) = quotLeftToQuotSup I J

Full source

@[simp]
theorem coe_quotLeftToQuotSupₐ : ⇑(quotLeftToQuotSupₐ R I J) = quotLeftToQuotSup I J :=
  rfl

Equality of Underlying Functions in Quotient Algebra Homomorphism

Informal description

The underlying function of the algebra homomorphism $\text{quotLeftToQuotSupₐ} R I J$ from $A/I$ to $A/(I \sqcup J)$ is equal to the ring homomorphism $\text{quotLeftToQuotSup} I J$.

DoubleQuot.quotQuotToQuotSupₐ definition

: (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) →ₐ[R] A ⧸ I ⊔ J

Full source

/-- The algebra homomorphism `(A / I) / J' -> A / (I ⊔ J)` induced by `quotQuotToQuotSup`,
  where `J'` is the projection of `J` in `A / I`. -/
def quotQuotToQuotSupₐ : (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)(A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) →ₐ[R] A ⧸ I ⊔ J :=
  AlgHom.mk (quotQuotToQuotSup I J) fun _ => rfl

Algebra homomorphism from double quotient to quotient by ideal supremum

Informal description

The algebra homomorphism from the double quotient ring $(A/I)/J'$ to the quotient ring $A/(I \sqcup J)$, where $J'$ is the image of the ideal $J$ in $A/I$ under the canonical quotient map. This homomorphism is induced by the canonical homomorphism $\text{quotLeftToQuotSup} : A/I \to A/(I \sqcup J)$, which maps an equivalence class $[x]_I$ to $[x]_{I \sqcup J}$.

DoubleQuot.quotQuotToQuotSupₐ_toRingHom theorem

: ((quotQuotToQuotSupₐ R I J) : _ ⧸ map (Ideal.Quotient.mkₐ R I) J →+* _) = quotQuotToQuotSup I J

Full source

@[simp]
theorem quotQuotToQuotSupₐ_toRingHom :
    ((quotQuotToQuotSupₐ R I J) : _ ⧸ map (Ideal.Quotient.mkₐ R I) J_ ⧸ map (Ideal.Quotient.mkₐ R I) J →+* _) =
      quotQuotToQuotSup I J :=
  rfl

Equality of Underlying Ring Homomorphisms in Double Quotient Algebra Homomorphism

Informal description

The underlying ring homomorphism of the algebra homomorphism $\text{quotQuotToQuotSupₐ} R I J$ from the double quotient ring $(A/I)/(J \text{ mod } I)$ to the quotient ring $A/(I \sqcup J)$ is equal to the ring homomorphism $\text{quotQuotToQuotSup} I J$.

DoubleQuot.coe_quotQuotToQuotSupₐ theorem

: ⇑(quotQuotToQuotSupₐ R I J) = quotQuotToQuotSup I J

Full source

@[simp]
theorem coe_quotQuotToQuotSupₐ : ⇑(quotQuotToQuotSupₐ R I J) = quotQuotToQuotSup I J :=
  rfl

Equality of Underlying Functions for Double Quotient to Quotient by Supremum Homomorphisms

Informal description

The underlying function of the algebra homomorphism $\text{quotQuotToQuotSupₐ}$ from the double quotient ring $(A/I)/J'$ to the quotient ring $A/(I \sqcup J)$ is equal to the ring homomorphism $\text{quotQuotToQuotSup}$ between the same rings.

DoubleQuot.quotQuotMkₐ definition

: A →ₐ[R] (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)

Full source

/-- The composition of the algebra homomorphisms `A → (A / I)` and `(A / I) → (A / I) / J'`,
  where `J'` is the projection `J` in `A / I`. -/
def quotQuotMkₐ : A →ₐ[R] (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) :=
  AlgHom.mk (quotQuotMk I J) fun _ => rfl

Composite quotient algebra homomorphism to double quotient ring

Informal description

The algebra homomorphism from an $R$-algebra $A$ to the double quotient ring $(A/I) / (J \text{ mod } I)$, where $I$ and $J$ are ideals of $A$. This map is obtained by first taking the quotient algebra homomorphism $A \to A/I$ and then the quotient algebra homomorphism $A/I \to (A/I) / (J \text{ mod } I)$.

DoubleQuot.quotQuotMkₐ_toRingHom theorem

: (quotQuotMkₐ R I J : _ →+* _ ⧸ J.map (Quotient.mkₐ R I)) = quotQuotMk I J

Full source

@[simp]
theorem quotQuotMkₐ_toRingHom :
    (quotQuotMkₐ R I J : _ →+* _ ⧸ J.map (Quotient.mkₐ R I)) = quotQuotMk I J :=
  rfl

Equality of Composite Quotient Homomorphisms: Algebra and Ring Cases

Informal description

The ring homomorphism obtained from the composite quotient algebra homomorphism `quotQuotMkₐ R I J` is equal to the composite quotient ring homomorphism `quotQuotMk I J`. That is, the following diagram commutes: \[ \begin{CD} A @>{\text{quotQuotMkₐ R I J}}>> (A/I) / (J \text{ mod } I) \\ @| @| \\ A @>{\text{quotQuotMk I J}}>> (A/I) / (J \text{ mod } I) \end{CD} \] where the vertical maps are the canonical identifications.

DoubleQuot.coe_quotQuotMkₐ theorem

: ⇑(quotQuotMkₐ R I J) = quotQuotMk I J

Full source

@[simp]
theorem coe_quotQuotMkₐ : ⇑(quotQuotMkₐ R I J) = quotQuotMk I J :=
  rfl

Equality of Underlying Functions in Composite Quotient Maps

Informal description

The underlying function of the composite quotient algebra homomorphism `quotQuotMkₐ R I J` from an $R$-algebra $A$ to the double quotient ring $(A/I) / (J \text{ mod } I)$ is equal to the composite quotient ring homomorphism `quotQuotMk I J`.

DoubleQuot.liftSupQuotQuotMkₐ definition

(I J : Ideal A) : A ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)

Full source

/-- The injective algebra homomorphism `A / (I ⊔ J) → (A / I) / J'`induced by `quot_quot_mk`,
  where `J'` is the projection `J` in `A / I`. -/
def liftSupQuotQuotMkₐ (I J : Ideal A) : A ⧸ I ⊔ JA ⧸ I ⊔ J →ₐ[R] (A ⧸ I) ⧸ J.map (Quotient.mkₐ R I) :=
  AlgHom.mk (liftSupQuotQuotMk I J) fun _ => rfl

Induced algebra homomorphism from quotient by supremum of ideals to double quotient

Informal description

Given a commutative semiring $ R $, an $ R $-algebra $ A $, and two ideals $ I $ and $ J $ of $ A $, the algebra homomorphism $ A/(I \sqcup J) \to (A/I) / (J \text{ mod } I) $ is induced by the composite quotient map $ \text{quotQuotMk} $. This map is well-defined because the kernel of $ \text{quotQuotMk} $ is contained in $ I \sqcup J $.

DoubleQuot.liftSupQuotQuotMkₐ_toRingHom theorem

: (liftSupQuotQuotMkₐ R I J : _ →+* _ ⧸ J.map (Quotient.mkₐ R I)) = liftSupQuotQuotMk I J

Full source

@[simp]
theorem liftSupQuotQuotMkₐ_toRingHom :
    (liftSupQuotQuotMkₐ R I J : _ →+* _ ⧸ J.map (Quotient.mkₐ R I)) = liftSupQuotQuotMk I J :=
  rfl

Equality of Ring Homomorphisms in Double Quotient Construction

Informal description

The ring homomorphism obtained by composing the algebra homomorphism `liftSupQuotQuotMkₐ R I J` from $A/(I \sqcup J)$ to $(A/I) / (J \text{ mod } I)$ is equal to the ring homomorphism `liftSupQuotQuotMk I J`.

DoubleQuot.coe_liftSupQuotQuotMkₐ theorem

: ⇑(liftSupQuotQuotMkₐ R I J) = liftSupQuotQuotMk I J

Full source

@[simp]
theorem coe_liftSupQuotQuotMkₐ : ⇑(liftSupQuotQuotMkₐ R I J) = liftSupQuotQuotMk I J :=
  rfl

Equality of Underlying Functions in Double Quotient Construction

Informal description

The underlying function of the algebra homomorphism $\text{liftSupQuotQuotMkₐ} \, R \, I \, J$ from $A/(I \sqcup J)$ to $(A/I) / (J \text{ mod } I)$ is equal to the ring homomorphism $\text{liftSupQuotQuotMk} \, I \, J$.

DoubleQuot.quotQuotEquivQuotSupₐ definition

: ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ I ⊔ J

Full source

/-- `quotQuotToQuotSup` and `liftSupQuotQuotMk` are inverse isomorphisms. In the case where
`I ≤ J`, this is the Third Isomorphism Theorem (see `DoubleQuot.quotQuotEquivQuotOfLE`). -/
def quotQuotEquivQuotSupₐ : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ I ⊔ J :=
  AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotSup I J) fun _ => rfl

Algebra isomorphism between double quotient and quotient by ideal supremum

Informal description

The algebra isomorphism between the double quotient algebra $(A/I)/J'$ and the quotient algebra $A/(I \sqcup J)$, where $J'$ is the image of the ideal $J$ in $A/I$ under the canonical quotient map. This isomorphism preserves the $R$-algebra structure and is constructed from the corresponding ring isomorphism `quotQuotEquivQuotSup I J`.

DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv theorem

: (quotQuotEquivQuotSupₐ R I J : _ ⧸ J.map (Quotient.mkₐ R I) ≃+* _) = quotQuotEquivQuotSup I J

Full source

@[simp]
theorem quotQuotEquivQuotSupₐ_toRingEquiv :
    (quotQuotEquivQuotSupₐ R I J : _ ⧸ J.map (Quotient.mkₐ R I)_ ⧸ J.map (Quotient.mkₐ R I) ≃+* _) = quotQuotEquivQuotSup I J :=
  rfl

Equality of Algebra and Ring Isomorphisms in Double Quotient Construction

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $I$, $J$ ideals of $A$. The algebra isomorphism $\text{quotQuotEquivQuotSupₐ} \, R \, I \, J$ between $(A/I)/J'$ and $A/(I \sqcup J)$ (where $J'$ is the image of $J$ in $A/I$) is equal to the underlying ring isomorphism $\text{quotQuotEquivQuotSup} \, I \, J$ when viewed as a ring homomorphism.

DoubleQuot.coe_quotQuotEquivQuotSupₐ theorem

: ⇑(quotQuotEquivQuotSupₐ R I J) = ⇑(quotQuotEquivQuotSup I J)

Full source

@[simp]
-- Porting note: had to add an extra coercion arrow on the right hand side.
theorem coe_quotQuotEquivQuotSupₐ : ⇑(quotQuotEquivQuotSupₐ R I J) = ⇑(quotQuotEquivQuotSup I J) :=
  rfl

Underlying Function Equality of Algebra and Ring Isomorphisms for Double Quotient

Informal description

The underlying function of the algebra isomorphism $\text{quotQuotEquivQuotSup}_R(I, J)$ between the double quotient algebra $(A/I)/J'$ and the quotient algebra $A/(I \sqcup J)$ is equal to the underlying function of the corresponding ring isomorphism $\text{quotQuotEquivQuotSup}(I, J)$.

DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv theorem

: ((quotQuotEquivQuotSupₐ R I J).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) = (quotQuotEquivQuotSup I J).symm

Full source

@[simp]
theorem quotQuotEquivQuotSupₐ_symm_toRingEquiv :
    ((quotQuotEquivQuotSupₐ R I J).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) =
      (quotQuotEquivQuotSup I J).symm :=
  rfl

Inverse of Algebra Isomorphism Equals Inverse of Ring Isomorphism for Double Quotient

Informal description

The inverse of the algebra isomorphism $\text{quotQuotEquivQuotSupₐ}$ between the double quotient algebra $(A/I)/J'$ and the quotient algebra $A/(I \sqcup J)$ is equal to the inverse of the corresponding ring isomorphism $\text{quotQuotEquivQuotSup}$ when viewed as a ring equivalence. Here $J'$ is the image of the ideal $J$ in $A/I$ under the canonical quotient map.

DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm theorem

: ⇑(quotQuotEquivQuotSupₐ R I J).symm = ⇑(quotQuotEquivQuotSup I J).symm

Full source

@[simp]
-- Porting note: had to add an extra coercion arrow on the right hand side.
theorem coe_quotQuotEquivQuotSupₐ_symm :
    ⇑(quotQuotEquivQuotSupₐ R I J).symm = ⇑(quotQuotEquivQuotSup I J).symm :=
  rfl

Inverse of Double Quotient Algebra Isomorphism Equals Inverse of Ring Isomorphism

Informal description

The underlying function of the inverse of the algebra isomorphism $\text{quotQuotEquivQuotSupₐ}(R, I, J)$ is equal to the underlying function of the inverse of the ring isomorphism $\text{quotQuotEquivQuotSup}(I, J)$. In other words, the inverse of the algebra isomorphism between the double quotient algebra $(A/I)/J'$ and the quotient algebra $A/(I \sqcup J)$ (where $J'$ is the image of $J$ under the quotient map) coincides with the inverse of the corresponding ring isomorphism when viewed as functions.

DoubleQuot.quotQuotEquivCommₐ definition

: ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] (A ⧸ J) ⧸ I.map (Quotient.mkₐ R J)

Full source

/-- The natural algebra isomorphism `(A / I) / J' → (A / J) / I'`,
  where `J'` (resp. `I'`) is the projection of `J` in `A / I` (resp. `I` in `A / J`). -/
def quotQuotEquivCommₐ :
    ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] (A ⧸ J) ⧸ I.map (Quotient.mkₐ R J) :=
  AlgEquiv.ofRingEquiv (f := quotQuotEquivComm I J) fun _ => rfl

Commutative algebra isomorphism of double quotient rings

Informal description

The natural algebra isomorphism between the double quotient rings $(A/I)/J'$ and $(A/J)/I'$, where $J'$ is the image of $J$ in $A/I$ under the canonical quotient map $\text{Quotient.mk}_R I$, and $I'$ is the image of $I$ in $A/J$ under the canonical quotient map $\text{Quotient.mk}_R J$. This isomorphism preserves the algebra structure over the commutative semiring $R$.

DoubleQuot.quotQuotEquivCommₐ_toRingEquiv theorem

 : (quotQuotEquivCommₐ R I J : _ ⧸ J.map (Quotient.mkₐ R I) ≃+* _ ⧸ I.map (Quotient.mkₐ R J)) = quotQuotEquivComm I J

Full source

@[simp]
theorem quotQuotEquivCommₐ_toRingEquiv :
    (quotQuotEquivCommₐ R I J : _ ⧸ J.map (Quotient.mkₐ R I)_ ⧸ J.map (Quotient.mkₐ R I) ≃+* _ ⧸ I.map (Quotient.mkₐ R J)) =
      quotQuotEquivComm I J :=
  -- Porting note: should just be `rfl` but `AlgEquiv.toRingEquiv` and `AlgEquiv.ofRingEquiv`
  -- involve repacking everything in the structure, so Lean ends up unfolding `quotQuotEquivComm`
  -- and timing out.
  RingEquiv.ext fun _ => rfl

Ring Equivalence Underlying Double Quotient Algebra Isomorphism

Informal description

The underlying ring equivalence of the algebra isomorphism $\text{quotQuotEquivCommₐ}(R, I, J)$ between the double quotient rings $(A/I)/J'$ and $(A/J)/I'$ (where $J'$ is the image of $J$ under the quotient map $\text{Quotient.mk}_R I$ and $I'$ is the image of $I$ under $\text{Quotient.mk}_R J$) is equal to the ring isomorphism $\text{quotQuotEquivComm}(I, J)$.

DoubleQuot.coe_quotQuotEquivCommₐ theorem

: ⇑(quotQuotEquivCommₐ R I J) = ⇑(quotQuotEquivComm I J)

Full source

@[simp]
theorem coe_quotQuotEquivCommₐ : ⇑(quotQuotEquivCommₐ R I J) = ⇑(quotQuotEquivComm I J) :=
  rfl

Equality of Underlying Functions in Double Quotient Isomorphisms

Informal description

The underlying function of the algebra isomorphism $\text{quotQuotEquivComm}_R I J$ between the double quotient rings $(A/I)/J'$ and $(A/J)/I'$ is equal to the underlying function of the ring isomorphism $\text{quotQuotEquivComm} I J$.

DoubleQuot.quotQuotEquivComm_symmₐ theorem

: (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I

Full source

@[simp]
theorem quotQuotEquivComm_symmₐ : (quotQuotEquivCommₐ R I J).symm = quotQuotEquivCommₐ R J I := by
  -- Porting note: should just be `rfl` but `AlgEquiv.toRingEquiv` and `AlgEquiv.ofRingEquiv`
  -- involve repacking everything in the structure, so Lean ends up unfolding `quotQuotEquivComm`
  -- and timing out.
  ext
  unfold quotQuotEquivCommₐ
  congr

Inverse of Double Quotient Algebra Isomorphism

Informal description

The inverse of the algebra isomorphism $\text{quotQuotEquivComm}_R(I, J)$ between the double quotient rings $(A/I)/J'$ and $(A/J)/I'$ is equal to the algebra isomorphism $\text{quotQuotEquivComm}_R(J, I)$ between $(A/J)/I'$ and $(A/I)/J'$, where $J'$ is the image of $J$ under the quotient map $\text{Quotient.mk}_R I$ and $I'$ is the image of $I$ under $\text{Quotient.mk}_R J$.

DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ theorem

: AlgHom.comp (↑(quotQuotEquivCommₐ R I J)) (quotQuotMkₐ R I J) = quotQuotMkₐ R J I

Full source

@[simp]
theorem quotQuotEquivComm_comp_quotQuotMkₐ :
    AlgHom.comp (↑(quotQuotEquivCommₐ R I J)) (quotQuotMkₐ R I J) = quotQuotMkₐ R J I :=
  AlgHom.ext <| quotQuotEquivComm_quotQuotMk I J

Commutativity of Double Quotient Construction via Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $I, J$ ideals of $A$. The composition of the algebra homomorphism $\text{quotQuotMk}_{R} I J : A \to (A/I)/(J \text{ mod } I)$ with the algebra isomorphism $\text{quotQuotEquivComm}_{R} I J : (A/I)/(J \text{ mod } I) \to (A/J)/(I \text{ mod } J)$ equals the algebra homomorphism $\text{quotQuotMk}_{R} J I : A \to (A/J)/(I \text{ mod } J)$. In other words, the following diagram commutes: $$ A \xrightarrow{\text{quotQuotMk}_{R} I J} (A/I)/(J \text{ mod } I) \xrightarrow{\text{quotQuotEquivComm}_{R} I J} (A/J)/(I \text{ mod } J) $$ equals: $$ A \xrightarrow{\text{quotQuotMk}_{R} J I} (A/J)/(I \text{ mod } J) $$

DoubleQuot.quotQuotEquivQuotOfLEₐ definition

(h : I ≤ J) : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ J

Full source

/-- The **third isomorphism theorem** for algebras. See `quotQuotEquivQuotSupₐ` for version
    that does not assume an inclusion of ideals. -/
def quotQuotEquivQuotOfLEₐ (h : I ≤ J) : ((A ⧸ I) ⧸ J.map (Quotient.mkₐ R I)) ≃ₐ[R] A ⧸ J :=
  AlgEquiv.ofRingEquiv (f := quotQuotEquivQuotOfLE h) fun _ => rfl

Third Isomorphism Theorem for Algebras (inclusion version)

Informal description

Given a commutative semiring $R$, an $R$-algebra $A$, and two ideals $I \leq J$ of $A$, there exists an algebra isomorphism between the double quotient $(A/I)/(J')$ (where $J'$ is the image of $J$ under the canonical quotient map $A \to A/I$) and the single quotient $A/J$. This isomorphism preserves the $R$-algebra structure.

DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv theorem

(h : I ≤ J) : (quotQuotEquivQuotOfLEₐ R h : _ ⧸ J.map (Quotient.mkₐ R I) ≃+* _) = quotQuotEquivQuotOfLE h

Full source

@[simp]
theorem quotQuotEquivQuotOfLEₐ_toRingEquiv (h : I ≤ J) :
    (quotQuotEquivQuotOfLEₐ R h : _ ⧸ J.map (Quotient.mkₐ R I)_ ⧸ J.map (Quotient.mkₐ R I) ≃+* _) = quotQuotEquivQuotOfLE h :=
  rfl

Compatibility of Third Isomorphism Theorem for Algebras with Underlying Ring Structure

Informal description

Let $R$ be a commutative semiring, $A$ an $R$-algebra, and $I \leq J$ two ideals of $A$. The algebra isomorphism $(A/I)/(J') \cong A/J$ (where $J'$ is the image of $J$ under the quotient map $A \to A/I$) is equal to the corresponding ring isomorphism when viewed through the forgetful functor from algebras to rings.

DoubleQuot.coe_quotQuotEquivQuotOfLEₐ theorem

(h : I ≤ J) : ⇑(quotQuotEquivQuotOfLEₐ R h) = ⇑(quotQuotEquivQuotOfLE h)

Full source

@[simp]
-- Porting note: had to add an extra coercion arrow on the right hand side.
theorem coe_quotQuotEquivQuotOfLEₐ (h : I ≤ J) :
    ⇑(quotQuotEquivQuotOfLEₐ R h) = ⇑(quotQuotEquivQuotOfLE h) :=
  rfl

Underlying Function of Third Isomorphism Theorem for Algebras

Informal description

For a commutative semiring $R$, an $R$-algebra $A$, and two ideals $I \leq J$ of $A$, the underlying function of the algebra isomorphism $(A/I)/(J') \cong A/J$ (where $J'$ is the image of $J$ under the quotient map $A \to A/I$) coincides with the underlying function of the corresponding ring isomorphism.

DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv theorem

 (h : I ≤ J) : ((quotQuotEquivQuotOfLEₐ R h).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) = (quotQuotEquivQuotOfLE h).symm

Full source

@[simp]
theorem quotQuotEquivQuotOfLEₐ_symm_toRingEquiv (h : I ≤ J) :
    ((quotQuotEquivQuotOfLEₐ R h).symm : _ ≃+* _ ⧸ J.map (Quotient.mkₐ R I)) =
      (quotQuotEquivQuotOfLE h).symm :=
  rfl

Inverse of Third Isomorphism Theorem for Algebras as Ring Equivalence

Informal description

For a commutative semiring $R$, an $R$-algebra $A$, and two ideals $I \leq J$ of $A$, the ring equivalence obtained by taking the inverse of the algebra isomorphism $(A/I)/(J') \cong A/J$ (where $J'$ is the image of $J$ under the quotient map $A \to A/I$) is equal to the inverse of the corresponding ring isomorphism.

DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm theorem

(h : I ≤ J) : ⇑(quotQuotEquivQuotOfLEₐ R h).symm = ⇑(quotQuotEquivQuotOfLE h).symm

Full source

@[simp]
-- Porting note: had to add an extra coercion arrow on the right hand side.
theorem coe_quotQuotEquivQuotOfLEₐ_symm (h : I ≤ J) :
    ⇑(quotQuotEquivQuotOfLEₐ R h).symm = ⇑(quotQuotEquivQuotOfLE h).symm :=
  rfl

Inverse Function Coincidence in Third Isomorphism Theorem for Algebras

Informal description

For any commutative semiring $R$, any $R$-algebra $A$, and two ideals $I \leq J$ of $A$, the underlying function of the inverse of the algebra isomorphism $(A/I)/(J') \cong A/J$ (where $J'$ is the image of $J$ under the quotient map $A \to A/I$) coincides with the underlying function of the inverse of the corresponding ring isomorphism.

DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ theorem

(h : I ≤ J) : AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h)) (quotQuotMkₐ R I J) = Quotient.mkₐ R J

Full source

@[simp]
theorem quotQuotEquivQuotOfLE_comp_quotQuotMkₐ (h : I ≤ J) :
    AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h)) (quotQuotMkₐ R I J) = Quotient.mkₐ R J :=
  rfl

Compatibility of Third Isomorphism Theorem with Quotient Maps

Informal description

Given a commutative semiring $R$, an $R$-algebra $A$, and two ideals $I \leq J$ of $A$, the composition of the algebra isomorphism $(A/I)/(J \text{ mod } I) \cong A/J$ with the composite quotient algebra homomorphism $A \to (A/I)/(J \text{ mod } I)$ equals the canonical quotient algebra homomorphism $A \to A/J$.

DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ theorem

(h : I ≤ J) : AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h).symm) (Quotient.mkₐ R J) = quotQuotMkₐ R I J

Full source

@[simp]
theorem quotQuotEquivQuotOfLE_symm_comp_mkₐ (h : I ≤ J) :
    AlgHom.comp (↑(quotQuotEquivQuotOfLEₐ R h).symm) (Quotient.mkₐ R J) = quotQuotMkₐ R I J :=
  rfl

Compatibility of Inverse Third Isomorphism with Quotient Maps

Informal description

Given a commutative semiring $R$, an $R$-algebra $A$, and two ideals $I \leq J$ of $A$, the composition of the inverse of the algebra isomorphism $(A/I)/(J \text{ mod } I) \cong A/J$ with the canonical quotient map $A \to A/J$ equals the composite quotient map $A \to (A/I)/(J \text{ mod } I)$.

Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow definition

 :
  ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃ₗ[R]
    Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)

Full source

/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the `R`-linear equivalence between the two. -/
noncomputable
def powQuotPowSuccLinearEquivMapMkPowSuccPow :
    ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃ₗ[R]
    Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) := by
  refine { LinearMap.codRestrict
    (Submodule.restrictScalars _ (Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)))
    (Submodule.mapQ (I • ⊤) (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?_) ?_,
    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
  · intro
    simp [Submodule.mem_smul_top_iff, pow_succ']
  · intro x
    obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ x
    simp [Ideal.mem_sup_left hy]
  · intro a b
    obtain ⟨⟨x, hx⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ a
    obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b
    simp [Ideal.Quotient.eq, Submodule.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ']
  · intro ⟨x, hx⟩
    rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx
    obtain ⟨y, hy, rfl⟩ := hx
    refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
    simp

Canonical linear equivalence between $ I^n / I^{n+1} $ and its image in $ R / I^{n+1} $

Informal description

For a commutative ring $ R $ and an ideal $ I $ of $ R $, there is a canonical $ R $-linear equivalence between the quotient module $ I^n / I^{n+1} $ and the ideal $ \text{map} \, (\text{Quotient.mk} \, I^{n+1}) \, I^n $ in the quotient ring $ R / I^{n+1} $. Here, $ I^n $ denotes the $ n $-th power of the ideal $ I $, and $ I^{n+1} $ is the $ (n+1) $-th power. The equivalence is constructed via the natural quotient maps and the canonical inclusion of $ I^n $ into $ R $.

Ideal.powQuotPowSuccEquivMapMkPowSuccPow definition

 : ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃ Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)

Full source

/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the equivalence between the two, instead of the `R`-linear equivalence,
to bypass typeclass synthesis issues on complex `Module` goals. -/
noncomputable
def powQuotPowSuccEquivMapMkPowSuccPow :
    ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃
    Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) :=
  powQuotPowSuccLinearEquivMapMkPowSuccPow I n

Equivalence between $ I^n / I^{n+1} $ and its image in $ R / I^{n+1} $

Informal description

For a commutative ring $ R $ and an ideal $ I $ of $ R $, there is a canonical equivalence between the quotient module $ I^n / I^{n+1} $ and the image of $ I^n $ under the quotient map $ R \to R/I^{n+1} $. Here, $ I^n $ denotes the $ n $-th power of the ideal $ I $, and $ I^{n+1} $ is the $ (n+1) $-th power. This equivalence bypasses typeclass synthesis issues by avoiding the use of $ R $-linear equivalence.

Main results: