isIso_whiskerLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance isIso_whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [IsIso α] : IsIso (whiskerLeft F α) :=
  (isoWhiskerLeft F (asIso α)).isIso_hom

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