English
Let e: X ≅ Y be an isomorphism of graded objects, and F: C ⥤ D ⥤ E a functor-valued functor. For every j ∈ J and every object Y ∈ D, the app at Y of the morphism (F.map (e.hom j)) composed with the app at Y of (F.map (e.inv j)) is the identity on (F.obj X).obj Y.
Русский
Пусть e: X ≅ Y — изоморфизм градуированного объекта, и F: C ⥤ D ⥤ E — функтор-категория. Для каждого j ∈ J и объекта Y ∈ D композиция \n( F.map (e.hom j) ).app Y и ( F.map (e.inv j) ).app Y дает тождественный морфизм на (F.obj X).obj Y.
LaTeX
$$$ (F.map (e.hom j)).app Y \\circ (F.map (e.inv j)).app Y = \\mathrm{id}_{(F.obj X).obj Y} $$$
Lean4
@[reassoc (attr := simp)]
theorem map_hom_inv_id_eval_app (e : X ≅ Y) (F : C ⥤ D ⥤ E) (j : J) (Y : D) :
(F.map (e.hom j)).app Y ≫ (F.map (e.inv j)).app Y = 𝟙 _ := by
rw [← NatTrans.comp_app, ← F.map_comp, hom_inv_id_eval, Functor.map_id, NatTrans.id_app]
