Mathlib.RingTheory.Ideal.Quotient.Defs

Ideal.instHasQuotient instance

: HasQuotient R (Ideal R)

Full source

/-- The quotient `R/I` of a ring `R` by an ideal `I`,
defined to equal the quotient of `I` as an `R`-submodule of `R`. -/
instance instHasQuotient : HasQuotient R (Ideal R) := Submodule.hasQuotient

Quotient Ring by an Ideal

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient $R ⧸ I$ is defined as the set of equivalence classes of elements of $R$ under the relation $x \sim y$ if and only if $x - y \in I$.

Ideal.instHasQuotient_1 instance

{R} [CommRing R] : HasQuotient R (Ideal R)

Full source

/-- Shortcut instance for commutative rings. -/
instance {R} [CommRing R] : HasQuotient R (Ideal R) := inferInstance

Quotient Ring by an Ideal in Commutative Rings

Informal description

For any commutative ring $R$, the quotient $R ⧸ I$ by an ideal $I$ of $R$ is well-defined.

Ideal.Quotient.one instance

(I : Ideal R) : One (R ⧸ I)

Full source

instance one (I : Ideal R) : One (R ⧸ I) :=
  ⟨Submodule.Quotient.mk 1⟩

Existence of One in Quotient Ring

Informal description

For any commutative ring $R$ and ideal $I$ of $R$, the quotient ring $R ⧸ I$ has a multiplicative identity element.

Ideal.Quotient.ringCon definition

(I : Ideal R) [I.IsTwoSided] : RingCon R

Full source

/-- On `Ideal`s, `Submodule.quotientRel` is a ring congruence. -/
protected def ringCon (I : Ideal R) [I.IsTwoSided] : RingCon R where
  __ := QuotientAddGroup.con I.toAddSubgroup
  mul' {a₁ b₁ a₂ b₂} h₁ h₂ := by
    rw [Submodule.quotientRel_def] at h₁ h₂ ⊢
    exact mul_sub_mul_mem I h₁ h₂

Ring congruence induced by an ideal

Informal description

Given a two-sided ideal $I$ of a ring $R$, the relation $\sim$ defined by $x \sim y$ if and only if $x - y \in I$ is a ring congruence. That is, it is an equivalence relation that preserves both addition and multiplication: if $x_1 \sim y_1$ and $x_2 \sim y_2$, then $x_1 + x_2 \sim y_1 + y_2$ and $x_1 \cdot x_2 \sim y_1 \cdot y_2$.

Ideal.Quotient.ring instance

(I : Ideal R) [I.IsTwoSided] : Ring (R ⧸ I)

Full source

instance ring (I : Ideal R) [I.IsTwoSided] : Ring (R ⧸ I) := fast_instance%
  { __ : AddCommGroup (R ⧸ I) := inferInstance
    __ : Ring (Quotient.ringCon I).Quotient := inferInstance }

Ring Structure on Quotient by Ideal

Informal description

For any ring $R$ and any two-sided ideal $I$ of $R$, the quotient $R ⧸ I$ inherits a ring structure from $R$.

Ideal.Quotient.commRing instance

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

Full source

instance commRing {R} [CommRing R] (I : Ideal R) : CommRing (R ⧸ I) := fast_instance%
  { mul_comm := by rintro ⟨a⟩ ⟨b⟩; exact congr_arg _ (mul_comm a b) }

Commutative Ring Structure on Quotient by Ideal

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient ring $R ⧸ I$ is a commutative ring.

Ideal.Quotient.instRingQuotient instance

{R} [CommRing R] (I : Ideal R) : Ring (R ⧸ I)

Full source

instance {R} [CommRing R] (I : Ideal R) : Ring (R ⧸ I) := fast_instance% inferInstance

Ring Structure on Quotient of Commutative Ring by Ideal

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient ring $R ⧸ I$ inherits a ring structure from $R$.

Ideal.Quotient.commSemiring instance

{R} [CommRing R] (I : Ideal R) : CommSemiring (R ⧸ I)

Full source

instance commSemiring {R} [CommRing R] (I : Ideal R) : CommSemiring (R ⧸ I) := fast_instance%
  inferInstance

Commutative Semiring Structure on Quotient by Ideal

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient ring $R ⧸ I$ is a commutative semiring.

Ideal.Quotient.semiring instance

{R} [CommRing R] (I : Ideal R) : Semiring (R ⧸ I)

Full source

instance semiring {R} [CommRing R] (I : Ideal R) : Semiring (R ⧸ I) := fast_instance% inferInstance

