Port/Algebra.Category.Module.FilteredColimits (#4949)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Author: riccardobrasca

Mathlib.lean

@@ -52,6 +52,7 @@ import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Biproducts
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
+import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
 import Mathlib.Algebra.Category.ModuleCat.Images
 import Mathlib.Algebra.Category.ModuleCat.Kernels
 import Mathlib.Algebra.Category.ModuleCat.Limits

Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean

@@ -47,7 +47,7 @@ open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
 
 -- We use parameters here, mainly so we can have the abbreviations `G` and `G.mk` below, without
 -- passing around `F` all the time.
-variable {J : Type v}[SmallCategory J] [IsFiltered J] (F : J ⥤ GroupCat.{max v u})
+variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ GroupCat.{max v u})
 
 /-- The colimit of `F ⋙ forget₂ Group Mon` in the category `Mon`.
 In the following, we will show that this has the structure of a group.

Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean

@@ -0,0 +1,227 @@
+/-
+Copyright (c) 2021 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+
+! This file was ported from Lean 3 source module algebra.category.Module.filtered_colimits
+! leanprover-community/mathlib commit 806bbb0132ba63b93d5edbe4789ea226f8329979
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Category.GroupCat.FilteredColimits
+import Mathlib.Algebra.Category.ModuleCat.Basic
+
+/-!
+# The forgetful functor from `R`-modules preserves filtered colimits.
+
+Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
+to preserve _filtered_ colimits.
+
+In this file, we start with a ring `R`, a small filtered category `J` and a functor
+`F : J ⥤ Module R`. We show that the colimit of `F ⋙ forget₂ (Module R) AddCommGroup`
+(in `AddCommGroup`) carries the structure of an `R`-module, thereby showing that the forgetful
+functor `forget₂ (Module R) AddCommGroup` preserves filtered colimits. In particular, this implies
+that `forget (Module R)` preserves filtered colimits.
+
+-/
+
+
+universe v u
+
+noncomputable section
+
+open scoped Classical
+
+open CategoryTheory CategoryTheory.Limits
+
+-- avoid name collision with `_root_.max`.
+open CategoryTheory.IsFiltered renaming max → max'
+
+open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
+
+namespace ModuleCat.FilteredColimits
+
+section
+
+variable {R : Type u} [Ring R] {J : Type v} [SmallCategory J] [IsFiltered J]
+
+variable (F : J ⥤ ModuleCatMax.{v, u, u} R)
+
+/-- The colimit of `F ⋙ forget₂ (Module R) AddCommGroup` in the category `AddCommGroup`.
+In the following, we will show that this has the structure of an `R`-module.
+-/
+abbrev M : AddCommGroupCat :=
+  AddCommGroupCat.FilteredColimits.colimit.{v, u}
+    (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat.{max v u})
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.M ModuleCat.FilteredColimits.M
+
+/-- The canonical projection into the colimit, as a quotient type. -/
+abbrev M.mk : (Σ j, F.obj j) → M F :=
+  Quot.mk (Types.Quot.Rel (F ⋙ forget (ModuleCat R)))
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.M.mk ModuleCat.FilteredColimits.M.mk
+
+theorem M.mk_eq (x y : Σ j, F.obj j)
+    (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) : M.mk F x = M.mk F y :=
+  Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget (ModuleCat R)) x y h)
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.M.mk_eq ModuleCat.FilteredColimits.M.mk_eq
+
+/-- The "unlifted" version of scalar multiplication in the colimit. -/
+def colimitSmulAux (r : R) (x : Σ j, F.obj j) : M F :=
+  M.mk F ⟨x.1, r • x.2⟩
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_smul_aux ModuleCat.FilteredColimits.colimitSmulAux
+
+theorem colimitSmulAux_eq_of_rel (r : R) (x y : Σ j, F.obj j)
+    (h : Types.FilteredColimit.Rel.{v, u} (F ⋙ forget (ModuleCat R)) x y) :
+    colimitSmulAux F r x = colimitSmulAux F r y := by
+  apply M.mk_eq
+  obtain ⟨k, f, g, hfg⟩ := h
+  use k, f, g
+  simp only [Functor.comp_obj, Functor.comp_map, forget_map] at hfg
+  simp [hfg]
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_smul_aux_eq_of_rel ModuleCat.FilteredColimits.colimitSmulAux_eq_of_rel
+
+/-- Scalar multiplication in the colimit. See also `colimitSmulAux`. -/
+instance colimitHasSmul : SMul R (M F) where
+  smul r x := by
+    refine' Quot.lift (colimitSmulAux F r) _ x
+    intro x y h
+    apply colimitSmulAux_eq_of_rel
+    apply Types.FilteredColimit.rel_of_quot_rel
+    exact h
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_has_smul ModuleCat.FilteredColimits.colimitHasSmul
+
+@[simp]
+theorem colimit_smul_mk_eq (r : R) (x : Σ j, F.obj j) : r • M.mk F x = M.mk F ⟨x.1, r • x.2⟩ :=
+  rfl
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_smul_mk_eq ModuleCat.FilteredColimits.colimit_smul_mk_eq
+
+private theorem colimitModule.one_smul (x : (M F)) : (1 : R) • x = x := by
+  refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+  erw [colimit_smul_mk_eq F 1 ⟨j, x⟩]
+  simp
+  rfl
+
+-- Porting note: writing directly the `Module` instance makes things very slow.
+instance colimitMulAction : MulAction R (M F) where
+  one_smul x := by
+    refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+    erw [colimit_smul_mk_eq F 1 ⟨j, x⟩, one_smul]
+    rfl
+  mul_smul r s x := by
+    refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+    erw [colimit_smul_mk_eq F (r * s) ⟨j, x⟩, colimit_smul_mk_eq F s ⟨j, x⟩,
+      colimit_smul_mk_eq F r ⟨j, _⟩, mul_smul]
+
+instance colimitSMulWithZero : SMulWithZero R (M F) :=
+{ colimitMulAction F with
+  smul_zero := fun r => by
+    erw [colimit_zero_eq _ (IsFiltered.Nonempty.some : J), colimit_smul_mk_eq, smul_zero]
+    rfl
+  zero_smul := fun x => by
+    refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+    erw [colimit_smul_mk_eq, zero_smul, colimit_zero_eq _ j]
+    rfl }
+
+private theorem colimitModule.add_smul (r s : R) (x : (M F)) : (r + s) • x = r • x + s • x := by
+  refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+  erw [colimit_smul_mk_eq, _root_.add_smul, colimit_smul_mk_eq, colimit_smul_mk_eq,
+      colimit_add_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j), CategoryTheory.Functor.map_id, id_apply,
+      id_apply]
+  rfl
+
+instance colimitModule : Module R (M F) :=
+{ colimitMulAction F,
+  colimitSMulWithZero F with
+  smul_add := fun r x y => by
+    refine' Quot.induction_on₂ x y _; clear x y; intro x y; cases' x with i x; cases' y with j y
+    erw [colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
+      (IsFiltered.rightToMax i j), colimit_smul_mk_eq, smul_add, colimit_smul_mk_eq,
+      colimit_smul_mk_eq, colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
+      (IsFiltered.rightToMax i j), LinearMap.map_smul, LinearMap.map_smul]
+    rfl
+  add_smul := colimitModule.add_smul F }
+
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_module ModuleCat.FilteredColimits.colimitModule
+
+/-- The bundled `R`-module giving the filtered colimit of a diagram. -/
+def colimit : ModuleCatMax.{v, u, u} R :=
+  ModuleCat.of R (M F)
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit ModuleCat.FilteredColimits.colimit
+
+/-- The linear map from a given `R`-module in the diagram to the colimit module. -/
+def coconeMorphism (j : J) : F.obj j ⟶ colimit F :=
+  { (AddCommGroupCat.FilteredColimits.colimitCocone
+      (F ⋙ forget₂ (ModuleCat R) AddCommGroupCat.{max v u})).ι.app j with
+    map_smul' := fun r x => by erw [colimit_smul_mk_eq F r ⟨j, x⟩]; rfl }
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.cocone_morphism ModuleCat.FilteredColimits.coconeMorphism
+
+/-- The cocone over the proposed colimit module. -/
+def colimitCocone : Cocone F where
+  pt := colimit F
+  ι :=
+    { app := coconeMorphism F
+      naturality := fun _ _' f =>
+        LinearMap.coe_injective ((Types.colimitCocone (F ⋙ forget (ModuleCat R))).ι.naturality f) }
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_cocone ModuleCat.FilteredColimits.colimitCocone
+
+/-- Given a cocone `t` of `F`, the induced monoid linear map from the colimit to the cocone point.
+We already know that this is a morphism between additive groups. The only thing left to see is that
+it is a linear map, i.e. preserves scalar multiplication.
+-/
+def colimitDesc (t : Cocone F) : colimit F ⟶ t.pt :=
+  { (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit
+          (F ⋙ forget₂ (ModuleCatMax.{v, u} R) AddCommGroupCat.{max v u})).desc
+      ((forget₂ (ModuleCat R) AddCommGroupCat.{max v u}).mapCocone t) with
+    map_smul' := fun r x => by
+      refine' Quot.inductionOn x _; clear x; intro x; cases' x with j x
+      erw [colimit_smul_mk_eq]
+      exact LinearMap.map_smul (t.ι.app j) r x }
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_desc ModuleCat.FilteredColimits.colimitDesc
+
+/-- The proposed colimit cocone is a colimit in `Module R`. -/
+def colimitCoconeIsColimit : IsColimit (colimitCocone F) where
+  desc := colimitDesc F
+  fac t j :=
+    LinearMap.coe_injective <|
+      (Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget (ModuleCat R))).fac
+        ((forget (ModuleCat R)).mapCocone t) j
+  uniq t _ h :=
+    LinearMap.coe_injective <|
+      (Types.colimitCoconeIsColimit (F ⋙ forget (ModuleCat R))).uniq
+        ((forget (ModuleCat R)).mapCocone t) _ fun j => funext fun x => LinearMap.congr_fun (h j) x
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.colimit_cocone_is_colimit ModuleCat.FilteredColimits.colimitCoconeIsColimit
+
+instance forget₂AddCommGroupPreservesFilteredColimits :
+    PreservesFilteredColimits (forget₂ (ModuleCat.{u} R) AddCommGroupCat.{u}) where
+  preserves_filtered_colimits J _ _ :=
+  { -- Porting note: without the curly braces for `F`
+    -- here we get a confusing error message about universes.
+    preservesColimit := fun {F : J ⥤ ModuleCat.{u} R} =>
+      preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit F)
+        (AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit
+          (F ⋙ forget₂ (ModuleCat.{u} R) AddCommGroupCat.{u})) }
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.forget₂_AddCommGroup_preserves_filtered_colimits ModuleCat.FilteredColimits.forget₂AddCommGroupPreservesFilteredColimits
+
+instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget (ModuleCat.{u} R)) :=
+  Limits.compPreservesFilteredColimits (forget₂ (ModuleCat R) AddCommGroupCat)
+    (forget AddCommGroupCat)
+set_option linter.uppercaseLean3 false in
+#align Module.filtered_colimits.forget_preserves_filtered_colimits ModuleCat.FilteredColimits.forgetPreservesFilteredColimits
+
+end
+
+end ModuleCat.FilteredColimits

Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

