English
If two star-algebra homomorphisms f,g from the adjoin algebra Adjoin_R S agree on the generating set S, then f = g.
Русский
Если две звездно-алгебра-хомоморфизма f,g из алгебры, порождаемой adjoin_R S, совпадают на генераторах S, то f = g.
LaTeX
$$$ (\\forall x \\in S, f x = g x) \\Rightarrow f = g $ \\, (on the algebra \\operatorname{adjoin}_R S)$$
Lean4
theorem ext_adjoin {s : Set A} [FunLike F (adjoin R s) B] [AlgHomClass F R (adjoin R s) B]
[StarHomClass F (adjoin R s) B] {f g : F} (h : ∀ x : adjoin R s, (x : A) ∈ s → f x = g x) : f = g :=
by
refine
DFunLike.ext f g fun a =>
adjoin_induction_subtype (p := fun y => f y = g y) a (fun x hx => ?_) (fun r => ?_) (fun x y hx hy => ?_)
(fun x y hx hy => ?_) fun x hx => ?_
· exact h ⟨x, subset_adjoin R s hx⟩ hx
· simp only [AlgHomClass.commutes]
· simp only [map_add, map_add, hx, hy]
· simp only [map_mul, map_mul, hx, hy]
· simp only [map_star, hx]
