feat(algebra/category/Module): the category of R-modules is abelian (#3606)

Author: kim-em

src/algebra/category/Module/abelian.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import algebra.category.Module.kernels
+import algebra.category.Module.limits
+import category_theory.abelian.basic
+
+/-!
+# The category of left R-modules is abelian.
+-/
+
+open category_theory
+open category_theory.limits
+
+noncomputable theory
+
+universe u
+
+namespace Module
+variables {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N)
+
+/-- In the category of modules, every monomorphism is normal. -/
+def normal_mono [mono f] : normal_mono f :=
+{ Z := of R f.range.quotient,
+  g := f.range.mkq,
+  w := linear_map.range_mkq_comp _,
+  is_limit :=
+    is_kernel.iso_kernel _ _ (kernel_is_limit _)
+      /- The following [invalid Lean code](https://github.com/leanprover-community/lean/issues/341)
+        might help you understand what's going on here:
+        ```
+        calc
+        M   ≃ₗ[R] f.ker.quotient  : (submodule.quot_equiv_of_eq_bot _ (ker_eq_bot_of_mono _)).symm
+        ... ≃ₗ[R] f.range         : linear_map.quot_ker_equiv_range f
+        ... ≃ₗ[R] r.range.mkq.ker : linear_equiv.of_eq _ _ (submodule.ker_mkq _).symm
+        ```
+      -/
+      (linear_equiv.to_Module_iso'
+        (linear_equiv.trans (submodule.quot_equiv_of_eq_bot _ (ker_eq_bot_of_mono _)).symm
+          (linear_equiv.trans (linear_map.quot_ker_equiv_range f)
+            (linear_equiv.of_eq _ _ (submodule.ker_mkq _).symm)))) $
+      by { ext, refl } }
+
+/-- In the category of modules, every epimorphism is normal. -/
+def normal_epi [epi f] : normal_epi f :=
+{ W := of R f.ker,
+  g := f.ker.subtype,
+  w := linear_map.comp_ker_subtype _,
+  is_colimit :=
+    is_cokernel.cokernel_iso _ _ (cokernel_is_colimit _)
+      (linear_equiv.to_Module_iso'
+      /- The following invalid Lean code might help you understand what's going on here:
+        ```
+        calc f.ker.subtype.range.quotient
+            ≃ₗ[R] f.ker.quotient : submodule.quot_equiv_of_eq _ _ (submodule.range_subtype _)
+        ... ≃ₗ[R] f.range        : linear_map.quot_ker_equiv_range f
+        ... ≃ₗ[R] N              : linear_equiv.of_top _ (range_eq_top_of_epi _)
+        ```
+      -/
+        (linear_equiv.trans
+          (linear_equiv.trans (submodule.quot_equiv_of_eq _ _ (submodule.range_subtype _))
+            (linear_map.quot_ker_equiv_range f)) (linear_equiv.of_top _ (range_eq_top_of_epi _)))) $
+      by { ext, refl } }
+
+local attribute [instance] has_equalizers_of_has_finite_limits
+
+/-- The category of R-modules is abelian. -/
+instance : abelian (Module R) :=
+{ has_finite_products := by apply_instance,
+  has_kernels := by apply_instance,
+  has_cokernels := has_cokernels_Module,
+  normal_mono := λ X Y f m, by exactI normal_mono f,
+  normal_epi := λ X Y f e, by exactI normal_epi f }
+
+end Module

src/algebra/category/Module/basic.lean

@@ -86,6 +86,10 @@ end Module
 variables {R}
 variables {X₁ X₂ : Type u}
 
+/-- Reinterpreting a linear map in the category of `R`-modules. -/
+def Module.as_hom [add_comm_group X₁] [module R X₁] [add_comm_group X₂] [module R X₂] :
+  (X₁ →ₗ[R] X₂) → (Module.of R X₁ ⟶ Module.of R X₂) := id
+
 /-- Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s. -/
 @[simps]
 def linear_equiv.to_Module_iso
@@ -96,6 +100,18 @@ def linear_equiv.to_Module_iso
   hom_inv_id' := begin ext, exact e.left_inv x, end,
   inv_hom_id' := begin ext, exact e.right_inv x, end, }
 
+/--
+Build an isomorphism in the category `Module R` from a `linear_equiv` between `module`s.
+
+This version is better than `linear_equiv_to_Module_iso` when applicable, because Lean can't see `Module.of R M` is defeq to `M` when `M : Module R`.
+  -/
+@[simps]
+def linear_equiv.to_Module_iso' {M N : Module R} (i : M ≃ₗ[R] N) : M ≅ N :=
+{ hom := i,
+  inv := i.symm,
+  hom_inv_id' := linear_map.ext $ λ x, by simp,
+  inv_hom_id' := linear_map.ext $ λ x, by simp }
+
 namespace category_theory.iso
 
 /-- Build a `linear_equiv` from an isomorphism in the category `Module R`. -/
@@ -129,41 +145,22 @@ instance : preadditive (Module R) :=
 
 end preadditive
 
-section kernel
-variables {R} {M N : Module R} (f : M ⟶ N)
-
-/-- The cone on the equalizer diagram of f and 0 induced by the kernel of f -/
-def kernel_cone : cone (parallel_pair f 0) :=
-{ X := of R f.ker,
-  π :=
-  { app := λ j,
-    match j with
-    | zero := f.ker.subtype
-    | one := 0
-    end,
-    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) :=
-{ 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 }),
-  fac' := λ s j, linear_map.ext $ λ x,
-  begin
-    rw [coe_comp, function.comp_app, ←linear_map.comp_apply],
-    cases j,
-    { erw @linear_map.subtype_comp_cod_restrict _ _ _ _ _ _ _ _ (fork.ι s) f.ker _ },
-    { rw [←fork.app_zero_left, ←fork.app_zero_left], refl }
-  end,
-  uniq' := λ s m h, linear_map.ext $ λ x, subtype.ext_iff_val.2 $
-    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 }
-
-end kernel
-
-instance : has_kernels (Module R) :=
-⟨λ _ _ f, ⟨kernel_cone f, kernel_is_limit f⟩⟩
+section epi_mono
+variables {M N : Module R} (f : M ⟶ N)
+
+lemma ker_eq_bot_of_mono [mono f] : f.ker = ⊥ :=
+linear_map.ker_eq_bot_of_cancel $ λ u v, (@cancel_mono _ _ _ _ _ f _ (as_hom u) (as_hom v)).1
+
+lemma range_eq_top_of_epi [epi f] : f.range = ⊤ :=
+linear_map.range_eq_top_of_cancel $ λ u v, (@cancel_epi _ _ _ _ _ f _ (as_hom u) (as_hom v)).1
+
+lemma mono_of_ker_eq_bot (hf : f.ker = ⊥) : mono f :=
+concrete_category.mono_of_injective _ $ linear_map.ker_eq_bot.1 hf
+
+lemma epi_of_range_eq_top (hf : f.range = ⊤) : epi f :=
+concrete_category.epi_of_surjective _ $ linear_map.range_eq_top.1 hf
+
+end epi_mono
 
 end Module
 

src/algebra/category/Module/kernels.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import algebra.category.Module.basic
+
+/-!
+# The concrete (co)kernels in the category of modules are (co)kernels in the categorical sense.
+-/
+
+open category_theory
+open category_theory.limits
+open category_theory.limits.walking_parallel_pair
+
+universe u
+
+namespace Module
+variables {R : Type u} [ring R]
+
+section
+variables {M N : Module R} (f : M ⟶ N)
+
+/-- The kernel cone induced by the concrete kernel. -/
+def kernel_cone : kernel_fork f :=
+kernel_fork.of_ι (as_hom f.ker.subtype) $ by tidy
+
+/-- The kernel of a linear map is a kernel in the categorical sense. -/
+def kernel_is_limit : is_limit (kernel_cone f) :=
+fork.is_limit.mk _
+  (λ s, linear_map.cod_restrict f.ker (fork.ι s) (λ c, linear_map.mem_ker.2 $
+    by { rw [←@function.comp_apply _ _ _ f (fork.ι s) c, ←coe_comp, fork.condition,
+      has_zero_morphisms.comp_zero (fork.ι s) N], refl }))
+  (λ s, linear_map.subtype_comp_cod_restrict _ _ _)
+  (λ s m h, linear_map.ext $ λ x, subtype.ext_iff_val.2 $
+    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 )
+
+/-- The cokernel cocone induced by the projection onto the quotient. -/
+def cokernel_cocone : cokernel_cofork f :=
+cokernel_cofork.of_π (as_hom f.range.mkq) $ linear_map.range_mkq_comp _
+
+/-- The projection onto the quotient is a cokernel in the categorical sense. -/
+def cokernel_is_colimit : is_colimit (cokernel_cocone f) :=
+cofork.is_colimit.mk _
+  (λ s, f.range.liftq (cofork.π s) $ linear_map.range_le_ker_iff.2 $ cokernel_cofork.condition s)
+  (λ s, f.range.liftq_mkq (cofork.π s) _)
+  (λ s m h,
+  begin
+    haveI : epi (as_hom f.range.mkq) := epi_of_range_eq_top _ (submodule.range_mkq _),
+    apply (cancel_epi (as_hom f.range.mkq)).1,
+    convert h walking_parallel_pair.one,
+    exact submodule.liftq_mkq _ _ _
+  end)
+end
+
+/-- The category of R-modules has kernels, given by the inclusion of the kernel submodule. -/
+def has_kernels_Module : has_kernels (Module R) :=
+⟨λ X Y f, ⟨_, kernel_is_limit f⟩⟩
+
+/-- The category or R-modules has cokernels, given by the projection onto the quotient. -/
+def has_cokernels_Module : has_cokernels (Module R) :=
+⟨λ X Y f, ⟨_, cokernel_is_colimit f⟩⟩
+
+end Module

src/linear_algebra/basic.lean

@@ -1083,6 +1083,9 @@ def ker (f : M →ₗ[R] M₂) : submodule R M := comap f ⊥
 
 @[simp] theorem map_coe_ker (f : M →ₗ[R] M₂) (x : ker f) : f x = 0 := mem_ker.1 x.2
 
+lemma comp_ker_subtype (f : M →ₗ[R] M₂) : f.comp f.ker.subtype = 0 :=
+linear_map.ext $ λ x, suffices f x = 0, by simp [this], mem_ker.1 x.2
+
 theorem ker_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : ker (g.comp f) = comap f (ker g) := rfl
 
 theorem ker_le_ker_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) : ker f ≤ ker (g.comp f) :=
@@ -1534,6 +1537,32 @@ end ring
 
 end submodule
 
+namespace linear_map
+variables [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
+
+lemma range_mkq_comp (f : M →ₗ[R] M₂) : f.range.mkq.comp f = 0 :=
+linear_map.ext $ λ x, by { simp, use x }
+
+/-- A monomorphism is injective. -/
+lemma ker_eq_bot_of_cancel {f : M →ₗ[R] M₂}
+  (h : ∀ (u v : f.ker →ₗ[R] M), f.comp u = f.comp v → u = v) : f.ker = ⊥ :=
+begin
+  have h₁ : f.comp (0 : f.ker →ₗ[R] M) = 0 := comp_zero _,
+  rw [←submodule.range_subtype f.ker, ←h 0 f.ker.subtype (eq.trans h₁ (comp_ker_subtype f).symm)],
+  exact range_zero
+end
+
+/-- An epimorphism is surjective. -/
+lemma range_eq_top_of_cancel {f : M →ₗ[R] M₂}
+  (h : ∀ (u v : M₂ →ₗ[R] f.range.quotient), u.comp f = v.comp f → u = v) : f.range = ⊤ :=
+begin
+  have h₁ : (0 : M₂ →ₗ[R] f.range.quotient).comp f = 0 := zero_comp _,
+  rw [←submodule.ker_mkq f.range, ←h 0 f.range.mkq (eq.trans h₁ (range_mkq_comp _).symm)],
+  exact ker_zero
+end
+
+end linear_map
+
 @[simp] lemma linear_map.range_range_restrict [semiring R] [add_comm_monoid M] [add_comm_monoid M₂]
   [semimodule R M] [semimodule R M₂] (f : M →ₗ[R] M₂) :
   f.range_restrict.range = ⊤ :=
@@ -1993,6 +2022,13 @@ linear_equiv.of_linear (p.liftq id $ hp.symm ▸ bot_le) p.mkq (liftq_mkq _ _ _)
 @[simp] lemma coe_quot_equiv_of_eq_bot_symm (hp : p = ⊥) :
   ((p.quot_equiv_of_eq_bot hp).symm : M →ₗ[R] p.quotient) = p.mkq := rfl
 
+variables (q : submodule R M)
+
+/-- Quotienting by equal submodules gives linearly equivalent quotients. -/
+def quot_equiv_of_eq (h : p = q) : p.quotient ≃ₗ[R] q.quotient :=
+{ map_add' := by { rintros ⟨x⟩ ⟨y⟩, refl }, map_smul' := by { rintros x ⟨y⟩, refl },
+  ..@quotient.congr _ _ (quotient_rel p) (quotient_rel q) (equiv.refl _) $ λ a b, by { subst h, refl } }
+
 end submodule
 
 namespace submodule