Lean4
/-- (Impl)
Construct the limiting coalgebra from the map `λ : L ⟶ TL` given by `lambda`. We are required to
show it satisfies the two coalgebra laws, which follow from the coalgebra laws for the image of `D`
and our `commuting` lemma.
-/
@[simps]
noncomputable def conePoint : Coalgebra T where
A := c.pt
a := lambda c t
counit :=
t.hom_ext fun j ↦
by
rw [assoc, ← show _ = _ ≫ c.π.app j from T.ε.naturality _, ← assoc, commuting, assoc]
simp [Coalgebra.counit (D.obj j)]
coassoc := by
refine (isLimitOfPreserves _ (isLimitOfPreserves _ t)).hom_ext fun j => ?_
rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc, ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _,
assoc, ← Functor.map_comp, commuting, Functor.map_comp, ← assoc, commuting]
simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, assoc]
rw [(D.obj j).coassoc, ← assoc, ← assoc, commuting]
