English
Given a morphism φ between graded objects, the left unitor is compatible with φ in the sense that φ composed with the inverse left unitor equals the inverse left unitor composed with map application on φ.
Русский
Пусть есть мономорфизм φ между градуированными объектами; левый унитор сохраняет совместимость: φ ∘ (LeftUnitor)^{-1} = (LeftUnitor)^{-1} ∘ mapMap φ.
LaTeX
$$$ φ \\, ≫ \\, (mapBifunctorLeftUnitor F X e p hp Y').inv \\\\; = \\\\; (mapBifunctorLeftUnitor F X e p hp Y).inv \\\\; ≫ \\\\; mapBifunctorMapMap F p (𝟙 _) φ $$$
Lean4
@[reassoc]
theorem mapBifunctorLeftUnitor_inv_naturality :
φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv =
(mapBifunctorLeftUnitor F X e p hp Y).inv ≫ mapBifunctorMapMap F p (𝟙 _) φ :=
by
ext j
dsimp
rw [mapBifunctorLeftUnitor_inv_apply, mapBifunctorLeftUnitor_inv_apply, assoc, assoc, ι_mapBifunctorMapMap]
dsimp
rw [Functor.map_id, NatTrans.id_app, id_comp, ← NatTrans.naturality_assoc, ← NatTrans.naturality_assoc]
rfl
