English
Let e: X ≅ Y be an isomorphism of J-graded objects in C, and F: C ⥤ D a functor to some category D. For every j ∈ J, the two morphisms F.map (e.inv j) and F.map (e.hom j) compose to the identity on F.obj (Y j); equivalently, F.map (e.inv j) is a two-sided inverse of F.map (e.hom j) at level j.
Русский
Пусть e: X ≅ Y — изоморфизм градуированного объекта X и Y в категорий C, а F: C ⥤ D — функтор в некоторую категорию D. Для каждого j ∈ J композиция F.map (e.inv j) и F.map (e.hom j) дает тождественный морфизм на F.obj (Y j); следовательно, F.map (e.inv j) является двухсторонним обратным к F.map (e.hom j) в уровне j.
LaTeX
$$$ F.map (e.inv j) \circ F.map (e.hom j) = \mathrm{id}_{F.obj (Y j)} $$$
Lean4
@[reassoc (attr := simp)]
theorem map_inv_hom_id_eval (e : X ≅ Y) (F : C ⥤ D) (j : J) : F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 _ := by
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id, GradedObject.categoryOfGradedObjects_id,
Functor.map_id]
