Lean4
/-- Implementation of `Mon.hasLimitsOfShape`:
the proposed cone over a functor `F : J ⥤ Mon C` is a limit cone.
-/
@[simps]
def limitConeIsLimit (F : J ⥤ Mon C) : IsLimit (limitCone F)
where
lift
s :=
{ hom := limit.lift (F ⋙ Mon.forget C) ((Mon.forget C).mapCone s)
isMonHom_hom.mul_hom :=
limit.hom_ext fun j ↦ by
dsimp
simp only [Category.assoc, limit.lift_π, Functor.mapCone_pt, forget_obj, Functor.mapCone_π_app, forget_map,
IsMonHom.mul_hom, limMap_π, tensorObj_obj, Functor.comp_obj,
MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, lim_μ_π_assoc, lim_obj,
tensorHom_comp_tensorHom_assoc] }
fac s h := by ext; simp
uniq s m
w := by
ext1
refine limit.hom_ext (fun j => ?_)
dsimp; simp only [Mon.forget_map, limit.lift_π, Functor.mapCone_π_app]
exact congr_arg Mon.Hom.hom (w j)
