mapIsoWhiskerLeft_inv — Mathlib

English

If α is an isomorphism of functors, then mapIsoWhiskerLeft H α equals whiskerLeft H α.inv.

Русский

Если α — изоморфизм функторов, то mapIsoWhiskerLeft H α равняется whiskerLeft H α.inv.

LaTeX

$$$ (\mathrm{mapIsoWhiskerLeft} H α).\mathrm{inv} = \mathrm{mapWhiskerLeft} H α^{-1} $$$

Lean4

theorem mapIsoWhiskerLeft_inv (H : C ⥤ E) {Fᵣ : D ⥤ E'} {Gᵣ : D ⥤ E'} (α : Fᵣ ≅ Gᵣ) :
    (mapIsoWhiskerLeft H α).inv = mapWhiskerLeft H α.inv :=
  by
  ext x
  cases x <;> simp [mapIsoWhiskerLeft]

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