@@ -41,7 +41,7 @@ related work.
 -/
 
 
-universe w v v' u
+universe w w' v v' u
 
 namespace CategoryTheory
 
@@ -201,8 +201,8 @@ end
 /-- `HasForget₂ C D`, where `C` and `D` are both concrete categories, provides a functor
 `forget₂ C D : C ⥤ D` and a proof that `forget₂ ⋙ (forget D) = forget C`.
 -/
-class HasForget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory.{u} C] [Category D]
-  [ConcreteCategory.{u} D] where
+class HasForget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
+  [Category.{v'} D] [ConcreteCategory.{w} D] where
   /-- A functor from `C` to `D` -/
   forget₂ : C ⥤ D
   /-- It covers the `ConcreteCategory.forget` for `C` and `D` -/
@@ -212,61 +212,65 @@ class HasForget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory.{u}
 /-- The forgetful functor `C ⥤ D` between concrete categories for which we have an instance
 `HasForget₂ C `. -/
 @[reducible]
-def forget₂ (C : Type v) (D : Type v') [Category C] [ConcreteCategory C] [Category D]
-    [ConcreteCategory D] [HasForget₂ C D] : C ⥤ D :=
+def forget₂ (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
+    [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : C ⥤ D :=
   HasForget₂.forget₂
 #align category_theory.forget₂ CategoryTheory.forget₂
 
-instance forget₂_faithful (C : Type v) (D : Type v') [Category C] [ConcreteCategory C] [Category D]
-    [ConcreteCategory D] [HasForget₂ C D] : Faithful (forget₂ C D) :=
+instance forget₂_faithful (C : Type u) (D : Type u') [Category.{v} C] [ConcreteCategory.{w} C]
+    [Category.{v'} D] [ConcreteCategory.{w} D] [HasForget₂ C D] : Faithful (forget₂ C D) :=
   HasForget₂.forget_comp.faithful_of_comp
 #align category_theory.forget₂_faithful CategoryTheory.forget₂_faithful
 
-instance forget₂_preservesMonomorphisms (C : Type v) (D : Type v') [Category C] [ConcreteCategory C]
-    [Category D] [ConcreteCategory D] [HasForget₂ C D] [(forget C).PreservesMonomorphisms] :
+instance forget₂_preservesMonomorphisms (C : Type u) (D : Type u')
+    [Category.{v} C] [ConcreteCategory.{w} C] [Category.{v'} D] [ConcreteCategory.{w} D]
+    [HasForget₂ C D] [(forget C).PreservesMonomorphisms] :
     (forget₂ C D).PreservesMonomorphisms :=
   have : (forget₂ C D ⋙ forget D).PreservesMonomorphisms := by
     simp only [HasForget₂.forget_comp]
     infer_instance
   Functor.preservesMonomorphisms_of_preserves_of_reflects _ (forget D)
 #align category_theory.forget₂_preserves_monomorphisms CategoryTheory.forget₂_preservesMonomorphisms
 
-instance forget₂_preservesEpimorphisms (C : Type v) (D : Type v') [Category C] [ConcreteCategory C]
-    [Category D] [ConcreteCategory D] [HasForget₂ C D] [(forget C).PreservesEpimorphisms] :
+instance forget₂_preservesEpimorphisms (C : Type u) (D : Type u')
+    [Category.{v} C] [ConcreteCategory.{w} C] [Category.{v'} D] [ConcreteCategory.{w} D]
+    [HasForget₂ C D] [(forget C).PreservesEpimorphisms] :
     (forget₂ C D).PreservesEpimorphisms :=
   have : (forget₂ C D ⋙ forget D).PreservesEpimorphisms := by
     simp only [HasForget₂.forget_comp]
     infer_instance
   Functor.preservesEpimorphisms_of_preserves_of_reflects _ (forget D)
 #align category_theory.forget₂_preserves_epimorphisms CategoryTheory.forget₂_preservesEpimorphisms
 
-instance InducedCategory.concreteCategory {C : Type v} {D : Type v'} [Category D]
-    [ConcreteCategory D] (f : C → D) : ConcreteCategory (InducedCategory D f) where
+instance InducedCategory.concreteCategory {C : Type u} {D : Type u'}
+    [Category.{v'} D] [ConcreteCategory.{w} D] (f : C → D) :
+      ConcreteCategory (InducedCategory D f) where
   forget := inducedFunctor f ⋙ forget D
 #align category_theory.induced_category.concrete_category CategoryTheory.InducedCategory.concreteCategory
 
-instance InducedCategory.hasForget₂ {C : Type v} {D : Type v'} [Category D] [ConcreteCategory D]
-    (f : C → D) : HasForget₂ (InducedCategory D f) D where
+instance InducedCategory.hasForget₂ {C : Type u} {D : Type u'} [Category.{v} D]
+    [ConcreteCategory.{w} D] (f : C → D) : HasForget₂ (InducedCategory D f) D where
   forget₂ := inducedFunctor f
   forget_comp := rfl
 #align category_theory.induced_category.has_forget₂ CategoryTheory.InducedCategory.hasForget₂
 
-instance FullSubcategory.concreteCategory {C : Type v} [Category C] [ConcreteCategory C]
+instance FullSubcategory.concreteCategory {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C]
     (Z : C → Prop) : ConcreteCategory (FullSubcategory Z) where
   forget := fullSubcategoryInclusion Z ⋙ forget C
 #align category_theory.full_subcategory.concrete_category CategoryTheory.FullSubcategoryₓ.concreteCategory
 
-instance FullSubcategory.hasForget₂ {C : Type v} [Category C] [ConcreteCategory C] (Z : C → Prop) :
-    HasForget₂ (FullSubcategory Z) C where
+instance FullSubcategory.hasForget₂ {C : Type u} [Category.{v} C] [ConcreteCategory.{w} C]
+    (Z : C → Prop) : HasForget₂ (FullSubcategory Z) C where
   forget₂ := fullSubcategoryInclusion Z
   forget_comp := rfl
 #align category_theory.full_subcategory.has_forget₂ CategoryTheory.FullSubcategoryₓ.hasForget₂
 
 /-- In order to construct a “partially forgetting” functor, we do not need to verify functor laws;
 it suffices to ensure that compositions agree with `forget₂ C D ⋙ forget D = forget C`.
 -/
-def HasForget₂.mk' {C : Type v} {D : Type v'} [Category C] [ConcreteCategory C] [Category D]
-    [ConcreteCategory D] (obj : C → D) (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X)
+def HasForget₂.mk' {C : Type u} {D : Type u'} [Category.{v} C] [ConcreteCategory.{w} C]
+    [Category.{v'} D] [ConcreteCategory.{w} D]
+    (obj : C → D) (h_obj : ∀ X, (forget D).obj (obj X) = (forget C).obj X)
     (map : ∀ {X Y}, (X ⟶ Y) → (obj X ⟶ obj Y))
     (h_map : ∀ {X Y} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)) : HasForget₂ C D
     where
@@ -276,7 +280,8 @@ def HasForget₂.mk' {C : Type v} {D : Type v'} [Category C] [ConcreteCategory C
 
 /-- Every forgetful functor factors through the identity functor. This is not a global instance as
     it is prone to creating type class resolution loops. -/
-def hasForgetToType (C : Type v) [Category C] [ConcreteCategory C] : HasForget₂ C (Type u) where
+def hasForgetToType (C : Type u) [Category.{v} C] [ConcreteCategory.{w} C] :
+    HasForget₂ C (Type w) where
   forget₂ := forget C
   forget_comp := Functor.comp_id _
 #align category_theory.has_forget_to_Type CategoryTheory.hasForgetToType