English
For F: C ⥤ D with IsEquivalence F, and morphism f: X → Y in C, the equation F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y holds, expressing naturality of the unit with respect to F.
Русский
Для F: C ⥤ D с IsEquivalence F верно равенство F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y, выражающее натуральность единицы.
LaTeX
$$$F.inv.map (F.map f) = F.asEquivalence.unitInv.app X \;\circ\; f \;\circ\; F.asEquivalence.unit.app Y$$$
Lean4
@[simp]
theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) :
F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y := by
simpa using (NatIso.naturality_1 (α := F.asEquivalence.unitIso) (f := f)).symm
