refactor: colimits in ModuleCat (#6925)

This PR refactors the construction of colimits of modules in order to prove that the forgetful functor to abelian groups preserves colimits.

Author: joelriou

Mathlib/Algebra/Category/AlgebraCat/Limits.lean

@@ -159,12 +159,12 @@ instance forget₂RingPreservesLimits : PreservesLimits (forget₂ (AlgebraCat R
 /-- The forgetful functor from R-algebras to R-modules preserves all limits.
 -/
 instance forget₂ModulePreservesLimitsOfSize : PreservesLimitsOfSize.{v, v}
-    (forget₂ (AlgebraCatMax.{v, w} R) (ModuleCat.ModuleCatMax.{v, w} R)) where
+    (forget₂ (AlgebraCatMax.{v, w} R) (ModuleCatMax.{v, w} R)) where
   preservesLimitsOfShape :=
     { preservesLimit :=
         preservesLimitOfPreservesLimitCone (limitConeIsLimit _)
           (ModuleCat.HasLimits.limitConeIsLimit
-            (_ ⋙ forget₂ (AlgebraCatMax.{v, w} R) (ModuleCat.ModuleCatMax.{v, w} R))) }
+            (_ ⋙ forget₂ (AlgebraCatMax.{v, w} R) (ModuleCatMax.{v, w} R))) }
 #align Algebra.forget₂_Module_preserves_limits_of_size AlgebraCat.forget₂ModulePreservesLimitsOfSize
 
 instance forget₂ModulePreservesLimits :

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -512,3 +512,23 @@ set_option linter.uppercaseLean3 false in
 #align CommGroup.forget_reflects_isos CommGroupCat.forget_reflects_isos
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.forget_reflects_isos AddCommGroupCat.forget_reflects_isos
+
+-- note: in the following definitions, there is a problem with `@[to_additive]`
+-- as the `Category` instance is not found on the additive variant
+-- this variant is then renamed with a `Aux` suffix
+
+/-- An alias for `GroupCat.{max u v}`, to deal around unification issues. -/
+@[to_additive (attr := nolint checkUnivs) GroupCatMaxAux
+  "An alias for `AddGroupCat.{max u v}`, to deal around unification issues."]
+abbrev GroupCatMax.{u1, u2} := GroupCat.{max u1 u2}
+/-- An alias for `AddGroupCat.{max u v}`, to deal around unification issues. -/
+@[nolint checkUnivs]
+abbrev AddGroupCatMax.{u1, u2} := AddGroupCat.{max u1 u2}
+
+/-- An alias for `CommGroupCat.{max u v}`, to deal around unification issues. -/
+@[to_additive (attr := nolint checkUnivs) AddCommGroupCatMaxAux
+  "An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues."]
+abbrev CommGroupCatMax.{u1, u2} := CommGroupCat.{max u1 u2}
+/-- An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues. -/
+@[nolint checkUnivs]
+abbrev AddCommGroupCatMax.{u1, u2} := AddCommGroupCat.{max u1 u2}

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -6,6 +6,7 @@ Authors: Scott Morrison
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.GroupTheory.QuotientGroup
 import Mathlib.CategoryTheory.Limits.Shapes.Kernels
+import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 
 #align_import algebra.category.Group.colimits from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
@@ -25,16 +26,18 @@ of finitely supported functions, and we really should implement this as well (or
 -- porting note: `AddCommGroup` in all the names
 set_option linter.uppercaseLean3 false
 
-universe u v
+universe w u v
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits
 
 -- [ROBOT VOICE]:
 -- You should pretend for now that this file was automatically generated.
 -- It follows the same template as colimits in Mon.
-namespace AddCommGroupCat.Colimits
+namespace AddCommGroupCat
+
+variable {J : Type u} [Category.{v} J] (F : J ⥤ AddCommGroupCat.{max u v w})
+
+namespace Colimits
 
 /-!
 We build the colimit of a diagram in `AddCommGroupCat` by constructing the
@@ -43,9 +46,6 @@ then taking the quotient by the abelian group laws within each abelian group,
 and the identifications given by the morphisms in the diagram.
 -/
 
-
-variable {J : Type v} [SmallCategory J] (F : J ⥤ AddCommGroupCat.{v})
-
 /-- An inductive type representing all group expressions (without relations)
 on a collection of types indexed by the objects of `J`.
 -/
@@ -58,7 +58,7 @@ inductive Prequotient
   | add : Prequotient → Prequotient → Prequotient
 #align AddCommGroup.colimits.prequotient AddCommGroupCat.Colimits.Prequotient
 
-instance : Inhabited (Prequotient F) :=
+instance : Inhabited (Prequotient.{w} F) :=
   ⟨Prequotient.zero⟩
 
 open Prequotient
@@ -67,7 +67,7 @@ open Prequotient
 because of the abelian group laws, or
 because one element is mapped to another by a morphism in the diagram.
 -/
-inductive Relation : Prequotient F → Prequotient F → Prop
+inductive Relation : Prequotient.{w} F → Prequotient.{w} F → Prop
   -- Make it an equivalence relation:
   | refl : ∀ x, Relation x x
   | symm : ∀ (x y) (_ : Relation x y), Relation y x
@@ -95,7 +95,7 @@ inductive Relation : Prequotient F → Prequotient F → Prop
 /--
 The setoid corresponding to group expressions modulo abelian group relations and identifications.
 -/
-def colimitSetoid : Setoid (Prequotient F) where
+def colimitSetoid : Setoid (Prequotient.{w} F) where
   r := Relation F
   iseqv := ⟨Relation.refl, fun r => Relation.symm _ _ r, fun r => Relation.trans _ _ _ r⟩
 #align AddCommGroup.colimits.colimit_setoid AddCommGroupCat.Colimits.colimitSetoid
@@ -104,11 +104,11 @@ attribute [instance] colimitSetoid
 
 /-- The underlying type of the colimit of a diagram in `AddCommGroupCat`.
 -/
-def ColimitType : Type v :=
-  Quotient (colimitSetoid F)
+def ColimitType : Type max u v w :=
+  Quotient (colimitSetoid.{w} F)
 #align AddCommGroup.colimits.colimit_type AddCommGroupCat.Colimits.ColimitType
 
-instance : AddCommGroup (ColimitType F) where
+instance : AddCommGroup (ColimitType.{w} F) where
   zero := Quotient.mk _ zero
   neg := Quotient.map neg Relation.neg_1
   add := Quotient.map₂ add <| fun x x' rx y y' ry =>
@@ -120,79 +120,79 @@ instance : AddCommGroup (ColimitType F) where
   add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
 
-instance ColimitTypeInhabited : Inhabited (ColimitType.{v} F) := ⟨0⟩
+instance ColimitTypeInhabited : Inhabited (ColimitType.{w} F) := ⟨0⟩
 
 @[simp]
-theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType F) :=
+theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType.{w} F) :=
   rfl
 #align AddCommGroup.colimits.quot_zero AddCommGroupCat.Colimits.quot_zero
 
 @[simp]
 theorem quot_neg (x) : Quot.mk Setoid.r (neg x) =
     -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