Semiring Structure on Quotient Ring by Ideal

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient ring $R ⧸ I$ is a semiring.

Ideal.Quotient.mk definition

: R →+* R ⧸ I

Full source

/-- The ring homomorphism from a ring `R` to a quotient ring `R/I`. -/
def mk : R →+* R ⧸ I where
  toFun a := Submodule.Quotient.mk a
  map_zero' := rfl
  map_one' := rfl
  map_mul' _ _ := rfl
  map_add' _ _ := rfl

Quotient map from a ring to its quotient ring

Informal description

The ring homomorphism from a commutative ring $ R $ to its quotient ring $ R/I $, mapping each element $ x \in R $ to its equivalence class $ [x] $ in $ R/I $. This map preserves the ring structure, i.e., it is additive and multiplicative and sends the multiplicative identity to the identity in the quotient.

Ideal.Quotient.instCoeQuotient instance

: Coe R (R ⧸ I)

Full source

instance : Coe R (R ⧸ I) :=
  ⟨Ideal.Quotient.mk I⟩

Canonical Map to Quotient Ring

Informal description

For any commutative ring $R$ and ideal $I$ of $R$, there is a canonical map from $R$ to the quotient ring $R ⧸ I$ that sends each element $x \in R$ to its equivalence class $[x] \in R ⧸ I$.

Ideal.Quotient.ringHom_ext theorem

[NonAssocSemiring S] ⦃f g : R ⧸ I →+* S⦄ (h : f.comp (mk I) = g.comp (mk I)) : f = g

Full source

/-- Two `RingHom`s from the quotient by an ideal are equal if their
compositions with `Ideal.Quotient.mk'` are equal.

See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem ringHom_ext [NonAssocSemiring S] ⦃f g : R ⧸ IR ⧸ I →+* S⦄ (h : f.comp (mk I) = g.comp (mk I)) :
    f = g :=
  RingHom.ext fun x => Quotient.inductionOn' x <| (RingHom.congr_fun h :)

Uniqueness of Ring Homomorphisms from Quotient Ring via Composition with Quotient Map

Informal description

Let $R$ be a commutative ring with an ideal $I$, and let $S$ be a non-associative semiring. For any two ring homomorphisms $f, g: R/I \to S$, if the compositions $f \circ \pi$ and $g \circ \pi$ are equal (where $\pi: R \to R/I$ is the canonical quotient map), then $f = g$.

Ideal.Quotient.instNonemptyQuotient instance

: Nonempty (R ⧸ I)

Full source

instance : Nonempty (R ⧸ I) :=
  ⟨mk I 37⟩

Nonemptiness of Quotient Rings

Informal description

For any commutative ring $R$ and any ideal $I$ of $R$, the quotient ring $R ⧸ I$ is nonempty.

Ideal.Quotient.eq theorem

: mk I x = mk I y ↔ x - y ∈ I

Full source

protected theorem eq : mkmk I x = mk I y ↔ x - y ∈ I :=
  Submodule.Quotient.eq I

Equivalence in Quotient Ring via Ideal Membership

Informal description

For any elements $x, y$ in a commutative ring $R$ and an ideal $I$ of $R$, the equivalence classes $[x]$ and $[y]$ in the quotient ring $R/I$ are equal if and only if their difference $x - y$ belongs to $I$.

Ideal.Quotient.mk_eq_mk theorem

(x : R) : (Submodule.Quotient.mk x : R ⧸ I) = mk I x

Full source

@[simp]
theorem mk_eq_mk (x : R) : (Submodule.Quotient.mk x : R ⧸ I) = mk I x := rfl

Equality of Quotient Maps: Module vs. Ring Quotient

Informal description

For any element $x$ in a commutative ring $R$ and any ideal $I$ of $R$, the equivalence class of $x$ in the quotient module $R ⧸ I$ (via `Submodule.Quotient.mk`) is equal to the equivalence class of $x$ in the quotient ring $R ⧸ I$ (via `Ideal.Quotient.mk`). In other words, $[x]_{R ⧸ I} = [x]_{R/I}$.

Ideal.Quotient.mk_eq_mk_iff_sub_mem theorem

(x y : R) : mk I x = mk I y ↔ x - y ∈ I

Full source

theorem mk_eq_mk_iff_sub_mem (x y : R) : mkmk I x = mk I y ↔ x - y ∈ I := by
  rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]

Equivalence of Quotient Elements via Ideal Membership

Informal description

