Module R is abelian

src/algebra/category/Module/abelian.lean

@@ -0,0 +1,56 @@
+/-
+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 :=
+  begin
+    refine is_kernel.iso_kernel _ _ (kernel_is_limit _) _ _,
+    { exact linear_equiv.to_Module_iso' (linear_map.equiv_range_mkq_ker_of_ker_eq_bot (ker_eq_bot_of_mono f)), },
+    ext, refl
+  end }
+
+/-- 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 :=
+  begin
+    refine is_cokernel.cokernel_iso _ _ (cokernel_is_colimit _) _ _,
+    { exact linear_equiv.to_Module_iso' (linear_map.ker_subtype_range_quotient_equiv_of_range_eq_top (range_eq_top_of_epi f)) },
+    ext, refl
+  end }
+
+/-- The category of R-modules is abelian. -/
+instance : abelian (Module R) :=
+{ has_finite_products := by apply_instance,
+  has_kernels := by apply_instance,
+  has_cokernels := by apply_instance,
+  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,13 @@ 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, }
 
+@[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 +140,34 @@ 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 :=
+⟨λ Z u v h, begin
+  ext,
+  apply (linear_map.ker_eq_bot.1 hf),
+  rw [←linear_map.comp_apply, ←linear_map.comp_apply],
+  congr,
+  exact h
+end⟩
+
+lemma epi_of_range_eq_top (hf : f.range = ⊤) : epi f :=
+⟨λ Z u v h, begin
+  ext,
+  cases linear_map.range_eq_top.1 hf x with y hy,
+  rw [←hy, ←linear_map.comp_apply, ←linear_map.comp_apply],
+  congr,
+  exact h
+end⟩
+
+end epi_mono
 
 end Module
 

src/algebra/category/Module/kernels.lean

@@ -0,0 +1,69 @@
+/-
+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) :=
+{ lift := λ 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 }),
+  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 }
+
+/-- 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
+
+instance : has_kernels (Module R) :=
+⟨λ X Y f, ⟨_, kernel_is_limit f⟩⟩
+
+instance : has_cokernels (Module R) :=
+⟨λ X Y f, ⟨_, cokernel_is_colimit f⟩⟩
+
+end Module

src/linear_algebra/basic.lean

@@ -1089,6 +1089,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) :=
@@ -1540,6 +1543,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 = ⊤ :=
@@ -1999,6 +2028,12 @@ 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
 
+/-- If `p = ⊤`, then `p ≃ₗ[R] M`. -/
+/- This could in theory be made computable. -/
+def equiv_of_eq_top (hp : p = ⊤) : p ≃ₗ[R] M :=
+linear_equiv.of_bijective p.subtype (submodule.ker_subtype p)
+  (linear_map.range_eq_top.2 $ λ x, ⟨⟨x, by { rw hp, trivial }⟩, rfl⟩)
+
 end submodule
 
 namespace submodule
@@ -2141,6 +2176,36 @@ quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff.2 hx
 
 end isomorphism_laws
 
+section
+variables [ring R] [add_comm_group M] [add_comm_group M₂] [module R M] [module R M₂]
+variables {f : M →ₗ[R] M₂}
+
+/-- If `f : M → M₂` is an injective linear map, then by the first isomorphism law `M` is just the
+    kernel of the quotient map onto the quotient by the range of `f`. -/
+def equiv_range_mkq_ker_of_ker_eq_bot (h : f.ker = ⊥) : M ≃ₗ[R] f.range.mkq.ker :=
+linear_equiv.trans (submodule.quot_equiv_of_eq_bot _ h).symm
+  (linear_equiv.trans (quot_ker_equiv_range f)
+    (linear_equiv.of_eq _ _ (submodule.ker_mkq _).symm))
+
+section
+variables (p 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
+
+/-- If `f : M → M₂` is a surjective linear map, then by the first isomorphism law `M₂` is just
+    the quotient by the image of the inclusion of the kernel of `f`. -/
+def ker_subtype_range_quotient_equiv_of_range_eq_top (h : f.range = ⊤) :
+  f.ker.subtype.range.quotient ≃ₗ[R] M₂ :=
+linear_equiv.trans (linear_equiv.trans (quot_equiv_of_eq _ _ (submodule.range_subtype _))
+  (quot_ker_equiv_range f)) (linear_equiv.of_top _ h)
+
+end
+
 section prod
 
 lemma is_linear_map_prod_iso {R M M₂ M₃ : Type*}