feat(algebra): monoidal category of R-modules (#2125)

* feat(algebra): monoidal category of R-modules

* docstrings

* minor

* tweaks

* fix import

* fixes

* reduce use of @

* broken

* fixes

* Update src/algebra/category/Module/basic.lean

Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

Author: 4 people

src/algebra/category/Module/basic.lean

@@ -5,10 +5,12 @@ Authors: Robert A. Spencer, Markus Himmel
 -/
 import algebra.module
 import algebra.punit_instances
+import algebra.category.Group
 import category_theory.concrete_category
 import category_theory.limits.shapes.zero
 import category_theory.limits.shapes.kernels
 import linear_algebra.basic
+
 open category_theory
 open category_theory.limits
 open category_theory.limits.walking_parallel_pair
@@ -44,8 +46,13 @@ def of (X : Type u) [add_comm_group X] [module R X] : Module R := ⟨R, X⟩
 
 instance : inhabited (Module R) := ⟨of R punit⟩
 
+@[simp]
 lemma of_apply (X : Type u) [add_comm_group X] [module R X] : (of R X : Type u) = X := rfl
 
+/-- Forgetting the underlying type and then building the bundled object returns the original module. -/
+def of_self (M : Module R) : Module.of R M ≅ M :=
+{ hom := 𝟙 M, inv := 𝟙 M }
+
 instance : subsingleton (of R punit) :=
 by { rw of_apply R punit, apply_instance }
 
@@ -60,18 +67,56 @@ instance : has_zero_object.{u} (Module R) :=
   { default := (0 : X →ₗ[R] punit),
     uniq := λ _, linear_map.ext $ λ x, subsingleton.elim _ _ } }
 
-variables (M N U : Module R)
+variables {R} {M N U : Module R}
 
 @[simp] lemma id_apply (m : M) : (𝟙 M : M → M) m = m := rfl
 
 @[simp] lemma coe_comp (f : M ⟶ N) (g : N ⟶ U) :
   ((f ≫ g) : M → U) = g ∘ f := rfl
 
