coconePoint — Mathlib

Lean4
/-- The coalgebra structure which will be the point of the new colimit cone for `D`. -/
@[simps]
def coconePoint : Coalgebra T where
  A := c.pt
  a := t.desc (newCocone D c)
  counit :=
    t.hom_ext fun j ↦
      by
      simp only [Functor.comp_obj, forget_obj, Functor.id_obj, Functor.const_obj_obj, IsColimit.fac_assoc,
        newCocone_ι_app, assoc, NatTrans.naturality, Functor.id_map, comp_id]
      rw [← Category.assoc, (D.obj j).counit, Category.id_comp]
  coassoc :=
    t.hom_ext fun j ↦
      by
      simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsColimit.fac_assoc, newCocone_ι_app, assoc,
        NatTrans.naturality, Functor.comp_map]
      rw [← Category.assoc, (D.obj j).coassoc, ← Functor.map_comp, t.fac (newCocone D c) j, newCocone_ι_app,
        Functor.map_comp, assoc]
Похожие утверждения