English
Two algebra homomorphisms from the graded tensor product are equal if their compositions with the left and with the right inclusions agree.
Русский
Два гомоморфизма алгебр из градуированного тензорного произведения равны, если их композиции с левой и правой вложениями совпадают.
LaTeX
$$$\forall f,g:\,(𝒜 ᵍ⊗[R] ℬ) \rightarrow_ℝ C,\\ (f \circ \mathrm{includeLeft} = g \circ \mathrm{includeLeft}) \, \land \, (f \circ \mathrm{includeRight} = g \circ \mathrm{includeRight}) \, \Rightarrow \, f = g$$$
Lean4
/-- Two algebra morphism from the graded tensor product agree if their compositions with the left
and right inclusions agree. -/
@[ext]
theorem algHom_ext ⦃f g : (𝒜 ᵍ⊗[R] ℬ) →ₐ[R] C⦄ (ha : f.comp (includeLeft 𝒜 ℬ) = g.comp (includeLeft 𝒜 ℬ))
(hb : f.comp (includeRight 𝒜 ℬ) = g.comp (includeRight 𝒜 ℬ)) : f = g :=
(liftEquiv 𝒜 ℬ).symm.injective <| Subtype.ext <| Prod.ext ha hb
