English
The inj component of the right unitor cofan agrees with the explicit formula involving e.inv, F.obj map, and ιMapBifunctorObjIso.
Русский
Компонента inj кофана правого унитора соответствует явной формуле, включающей e.inv, отображение F obj и ιMapBifunctorObjIso.
LaTeX
$$$ (mapBifunctorRightUnitorCofan F Y e p hp X j).inj \\langle\\langle j, 0\\rangle, hp j\\rangle = (F.obj (X j)).map (singleObjApplyIso (0 : I) Y).hom ≫ e.hom.app (X j) $$$
Lean4
theorem mapBifunctor_triangle
(triangle :
∀ (X₁ : C₁) (X₃ : C₃),
((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃) :
(mapBifunctorAssociator associator τ.ρ₁₂ τ.ρ₂₃ X₁ ((single₀ I₂).obj X₂) X₃).hom ≫
mapBifunctorMapMap G π (𝟙 X₁) (mapBifunctorLeftUnitor F₂ X₂ e₂ τ.p₂₃ τ.h₃ X₃).hom =
mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ τ.h₁ X₁).hom (𝟙 X₃) :=
by
rw [← cancel_epi ((mapBifunctorMapMap G π (mapBifunctorRightUnitor F₁ X₂ e₁ τ.p₁₂ τ.h₁ X₁).inv (𝟙 X₃)))]
ext j i₁ i₃ hj
simp only [categoryOfGradedObjects_comp, ι_mapBifunctorMapMap_assoc, mapBifunctorRightUnitor_inv_apply,
Functor.id_obj, Functor.flip_obj_obj, Functor.map_comp, NatTrans.comp_app, categoryOfGradedObjects_id,
Functor.map_id, id_comp, assoc, ι_mapBifunctorMapMap]
congr 2
rw [← ιMapBifunctor₁₂BifunctorMapObj_eq_assoc F₁ G τ.ρ₁₂ _ _ _ i₁ 0 i₃ j (by rw [τ.r_zero, hj]) i₁ (by simp),
ι_mapBifunctorAssociator_hom_assoc,
ιMapBifunctorBifunctor₂₃MapObj_eq_assoc G F₂ τ.ρ₂₃ _ _ _ i₁ 0 i₃ j (by rw [τ.r_zero, hj]) i₃ (by simp),
ι_mapBifunctorMapMap]
dsimp
rw [Functor.map_id, NatTrans.id_app, id_comp, ← Functor.map_comp_assoc, ← NatTrans.comp_app_assoc, ← Functor.map_comp,
ι_mapBifunctorLeftUnitor_hom_apply F₂ X₂ e₂ τ.p₂₃ τ.h₃ X₃ i₃,
ι_mapBifunctorRightUnitor_hom_apply F₁ X₂ e₁ τ.p₁₂ τ.h₁ X₁ i₁]
dsimp
simp only [Functor.map_comp, NatTrans.comp_app, ← triangle (X₁ i₁) (X₃ i₃), ← assoc]
congr 2
symm
apply NatTrans.naturality_app (associator.hom.app (X₁ i₁))
