instMonoidalCategoryStruct — Mathlib

English

A theorem stating that the isometry associated to the tensor product of maps equals the tmul of the individual isometries.

Русский

Теорема, что изометрия тензорного гомоморфизма равна tmul отдельной изометрии.

LaTeX

$$$ (f \\otimes g).\\mathrm{toIsometry} = f.\\mathrm{toIsometry} \\mathrm{tmul} g.\\mathrm{toIsometry}. $$$

Lean4

instance : MonoidalCategoryStruct (QuadraticModuleCat.{u} R)
    where
  tensorObj := instMonoidalCategory.tensorObj
  whiskerLeft X _ _ f := tensorHom (𝟙 X) f
  whiskerRight {X₁ X₂} (f : X₁ ⟶ X₂) Y := tensorHom f (𝟙 Y)
  tensorHom := tensorHom
  tensorUnit := of (sq (R := R))
  associator X Y Z := ofIso (tensorAssoc X.form Y.form Z.form)
  leftUnitor X := ofIso (tensorLId X.form)
  rightUnitor X := ofIso (tensorRId X.form)

Похожие утверждения