inv_whiskerRight — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{inv}(\\mathrm{whiskerRight}\\,α\\,F) = \\mathrm{whiskerRight}(\\operatorname{inv}α)\\,F.$$$

Lean4

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

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