English
The left unitor morphism associated with mapBifunctorLeftUnitorCofan is injective on the apex via the chosen index.
Русский
Левый униторный морфизм, связанный с mapBifunctorLeftUnitorCofan, инъективен на апексе по выбранному индексу.
LaTeX
$$$$mapBifunctorLeftUnitorCofan\;inj\;⟨⟨0,j⟩,hp j⟩ = (F.map (singleObjApplyIso (0 : I) X).hom) \app (Y j) \; \text{(and)} \; e.hom.app (Y j).$$$$
Lean4
/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D`, `Y : GradedObject J D` and
`p : I × J → J` such that `p ⟨0, j⟩ = j` for all `j`,
this is the (colimit) cofan which shall be used to construct the isomorphism
`mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y`, see `mapBifunctorLeftUnitor`. -/
noncomputable def mapBifunctorLeftUnitorCofan (hp : ∀ (j : J), p ⟨0, j⟩ = j) (Y) (j : J) :
(((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).CofanMapObjFun p j :=
CofanMapObjFun.mk _ _ _ (Y j)
(fun a ha =>
if ha : a.1 = 0 then (mapBifunctorObjSingle₀ObjIso F X e Y a ha).hom ≫ eqToHom (by aesop)
else (mapBifunctorObjSingle₀ObjIsInitial F X Y a ha).to _)
