doc-next-gen

Mathlib.RingTheory.Ideal.Quotient.Basic

Module docstring

{"# Ideal quotients

This file defines ideal quotients as a special case of submodule quotients and proves some basic results about these quotients.

See Algebra.RingQuot for quotients of semirings.

Main definitions

  • Ideal.Quotient.Ring: the quotient of a ring R by a two-sided ideal I : Ideal R

"}

Ideal.Quotient.zero_eq_one_iff theorem
: (0 : R ⧸ I) = 1 ↔ I = ⊤
Full source 
theorem zero_eq_one_iff : (0 : R ⧸ I) = 1 ↔ I = ⊤ :=
  eq_comm.trans <| (Submodule.Quotient.mk_eq_zero _).trans (eq_top_iff_one _).symm
Zero Equals One in Quotient Ring if and only if Ideal is Improper
Informal description
For any commutative ring $R$ and ideal $I$ of $R$, the zero and one elements in the quotient ring $R ⧸ I$ are equal if and only if $I$ is the improper ideal (i.e., $I = R$).
Ideal.Quotient.zero_ne_one_iff theorem
: (0 : R ⧸ I) ≠ 1 ↔ I ≠ ⊤
Full source 
theorem zero_ne_one_iff : (0 : R ⧸ I) ≠ 1(0 : R ⧸ I) ≠ 1 ↔ I ≠ ⊤ :=
  not_congr zero_eq_one_iff
Distinctness of Zero and One in Quotient Ring Characterizes Proper Ideals
Informal description
For any commutative ring $R$ and ideal $I$ of $R$, the zero and one elements in the quotient ring $R ⧸ I$ are distinct if and only if $I$ is a proper ideal (i.e., $I \neq R$).
Ideal.Quotient.nontrivial theorem
(hI : I ≠ ⊤) : Nontrivial (R ⧸ I)
Full source 
protected theorem nontrivial (hI : I ≠ ⊤) : Nontrivial (R ⧸ I) :=
  ⟨⟨0, 1, zero_ne_one_iff.2 hI⟩⟩
Nontriviality of Quotient Ring by Proper Ideal
Informal description
For any commutative ring $R$ and proper ideal $I$ of $R$ (i.e., $I \neq R$), the quotient ring $R ⧸ I$ is nontrivial (i.e., contains at least two distinct elements).
Ideal.Quotient.isScalarTower_right instance
{α} [SMul α R] [IsScalarTower α R R] : IsScalarTower α (R ⧸ I) (R ⧸ I)
Full source 
instance (priority := 100) isScalarTower_right {α} [SMul α R] [IsScalarTower α R R] :
    IsScalarTower α (R ⧸ I) (R ⧸ I) :=
  (Quotient.ringCon I).isScalarTower_right
Scalar Multiplication Compatibility in Quotient Rings by Ideals
Informal description
For any ring $R$ with a scalar multiplication operation by elements of type $\alpha$ that is compatible with the ring multiplication (i.e., $a \cdot (x \cdot y) = (a \cdot x) \cdot y$ for all $a \in \alpha$ and $x, y \in R$), and any two-sided ideal $I$ of $R$, the quotient ring $R/I$ inherits a compatible scalar multiplication operation where $a \cdot ([x] \cdot [y]) = (a \cdot [x]) \cdot [y]$ for all $a \in \alpha$ and equivalence classes $[x], [y] \in R/I$.
Ideal.Quotient.smulCommClass instance
{α} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] : SMulCommClass α (R ⧸ I) (R ⧸ I)
Full source 
instance smulCommClass {α} [SMul α R] [IsScalarTower α R R] [SMulCommClass α R R] :
    SMulCommClass α (R ⧸ I) (R ⧸ I) :=
  (Quotient.ringCon I).smulCommClass
Commutativity of Scalar Multiplication on Quotient Rings
Informal description
For any ring $R$ with a scalar multiplication operation by elements of type $\alpha$, if the scalar multiplication on $R$ is commutative (i.e., $a \cdot (x \cdot y) = x \cdot (a \cdot y)$ for all $a \in \alpha$ and $x, y \in R$), then the induced scalar multiplication on the quotient ring $R/I$ is also commutative.
Ideal.Quotient.smulCommClass' instance
{α} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] : SMulCommClass (R ⧸ I) α (R ⧸ I)
Full source 
instance smulCommClass' {α} [SMul α R] [IsScalarTower α R R] [SMulCommClass R α R] :
    SMulCommClass (R ⧸ I) α (R ⧸ I) :=
  (Quotient.ringCon I).smulCommClass'
