Morphisms out of the tensor product with a free module #
A morphism out of the tensor product M₁ ⊗ (ModuleCat.free S).obj X of a module with a free
module is determined by its values on the pure tensors m ⊗ₜ ModuleCat.freeMk x of an element of
M₁ with a basis element: TauCeti.ModuleCat.tensor_free_hom_ext combines Mathlib's
extensionality lemmas ModuleCat.MonoidalCategory.tensor_ext for tensor products and
ModuleCat.free_hom_ext for free modules.
theorem
TauCeti.ModuleCat.tensor_free_hom_ext
{S : Type u}
[CommRing S]
{M₁ M₂ : ModuleCat S}
{X : Type u}
{f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ ((ModuleCat.free S).obj X) ⟶ M₂}
(h :
∀ (m : ↑M₁) (x : X),
(CategoryTheory.ConcreteCategory.hom f) (m ⊗ₜ[S] ModuleCat.freeMk x) = (CategoryTheory.ConcreteCategory.hom g) (m ⊗ₜ[S] ModuleCat.freeMk x))
:
Two morphisms out of the tensor product of a module with a free module agree once they agree on pure tensors with basis elements.