-instance hom_is_module_hom {M₁ M₂ : Module R} (f : M₁ ⟶ M₂) :
-  is_linear_map R (f : M₁ → M₂) := linear_map.is_linear _
+instance hom_is_module_hom (f : M ⟶ N) :
+  is_linear_map R (f : M → N) := linear_map.is_linear _
+
+end Module
+
+variables {R}
+variables {X₁ X₂ : Type u}
+
+/-- Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s. -/
+@[simps]
+def linear_equiv.to_Module_iso
+  {g₁ : add_comm_group X₁} {g₂ : add_comm_group X₂} {m₁ : module R X₁} {m₂ : module R X₂} (e : X₁ ≃ₗ[R] X₂) :
+  Module.of R X₁ ≅ Module.of R X₂ :=
+{ hom := (e : X₁ →ₗ[R] X₂),
+  inv := (e.symm : X₂ →ₗ[R] X₁),
+  hom_inv_id' := begin ext, exact e.left_inv x, end,
+  inv_hom_id' := begin ext, exact e.right_inv x, end, }
+
+namespace category_theory.iso
+
+/-- Build a `linear_equiv` from an isomorphism in the category `Module R`. -/
+@[simps]
+def to_linear_equiv {X Y : Module.{u} R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
+{ to_fun    := i.hom,
+  inv_fun   := i.inv,
+  left_inv  := by tidy,
+  right_inv := by tidy,
+  add       := by tidy,
+  smul      := by tidy, }.
+
+end category_theory.iso
+
+/-- linear equivalences between `module`s are the same as (isomorphic to) isomorphisms in `Module` -/
+@[simps]
+def linear_equiv_iso_Group_iso {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] :
+  (X ≃ₗ[R] Y) ≅ (Module.of R X ≅ Module.of R Y) :=
+{ hom := λ e, e.to_Module_iso,
+  inv := λ i, i.to_linear_equiv, }
+
+namespace Module
 
 section kernel
-variable (f : M ⟶ N)
+variables {R} {M N : Module R} (f : M ⟶ N)
 
 local attribute [instance] has_zero_object.zero_morphisms_of_zero_object
 
@@ -87,7 +132,7 @@ def kernel_cone : cone (parallel_pair f 0) :=
     naturality' := λ j j' g, by { cases j; cases j'; cases g; tidy } } }
 
 /-- The kernel of a linear map is a kernel in the categorical sense -/
-def kernel_is_limit : is_limit (kernel_cone _ _ _ f) :=
+def kernel_is_limit : is_limit (kernel_cone f) :=
 { lift := λ s, linear_map.cod_restrict f.ker (fork.ι s) (λ c, linear_map.mem_ker.2 $
   by { erw [←@function.comp_apply _ _ _ f (fork.ι s) c, ←coe_comp, fork.condition,
     has_zero_morphisms.comp_zero _ (fork.ι s) N], refl }),
@@ -99,7 +144,7 @@ def kernel_is_limit : is_limit (kernel_cone _ _ _ f) :=
     { rw [←cone_parallel_pair_right, ←cone_parallel_pair_right], refl }
   end,
   uniq' := λ s m h, linear_map.ext $ λ x, subtype.ext.2 $
-    have h₁ : (m ≫ (kernel_cone _ _ _ f).π.app zero).to_fun = (s.π.app zero).to_fun,
+    have h₁ : (m ≫ (kernel_cone f).π.app zero).to_fun = (s.π.app zero).to_fun,
     by { congr, exact h zero },
     by convert @congr_fun _ _ _ _ h₁ x }
 
@@ -108,7 +153,7 @@ end kernel
 local attribute [instance] has_zero_object.zero_morphisms_of_zero_object
 
 instance : has_kernels.{u} (Module R) :=
-⟨λ _ _ f, ⟨kernel_cone _ _ _ f, kernel_is_limit _ _ _ f⟩⟩
+⟨λ _ _ f, ⟨kernel_cone f, kernel_is_limit f⟩⟩
 
 end Module
 

src/algebra/category/Module/monoidal.lean

@@ -0,0 +1,127 @@
+import category_theory.monoidal.category
+import algebra.category.Module.basic
+import linear_algebra.tensor_product
+
+/-!
+# The monoidal category structure on R-modules
+
+Mostly this uses existing machinery in `linear_algebra.tensor_product`.
+We just need to provide a few small missing pieces to build the
+`monoidal_category` instance.
+
+If you're happy using the bundled `Module R`, it may be possible to mostly
+use this as an interface and not need to interact much with the implementation details.
+-/
+
+universe u
+
+open category_theory
+
+namespace Module
+
+variables {R : Type u} [comm_ring R]
+
+namespace monoidal_category
+-- The definitions inside this namespace are essentially private.
+-- After we build the `monoidal_category (Module R)` instance,
+-- you should use that API.
+
+open_locale tensor_product
+
+/-- (implementation) tensor product of R-modules -/
+def tensor_obj (M N : Module R) : Module R := Module.of R (M ⊗[R] N)
+/-- (implementation) tensor product of morphisms R-modules -/
+def tensor_hom {M N M' N' : Module R} (f : M ⟶ N) (g : M' ⟶ N') : tensor_obj M M' ⟶ tensor_obj N N' :=
+tensor_product.map f g
+
+lemma tensor_id (M N : Module R) : tensor_hom (𝟙 M) (𝟙 N) = 𝟙 (Module.of R (↥M ⊗ ↥N)) :=
+by tidy
+
+lemma tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Module R}
+  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
+    tensor_hom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensor_hom f₁ f₂ ≫ tensor_hom g₁ g₂ :=
+by tidy
+
+/-- (implementation) the associator for R-modules -/
+def associator (M N K : Module R) : tensor_obj (tensor_obj M N) K ≅ tensor_obj M (tensor_obj N K) :=
+linear_equiv.to_Module_iso (tensor_product.assoc R M N K)
+
+lemma associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : Module R}
+  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :
+    tensor_hom (tensor_hom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
+    (associator X₁ X₂ X₃).hom ≫ tensor_hom f₁ (tensor_hom f₂ f₃) :=
+begin
+  apply tensor_product.ext_threefold,
+  intros x y z,
+  refl
+end
+
+lemma pentagon (W X Y Z : Module R) :
+  tensor_hom (associator W X Y).hom (𝟙 Z) ≫ (associator W (tensor_obj X Y) Z).hom ≫ tensor_hom (𝟙 W) (associator X Y Z).hom =
+    (associator (tensor_obj W X) Y Z).hom ≫ (associator W X (tensor_obj Y Z)).hom :=
+begin
+  apply tensor_product.ext_fourfold,
+  intros w x y z,
+  refl
+end
+
+/-- (implementation) the left unitor for R-modules -/
+def left_unitor (M : Module R) : Module.of R (R ⊗[R] M) ≅ M :=
+(linear_equiv.to_Module_iso (tensor_product.lid R M) : of R (R ⊗ M) ≅ of R M).trans (of_self R M)
+
+lemma left_unitor_naturality {M N : Module R} (f : M ⟶ N) :
+  tensor_hom (𝟙 (Module.of R R)) f ≫ (left_unitor N).hom = (left_unitor M).hom ≫ f :=
+begin
+  ext x y, simp,
+  erw [tensor_product.lid_tmul, tensor_product.lid_tmul],
+  rw linear_map.map_smul,
+  refl,
+end
+
+/-- (implementation) the right unitor for R-modules -/
+def right_unitor (M : Module R) : Module.of R (M ⊗[R] R) ≅ M :=
+(linear_equiv.to_Module_iso (tensor_product.rid R M) : of R (M ⊗ R) ≅ of R M).trans (of_self R M)
+
+lemma right_unitor_naturality {M N : Module R} (f : M ⟶ N) :
+  tensor_hom f (𝟙 (Module.of R R)) ≫ (right_unitor N).hom = (right_unitor M).hom ≫ f :=
+begin
+  ext x y, simp,
+  erw [tensor_product.rid_tmul, tensor_product.rid_tmul],
+  rw linear_map.map_smul,
+  refl,
+end
+
+lemma triangle (M N : Module R) :
+  (associator M (Module.of R R) N).hom ≫ tensor_hom (𝟙 M) (left_unitor N).hom =
+    tensor_hom (right_unitor M).hom (𝟙 N) :=
+begin
+  apply tensor_product.ext_threefold,
+  intros x y z,
+  change R at y,
+  dsimp [tensor_hom, associator],
+  erw [tensor_product.lid_tmul, tensor_product.rid_tmul],
+  apply (tensor_product.smul_tmul _ _ _).symm
+end
+
+end monoidal_category
+
+open monoidal_category
+
+instance : monoidal_category (Module.{u} R) :=
+{ -- data
+  tensor_obj   := tensor_obj,
+  tensor_hom   := @tensor_hom _ _,
+  tensor_unit  := Module.of R R,
+  associator   := associator,
+  left_unitor  := left_unitor,
+  right_unitor := right_unitor,
+  -- properties
+  tensor_id'               := λ M N, tensor_id M N,
+  tensor_comp'             := λ M N K M' N' K' f g h, tensor_comp f g h,
+  associator_naturality'   := λ M N K M' N' K' f g h, associator_naturality f g h,
+  left_unitor_naturality'  := λ M N f, left_unitor_naturality f,
+  right_unitor_naturality' := λ M N f, right_unitor_naturality f,
+  pentagon'                := λ M N K L, pentagon M N K L,
+  triangle'                := λ M N, triangle M N, }
+
+end Module

src/category_theory/limits/types.lean

@@ -14,12 +14,14 @@ namespace category_theory.limits.types
 
 variables {J : Type u} [small_category J]
 
-def limit (F : J ⥤ Type u) : cone F :=
+/-- (implementation) the limit cone of a functor to Type -/
+def limit_ (F : J ⥤ Type u) : cone F :=
 { X := F.sections,
   π := { app := λ j u, u.val j } }
 
 local attribute [elab_simple] congr_fun
-def limit_is_limit (F : J ⥤ Type u) : is_limit (limit F) :=
+/-- (implementation) the fact that the proposed limit cone is the limit -/
+def limit_is_limit_ (F : J ⥤ Type u) : is_limit (limit_ F) :=
 { lift := λ s v, ⟨λ j, s.π.app j v, λ j j' f, congr_fun (cone.w s f) _⟩,
   uniq' :=
   begin
@@ -29,51 +31,53 @@ def limit_is_limit (F : J ⥤ Type u) : is_limit (limit F) :=
 
 instance : has_limits.{u} (Type u) :=
 { has_limits_of_shape := λ J 𝒥,
-  { has_limit := λ F, by exactI { cone := limit F, is_limit := limit_is_limit F } } }
+  { has_limit := λ F, by exactI { cone := limit_ F, is_limit := limit_is_limit_ F } } }
 
 @[simp] lemma types_limit (F : J ⥤ Type u) :
   limits.limit F = {u : Π j, F.obj j // ∀ {j j'} f, F.map f (u j) = u j'} := rfl
-@[simp] lemma types_limit_π (F : J ⥤ Type u) (j : J) (g : (limit F).X) :
+@[simp] lemma types_limit_π (F : J ⥤ Type u) (j : J) (g : limit F) :
   limit.π F j g = g.val j := rfl
 @[simp] lemma types_limit_pre
-  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : (limit F).X) :
-  limit.pre F E g = (⟨λ k, g.val (E.obj k), by obviously⟩ : (limit (E ⋙ F)).X) := rfl
-@[simp] lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : (limit F).X) :
-  (lim.map α : (limit F).X → (limit G).X) g =
+  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : limit F) :
+  limit.pre F E g = (⟨λ k, g.val (E.obj k), by obviously⟩ : limit (E ⋙ F)) := rfl
+@[simp] lemma types_limit_map {F G : J ⥤ Type u} (α : F ⟶ G) (g : limit F) :
+  (lim.map α : limit F → limit G) g =
   (⟨λ j, (α.app j) (g.val j), λ j j' f,
-    by {rw ←functor_to_types.naturality, dsimp, rw ←(g.property f)}⟩ : (limit G).X) := rfl
+    by {rw ←functor_to_types.naturality, dsimp, rw ←(g.property f)}⟩ : limit G) := rfl
 
 @[simp] lemma types_limit_lift (F : J ⥤ Type u) (c : cone F) (x : c.X) :
