English
Let R be a ring and I an ideal. For every n > 0 and every a in R / I^(n+1), if the image of a under the natural projection to R / I^n is a unit, then a is a unit in R / I^(n+1).
Русский
Пусть R — кольцо, I — идеал. Для любого n > 0 и элемента a ∈ R / I^(n+1), если образ a в R / I^n является единицей, то a является единицей в R / I^(n+1).
LaTeX
$$$\\forall \\text{R ring}, \\forall I \\text{ ideal in } R,\\ \\forall n \\in \\mathbb{N}, n > 0,\\ \\forall a \\in R / I^{n+1},\\; \\pi_n(a) \\in (R / I^{n})^{\\times} \\Rightarrow a \\in (R / I^{n+1})^{\\times}$$$
Lean4
theorem isUnit_of_isUnit_image {n : ℕ} (npos : n > 0) {a : R ⧸ I ^ (n + 1)} (h : IsUnit (factorPow I n.le_succ a)) :
IsUnit a := by
rcases isUnit_iff_exists.mp h with ⟨b, hb, _⟩
rcases factor_surjective (pow_le_pow_right n.le_succ) b with ⟨b', hb'⟩
rw [← hb', ← map_one (factorPow I n.le_succ), ← map_mul] at hb
apply(RingHom.sub_mem_ker_iff (factorPow I n.le_succ)).mpr at hb
rw [factor_ker (pow_le_pow_right n.le_succ)] at hb
rcases Ideal.mem_image_of_mem_map_of_surjective (Ideal.Quotient.mk (I ^ (n + 1))) Ideal.Quotient.mk_surjective hb with
⟨c, hc, eq⟩
apply isUnit_of_mul_eq_one _ (b' * (1 - ((Ideal.Quotient.mk (I ^ (n + 1))) c)))
calc
_ = (a * b' - 1) * (1 - ((Ideal.Quotient.mk (I ^ (n + 1))) c)) + (1 - ((Ideal.Quotient.mk (I ^ (n + 1))) c)) := by
ring
_ = 1 :=
by
rw [← eq, mul_sub, mul_one, sub_add_sub_cancel', sub_eq_self, ← map_mul, Ideal.Quotient.eq_zero_iff_mem, pow_add]
apply Ideal.mul_mem_mul hc (Ideal.mul_le_left (I := I ^ (n - 1)) _)
simpa only [← pow_add, Nat.sub_add_cancel npos] using hc
