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 #
Ideal.instHasQuotient
: the quotient of a commutative ringR
by an idealI : Ideal R
Ideal.Quotient.commRing
: the ring structure of the ideal quotientIdeal.Quotient.mk
: map an element ofR
to the quotientR ⧸ I
Ideal.Quotient.lift
: turn a mapR → S
into a mapR ⧸ I → S
Ideal.quotEquivOfEq
: quotienting by equal ideals gives isomorphic rings
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
.
Equations
Shortcut instance for commutative rings.
Equations
Equations
Equations
The ring homomorphism from a ring R
to a quotient ring R/I
.
Equations
Instances For
Equations
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].
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
.
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
.
Equations
Instances For
Quotienting by equal ideals gives equivalent rings.
See also Submodule.quotEquivOfEq
and Ideal.quotientEquivAlgOfEq
.