feat(CategoryTheory/Monoidal/Limits): generalise universes and explicit limits for limits of monoid objects (leanprover-community#35996)

This PR makes two major refactors to the file. These are easiest to make simultaneously, as they are heavily linked.
- Generalise the smallness assumptions on the shape category
- Take explicit limit cones as inputs rather than assuming HasLimitsOfShape and using the choice-cone

Author: b-mehta

Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

@@ -1,13 +1,14 @@
 /-
 Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison
+Authors: Kim Morrison, Bhavik Mehta
 -/
 module
 
 public import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
 public import Mathlib.CategoryTheory.Monoidal.Limits.Basic
 public import Mathlib.CategoryTheory.Limits.Preserves.Basic
+public import Mathlib.CategoryTheory.Limits.Creates
 
 /-!
 # Limits of monoid objects.
@@ -31,65 +32,88 @@ noncomputable section
 namespace CategoryTheory
 namespace Mon
 
-variable {J : Type w} [SmallCategory J]
-variable {C : Type u} [Category.{v} C] [HasLimitsOfShape J C] [MonoidalCategory.{v} C]
+variable {J : Type w} [Category* J]
+variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C]
 
-/-- We construct the (candidate) limit of a functor `F : J ⥤ Mon C`
-by interpreting it as a functor `Mon (J ⥤ C)`,
-and noting that taking limits is a lax monoidal functor,
-and hence sends monoid objects to monoid objects.
+open MonObj
+
+set_option backward.isDefEq.respectTransparency false in
+/--
+We construct the limit object of a functor `F : J ⥤ Mon C` given a limit cone `c` of
+`F ⋙ forget C`.
 -/
 @[simps!]
-def limit (F : J ⥤ Mon C) : Mon C :=
-  lim.mapMon.obj ((monFunctorCategoryEquivalence J C).inverse.obj F)
+def limit (F : J ⥤ Mon C) (c : Cone (F ⋙ Mon.forget C)) (hc : IsLimit c) :
+    Mon C where
+  X := c.pt
+  mon.one := hc.lift
+    { pt := _
+      π.app X := η[(F.obj X).X] }
+  mon.mul := hc.lift
+    { pt := _
+      π.app X := (c.π.app X ⊗ₘ c.π.app X) ≫ μ[(F.obj X).X]
+      π.naturality i j f := by have := c.π.naturality f; simp_all }
+  mon.one_mul := hc.hom_ext <| by simp [whiskerRight_comp_tensorHom_assoc]
+  mon.mul_one := hc.hom_ext <| by simp [whiskerLeft_comp_tensorHom_assoc]
+  mon.mul_assoc := by
+    apply hc.hom_ext
+    simp only [Functor.comp_obj, forget_obj, Functor.const_obj_obj, IsLimit.fac,
+      mon_tauto, implies_true]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Implementation of `Mon.hasLimits`: a limiting cone over a functor `F : J ⥤ Mon C`.
 -/
 @[simps]
-def limitCone (F : J ⥤ Mon C) : Cone F where
-  pt := limit F
-  π :=
-    { app := fun j => .mk' (limit.π (F ⋙ Mon.forget C) j)
-      naturality := fun j j' f => by ext; exact (limit.cone (F ⋙ Mon.forget C)).π.naturality f }
+def limitCone (F : J ⥤ Mon C) (c : Cone (F ⋙ Mon.forget C)) (hc : IsLimit c) : Cone F where
+  pt := limit F c hc
+  π.app j := .mk' (c.π.app j)
+  π.naturality j j' f := Hom.ext' (c.π.naturality f)
 
 /-- The image of the proposed limit cone for `F : J ⥤ Mon C` under the forgetful functor
 `forget C : Mon C ⥤ C` is isomorphic to the limit cone of `F ⋙ forget C`.
 -/
-def forgetMapConeLimitConeIso (F : J ⥤ Mon C) :
-    (forget C).mapCone (limitCone F) ≅ limit.cone (F ⋙ forget C) :=
+@[simps!]
+def forgetMapConeLimitConeIso (F : J ⥤ Mon C) (c : Cone (F ⋙ Mon.forget C)) (hc : IsLimit c) :
+    (forget C).mapCone (limitCone F c hc) ≅ c :=
   Cones.ext (Iso.refl _) (by simp)
 
 set_option backward.isDefEq.respectTransparency false in
 /-- 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
+def limitConeIsLimit (F : J ⥤ Mon C) (c : Cone (F ⋙ Mon.forget C)) (hc : IsLimit c) :
+    IsLimit (limitCone F c hc) 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] }
+    { hom := hc.lift ((Mon.forget C).mapCone s)
+      isMonHom_hom.mul_hom := hc.hom_ext <| by simp
+      isMonHom_hom.one_hom := hc.hom_ext <| by simp }
   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)
-
-instance hasLimitsOfShape [HasLimitsOfShape J C] : HasLimitsOfShape J (Mon C) where
-  has_limit := fun F => HasLimit.mk
-    { cone := limitCone F
-      isLimit := limitConeIsLimit F }
-
-instance forget_preservesLimitsOfShape : PreservesLimitsOfShape J (Mon.forget C) where
-  preservesLimit := fun {F} =>
-    preservesLimit_of_preserves_limit_cone (limitConeIsLimit F)
-      (IsLimit.ofIsoLimit (limit.isLimit (F ⋙ Mon.forget C)) (forgetMapConeLimitConeIso F).symm)
+  uniq s m w := Hom.ext' <| hc.hom_ext fun j ↦ by simpa using congr($(w j).hom)
+
+/--
+A helper definition to show that the forgetful functor `forget C : Mon C ⥤ C` creates limits:
+given a limit cone `c` of `F ⋙ forget C`, we can lift it to a limit cone of `F`.
+-/
+def limitConeLiftsToLimit (F : J ⥤ Mon C) (c : Cone (F ⋙ Mon.forget C)) (hc : IsLimit c) :
+    LiftsToLimit F (forget C) c hc where
+  liftedCone := limitCone F c hc
+  validLift := forgetMapConeLimitConeIso _ _ _
+  makesLimit := limitConeIsLimit _ _ _
+
+instance (F : J ⥤ Mon C) : CreatesLimit F (forget C) :=
+  createsLimitOfReflectsIso (limitConeLiftsToLimit _)
+
+instance : CreatesLimitsOfShape J (forget C) := ⟨inferInstance⟩
+instance : CreatesLimitsOfSize.{w} (forget C) := ⟨inferInstance⟩
+instance : CreatesLimits (forget C) := ⟨inferInstance⟩
+
+instance [HasLimitsOfShape J C] : HasLimitsOfShape J (Mon C) :=
+  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (forget C)
+
+instance [HasLimitsOfShape J C] :
+    PreservesLimitsOfShape J (Mon.forget C) :=
+  CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape _
 
 end Mon
 end CategoryTheory