English
If I is a nilpotent ideal and P is a property of ideals such that P(I^2 = 0) and P(I) and P(J) imply P(J) for I ≤ J, then P(I) holds.
Русский
Если I нильпотентный идеал, а P — свойство идеалов, удовлетворяющее условиям для степеней и расширения, тогда P(I) выполняется.
LaTeX
$$$$ ext{IsNilpotent}(I) \Rightarrow [P(I^2 = 0) \,\&\, (I ≤ J) \Rightarrow P(I) \Rightarrow P(J)] \Rightarrow P(I).$$$$
Lean4
/-- Let `P` be a property on ideals. If `P` holds for square-zero ideals, and if
`P I → P (J ⧸ I) → P J`, then `P` holds for all nilpotent ideals. -/
theorem induction_on (hI : IsNilpotent I) {P : ∀ ⦃S : Type _⦄ [CommRing S], Ideal S → Prop}
(h₁ : ∀ ⦃S : Type _⦄ [CommRing S], ∀ I : Ideal S, I ^ 2 = ⊥ → P I)
(h₂ : ∀ ⦃S : Type _⦄ [CommRing S], ∀ I J : Ideal S, I ≤ J → P I → P (J.map (Ideal.Quotient.mk I)) → P J) : P I :=
by
obtain ⟨n, hI : I ^ n = ⊥⟩ := hI
induction n using Nat.strong_induction_on generalizing S with
| _ n H
by_cases hI' : I = ⊥
· subst hI'
apply h₁
rw [← Ideal.zero_eq_bot, zero_pow two_ne_zero]
rcases n with - | n
· rw [pow_zero, Ideal.one_eq_top] at hI
haveI := subsingleton_of_bot_eq_top hI.symm
exact (hI' (Subsingleton.elim _ _)).elim
rcases n with - | n
· rw [pow_one] at hI
exact (hI' hI).elim
apply h₂ (I ^ 2) _ (Ideal.pow_le_self two_ne_zero)
· apply H n.succ _ (I ^ 2)
· rw [← pow_mul, eq_bot_iff, ← hI, Nat.succ_eq_add_one]
apply Ideal.pow_le_pow_right (by cutsat)
· exact n.succ.lt_succ_self
· apply h₁
rw [← Ideal.map_pow, Ideal.map_quotient_self]
