whiskerLeftIso_trans — Mathlib

English

Let W be an object and f : X ≅ Y, g : Y ≅ Z be isomorphisms. Then left-whiskering by W is compatible with composition of isomorphisms: whiskerLeftIso W (f ≪≫ g) = whiskerLeftIso W f ≪≫ whiskerLeftIso W g.

Русский

Пусть W — произвольный объект, а f : X ≅ Y и g : Y ≅ Z — изоморфизмы. Тогда левый whisker по W сохраняет композицию изоморфизмов: whiskerLeftIso W (f ≪≫ g) = whiskerLeftIso W f ≪≫ whiskerLeftIso W g.

LaTeX

$$$ \mathrm{whiskerLeftIso}(W, f \circ g) = \mathrm{whiskerLeftIso}(W, f) \circ \mathrm{whiskerLeftIso}(W, g). $$$

Lean4

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

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