tensorIso_def' — Mathlib

English

A variant expression for the tensor of iso's: f ⊗ᵢ g = whiskerLeftIso X g ≪≫ whiskerRightIso f Y'.

Русский

Вариант выражения тензора изоморфизмов: f ⊗ᵢ g = whiskerLeftIso X g ≪≫ whiskerRightIso f Y'.

LaTeX

$$$ f ⊗ᵢ g = \mathrm{whiskerLeftIso} X g \; \ll≫ \mathrm{whiskerRightIso} f Y'. $$$

Lean4

theorem tensorIso_def' {X Y X' Y' : C} (f : X ≅ Y) (g : X' ≅ Y') :
    f ⊗ᵢ g = whiskerLeftIso X g ≪≫ whiskerRightIso f Y' :=
  Iso.ext (tensorHom_def' f.hom g.hom)

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