English
Let F be a bifunctorial construction on graded objects with a left unitor isomorphism. For every j in J, the j-th component of the left unitor intertwines the bifunctorial map with the structural isomorphism e, yielding the equality of the two ways to map Y(j) into the X-structure.
Русский
Пусть задано левое единичное преобразование для билинктора на градуированных объектах с изоморфизмом e. Для каждого j ∈ J j-й компонент левого унитора связывает билинкторную переобозначение с исходной структурой e, что приводит к равенству двух путей отображения Y(j) в структуру X.
LaTeX
$$$ \\forall j \\in J: \\\\ ιMapBifunctorMapObj F p ((single_0 I).obj X) Y 0 j j (hp j) \\\\; ≫ \\, (mapBifunctorLeftUnitor F X e p hp Y).hom j \\\\; = \\\\; (F.map (singleObjApplyIso (0 : I) X).hom).app (Y j) \\\\; ≫ \\, e.hom.app (Y j) $$$
Lean4
@[reassoc (attr := simp)]
theorem ι_mapBifunctorLeftUnitor_hom_apply (j : J) :
ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j (hp j) ≫ (mapBifunctorLeftUnitor F X e p hp Y).hom j =
(F.map (singleObjApplyIso (0 : I) X).hom).app _ ≫ e.hom.app (Y j) :=
by
dsimp [mapBifunctorLeftUnitor]
erw [CofanMapObjFun.ιMapObj_iso_inv]
rw [mapBifunctorLeftUnitorCofan_inj]