-    Neg.neg (α := ColimitType.{v} F) (Quot.mk Setoid.r x : ColimitType.{v} F) :=
+    Neg.neg (α := ColimitType.{w} F) (Quot.mk Setoid.r x : ColimitType.{w} F) :=
   rfl
 #align AddCommGroup.colimits.quot_neg AddCommGroupCat.Colimits.quot_neg
 
 @[simp]
 theorem quot_add (x y) :
     Quot.mk Setoid.r (add x y) =
     -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
-    Add.add (α := ColimitType.{v} F) (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) :=
+    Add.add (α := ColimitType.{w} F) (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) :=
   rfl
 #align AddCommGroup.colimits.quot_add AddCommGroupCat.Colimits.quot_add
 
 /-- The bundled abelian group giving the colimit of a diagram. -/
 def colimit : AddCommGroupCat :=
-  AddCommGroupCat.of (ColimitType F)
+  AddCommGroupCat.of (ColimitType.{w} F)
 #align AddCommGroup.colimits.colimit AddCommGroupCat.Colimits.colimit
 
 /-- The function from a given abelian group in the diagram to the colimit abelian group. -/
-def coconeFun (j : J) (x : F.obj j) : ColimitType F :=
+def coconeFun (j : J) (x : F.obj j) : ColimitType.{w} F :=
   Quot.mk _ (Prequotient.of j x)
 #align AddCommGroup.colimits.cocone_fun AddCommGroupCat.Colimits.coconeFun
 
 /-- The group homomorphism from a given abelian group in the diagram to the colimit abelian
 group. -/
