Nonzero representatives of residue classes #
Ideal.Quotient.mk_surjective produces some representative of a class in R ⧸ I, with no
control over it. Modulo a nonzero two-sided ideal the representative can be chosen nonzero: a
representative that happens to vanish is corrected by a nonzero element of the ideal, which does
not change its class. This is what a residue class needs before its representative can be
inverted in an appropriate fraction field.
Main results #
Ideal.Quotient.exists_ne_zero_mk_eq: every residue class modulo a nonzero ideal is the class of a nonzero element.
theorem
Ideal.Quotient.exists_ne_zero_mk_eq
{R : Type u_1}
[Ring R]
{I : Ideal R}
[I.IsTwoSided]
(hI : I ≠ ⊥)
(y : R ⧸ I)
:
A nonzero ideal has a nonzero representative for every residue class. A representative that happens to vanish can be corrected by a nonzero element of the ideal.