English
Let s be a subset of A and let p be a property on the subalgebra adjoin R s. If p holds for every generator ⟨x, h⟩ with x ∈ s, is preserved under algebra maps, addition, multiplication, and star, and holds for all elements coming from scalars via algebra maps, then p holds for every element of adjoin R s.
Русский
Пусть s ⊆ A и пусть P — свойство для элементов подалгебры adjoin R s. Если P выполняется для каждого генератора ⟨x, h⟩ с x ∈ s, свойство сохраняется под алгебраическими отображениями, сложением, умножением и заменой на сон, а также выполняется для скалярных изображений через алгебраические отображения, тогда P выполняется для каждого элемента adjoin R s.
LaTeX
$$$\forall s \subseteq A, \forall p: (\mathrm{adjoin}\; R\, s) \to \mathrm{Prop}, \forall a\in \mathrm{adjoin}\; R\, s,\bigg(\Big(\forall x\in s, p(\langle x, \subseteq \mathrm{adjoin}\; R\, s\ h\rangle)\Big)\land\Big(\forall r\in R, p(\mathrm{algebraMap}\; R\, A\; r)\Big) \land\Big(\forall x,y, p(x) \Rightarrow p(y) \Rightarrow p(x+y)\Big) \land\Big(\forall x,y, p(x) \Rightarrow p(y) \Rightarrow p(x\cdot y)\Big) \land\Big(\forall x, p(x) \Rightarrow p(\star x)\Big)\bigg) \Rightarrow p(a).$$
Lean4
/-- The difference with `StarSubalgebra.adjoin_induction` is that this acts on the subtype. -/
@[elab_as_elim]
theorem adjoin_induction_subtype {s : Set A} {p : adjoin R s → Prop} (a : adjoin R s)
(mem : ∀ (x) (h : x ∈ s), p ⟨x, subset_adjoin R s h⟩) (algebraMap : ∀ r, p (algebraMap R _ r))
(add : ∀ x y, p x → p y → p (x + y)) (mul : ∀ x y, p x → p y → p (x * y)) (star : ∀ x, p x → p (star x)) : p a :=
Subtype.recOn a fun b hb => by
induction hb using adjoin_induction with
| mem _ h => exact mem _ h
| algebraMap _ => exact algebraMap _
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂
| star _ _ h => exact star _ h
