map_hom_inv_id_eval — Mathlib

English

For a morphism between graded objects transported through a functor F, the map of the composition of hom and inv equals the identity.

Русский

Для отображения гомоморфизма между градуированными объектами через F отображение композиции гомома и обратного равняется тождественному отображению.

LaTeX

$$$ F.map (e.hom j) \\;∘\\; F.map (e.inv j) = 𝟙 _ $$$

Lean4

@[reassoc (attr := simp)]
theorem map_hom_inv_id_eval (e : X ≅ Y) (F : C ⥤ D) (j : J) : F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 _ := by
  rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.hom_inv_id, GradedObject.categoryOfGradedObjects_id,
    Functor.map_id]

Похожие утверждения