whiskerRightIso_trans — Mathlib

English

For isomorphisms f : X ≅ Y and g : Y ≅ Z, whiskerRightIso (f ≪≫ g) W = whiskerRightIso f W ≪≫ whiskerRightIso g W.

Русский

Для изоморфизмов f : X ≅ Y и g : Y ≅ Z выполняется равенство: whiskerRightIso (f ≪≫ g) W = whiskerRightIso f W ≪≫ whiskerRightIso g W.

LaTeX

$$$ \mathrm{whiskerRightIso}(f \xrightarrow{~} g, W) = \mathrm{whiskerRightIso}(f, W) \circ \mathrm{whiskerRightIso}(g, W). $$$

Lean4

@[simp]
theorem whiskerRightIso_trans {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) (W : C) :
    whiskerRightIso (f ≪≫ g) W = whiskerRightIso f W ≪≫ whiskerRightIso g W :=
  Iso.ext (comp_whiskerRight f.hom g.hom W)

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