Ideal.IsNilpotent.induction_on

theorem Ideal.IsNilpotent.induction_on : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommRing S] [inst : Algebra R S] (I : Ideal S), IsNilpotent I → ∀ {P : ⦃S : Type u_2⦄ → [inst : CommRing S] → Ideal S → Prop}, (∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I) → (∀ ⦃S : Type u_2⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (Ideal.map (Ideal.Quotient.mk I) J) → P J) → P I

This theorem is a principle of induction on nilpotent ideals. Given a property `P` on ideals in a commutative ring `S`, if `P` holds for all square-zero ideals and whenever `P` holds for an ideal `I` and the quotient `J/I`, it also holds for `J`, then `P` holds for all nilpotent ideals. In more detail, assume that we have a commutative semiring `R`, a commutative ring `S`, and `R` is an algebra over `S`. For a given ideal `I` in `S` that is nilpotent (i.e., some power of it equals zero), and a property `P` on ideals in `S`, the following two conditions are required: 1. `P` holds for all square-zero ideals in `S`. A square-zero ideal is an ideal `I` such that when you square it (in the sense of ideal multiplication), you get the zero ideal. 2. For any two ideals `I` and `J` in `S` where `I` is a subset of `J`, if the property `P` holds for `I` and the ideal obtained by mapping `J` to the quotient ring `J/I` via the natural projection, then `P` also holds for `J`. If these conditions are satisfied, then this theorem asserts that the property `P` holds for the given nilpotent ideal `I`.

More concisely: If a property holds for all square-zero ideals and is preserved under quotients, then it holds for all nilpotent ideals.