tensorIso_def — Mathlib

English

The tensor of two isomorphisms f : X ≅ Y and g : X' ≅ Y' is given by f ⊗ᵢ g, and equals whiskerRightIso f X' ≪≫ whiskerLeftIso Y g.

Русский

Тензор двух изоморфизмов f : X ≅ Y и g : X' ≅ Y' задаётся как f ⊗ᵢ g и равен whiskerRightIso f X' ≪≫ whiskerLeftIso Y g.

LaTeX

$$$ f \otimesᵢ g = \mathrm{whiskerRightIso}(f, X') \; \ll\; \mathrm{whiskerLeftIso}(Y, g). $$$

Lean4

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

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