chore: cleanup of filtered colimits in concrete categories (#5407)

Just formatting changes, except that I've split the `colimitMonoid` instances into two steps, as this was already close to the time limit, and timing out on another branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jun 23, 2023 · 969f613 · 969f613
1 parent ccc5499
commit 969f613
Show file tree

Hide file tree

Showing 4 changed files with 35 additions and 36 deletions.
diff --git a/Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean b/Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean
@@ -36,9 +36,8 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
-open CategoryTheory.IsFiltered renaming max → max'
+open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 
--- avoid name collision with `_root_.max`.
 namespace GroupCat.FilteredColimits
 
 section
@@ -184,7 +183,8 @@ set_option linter.uppercaseLean3 false in
 @[to_additive forget₂AddMonPreservesFilteredColimits]
 noncomputable instance forget₂MonPreservesFilteredColimits :
     PreservesFilteredColimits.{u} (forget₂ GroupCat.{u} MonCat.{u}) where
-      preserves_filtered_colimits := fun x hx1 _ => letI : Category.{u, u} x := hx1
+      preserves_filtered_colimits x hx1 _ :=
+      letI : Category.{u, u} x := hx1
       ⟨fun {F} => preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (MonCat.FilteredColimits.colimitCoconeIsColimit.{u, u} _)⟩
 set_option linter.uppercaseLean3 false in
@@ -250,8 +250,7 @@ set_option linter.uppercaseLean3 false in
 noncomputable def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι :=
-    {
-      (GroupCat.FilteredColimits.colimitCocone
+    { (GroupCat.FilteredColimits.colimitCocone
           (F ⋙ forget₂ CommGroupCat GroupCat.{max v u})).ι with }
 set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.colimit_cocone CommGroupCat.FilteredColimits.colimitCocone
@@ -280,12 +279,13 @@ set_option linter.uppercaseLean3 false in
 
 @[to_additive]
 noncomputable instance forget₂GroupPreservesFilteredColimits :
-    PreservesFilteredColimits (forget₂ CommGroupCat GroupCat.{u})
-    where preserves_filtered_colimits J hJ1 _ := letI : Category J := hJ1
-  { preservesColimit := fun {F} =>
-      preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
-        (GroupCat.FilteredColimits.colimitCoconeIsColimit.{u, u}
-          (F ⋙ forget₂ CommGroupCat GroupCat.{u})) }
+    PreservesFilteredColimits (forget₂ CommGroupCat GroupCat.{u}) where
+  preserves_filtered_colimits J hJ1 _ :=
+    letI : Category J := hJ1
+    { preservesColimit := fun {F} =>
+        preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
+          (GroupCat.FilteredColimits.colimitCoconeIsColimit.{u, u}
+            (F ⋙ forget₂ CommGroupCat GroupCat.{u})) }
 set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.forget₂_Group_preserves_filtered_colimits CommGroupCat.FilteredColimits.forget₂GroupPreservesFilteredColimits
 set_option linter.uppercaseLean3 false in

diff --git a/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean b/Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
@@ -34,8 +34,7 @@ open scoped Classical
 
 open CategoryTheory CategoryTheory.Limits
 
--- avoid name collision with `_root_.max`.
-open CategoryTheory.IsFiltered renaming max → max'
+open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 
 open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
 

diff --git a/Mathlib/Algebra/Category/Mon/FilteredColimits.lean b/Mathlib/Algebra/Category/Mon/FilteredColimits.lean
@@ -94,7 +94,6 @@ set_option linter.uppercaseLean3 false in
 set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_has_zero AddMonCat.FilteredColimits.colimitZero
 
-
 /-- The definition of the "one" in the colimit is independent of the chosen object of `J`.
 In particular, this lemma allows us to "unfold" the definition of `colimit_one` at a custom chosen
 object `j`.
@@ -227,7 +226,7 @@ set_option linter.uppercaseLean3 false in
 #align AddMon.filtered_colimits.colimit_add_mk_eq AddMonCat.FilteredColimits.colimit_add_mk_eq
 
 @[to_additive]
-noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
+noncomputable instance colimitMulOneClass : MulOneClass (M.{v, u} F) :=
   { colimitOne F,
     colimitMul F with
     one_mul := fun x => by
@@ -245,7 +244,11 @@ noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
       rw [colimit_one_eq F j, colimit_mul_mk_eq F ⟨j, x⟩ ⟨j, 1⟩ j (𝟙 j) (𝟙 j), MonoidHom.map_one,
         mul_one, F.map_id]
       -- Porting note : `id_apply` does not work here, but the two sides are def-eq
-      rfl
+      rfl }
+
+@[to_additive]
+noncomputable instance colimitMonoid : Monoid (M.{v, u} F) :=
+  { colimitMulOneClass F with
     mul_assoc := fun x y z => by
       refine Quot.induction_on₃ x y z ?_
       clear x y z

diff --git a/Mathlib/Algebra/Category/Ring/FilteredColimits.lean b/Mathlib/Algebra/Category/Ring/FilteredColimits.lean
@@ -36,9 +36,8 @@ open CategoryTheory
 
 open CategoryTheory.Limits
 
-open CategoryTheory.IsFiltered renaming max → max'
+open CategoryTheory.IsFiltered renaming max → max' -- avoid name collision with `_root_.max`.
 
--- avoid name collision with `_root_.max`.
 open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
 
 open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
@@ -72,10 +71,7 @@ set_option linter.uppercaseLean3 false in
 instance colimitSemiring : Semiring.{max v u} <| R.{v, u} F :=
   { (R.{v, u} F).str,
     AddCommMonCat.FilteredColimits.colimitAddCommMonoid
-      (F ⋙
-        forget₂ SemiRingCat
-          AddCommMonCat.{max v
-              u}) with
+      (F ⋙ forget₂ SemiRingCat AddCommMonCat.{max v u}) with
     mul_zero := fun x => by
       refine Quot.inductionOn x ?_; clear x; intro x
       cases' x with j x
@@ -144,8 +140,7 @@ set_option linter.uppercaseLean3 false in
 /-- The proposed colimit cocone is a colimit in `SemiRing`. -/
 def colimitCoconeIsColimit : IsColimit <| colimitCocone.{v, u} F where
   desc t :=
-    {
-      (MonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
+    { (MonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
             (F ⋙ forget₂ SemiRingCatMax.{v, u} MonCat)).desc
         ((forget₂ SemiRingCatMax.{v, u} MonCat).mapCocone t),
       (AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
@@ -163,8 +158,9 @@ set_option linter.uppercaseLean3 false in
 #align SemiRing.filtered_colimits.colimit_cocone_is_colimit SemiRingCat.FilteredColimits.colimitCoconeIsColimit
 
 instance forget₂MonPreservesFilteredColimits :
-    PreservesFilteredColimits (forget₂ SemiRingCat MonCat.{u})
-    where preserves_filtered_colimits {J hJ1 _} := letI : Category J := hJ1
+    PreservesFilteredColimits (forget₂ SemiRingCat MonCat.{u}) where
+  preserves_filtered_colimits {J hJ1 _} :=
+    letI : Category J := hJ1
     { preservesColimit := fun {F} =>
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ SemiRingCat MonCat.{u})) }
@@ -213,8 +209,7 @@ set_option linter.uppercaseLean3 false in
 def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι :=
-    {
-      (SemiRingCat.FilteredColimits.colimitCocone
+    { (SemiRingCat.FilteredColimits.colimitCocone
           (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{max v u})).ι with }
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing.filtered_colimits.colimit_cocone CommSemiRingCat.FilteredColimits.colimitCocone
@@ -237,8 +232,9 @@ set_option linter.uppercaseLean3 false in
 #align CommSemiRing.filtered_colimits.colimit_cocone_is_colimit CommSemiRingCat.FilteredColimits.colimitCoconeIsColimit
 
 instance forget₂SemiRingPreservesFilteredColimits :
-    PreservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat.{u})
-    where preserves_filtered_colimits {J hJ1 _} := letI : Category J := hJ1
+    PreservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat.{u}) where
+  preserves_filtered_colimits {J hJ1 _} :=
+    letI : Category J := hJ1
     { preservesColimit := fun {F} =>
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (SemiRingCat.FilteredColimits.colimitCoconeIsColimit
@@ -289,8 +285,7 @@ set_option linter.uppercaseLean3 false in
 def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι :=
-    {
-      (SemiRingCat.FilteredColimits.colimitCocone
+    { (SemiRingCat.FilteredColimits.colimitCocone
           (F ⋙ forget₂ RingCat SemiRingCat.{max v u})).ι with }
 set_option linter.uppercaseLean3 false in
 #align Ring.filtered_colimits.colimit_cocone RingCat.FilteredColimits.colimitCocone
@@ -313,8 +308,9 @@ set_option linter.uppercaseLean3 false in
 #align Ring.filtered_colimits.colimit_cocone_is_colimit RingCat.FilteredColimits.colimitCoconeIsColimit
 
 instance forget₂SemiRingPreservesFilteredColimits :
-    PreservesFilteredColimits (forget₂ RingCat SemiRingCat.{u})
-    where preserves_filtered_colimits {J hJ1 _} := letI : Category J := hJ1
+    PreservesFilteredColimits (forget₂ RingCat SemiRingCat.{u}) where
+  preserves_filtered_colimits {J hJ1 _} :=
+    letI : Category J := hJ1
     { preservesColimit := fun {F} =>
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (SemiRingCat.FilteredColimits.colimitCoconeIsColimit
@@ -386,8 +382,9 @@ set_option linter.uppercaseLean3 false in
 #align CommRing.filtered_colimits.colimit_cocone_is_colimit CommRingCat.FilteredColimits.colimitCoconeIsColimit
 
 instance forget₂RingPreservesFilteredColimits :
-    PreservesFilteredColimits (forget₂ CommRingCat RingCat.{u})
-    where preserves_filtered_colimits {J hJ1 _} := letI : Category J := hJ1
+    PreservesFilteredColimits (forget₂ CommRingCat RingCat.{u}) where
+  preserves_filtered_colimits {J hJ1 _} :=
+    letI : Category J := hJ1
     { preservesColimit := fun {F} =>
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (RingCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ CommRingCat RingCat.{u})) }