/
abelian.lean
110 lines (91 loc) · 4.03 KB
/
abelian.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
/-
Copyright (c) 2020 Markus Himmel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Markus Himmel
-/
import linear_algebra.isomorphisms
import algebra.category.Module.kernels
import algebra.category.Module.limits
import category_theory.abelian.exact
/-!
# The category of left R-modules is abelian.
Additionally, two linear maps are exact in the categorical sense iff `range f = ker g`.
-/
open category_theory
open category_theory.limits
noncomputable theory
universes w v u
namespace Module
variables {R : Type u} [ring R] {M N : Module.{v} R} (f : M ⟶ N)
/-- In the category of modules, every monomorphism is normal. -/
def normal_mono (hf : mono f) : normal_mono f :=
{ Z := of R (N ⧸ f.range),
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'
((submodule.quot_equiv_of_eq_bot _ (ker_eq_bot_of_mono _)).symm ≪≫ₗ
((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 (hf : 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 _)
```
-/
(((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 } }
/-- The category of R-modules is abelian. -/
instance : abelian (Module R) :=
{ has_finite_products := ⟨λ n, limits.has_limits_of_shape_of_has_limits⟩,
has_kernels := limits.has_kernels_of_has_equalizers (Module R),
has_cokernels := has_cokernels_Module,
normal_mono_of_mono := λ X Y, normal_mono,
normal_epi_of_epi := λ X Y, normal_epi }
section reflects_limits
/- We need to put this in this weird spot because we need to know that the category of modules
is balanced. -/
instance forget_reflects_limits_of_size :
reflects_limits_of_size.{v v} (forget (Module.{max v w} R)) :=
reflects_limits_of_reflects_isomorphisms
instance forget₂_reflects_limits_of_size :
reflects_limits_of_size.{v v} (forget₂ (Module.{max v w} R) AddCommGroup.{max v w}) :=
reflects_limits_of_reflects_isomorphisms
instance forget_reflects_limits : reflects_limits (forget (Module.{v} R)) :=
Module.forget_reflects_limits_of_size.{v v}
instance forget₂_reflects_limits : reflects_limits (forget₂ (Module.{v} R) AddCommGroup.{v}) :=
Module.forget₂_reflects_limits_of_size.{v v}
end reflects_limits
variables {O : Module.{v} R} (g : N ⟶ O)
open linear_map
local attribute [instance] preadditive.has_equalizers_of_has_kernels
theorem exact_iff : exact f g ↔ f.range = g.ker :=
begin
rw abelian.exact_iff' f g (kernel_is_limit _) (cokernel_is_colimit _),
exact ⟨λ h, le_antisymm (range_le_ker_iff.2 h.1) (ker_le_range_iff.2 h.2),
λ h, ⟨range_le_ker_iff.1 $ le_of_eq h, ker_le_range_iff.1 $ le_of_eq h.symm⟩⟩
end
end Module