isIso_whiskerRight — Mathlib

English

If α is an isomorphism between functors G ⟶ H, then whiskerRight α F is an isomorphism for any F.

Русский

Если α — изоморфизм между функторaми G ⟶ H, то whiskerRight α F — изоморфизм для любого F.

LaTeX

$$$\\text{If } α:\\,G\\to H\\text{ is an isomorphism, then } \\mathrm{whiskerRight}\\,α\\,F\\text{ is an isomorphism.}$$$

Lean4

instance isIso_whiskerRight {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [IsIso α] : IsIso (whiskerRight α F) :=
  (isoWhiskerRight (asIso α) F).isIso_hom

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