English
There is a canonical function-like structure on the type of nonunital algebra homomorphisms A →ₛₙₐ[φ] B given by the underlying function, and this underlying function-map is injective, so a homomorphism is determined by its action on elements.
Русский
Существует каноническая структура, превращающая множество гомоморфизмов без единицы из A в B в подобный функциям тип, заданный своим действием на элементы; отображение к функции несложно обратимо, то есть гомоморфизм определяется своей действием на элементы.
LaTeX
$$$\forall f,g : A \to_{\varphi} B,\ f.toFun = g.toFun \Rightarrow f = g$$$
Lean4
instance : FunLike (A →ₛₙₐ[φ] B) A B where
coe f := f.toFun
coe_injective' := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h; congr
