English
For any X, Y and morphism f: X → Y in D, the equation F.map(F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y holds, expressing naturality of the counit with respect to F.
Русский
Для любого X, Y и морфизма f: X → Y в D выполняется равенство F.map(F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y, выражающее натуральность коутины.
LaTeX
$$$F.map (F.inv.map f) = F.asEquivalence.counit.app X \;\circ\; f \;\circ\; F.asEquivalence.counitInv.app Y$$$
Lean4
@[simp]
theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) :
F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y := by
simpa using (NatIso.naturality_2 (α := F.asEquivalence.counitIso) (f := f)).symm
