English
A partially-applied ext principle for non-unital algebra homs: if the underlying MulHom compositions agree, then the non-unital algebra homs agree.
Русский
Принцип экстенсивности для негомоморфизмов без единицы: если соответствующие умножающие отображения согласны, то сами негомоморфизмы согласны.
LaTeX
$$$\forall \phi_1,\phi_2:\ SkewMonoidAlgebra k G \to_{n_a[k]} A,\ (\phi_1.toMulHom)\circ (of k G) = (\phi_2.toMulHom)\circ (of k G) \Rightarrow \phi_1 = \phi_2$$$
Lean4
/-- A non_unital `k`-algebra homomorphism from `SkewMonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem nonUnitalAlgHom_ext [DistribMulAction k A] {φ₁ φ₂ : SkewMonoidAlgebra k G →ₙₐ[k] A}
(h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
by
apply NonUnitalAlgHom.to_distribMulActionHom_injective
apply distribMulActionHom_ext'
intro a
ext
simp [singleAddHom_apply, h]
