mapBifunctorObjObjSingle₀IsInitial

English

The right unitor construction provides a HasMap structure for the target graded object, i.e., the necessary map structure exists for all indices with respect to p.

Русский

Построение правого унитора задаёт структуру HasMap для целевого градуированного объекта, то есть существует необходимая структура отображений по всем индексам относительно p.

LaTeX

$$HasMap (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)) p$$

Lean4

/-- Given `F : D ⥤ C ⥤ D`, `Y : C` and `X : GradedObject J D`,
`((mapBifunctor F J I).obj X).obj ((single₀ I).obj X) a` is an initial when `a : J × I`
is such that `a.2 ≠ 0`. -/
noncomputable def mapBifunctorObjObjSingle₀IsInitial (a : J × I) (ha : a.2 ≠ 0) :
    IsInitial (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y) a) :=
  IsInitial.isInitialObj (F.obj (X a.1)) _ (isInitialSingleObjApply _ _ _ ha)

Похожие утверждения