English
If two morphisms f,g out of the coinvariants tensor object satisfy that their compositions with the canonical coinvariants map are equal, then f = g. In other words, the coinvariants-tensor construction is determined by its effect on the universal map.
Русский
Если два гомоморфизма f, g из объекта коинвариантов тензора удовлетворяют условию равенства их композиции с канонической картой коинвариантов, то f = g. Иными словами, конструирование коинвариантов тензора определяется по действию на универсальную карту.
LaTeX
$$$(coinvariantsTensorMk\\;A\\;B).compr_2\\;f.hom = (coinvariantsTensorMk\\;A\\;B).compr_2\\;g.hom \\;\\Rightarrow\\; f = g$$$
Lean4
@[ext]
theorem coinvariantsTensor_hom_ext {M : ModuleCat k} {f g : ((coinvariantsTensor k G).obj A).obj B ⟶ M}
(hfg : (coinvariantsTensorMk A B).compr₂ f.hom = (coinvariantsTensorMk A B).compr₂ g.hom) : f = g :=
coinvariantsFunctor_hom_ext <| ModuleCat.hom_ext <| TensorProduct.ext <| hfg