Commutative Scalar Multiplication on Quotient Rings
Informal description
For any ring $R$ with a two-sided ideal $I$, and any scalar action of a type $\alpha$ on $R$ that satisfies the conditions of being a scalar tower and having commutative scalar multiplication (i.e., $r \cdot (a \cdot s) = a \cdot (r \cdot s)$ for all $a \in \alpha$ and $r, s \in R$), the quotient ring $R ⧸ I$ inherits a commutative scalar multiplication operation from $\alpha$.
Ideal.Quotient.mk_singleton_self theorem
(x : R) [(Ideal.span { x }).IsTwoSided] : mk (Ideal.span { x }) x = 0
Full source 
@[simp]
lemma mk_singleton_self (x : R) [(Ideal.span {x}).IsTwoSided] : mk (Ideal.span {x}) x = 0 :=
  (Submodule.Quotient.mk_eq_zero _).mpr (mem_span_singleton_self _)
Quotient by Principal Ideal Maps Generator to Zero
Informal description
For any element $x$ in a ring $R$ such that the ideal generated by $\{x\}$ is two-sided, the equivalence class of $x$ in the quotient ring $R ⧸ (x)$ is equal to zero, i.e., $[x] = 0$.
Ideal.Quotient.noZeroDivisors instance
[hI : I.IsPrime] : NoZeroDivisors (R ⧸ I)
Full source 
instance noZeroDivisors [hI : I.IsPrime] : NoZeroDivisors (R ⧸ I) where
    eq_zero_or_eq_zero_of_mul_eq_zero {a b} := Quotient.inductionOn₂' a b fun {_ _} hab =>
      (hI.mem_or_mem (eq_zero_iff_mem.1 hab)).elim (Or.inlOr.inl ∘ eq_zero_iff_mem.2)
        (Or.inrOr.inr ∘ eq_zero_iff_mem.2)
Quotient Ring by Prime Ideal has No Zero Divisors
Informal description
For any commutative ring $R$ and any prime ideal $I$ of $R$, the quotient ring $R/I$ has no zero divisors.
Ideal.Quotient.isDomain_iff_prime theorem
: IsDomain (R ⧸ I) ↔ I.IsPrime
Full source 
theorem isDomain_iff_prime : IsDomainIsDomain (R ⧸ I) ↔ I.IsPrime := by
  refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
  · haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
    exact zero_ne_one
  · simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
    haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
    exact eq_zero_or_eq_zero_of_mul_eq_zero h
