English
If I is nilpotent, then an element x is a unit modulo I iff x is a unit in R.
Русский
Если I нильпотент, то элемент x является единицей по модулю I тогда и только тогда, когда x — единица в R.
LaTeX
$$$$\text{IsUnit}(\overline{x}) \iff \text{IsUnit}(x) \quad\text{for } I \text{ nilpotent}.$$$$
Lean4
theorem isUnit_quotient_mk_iff {R : Type*} [CommRing R] {I : Ideal R} (hI : IsNilpotent I) {x : R} :
IsUnit (Ideal.Quotient.mk I x) ↔ IsUnit x :=
by
refine ⟨?_, fun h => h.map <| Ideal.Quotient.mk I⟩
revert x
apply Ideal.IsNilpotent.induction_on (S := R) I hI <;> clear hI I
swap
· introv e h₁ h₂ h₃
apply h₁
apply h₂
exact h₃.map ((DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq (sup_eq_right.mpr e))).symm.toRingHom
· introv e H
obtain ⟨y, hy⟩ := Ideal.Quotient.mk_surjective (↑H.unit⁻¹ : S ⧸ I)
have : Ideal.Quotient.mk I (x * y) = Ideal.Quotient.mk I 1 := by rw [map_one, map_mul, hy, IsUnit.mul_val_inv]
rw [Ideal.Quotient.eq] at this
have : (x * y - 1) ^ 2 = 0 := by
rw [← Ideal.mem_bot, ← e]
exact Ideal.pow_mem_pow this _
have : x * (y * (2 - x * y)) = 1 := by
rw [eq_comm, ← sub_eq_zero, ← this]
ring
exact isUnit_of_mul_eq_one _ _ this
