feat(algebra/category/Module): Free R C, the free R-linear completion…

… of a category (#7177)

The free R-linear completion of a category.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

src/algebra/category/Module/adjunctions.lean

@@ -7,6 +7,7 @@ import algebra.category.Module.monoidal
 import category_theory.monoidal.functorial
 import category_theory.monoidal.types
 import linear_algebra.direct_sum.finsupp
+import category_theory.linear.linear_functor
 
 /-!
 The functor of forming finitely supported functions on a type with values in a `[ring R]`
@@ -16,12 +17,12 @@ the forgetful functor from `R`-modules to types.
 
 noncomputable theory
 
-universe u
-
 open category_theory
 
 namespace Module
 
+universe u
+
 open_locale classical
 
 variables (R : Type u)
@@ -114,3 +115,195 @@ instance : lax_monoidal.{u} (free R).obj :=
 end free
 
 end Module
+
+namespace category_theory
+
+universes v u
+
+/--
+`Free R C` is a type synonym for `C`, which, given `[comm_ring R]` and `[category C]`,
+we will equip with a category structure where the morphisms are formal `R`-linear combinations
+of the morphisms in `C`.
+-/
+@[nolint unused_arguments has_inhabited_instance]
+def Free (R : Type*) (C : Type u) := C
+
+/--
+Consider an object of `C` as an object of the `R`-linear completion.
+-/
+def Free.of (R : Type*) {C : Type u} (X : C) : Free R C := X
+
+variables (R : Type*) [comm_ring R] (C : Type u) [category.{v} C]
+
+open finsupp
+
+-- Conceptually, it would be nice to construct this via "transport of enrichment",
+-- using the fact that `Module.free R : Type ⥤ Module R` and `Module.forget` are both lax monoidal.
+-- This still seems difficult, so we just do it by hand.
+instance category_Free : category (Free R C) :=
+{ hom := λ (X Y : C), (X ⟶ Y) →₀ R,
+  id := λ (X : C), finsupp.single (𝟙 X) 1,
+  comp := λ (X Y Z : C) f g, f.sum (λ f' s, g.sum (λ g' t, finsupp.single (f' ≫ g') (s * t))),
+  assoc' := λ W X Y Z f g h,
+  begin
+    dsimp,
+    -- This imitates the proof of associativity for `monoid_algebra`.
+    simp only [sum_sum_index, sum_single_index,
+      single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
+      add_mul, mul_add, category.assoc, mul_assoc, zero_mul, mul_zero, sum_zero, sum_add],
+  end }.
+
+namespace Free
+
+section
+local attribute [simp] category_theory.category_Free
+
+@[simp]
+lemma single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
+  (single f r ≫ single g s : (Free.of R X) ⟶ (Free.of R Z)) = single (f ≫ g) (r * s) :=
+by { dsimp, simp, }
+
+instance : preadditive (Free R C) :=
+{ hom_group := λ X Y, finsupp.add_comm_group,
+  add_comp' := λ X Y Z f f' g, begin
+    dsimp,
+    rw [finsupp.sum_add_index];
+    { simp [add_mul], }
+  end,
+  comp_add' := λ X Y Z f g g', begin
+    dsimp,
+    rw ← finsupp.sum_add,
+    congr, ext r h,
+    rw [finsupp.sum_add_index];
+    { simp [mul_add], },
+  end, }
+
+instance : linear R (Free R C) :=
+{ hom_module := λ X Y, finsupp.module (X ⟶ Y) R,
+  smul_comp' := λ X Y Z r f g, begin
+    dsimp,
+    rw [finsupp.sum_smul_index];
+    simp [finsupp.smul_sum, mul_assoc],
+  end,
+  comp_smul' := λ X Y Z f r g, begin
+    dsimp,
+    simp_rw [finsupp.smul_sum],
+    congr, ext h s,
+    rw [finsupp.sum_smul_index];
+    simp [finsupp.smul_sum, mul_left_comm],
+  end, }
+
+end
+
+/--
+A category embeds into its `R`-linear completion.
+-/
+@[simps]
+def embedding : C ⥤ Free R C :=
+{ obj := λ X, X,
+  map := λ X Y f, finsupp.single f 1,
+  map_id' := λ X, rfl,
+  map_comp' := λ X Y Z f g, by simp, }
+
+variables (R) {C} {D : Type u} [category.{v} D] [preadditive D] [linear R D]
+
+open preadditive linear
+
+/--
+A functor to a preadditive category lifts to a functor from its `R`-linear completion.
+-/
+@[simps]
+def lift (F : C ⥤ D) : Free R C ⥤ D :=
+{ obj := λ X, F.obj X,
+  map := λ X Y f, f.sum (λ f' r, r • (F.map f')),
+  map_id' := by { dsimp [category_theory.category_Free], simp },
+  map_comp' := λ X Y Z f g, begin
+    apply finsupp.induction_linear f,
+    { simp, },
+    { intros f₁ f₂ w₁ w₂,
+      rw add_comp,
+      rw [finsupp.sum_add_index, finsupp.sum_add_index],
+      { simp [w₁, w₂, add_comp], },
+      { simp, },
+      { intros, simp only [add_smul], },
+      { simp, },
+      { intros, simp only [add_smul], }, },
+    { intros f' r,
+      apply finsupp.induction_linear g,
+      { simp, },
+      { intros f₁ f₂ w₁ w₂,
+        rw comp_add,
+        rw [finsupp.sum_add_index, finsupp.sum_add_index],
+        { simp [w₁, w₂, add_comp], },
+        { simp, },
+        { intros, simp only [add_smul], },
+        { simp, },
+        { intros, simp only [add_smul], }, },
+      { intros g' s,
+        erw single_comp_single,
+        simp [mul_comm r s, mul_smul], } }
+  end, }
+
+@[simp]
+lemma lift_map_single (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) (r : R) :
+  (lift R F).map (single f r) = r • F.map f :=
+by simp
+
+instance lift_additive (F : C ⥤ D) : (lift R F).additive :=
+{ map_zero' := by simp,
+  map_add' := λ X Y f g, begin
+    dsimp,
+    rw finsupp.sum_add_index; simp [add_smul]
+  end, }
+
+instance lift_linear (F : C ⥤ D) : (lift R F).linear R :=
+{ map_smul' := λ X Y f r, begin
+    dsimp,
+    rw finsupp.sum_smul_index;
+    simp [finsupp.smul_sum, mul_smul],
+  end, }
+
+/--
+The embedding into the `R`-linear completion, followed by the lift,
+is isomorphic to the original functor.
+-/
+def embedding_lift_iso (F : C ⥤ D) : embedding R C ⋙ lift R F ≅ F :=
+nat_iso.of_components
+  (λ X, iso.refl _)
+  (by tidy)
+
+/--
+Two `R`-linear functors out of the `R`-linear completion are isomorphic iff their
+compositions with the embedding functor are isomorphic.
+-/
+@[ext]
+def ext {F G : Free R C ⥤ D} [F.additive] [F.linear R] [G.additive] [G.linear R]
+  (α : embedding R C ⋙ F ≅ embedding R C ⋙ G) : F ≅ G :=
+nat_iso.of_components
+  (λ X, α.app X)
+  begin
+    intros X Y f,
+    apply finsupp.induction_linear f,
+    { simp, },
+    { intros f₁ f₂ w₁ w₂,
+      simp only [F.map_add, G.map_add, add_comp, comp_add, w₁, w₂], },
+    { intros f' r,
+      rw [iso.app_hom, iso.app_hom, ←smul_single_one, F.map_smul, G.map_smul, smul_comp, comp_smul],
+      change r • (embedding R C ⋙ F).map f' ≫ _ = r • _ ≫ (embedding R C ⋙ G).map f',
+      rw α.hom.naturality f',
+      apply_instance, -- Why are these not picked up automatically when we rewrite?
+      apply_instance, }
+  end
+
+/--
+`Free.lift` is unique amongst `R`-linear functors `Free R C ⥤ D`
+which compose with `embedding ℤ C` to give the original functor.
+-/
+def lift_unique (F : C ⥤ D) (L : Free R C ⥤ D) [L.additive] [L.linear R]
+  (α : embedding R C ⋙ L ≅ F) :
+  L ≅ lift R F :=
+ext R (α.trans (embedding_lift_iso R F).symm)
+
+end Free
+
+end category_theory