-def coconeMorphism (j : J) : F.obj j ⟶ colimit F where
+def coconeMorphism (j : J) : F.obj j ⟶ colimit.{w} F where
   toFun := coconeFun F j
   map_zero' := by apply Quot.sound; apply Relation.zero
   map_add' := by intros; apply Quot.sound; apply Relation.add
 #align AddCommGroup.colimits.cocone_morphism AddCommGroupCat.Colimits.coconeMorphism
 
 @[simp]
 theorem cocone_naturality {j j' : J} (f : j ⟶ j') :
-    F.map f ≫ coconeMorphism F j' = coconeMorphism F j := by
+    F.map f ≫ coconeMorphism.{w} F j' = coconeMorphism F j := by
   ext
   apply Quot.sound
   apply Relation.map
 #align AddCommGroup.colimits.cocone_naturality AddCommGroupCat.Colimits.cocone_naturality
 
 @[simp]
 theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
-    (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x := by
+    (coconeMorphism.{w} F j') (F.map f x) = (coconeMorphism F j) x := by
   rw [← cocone_naturality F f]
   rfl
 #align AddCommGroup.colimits.cocone_naturality_components AddCommGroupCat.Colimits.cocone_naturality_components
 
 /-- The cocone over the proposed colimit abelian group. -/
 def colimitCocone : Cocone F where
-  pt := colimit F
+  pt := colimit.{w} F
   ι := { app := coconeMorphism F }
 #align AddCommGroup.colimits.colimit_cocone AddCommGroupCat.Colimits.colimitCocone
 
 /-- The function from the free abelian group on the diagram to the cone point of any other
 cocone. -/
 @[simp]
-def descFunLift (s : Cocone F) : Prequotient F → s.pt
+def descFunLift (s : Cocone F) : Prequotient.{w} F → s.pt
   | Prequotient.of j x => (s.ι.app j) x
   | zero => 0
   | neg x => -descFunLift s x
   | add x y => descFunLift s x + descFunLift s y
 #align AddCommGroup.colimits.desc_fun_lift AddCommGroupCat.Colimits.descFunLift
 
 /-- The function from the colimit abelian group to the cone point of any other cocone. -/
-def descFun (s : Cocone F) : ColimitType F → s.pt := by
+def descFun (s : Cocone F) : ColimitType.{w} F → s.pt := by
   fapply Quot.lift
   · exact descFunLift F s
   · intro x y r
@@ -216,15 +216,15 @@ def descFun (s : Cocone F) : ColimitType F → s.pt := by
 #align AddCommGroup.colimits.desc_fun AddCommGroupCat.Colimits.descFun
 
 /-- The group homomorphism from the colimit abelian group to the cone point of any other cocone. -/
-def descMorphism (s : Cocone F) : colimit.{v} F ⟶ s.pt where
+def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where
   toFun := descFun F s
   map_zero' := rfl
   -- Porting note : in `mathlib3`, nothing needs to be done after `induction`
   map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp [(· + ·)]; rw [←quot_add F]; rfl
 #align AddCommGroup.colimits.desc_morphism AddCommGroupCat.Colimits.descMorphism
 
 /-- Evidence that the proposed colimit is the colimit. -/
-def colimitCoconeIsColimit : IsColimit (colimitCocone.{v} F) where
+def colimitCoconeIsColimit : IsColimit (colimitCocone.{w} F) where
   desc s := descMorphism F s
   uniq s m w := FunLike.ext _ _ <| fun x => Quot.inductionOn x fun x => by
     change (m : ColimitType F →+ s.pt) _ = (descMorphism F s : ColimitType F →+ s.pt) _
@@ -241,15 +241,37 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v} F) where
       erw [m.map_add, (descMorphism F s).map_add, ihx, ihy]
 #align AddCommGroup.colimits.colimit_cocone_is_colimit AddCommGroupCat.Colimits.colimitCoconeIsColimit
 
