mapBifunctorLeftUnitorCofanIsColimit

English

The left unitor cofan induces a HasMap structure on the apices of the graded-object action.

Русский

Кофан левого унитора индуцирует структуру HasMap на апексах действия градуированных объектов.

LaTeX

$$$$mapBifunctorLeftUnitor_hasMap : HasMap (mapBifunctorMapObj F p ((single₀ I).obj X) Y) p.$$$$

Lean4

/-- The cofan `mapBifunctorLeftUnitorCofan F X e p hp Y j` is a colimit. -/
noncomputable def mapBifunctorLeftUnitorCofanIsColimit (j : J) :
    IsColimit (mapBifunctorLeftUnitorCofan F X e p hp Y j) :=
  mkCofanColimit _
    (fun s => e.inv.app (Y j) ≫ (F.map (singleObjApplyIso (0 : I) X).inv).app (Y j) ≫ s.inj ⟨⟨0, j⟩, hp j⟩)
    (fun s => by
      rintro ⟨⟨i, j'⟩, h⟩
      by_cases hi : i = 0
      · subst hi
        simp only [Set.mem_preimage, hp, Set.mem_singleton_iff] at h
        subst h
        simp
      · apply IsInitial.hom_ext
        exact mapBifunctorObjSingle₀ObjIsInitial _ _ _ _ hi)
    (fun s m hm => by simp [← hm ⟨⟨0, j⟩, hp j⟩])

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