whiskerRight_isIso — Mathlib

English

Let f : X ⟶ Y be an isomorphism and Z an object. The right whiskering by Z preserves isomorphisms: whiskerRightIso (asIso f) Z is an isomorphism.

Русский

Пусть f : X ⟶ Y — изоморфизм, и Z — объект. Правая whiskering по Z сохраняет изоморфизмы: whiskerRightIso (asIso f) Z является изоморфизмом.

LaTeX

$$$ \mathrm{whiskerRightIso}(f, Z) \text{ is an isomorphism when } f \text{ is an isomorphism.}$$$

Lean4

instance whiskerRight_isIso {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] : IsIso (f ▷ Z) :=
  (whiskerRightIso (asIso f) Z).isIso_hom

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