-  limit.lift F c x = (⟨λ j, c.π.app j x, λ j j' f, congr_fun (cone.w c f) x⟩ : (limit F).X) :=
+  limit.lift F c x = (⟨λ j, c.π.app j x, λ j j' f, congr_fun (cone.w c f) x⟩ : limit F) :=
 rfl
 
 
-def colimit (F : J ⥤ Type u) : cocone F :=
+/-- (implementation) the colimit cocone of a functor to Type -/
+def colimit_ (F : J ⥤ Type u) : cocone F :=
 { X := @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2),
   ι :=
   { app := λ j x, quot.mk _ ⟨j, x⟩,
     naturality' := λ j j' f, funext $ λ x, eq.symm (quot.sound ⟨f, rfl⟩) } }
 
 local attribute [elab_with_expected_type] quot.lift
 
-def colimit_is_colimit (F : J ⥤ Type u) : is_colimit (colimit F) :=
+/-- (implementation) the fact that the proposed colimit cocone is the colimit -/
+def colimit_is_colimit_ (F : J ⥤ Type u) : is_colimit (colimit_ F) :=
 { desc := λ s, quot.lift (λ (p : Σ j, F.obj j), s.ι.app p.1 p.2)
     (assume ⟨j, x⟩ ⟨j', x'⟩ ⟨f, hf⟩, by rw hf; exact (congr_fun (cocone.w s f) x).symm) }
 
 instance : has_colimits.{u} (Type u) :=
 { has_colimits_of_shape := λ J 𝒥,
-  { has_colimit := λ F, by exactI { cocone := colimit F, is_colimit := colimit_is_colimit F } } }
+  { has_colimit := λ F, by exactI { cocone := colimit_ F, is_colimit := colimit_is_colimit_ F } } }
 
 @[simp] lemma types_colimit (F : J ⥤ Type u) :
   limits.colimit F = @quot (Σ j, F.obj j) (λ p p', ∃ f : p.1 ⟶ p'.1, p'.2 = F.map f p.2) := rfl
 @[simp] lemma types_colimit_ι (F : J ⥤ Type u) (j : J) :
   colimit.ι F j = λ x, quot.mk _ ⟨j, x⟩ := rfl
 @[simp] lemma types_colimit_pre
-  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) (g : (colimit (E ⋙ F)).X) :
+  (F : J ⥤ Type u) {K : Type u} [𝒦 : small_category K] (E : K ⥤ J) :
   colimit.pre F E =
   quot.lift (λ p, quot.mk _ ⟨E.obj p.1, p.2⟩) (λ p p' ⟨f, h⟩, quot.sound ⟨E.map f, h⟩) := rfl
 @[simp] lemma types_colimit_map {F G : J ⥤ Type u} (α : F ⟶ G) :
-  (colim.map α : (colimit F).X → (colimit G).X) =
+  (colim.map α : colimit F → colimit G) =
   quot.lift
     (λ p, quot.mk _ ⟨p.1, (α.app p.1) p.2⟩)
     (λ p p' ⟨f, h⟩, quot.sound ⟨f, by rw h; exact functor_to_types.naturality _ _ α f _⟩) := rfl

src/linear_algebra/basic.lean

@@ -1331,22 +1331,26 @@ section
 variable (M)
 
 /-- The identity map is a linear equivalence. -/
-@[refl] def refl : M ≃ₗ[R] M := { .. linear_map.id, .. equiv.refl M }
+@[refl]
+def refl : M ≃ₗ[R] M := { .. linear_map.id, .. equiv.refl M }
 end
 
 /-- Linear equivalences are symmetric. -/
-@[symm] def symm (e : M ≃ₗ[R] M₂) : M₂ ≃ₗ[R] M :=
+@[symm]
+def symm (e : M ≃ₗ[R] M₂) : M₂ ≃ₗ[R] M :=
 { .. e.to_linear_map.inverse e.inv_fun e.left_inv e.right_inv,
   .. e.to_equiv.symm }
 
 /-- Linear equivalences are transitive. -/
-@[trans] def trans (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : M ≃ₗ[R] M₃ :=
+@[trans]
+def trans (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) : M ≃ₗ[R] M₃ :=
 { .. e₂.to_linear_map.comp e₁.to_linear_map,
   .. e₁.to_equiv.trans e₂.to_equiv }
 
 /-- A linear equivalence is an additive equivalence. -/
 def to_add_equiv (e : M ≃ₗ[R] M₂) : M ≃+ M₂ := { map_add' := e.add, .. e }
 
+@[simp] theorem trans_apply (e₁ : M ≃ₗ[R] M₂) (e₂ : M₂ ≃ₗ[R] M₃) (c : M) : (e₁.trans e₂) c = e₂ (e₁ c) := rfl
 @[simp] theorem apply_symm_apply (e : M ≃ₗ[R] M₂) (c : M₂) : e (e.symm c) = c := e.6 c
 @[simp] theorem symm_apply_apply (e : M ≃ₗ[R] M₂) (b : M) : e.symm (e b) = b := e.5 b