English
Let s be a subset of A. Consider the algebra A generated by s. If a predicate P(x,y) on pairs (x,y) with x,y in adjoin R s holds for all pairs drawn from s and is preserved under the natural algebraic operations (algebra maps from R, addition, and multiplication on both sides), then P(x,y) holds for all x,y in adjoin R s. In other words, to prove a property for all elements generated by s, it suffices to prove it for generators and ensure closure under the algebraic operations.
Русский
Пусть s — подмножество A. Рассмотрим порождаемую над R алгебру adjoin R s. Если предикат P(x,y) над парами (x,y) с x,y ∈ adjoin R s выполняется для всех пар, полученных из элементов s, и сохраняется при естественных алгебраических операциях (гомоморфизмы по R, сложение и умножение слева и справа), то P(x,y) выполняется для всех x,y ∈ adjoin R s. Другими словами, чтобы доказать свойство для всех элементов, порожденных s, достаточно проверить его на генераторах и обеспечить замкнутость относительно операции.
LaTeX
$$$\\forall {s : \\text{Set} A} \\; \\forall p : (x,y : A) \\to x \\in \\operatorname{adjoin} R\\,s \\to y \\in \\operatorname{adjoin} R\\,s \\to \\operatorname{Prop}, \n\\text{(base and closure hypotheses)} \\Rightarrow \\forall {x y}, x \\in \\operatorname{adjoin} R\\,s \\to y \\in \\operatorname{adjoin} R\\,s \\to p x y$,$$
Lean4
/-- Induction principle for the algebra generated by a set `s`: show that `p x y` holds for any
`x y ∈ adjoin R s` given that it holds for `x y ∈ s` and that it satisfies a number of
natural properties. -/
@[elab_as_elim]
theorem adjoin_induction₂ {s : Set A} {p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop}
(mem_mem : ∀ (x) (y) (hx : x ∈ s) (hy : y ∈ s), p x y (subset_adjoin hx) (subset_adjoin hy))
(algebraMap_both : ∀ r₁ r₂, p (algebraMap R A r₁) (algebraMap R A r₂) (algebraMap_mem _ r₁) (algebraMap_mem _ r₂))
(algebraMap_left : ∀ (r) (x) (hx : x ∈ s), p (algebraMap R A r) x (algebraMap_mem _ r) (subset_adjoin hx))
(algebraMap_right : ∀ (r) (x) (hx : x ∈ s), p x (algebraMap R A r) (subset_adjoin hx) (algebraMap_mem _ r))
(add_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x + y) z (add_mem hx hy) hz)
(add_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y + z) hx (add_mem hy hz))
(mul_left : ∀ x y z hx hy hz, p x z hx hz → p y z hy hz → p (x * y) z (mul_mem hx hy) hz)
(mul_right : ∀ x y z hx hy hz, p x y hx hy → p x z hx hz → p x (y * z) hx (mul_mem hy hz)) {x y : A}
(hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) : p x y hx hy := by
induction hy using adjoin_induction with
| mem z hz =>
induction hx using adjoin_induction with
| mem _ h => exact mem_mem _ _ h hz
| algebraMap _ => exact algebraMap_left _ _ hz
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| algebraMap r =>
induction hx using adjoin_induction with
| mem _ h => exact algebraMap_right _ _ h
| algebraMap _ => exact algebraMap_both _ _
| mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
| mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
