English
If two algebra homomorphisms φ, ψ from Unitization R A to B agree on A and on the embedded scalars from R, then φ = ψ.
Русский
Если две алгебра-гомоморфизма φ, ψ из Unitization(R,A) в B совпадают на A и на образах скаляров из R, то φ = ψ.
LaTeX
$$$\forall a\in A:\; φ(a)=ψ(a) \text{ and } \forall r:\; φ(\mathrm{algebraMap}_R(\mathrm{Unitization}(R,A), r))=ψ(\mathrm{algebraMap}_R(\mathrm{Unitization}(R,A), r)) \Rightarrow φ=ψ.$$$
Lean4
theorem algHom_ext {F : Type*} [FunLike F (Unitization R A) B] [AlgHomClass F S (Unitization R A) B] {φ ψ : F}
(h : ∀ a : A, φ a = ψ a) (h' : ∀ r, φ (algebraMap R (Unitization R A) r) = ψ (algebraMap R (Unitization R A) r)) :
φ = ψ := by
refine DFunLike.ext φ ψ (fun x ↦ ?_)
induction x
simp only [map_add, ← algebraMap_eq_inl, h, h']