src/category_theory/preadditive/additive_functor.lean

@@ -76,6 +76,10 @@ F.map_add_hom.map_neg _
 lemma map_sub {X Y : C} {f g : X ⟶ Y} : F.map (f - g) = F.map f - F.map g :=
 F.map_add_hom.map_sub _ _
 
+-- You can alternatively just use `functor.map_smul` here, with an explicit `(r : ℤ)` argument.
+lemma map_gsmul {X Y : C} {f : X ⟶ Y} {r : ℤ} : F.map (r • f) = r • F.map f :=
+F.map_add_hom.map_gsmul _ _
+
 open_locale big_operators
 
 @[simp]

src/category_theory/preadditive/default.lean

@@ -6,6 +6,7 @@ Authors: Markus Himmel
 import algebra.group.hom
 import category_theory.limits.shapes.kernels
 import algebra.big_operators.basic
+import algebra.module.basic
 import category_theory.endomorphism
 
 /-!
@@ -155,6 +156,25 @@ instance preadditive_has_zero_morphisms : has_zero_morphisms C :=
   comp_zero' := λ P Q f R, map_zero $ left_comp R f,
   zero_comp' := λ P Q R f, map_zero $ right_comp P f }
 
+-- This is not a `@[simp]` lemma,
+-- as `linear.comp_smul` handles it too.
+lemma comp_gsmul {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (r : ℤ) :
+  f ≫ (r • g) = r • (f ≫ g) :=
+begin
+  change left_comp _ _ (r • g) = _,
+  rw [add_monoid_hom.map_gsmul],
+  refl,
+end
+
+-- As with `comp_gsmul`, this does not need to be a `@[simp]` lemma.
+lemma gsmul_comp {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) (r : ℤ) :
+  (r • f) ≫ g = r • (f ≫ g) :=
+begin
+  change right_comp _ _ (r • f) = _,
+  rw [add_monoid_hom.map_gsmul],
+  refl,
+end
+
 lemma mono_of_cancel_zero {Q R : C} (f : Q ⟶ R) (h : ∀ {P : C} (g : P ⟶ Q), g ≫ f = 0 → g = 0) :
   mono f :=
 ⟨λ P g g' hg, sub_eq_zero.1 $ h _ $ (map_sub (right_comp P f) g g').trans $ sub_eq_zero.2 hg⟩

src/linear_algebra/tensor_product.lean

@@ -1005,7 +1005,7 @@ When `R` is a `ring` we get the required `tensor_product.compatible_smul` instan
 `is_scalar_tower`, but when it is only a `semiring` we need to build it from scratch.
 The instance diamond in `compatible_smul` doesn't matter because it's in `Prop`.
 -/
-instance compatible_smul.int : compatible_smul R ℤ M N :=
+instance compatible_smul.int [module ℤ M] [module ℤ N] : compatible_smul R ℤ M N :=
 ⟨λ r m n, int.induction_on r
   (by simp)
   (λ r ih, by simpa [add_smul, tmul_add, add_tmul] using ih)