Quotient Ring is Integral Domain iff Ideal is Prime
Informal description
The quotient ring $R/I$ is an integral domain if and only if the ideal $I$ is prime.
Ideal.Quotient.exists_inv theorem
[hI : I.IsMaximal] : ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b : R ⧸ I, a * b = 1
Full source 
theorem exists_inv [hI : I.IsMaximal] :
    ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b : R ⧸ I, a * b = 1 := by
  apply exists_right_inv_of_exists_left_inv
  rintro ⟨a⟩ h
  rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
  refine ⟨mk _ b, Quot.sound ?_⟩
  simp only [Submodule.quotientRel_def]
  rw [← eq_sub_iff_add_eq'] at abc
  rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc
Existence of Multiplicative Inverses in Quotient by Maximal Ideal
Informal description
For any maximal ideal $I$ of a commutative ring $R$ and any nonzero element $a$ in the quotient ring $R/I$, there exists an element $b$ in $R/I$ such that $a \cdot b = 1$.
Ideal.Quotient.groupWithZero abbrev
[hI : I.IsMaximal] : GroupWithZero (R ⧸ I)
Full source 
/-- The quotient by a maximal ideal is a group with zero. This is a `def` rather than `instance`,
since users will have computable inverses in some applications.

See note [reducible non-instances]. -/
protected noncomputable abbrev groupWithZero [hI : I.IsMaximal] :
    GroupWithZero (R ⧸ I) := fast_instance%
  { inv := fun a => if ha : a = 0 then 0 else Classical.choose (exists_inv ha)
    mul_inv_cancel := fun a (ha : a ≠ 0) =>
      show a * dite _ _ _ = _ by rw [dif_neg ha]; exact Classical.choose_spec (exists_inv ha)
    inv_zero := dif_pos rfl
    __ := Quotient.nontrivial hI.out.1 }
Quotient Ring by Maximal Ideal is a Group with Zero
Informal description
For any commutative ring $R$ and any maximal ideal $I$ of $R$, the quotient ring $R/I$ forms a group with zero, meaning it has a multiplicative group structure on its nonzero elements and satisfies the axioms of a group with zero.
Ideal.Quotient.divisionRing abbrev
[I.IsMaximal] : DivisionRing (R ⧸ I)
Full source 
/-- The quotient by a two-sided ideal that is maximal as a left ideal is a division ring.
This is a `def` rather than `instance`, since users
will have computable inverses (and `qsmul`, `ratCast`) in some applications.

See note [reducible non-instances]. -/
protected noncomputable abbrev divisionRing [I.IsMaximal] : DivisionRing (R ⧸ I) := fast_instance%
  { __ := ring _
    __ := Quotient.groupWithZero _
    nnqsmul := _
    nnqsmul_def _ _ := rfl
    qsmul := _
    qsmul_def _ _ := rfl }
Quotient by Maximal Ideal Yields Division Ring
Informal description
For any ring $R$ and any maximal two-sided ideal $I$ of $R$, the quotient ring $R/I$ forms a division ring.
Ideal.Quotient.field abbrev
{R} [CommRing R] (I : Ideal R) [I.IsMaximal] : Field (R ⧸ I)
Full source 
/-- The quotient of a commutative ring by a maximal ideal is a field.
This is a `def` rather than `instance`, since users
will have computable inverses (and `qsmul`, `ratCast`) in some applications.

See note [reducible non-instances]. -/
protected noncomputable abbrev field {R} [CommRing R] (I : Ideal R) [I.IsMaximal] :
    Field (R ⧸ I) := fast_instance%
  { __ := commRing _
    __ := Quotient.divisionRing I }
Quotient of Commutative Ring by Maximal Ideal is a Field
Informal description
For any commutative ring $R$ and any maximal ideal $I$ of $R$, the quotient ring $R/I$ is a field.
Ideal.Quotient.maximal_of_isField theorem
{R} [CommRing R] (I : Ideal R) (hqf : IsField (R ⧸ I)) : I.IsMaximal
Full source 
/-- If the quotient by an ideal is a field, then the ideal is maximal. -/
theorem maximal_of_isField {R} [CommRing R] (I : Ideal R) (hqf : IsField (R ⧸ I)) :
    I.IsMaximal := by
  apply Ideal.isMaximal_iff.2
  constructor
  · intro h
    rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
    exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))
  · intro J x hIJ hxnI hxJ
    rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
    rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
    exact J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))
Maximality of Ideal When Quotient is a Field
Informal description
Let $R$ be a commutative ring and $I$ an ideal of $R$. If the quotient ring $R/I$ is a field, then $I$ is a maximal ideal.
Ideal.Quotient.maximal_ideal_iff_isField_quotient theorem
{R} [CommRing R] (I : Ideal R) : I.IsMaximal ↔ IsField (R ⧸ I)
Full source 
/-- The quotient of a ring by an ideal is a field iff the ideal is maximal. -/
theorem maximal_ideal_iff_isField_quotient {R} [CommRing R] (I : Ideal R) :
    I.IsMaximal ↔ IsField (R ⧸ I) :=
  ⟨fun h =>
    let _i := @Quotient.field _ _ I h
    Field.toIsField _,
    maximal_of_isField _⟩
Maximal Ideal Characterization via Field Quotient
Informal description
Let $R$ be a commutative ring and $I$ an ideal of $R$. Then $I$ is a maximal ideal if and only if the quotient ring $R/I$ is a field.
Ideal.modulePi instance
[I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun _ ↦ I)
Full source 
/-- `R^n/I^n` is a `R/I`-module. -/
instance modulePi [I.IsTwoSided] : Module (R ⧸ I) ((ι → R) ⧸ pi fun _ ↦ I) where
  smul c m :=
    Quotient.liftOn₂' c m (fun r m ↦ Submodule.Quotient.mk <| r • m) <| by
      intro c₁ m₁ c₂ m₂ hc hm
      apply Ideal.Quotient.eq.2
      rw [Submodule.quotientRel_def] at hc hm
      intro i
      exact I.mul_sub_mul_mem hc (hm i)
  one_smul := by rintro ⟨a⟩; exact congr_arg _ (one_smul _ _)
  mul_smul := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (mul_smul _ _ _)
  smul_add := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (smul_add _ _ _)
  smul_zero := by rintro ⟨a⟩; exact congr_arg _ (smul_zero _)
  add_smul := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; exact congr_arg _ (add_smul _ _ _)
  zero_smul := by rintro ⟨a⟩; exact congr_arg _ (zero_smul _ _)
