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 non-commutative rings.
Main definitions #
theorem
Ideal.Quotient.isScalarTower_right
{R : Type u}
[CommRing R]
{I : Ideal R}
{α : Type u_1}
[SMul α R]
[IsScalarTower α R R]
:
IsScalarTower α (R ⧸ I) (R ⧸ I)
theorem
Ideal.Quotient.smulCommClass
{R : Type u}
[CommRing R]
{I : Ideal R}
{α : Type u_1}
[SMul α R]
[IsScalarTower α R R]
[SMulCommClass α R R]
:
SMulCommClass α (R ⧸ I) (R ⧸ I)
theorem
Ideal.Quotient.smulCommClass'
{R : Type u}
[CommRing R]
{I : Ideal R}
{α : Type u_1}
[SMul α R]
[IsScalarTower α R R]
[SMulCommClass R α R]
:
SMulCommClass (R ⧸ I) α (R ⧸ I)
theorem
Ideal.Quotient.eq_zero_iff_dvd
{R : Type u}
[CommRing R]
(x y : R)
:
(Ideal.Quotient.mk (Ideal.span {x})) y = 0 ↔ x ∣ y
@[simp]
theorem
Ideal.Quotient.mk_singleton_self
{R : Type u}
[CommRing R]
(x : R)
:
(Ideal.Quotient.mk (Ideal.span {x})) x = 0
theorem
Ideal.Quotient.nontrivial
{R : Type u}
[CommRing R]
{I : Ideal R}
(hI : I ≠ ⊤)
:
Nontrivial (R ⧸ I)
theorem
Ideal.Quotient.subsingleton_iff
{R : Type u}
[CommRing R]
{I : Ideal R}
:
Subsingleton (R ⧸ I) ↔ I = ⊤
theorem
Ideal.Quotient.noZeroDivisors
{R : Type u}
[CommRing R]
(I : Ideal R)
[hI : I.IsPrime]
:
NoZeroDivisors (R ⧸ I)
@[reducible, inline]
noncomputable abbrev
Ideal.Quotient.groupWithZero
{R : Type u}
[CommRing R]
(I : Ideal R)
[hI : I.IsMaximal]
:
GroupWithZero (R ⧸ I)
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].
Equations
- Ideal.Quotient.groupWithZero I = GroupWithZero.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯
Instances For
@[reducible, inline]
The quotient 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].
Equations
Instances For
theorem
Ideal.univ_eq_iUnion_image_add
{R : Type u_1}
[Ring R]
(I : Ideal R)
:
Set.univ = ⋃ (x : R ⧸ I), Quotient.out x +ᵥ ↑I
A ring is made up of a disjoint union of cosets of an ideal.