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 Y ∈ D, the app at Y of (F.map (e.inv j)) followed by the app at Y of (F.map (e.hom j)) equals the identity on (F.obj Y).obj Y.
Русский
Пусть e: X ≅ Y — изоморфизм градуированного объекта, и F: C ⥤ D ⥤ E — функтор-категория. Для каждого j ∈ J и объекта Y ∈ D композиция (F.map (e.inv j)).app Y и (F.map (e.hom j)).app Y дает тождественный морфизм на (F.obj Y).obj Y.
LaTeX
$$$ (F.map (e.inv j)).app Y \circ (F.map (e.hom j)).app Y = \mathrm{id}_{(F.obj Y).obj Y} $$$
Lean4
@[reassoc (attr := simp)]
theorem map_inv_hom_id_eval_app (e : X ≅ Y) (F : C ⥤ D ⥤ E) (j : J) (Y : D) :
(F.map (e.inv j)).app Y ≫ (F.map (e.hom j)).app Y = 𝟙 _ := by
rw [← NatTrans.comp_app, ← F.map_comp, inv_hom_id_eval, Functor.map_id, NatTrans.id_app]
