whiskerLeft_isIso — Mathlib

English

If η: g → h is an isomorphism in a hom-category between g and h, then whiskering on the left by any morphism f yields an isomorphism (f ◁ η) with explicit inverse given by f ◁ inv η.

Русский

Если η: g → h является изоморфизмом в гом-категории между g и h, то левое взвешивание на любом f даёт изоморфизм (f ◁ η) c явным обратным (f ◁ inv η).

LaTeX

$$$ \text{If } η \text{ is an isomorphism, then } f \triangleleft η \text{ is an isomorphism with inverse } f \triangleleft η^{-1}. $$$

Lean4

instance whiskerLeft_isIso (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [IsIso η] : IsIso (f ◁ η) :=
  (whiskerLeftIso f (asIso η)).isIso_hom

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