English
Given F: C ⥤ D ⥤ D, an object X ∈ C, and a graded object Y ∈ GradedObject J D, the object (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y) in degree a = (i, j) with a.1 ≠ 0 is initial.
Русский
Пусть F: C ⥤ D ⥤ D, X ∈ C, и Y ∈ GradedObject J D. Тогда в компоненте a = (i, j) с a.1 ≠ 0 объект (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y) является инициалом.
LaTeX
$$$$\text{For } a=(i,j)\in I×J,\; ha: a.1 \neq 0,\; IsInitial\Big(((mapBifunctor F I J).obj ((single_0 I).obj X)).obj Y\Big)\!_a.$$$$
Lean4
/-- Given `F : C ⥤ D ⥤ D`, `X : C` and `Y : GradedObject J D`,
`((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a` is an initial object
when `a : I × J` is such that `a.1 ≠ 0`. -/
noncomputable def mapBifunctorObjSingle₀ObjIsInitial (a : I × J) (ha : a.1 ≠ 0) :
IsInitial (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a) :=
IsInitial.isInitialObj (F.flip.obj (Y a.2)) _ (isInitialSingleObjApply _ _ _ ha)