Module Structure on Function Space Quotient by Ideal
Informal description
For any ring $R$ with a two-sided ideal $I$ and any index type $\iota$, the quotient module $(\iota \to R) ⧸ (\prod_{\_} I)$ is a module over the quotient ring $R ⧸ I$. Here, $\prod_{\_} I$ denotes the ideal of functions in $\iota \to R$ where each component lies in $I$.
Ideal.piQuotEquiv definition
[I.IsTwoSided] : ((ι → R) ⧸ pi fun _ ↦ I) ≃ₗ[R ⧸ I] ι → (R ⧸ I)
Full source 
/-- `R^n/I^n` is isomorphic to `(R/I)^n` as an `R/I`-module. -/
noncomputable def piQuotEquiv [I.IsTwoSided] : ((ι → R) ⧸ pi fun _ ↦ I) ≃ₗ[R ⧸ I] ι → (R ⧸ I) where
  toFun x := Quotient.liftOn' x (fun f i ↦ Ideal.Quotient.mk I (f i)) fun _ _ hab ↦
    funext fun i ↦ (Submodule.Quotient.eq' _).2 (QuotientAddGroup.leftRel_apply.mp hab i)
  map_add' := by rintro ⟨_⟩ ⟨_⟩; rfl
  map_smul' := by rintro ⟨_⟩ ⟨_⟩; rfl
  invFun x := Ideal.Quotient.mk _ (Quotient.out <| x ·)
  left_inv := by
    rintro ⟨x⟩
    exact Ideal.Quotient.eq.2 fun i ↦ Ideal.Quotient.eq.1 (Quotient.out_eq' _)
  right_inv x := funext fun i ↦ Quotient.out_eq' (x i)
Linear equivalence between function space quotient and quotient function space
Informal description
For a ring \( R \) with a two-sided ideal \( I \) and an index type \( \iota \), there is a linear equivalence between the quotient module \( (\iota \to R) ⧸ (\prod_{\_} I) \) and the function space \( \iota \to (R ⧸ I) \). This equivalence maps an equivalence class \( [f] \) in the quotient to the function \( i \mapsto [f(i)] \) in \( \iota \to (R ⧸ I) \), and its inverse maps a function \( g \) in \( \iota \to (R ⧸ I) \) to the equivalence class of any lift of \( g \) to \( \iota \to R \).
Ideal.map_pi theorem
[I.IsTwoSided] {ι : Type*} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I) (f : (ι → R) →ₗ[R] ι' → R) (i : ι') : f x i ∈ I
Full source 
/-- If `f : R^n → R^m` is an `R`-linear map and `I ⊆ R` is an ideal, then the image of `I^n` is
    contained in `I^m`. -/
theorem map_pi [I.IsTwoSided] {ι : Type*} [Finite ι] {ι' : Type w} (x : ι → R) (hi : ∀ i, x i ∈ I)
    (f : (ι → R) →ₗ[R] ι' → R) (i : ι') : f x i ∈ I := by
  classical
    cases nonempty_fintype ι
    rw [pi_eq_sum_univ x]
    simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
    exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)
Linear Maps Preserve Ideal Membership in Function Spaces
Informal description
Let $R$ be a ring with a two-sided ideal $I \subseteq R$, and let $\iota$ be a finite type. For any tuple $x \in \iota \to R$ where each component $x_i \in I$, and any $R$-linear map $f \colon (\iota \to R) \to (\iota' \to R)$, the $i$-th component of the image $f(x)$ lies in $I$ for any $i \in \iota'$.
Ideal.univ_eq_iUnion_image_add theorem
: (Set.univ (α := R)) = ⋃ x : R ⧸ I, x.out +ᵥ (I : Set R)
Full source 
/-- A ring is made up of a disjoint union of cosets of an ideal. -/
lemma univ_eq_iUnion_image_add : (Set.univ (α := R)) = ⋃ x : R ⧸ I, x.out +ᵥ (I : Set R) :=
  QuotientAddGroup.univ_eq_iUnion_vadd I.toAddSubgroup
Decomposition of Ring into Cosets of Ideal
Informal description
For a commutative ring $R$ and an ideal $I \subseteq R$, the universal set of $R$ can be expressed as the union of all cosets of $I$ in $R$. More precisely, we have: $$ R = \bigcup_{x \in R/I} (x_{\text{out}} + I) $$ where $x_{\text{out}}$ is a representative of the equivalence class $x$ in the quotient ring $R/I$, and $x_{\text{out}} + I$ denotes the coset of $I$ with respect to $x_{\text{out}}$.