For any elements $x, y$ in a commutative ring $R$ and any ideal $I$ of $R$, the equivalence classes of $x$ and $y$ in the quotient ring $R/I$ are equal if and only if their difference $x - y$ belongs to $I$. In other words, $[x] = [y]$ in $R/I$ if and only if $x - y \in I$.

Ideal.Quotient.mk_out theorem

(x : R ⧸ I) : Ideal.Quotient.mk I (Quotient.out x) = x

Full source

@[simp]
theorem mk_out (x : R ⧸ I) : Ideal.Quotient.mk I (Quotient.out x) = x :=
  Quotient.out_eq x

Quotient Representative Property: $\mathrm{mk}_I(\mathrm{out}(x)) = x$

Informal description

For any element $x$ in the quotient ring $R/I$, the image of its representative under the quotient map $\mathrm{mk}_I$ is equal to $x$ itself, i.e., $\mathrm{mk}_I(\mathrm{out}(x)) = x$.

Ideal.Quotient.mk_surjective theorem

: Function.Surjective (mk I)

Full source

theorem mk_surjective : Function.Surjective (mk I) := fun y =>
  Quotient.inductionOn' y fun x => Exists.intro x rfl

Surjectivity of the Quotient Ring Homomorphism

Informal description

The quotient map $\pi : R \to R/I$ from a commutative ring $R$ to its quotient ring $R/I$ by an ideal $I$ is surjective. That is, for every element $[x] \in R/I$, there exists an element $x \in R$ such that $\pi(x) = [x]$.

Ideal.Quotient.instRingHomSurjectiveQuotientMk instance

: RingHomSurjective (mk I)

Full source

instance : RingHomSurjective (mk I) :=
  ⟨mk_surjective⟩

Surjectivity of the Quotient Ring Homomorphism

Informal description

The quotient map $\pi : R \to R/I$ from a commutative ring $R$ to its quotient ring $R/I$ by an ideal $I$ is a surjective ring homomorphism.

Ideal.Quotient.quotient_ring_saturate theorem

(s : Set R) : mk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s

Full source

/-- If `I` is an ideal of a commutative ring `R`, if `q : R → R/I` is the quotient map, and if
`s ⊆ R` is a subset, then `q⁻¹(q(s)) = ⋃ᵢ(i + s)`, the union running over all `i ∈ I`. -/
theorem quotient_ring_saturate (s : Set R) :
    mkmk I ⁻¹' (mk I '' s) = ⋃ x : I, (fun y => x.1 + y) '' s := by
  ext x
  simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
  exact
    ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
      ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩

Preimage of Quotient Map Image Equals Union of Ideal Translates

Informal description

Let $I$ be an ideal of a commutative ring $R$, let $q : R \to R/I$ be the quotient map, and let $s \subseteq R$ be a subset. Then the preimage of the image of $s$ under $q$ is equal to the union of all translates of $s$ by elements of $I$, i.e., $$ q^{-1}(q(s)) = \bigcup_{i \in I} (i + s). $$

Ideal.Quotient.lift definition

