English
Two continuous star-algebra homomorphisms from the elemental R a to B that agree on the generator a are equal.
Русский
Два непрерывных гомоморфизма звёздной алгебры из элементарной R a в B, которые совпадают на генераторе a, тождественны.
LaTeX
$$$\forall\phi,\psi:\, F,\; \text{Continuous }\phi, \text{Continuous }\psi:\; \phi\langle a,\,\text{self_mem }R a\rangle = \psi\langle a,\,\text{self_mem }R a\rangle \Rightarrow \phi = \psi$$$
Lean4
@[elab_as_elim]
theorem induction_on {x y : A} (hy : y ∈ elemental R x) {P : (u : A) → u ∈ elemental R x → Prop}
(self : P x (self_mem R x)) (star_self : P (star x) (star_self_mem R x))
(algebraMap : ∀ r, P (algebraMap R A r) (_root_.algebraMap_mem _ r))
(add : ∀ u hu v hv, P u hu → P v hv → P (u + v) (add_mem hu hv))
(mul : ∀ u hu v hv, P u hu → P v hv → P (u * v) (mul_mem hu hv))
(closure :
∀ s : Set A,
(hs : s ⊆ elemental R x) →
(∀ u, (hu : u ∈ s) → P u (hs hu)) → ∀ v, (hv : v ∈ closure s) → P v (closure_minimal hs (isClosed R x) hv)) :
P y hy := by
apply closure (adjoin R { x } : Set A) subset_closure (fun y hy ↦ ?_) y hy
rw [SetLike.mem_coe, ← mem_toSubalgebra, adjoin_toSubalgebra] at hy
induction hy using Algebra.adjoin_induction with
| mem u hu =>
obtain ((rfl : u = x) | (hu : star u = x)) := by simpa using hu
· exact self
· simp_rw [← hu, star_star] at star_self
exact star_self
| algebraMap r => exact algebraMap r
| add u v hu_mem hv_mem hu hv => exact add u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
| mul u v hu_mem hv_mem hu hv => exact mul u (subset_closure hu_mem) v (subset_closure hv_mem) (hu hu_mem) (hv hv_mem)
