From 0f08541d770094c3e88ce1b45d6928c1defebafc Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 27 Jul 2020 15:37:54 +0200 Subject: [PATCH] Module R is abelian --- src/algebra/category/Module/abelian.lean | 56 ++++++++++++++++++ src/algebra/category/Module/basic.lean | 74 +++++++++++++----------- src/algebra/category/Module/kernels.lean | 69 ++++++++++++++++++++++ src/linear_algebra/basic.lean | 65 +++++++++++++++++++++ 4 files changed, 229 insertions(+), 35 deletions(-) create mode 100644 src/algebra/category/Module/abelian.lean create mode 100644 src/algebra/category/Module/kernels.lean diff --git a/src/algebra/category/Module/abelian.lean b/src/algebra/category/Module/abelian.lean new file mode 100644 index 0000000000000..97e8b5ac7ae52 --- /dev/null +++ b/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 diff --git a/src/algebra/category/Module/basic.lean b/src/algebra/category/Module/basic.lean index e53b48f7d24a9..78006f021f9f2 100644 --- a/src/algebra/category/Module/basic.lean +++ b/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 diff --git a/src/algebra/category/Module/kernels.lean b/src/algebra/category/Module/kernels.lean new file mode 100644 index 0000000000000..bcf0ab72e3adc --- /dev/null +++ b/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 diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 039e2e7f160b6..dc0c031c59a70 100644 --- a/src/linear_algebra/basic.lean +++ b/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*}