English
In a Noetherian setting, induction on adjoin proves that any property P holds for any subalgebra by extending by insertions.
Русский
В условиях Нётеровой теории индукция по adjoin доказывает, что свойство P выполняется для любой подалгебры при добавлении элементов.
LaTeX
$$$[IsNoetherian R A] (P) \\,\\to \\, (P(S) \\Rightarrow P(\\operatorname{adjoin}_R (\\text{insert } x S))) \\Rightarrow \\forall S, P(S)$$$
Lean4
theorem induction_on_adjoin [IsNoetherian R A] (P : Subalgebra R A → Prop) (base : P ⊥)
(ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x S))) (S : Subalgebra R A) : P S := by
classical
obtain ⟨t, rfl⟩ := S.fg_of_noetherian
refine Finset.induction_on t ?_ ?_
· simpa using base
intro x t _ h
rw [Finset.coe_insert]
simpa only [Algebra.adjoin_insert_adjoin] using ih _ x h