(f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : R ⧸ I →+* S

Full source

/-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
lift it to the quotient by this ideal. -/
def lift (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : R ⧸ IR ⧸ I →+* S :=
  { QuotientAddGroup.lift I.toAddSubgroup f.toAddMonoidHom H with
    map_one' := f.map_one
    map_mul' := fun a₁ a₂ => Quotient.inductionOn₂' a₁ a₂ f.map_mul }

Lifting of ring homomorphism through quotient by ideal

Informal description

Given a ring homomorphism $f \colon R \to S$ that sends all elements of an ideal $I$ of $R$ to zero, there exists a unique ring homomorphism from the quotient ring $R/I$ to $S$ that lifts $f$.

Ideal.Quotient.lift_mk theorem

(f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : lift I f H (mk I a) = f a

Full source

@[simp]
theorem lift_mk (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) :
    lift I f H (mk I a) = f a :=
  rfl

Lifted Homomorphism Evaluates to Original on Quotient Elements

Informal description

Let $R$ and $S$ be commutative rings, $I$ an 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 $\text{lift}(I, f, H) \colon R/I \to S$ satisfies $\text{lift}(I, f, H)([a]) = f(a)$ for any $a \in R$, where $[a]$ denotes the equivalence class of $a$ in $R/I$.

Ideal.Quotient.lift_comp_mk theorem

(f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : (lift I f H).comp (mk I) = f

Full source

lemma lift_comp_mk (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) :
    (lift I f H).comp (mk I) = f := rfl

Composition of Lift and Quotient Map Equals Original Homomorphism

Informal description

Let $R$ and $S$ be commutative rings, $I$ an ideal of $R$, and $f \colon R \to S$ a ring homomorphism such that $f(a) = 0$ for all $a \in I$. Then the composition of the lifted homomorphism $\text{lift}(I, f, H) \colon R/I \to S$ with the quotient map $\text{mk}(I) \colon R \to R/I$ equals $f$, i.e., \[ \text{lift}(I, f, H) \circ \text{mk}(I) = f. \]

Ideal.Quotient.lift_surjective_of_surjective theorem

 {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0) (hf : Function.Surjective f) :
  Function.Surjective (Ideal.Quotient.lift I f H)

Full source

theorem lift_surjective_of_surjective {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
    (hf : Function.Surjective f) : Function.Surjective (Ideal.Quotient.lift I f H) := by
  intro y
  obtain ⟨x, rfl⟩ := hf y
  use Ideal.Quotient.mk I x
  simp only [Ideal.Quotient.lift_mk]

Surjectivity of Lifted Homomorphism in Quotient Ring

Informal description

Let $R$ and $S$ be commutative rings, $I$ an ideal of $R$, and $f \colon R \to S$ a surjective ring homomorphism such that $f(a) = 0$ for all $a \in I$. Then the induced homomorphism $\text{lift}(I, f, H) \colon R/I \to S$ is also surjective.

Ideal.Quotient.factor definition

(H : S ≤ T) : R ⧸ S →+* R ⧸ T

Full source

/-- The ring homomorphism from the quotient by a smaller ideal to the quotient by a larger ideal.

This is the `Ideal.Quotient` version of `Quot.Factor`

When the two ideals are of the form `I^m` and `I^n` and `n ≤ m`,
please refer to the dedicated version `Ideal.Quotient.factorPow`. -/
def factor (H : S ≤ T) : R ⧸ SR ⧸ S →+* R ⧸ T :=
  Ideal.Quotient.lift S (mk T) fun _ hx => eq_zero_iff_mem.2 (H hx)

Ring homomorphism between quotient rings induced by ideal inclusion

Informal description

Given a commutative ring $ R $ and two ideals $ S $ and $ T $ of $ R $ such that $ S \subseteq T $, the ring homomorphism $ \text{factor} $ from the quotient ring $ R/S $ to the quotient ring $ R/T $ maps each equivalence class $ [x]_S $ to $ [x]_T $. This homomorphism is well-defined because $ S \subseteq T $ ensures that the map respects the equivalence relations.

Ideal.Quotient.factor_mk theorem

(H : S ≤ T) (x : R) : factor H (mk S x) = mk T x

Full source

@[simp]
theorem factor_mk (H : S ≤ T) (x : R) : factor H (mk S x) = mk T x :=
  rfl

Commutativity of Quotient Maps: $\text{factor}(H)([x]_S) = [x]_T$

Informal description

Let $R$ be a commutative ring and $S, T$ be ideals of $R$ with $S \subseteq T$. For any element $x \in R$, the image of the equivalence class $[x]_S$ under the quotient map $\text{factor}(H) : R/S \to R/T$ equals the equivalence class $[x]_T$ in $R/T$.

Ideal.Quotient.factor_eq theorem

: factor (le_refl S) = RingHom.id _

Full source

@[simp]
theorem factor_eq : factor (le_refl S) = RingHom.id _ := by
  ext
  simp

Factor Homomorphism is Identity for Reflexive Ideal Inclusion

Informal description

For any commutative ring $R$ and any ideal $S$ of $R$, the ring homomorphism $\text{factor}$ from $R ⧸ S$ to itself induced by the reflexive relation $S \leq S$ is equal to the identity ring homomorphism on $R ⧸ S$.

Ideal.Quotient.factor_comp_mk theorem

(H : S ≤ T) : (factor H).comp (mk S) = mk T

Full source

@[simp]
theorem factor_comp_mk (H : S ≤ T) : (factor H).comp (mk S) = mk T := by
  ext x
  rw [RingHom.comp_apply, factor_mk]

Composition of Quotient Maps: $\text{factor}(H) \circ \text{mk}_S = \text{mk}_T$

Informal description

Let $R$ be a commutative ring and $S, T$ be ideals of $R$ with $S \subseteq T$. The composition of the quotient map $\text{factor}(H) : R/S \to R/T$ with the canonical projection $\text{mk}_S : R \to R/S$ equals the canonical projection $\text{mk}_T : R \to R/T$. In other words, for any $x \in R$, we have $\text{factor}(H)([x]_S) = [x]_T$.

Ideal.Quotient.factor_comp theorem

(H1 : S ≤ T) (H2 : T ≤ U) : (factor H2).comp (factor H1) = factor (H1.trans H2)

Full source

@[simp]
theorem factor_comp (H1 : S ≤ T) (H2 : T ≤ U) :
    (factor H2).comp (factor H1) = factor (H1.trans H2) := by
  ext
  simp

Composition of Quotient Maps via Ideal Inclusions: $\text{factor}(H_2) \circ \text{factor}(H_1) = \text{factor}(H_1 \circ H_2)$

Informal description

Let $R$ be a commutative ring and $S, T, U$ be ideals of $R$ such that $S \subseteq T \subseteq U$. The composition of the quotient maps $\text{factor}(H_1) : R/S \to R/T$ and $\text{factor}(H_2) : R/T \to R/U$ equals the quotient map $\text{factor}(H_1 \circ H_2) : R/S \to R/U$, where $H_1 \circ H_2$ denotes the inclusion $S \subseteq U$ obtained by transitivity.

Ideal.Quotient.factor_comp_apply theorem

(H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S) : factor H2 (factor H1 x) = factor (H1.trans H2) x

Full source

@[simp]
theorem factor_comp_apply (H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S) :
    factor H2 (factor H1 x) = factor (H1.trans H2) x := by
  rw [← RingHom.comp_apply]
  simp

Compatibility of Quotient Maps: $\text{factor}(H_2) \circ \text{factor}(H_1) = \text{factor}(H_1 \circ H_2)$ on Elements

Informal description

Let $R$ be a commutative ring and $S, T, U$ be ideals of $R$ such that $S \subseteq T \subseteq U$. For any element $x \in R/S$, the composition of the quotient maps $\text{factor}(H_1) : R/S \to R/T$ and $\text{factor}(H_2) : R/T \to R/U$ applied to $x$ equals the quotient map $\text{factor}(H_1 \circ H_2) : R/S \to R/U$ applied to $x$, where $H_1 \circ H_2$ denotes the inclusion $S \subseteq U$ obtained by transitivity.

Ideal.quotEquivOfEq definition

(h : I = J) : R ⧸ I ≃+* R ⧸ J

Full source

/-- Quotienting by equal ideals gives equivalent rings.

See also `Submodule.quotEquivOfEq` and `Ideal.quotientEquivAlgOfEq`.
-/
def quotEquivOfEq (h : I = J) : R ⧸ IR ⧸ I ≃+* R ⧸ J :=
  { Submodule.quotEquivOfEq I J h with
    map_mul' := by
      rintro ⟨x⟩ ⟨y⟩
      rfl }

Ring isomorphism of quotient rings by equal ideals

Informal description

Given a commutative ring $R$ and two ideals $I$ and $J$ of $R$ such that $I = J$, there exists a ring isomorphism between the quotient rings $R ⧸ I$ and $R ⧸ J$. This isomorphism maps each equivalence class $[x]_I$ in $R ⧸ I$ to the corresponding equivalence class $[x]_J$ in $R ⧸ J$.

Ideal.quotEquivOfEq_mk theorem

(h : I = J) (x : R) : quotEquivOfEq h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x

Full source

@[simp]
theorem quotEquivOfEq_mk (h : I = J) (x : R) :
    quotEquivOfEq h (Ideal.Quotient.mk I x) = Ideal.Quotient.mk J x :=
  rfl

Compatibility of Quotient Map with Isomorphism of Equal Ideals

Informal description

Let $R$ be a commutative ring and $I, J$ be ideals of $R$ such that $I = J$. For any element $x \in R$, the image of the equivalence class $[x]_I$ under the ring isomorphism $\text{quotEquivOfEq}\ h$ equals the equivalence class $[x]_J$ in the quotient ring $R/J$.

Ideal.quotEquivOfEq_symm theorem

(h : I = J) : (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq h.symm

Full source

@[simp]
theorem quotEquivOfEq_symm (h : I = J) :
    (Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq h.symm := by ext; rfl

Inverse of Ring Isomorphism Between Quotients by Equal Ideals

Informal description

Given a commutative ring $R$ and two ideals $I$ and $J$ of $R$ such that $I = J$, the inverse of the ring isomorphism $\text{quotEquivOfEq}\ h$ between $R ⧸ I$ and $R ⧸ J$ is equal to the ring isomorphism $\text{quotEquivOfEq}\ h^{-1}$ between $R ⧸ J$ and $R ⧸ I$, where $h^{-1}$ is the inverse equality $J = I$.

Main definitions