English
Let 𝒜 and ℬ be graded algebras over R and let M be an additive R-module. Then any two R-linear maps f,g from the graded tensor product 𝒜ᵍ⊗[R]ℬ to M are equal if they coincide on the canonical underlying tensor product A⊗RF with respect to the inclusions of R 𝒜 ℬ. In other words, a morphism out of the graded tensor product is determined by its values on the underlying tensor product.
Русский
Пусть 𝒜 и ℬ — градуированные алгебры над кольцо R, а M — аддитивное модуль над R. Тогда любые две линейные отображения f,g из градуированного тензорного произведения 𝒜ᵍ⊗[R]ℬ в M равны, если они совпадают на соответствующем базовом тензорном произведении A⊗R B (через соответствующие вложения). Другими словами, однородная карта из градуированного тензорного произведения определяется его значениями на базовом тензорном произведении.
LaTeX
$$$\forall M\,[AddCommMonoid M] [Module\ R M],\; \forall f,g:\, 𝒜^g \otimes_R \ℬ \to_R M, \\ f \circ_ℓ \operatorname{of}_R(𝒜,ℬ) = g \circ_ℓ \operatorname{of}_R(𝒜,ℬ) \;\Rightarrow\; f = g$$$
Lean4
/-- Two linear maps from the graded tensor product agree if they agree on the underlying tensor
product. -/
@[ext]
theorem hom_ext {M} [AddCommMonoid M] [Module R M] ⦃f g : 𝒜 ᵍ⊗[R] ℬ →ₗ[R] M⦄
(h : f ∘ₗ of R 𝒜 ℬ = (g ∘ₗ of R 𝒜 ℬ : A ⊗[R] B →ₗ[R] M)) : f = g :=
h
