inv_whiskerLeft — Mathlib

English

If α is an isomorphism G ⟶ H, then inv(whiskerLeft F α) = whiskerLeft F (inv α) for any F.

Русский

Если α — изоморфизм G ⟶ H, то inv(whiskerLeft F α) = whiskerLeft F (inv α).

LaTeX

$$$\\operatorname{inv}(\\mathrm{whiskerLeft}\\;F\\;α) = \\mathrm{whiskerLeft}\\;F\\;(\\operatorname{inv} α).$$$

Lean4

@[simp]
theorem inv_whiskerLeft (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [IsIso α] :
    inv (whiskerLeft F α) = whiskerLeft F (inv α) := by
  symm
  apply IsIso.eq_inv_of_inv_hom_id
  simp [← whiskerLeft_comp]

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