-instance hasColimits_addCommGroupCat : HasColimits AddCommGroupCat
-    where has_colimits_of_shape {_ _} :=
-    { has_colimit := fun F =>
-        HasColimit.mk
-          { cocone := colimitCocone F
-            isColimit := colimitCoconeIsColimit F } }
-#align AddCommGroup.colimits.has_colimits_AddCommGroup AddCommGroupCat.Colimits.hasColimits_addCommGroupCat
+end Colimits
+
+lemma hasColimit : HasColimit F := ⟨_, Colimits.colimitCoconeIsColimit.{w} F⟩
+
+variable (J)
 
-end AddCommGroupCat.Colimits
+lemma hasColimitsOfShape : HasColimitsOfShape J AddCommGroupCat.{max u v w} where
+  has_colimit F := hasColimit.{w} F
+
+lemma hasColimitsOfSize : HasColimitsOfSize.{v, u} AddCommGroupCat.{max u v w} :=
+  ⟨fun _ => hasColimitsOfShape.{w} _⟩
+
+instance hasColimits : HasColimits AddCommGroupCat.{w} := hasColimitsOfSize.{w}
+#align AddCommGroup.colimits.has_colimits_AddCommGroup AddCommGroupCat.hasColimits
+
+instance : HasColimitsOfSize.{v, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
+instance : HasColimitsOfSize.{u, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{v}
+instance : HasColimitsOfSize.{u, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
+instance : HasColimitsOfSize.{v, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
+instance : HasColimitsOfSize.{0, 0} (AddCommGroupCat.{u}) := hasColimitsOfSize.{u, 0, 0}
+
+example : HasColimits AddCommGroupCatMax.{v, u} :=
+  inferInstance
+
+example : HasColimits AddCommGroupCatMax.{u, v} :=
+  inferInstance
+
+example : HasColimits AddCommGroupCat.{u} :=
+  inferInstance
+
+end AddCommGroupCat
 
 namespace AddCommGroupCat
 

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -29,13 +29,6 @@ noncomputable section
 
 variable {J : Type v} [SmallCategory J]
 
--- Porting note: typemax hack to fix universe complaints
-/-- An alias for `GroupCat.{max u v}`, to deal around unification issues. -/
-@[to_additive (attr := nolint checkUnivs)
-  "An alias for `AddGroupCat.{max u v}`, to deal around unification issues."]
-abbrev GroupCatMax.{u1, u2} := GroupCat.{max u1 u2}
-
-
 namespace GroupCat
 
 @[to_additive]
@@ -218,12 +211,6 @@ set_option linter.uppercaseLean3 false in
 
 end GroupCat
 
--- Porting note: typemax hack to fix universe complaints
-/-- An alias for `CommGroupCat.{max u v}`, to deal around unification issues. -/
-@[to_additive (attr := nolint checkUnivs)
-  "An alias for `AddCommGroupCat.{max u v}`, to deal around unification issues."]
-abbrev CommGroupCatMax.{u1, u2} := CommGroupCat.{max u1 u2}
-
 namespace CommGroupCat
 
 @[to_additive]