-
Notifications
You must be signed in to change notification settings - Fork 297
/
isomorphisms.lean
149 lines (119 loc) · 6.36 KB
/
isomorphisms.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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
-/
import linear_algebra.quotient
/-!
# Isomorphism theorems for modules.
> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
* The Noether's first, second, and third isomorphism theorems for modules are proved as
`linear_map.quot_ker_equiv_range`, `linear_map.quotient_inf_equiv_sup_quotient` and
`submodule.quotient_quotient_equiv_quotient`.
-/
universes u v
variables {R M M₂ M₃ : Type*}
variables [ring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃]
variables [module R M] [module R M₂] [module R M₃]
variables (f : M →ₗ[R] M₂)
/-! The first and second isomorphism theorems for modules. -/
namespace linear_map
open submodule
section isomorphism_laws
/-- The first isomorphism law for modules. The quotient of `M` by the kernel of `f` is linearly
equivalent to the range of `f`. -/
noncomputable def quot_ker_equiv_range : (M ⧸ f.ker) ≃ₗ[R] f.range :=
(linear_equiv.of_injective (f.ker.liftq f $ le_rfl) $
ker_eq_bot.mp $ submodule.ker_liftq_eq_bot _ _ _ (le_refl f.ker)).trans
(linear_equiv.of_eq _ _ $ submodule.range_liftq _ _ _)
/-- The first isomorphism theorem for surjective linear maps. -/
noncomputable def quot_ker_equiv_of_surjective
(f : M →ₗ[R] M₂) (hf : function.surjective f) : (M ⧸ f.ker) ≃ₗ[R] M₂ :=
f.quot_ker_equiv_range.trans
(linear_equiv.of_top f.range (linear_map.range_eq_top.2 hf))
@[simp] lemma quot_ker_equiv_range_apply_mk (x : M) :
(f.quot_ker_equiv_range (submodule.quotient.mk x) : M₂) = f x :=
rfl
@[simp] lemma quot_ker_equiv_range_symm_apply_image (x : M) (h : f x ∈ f.range) :
f.quot_ker_equiv_range.symm ⟨f x, h⟩ = f.ker.mkq x :=
f.quot_ker_equiv_range.symm_apply_apply (f.ker.mkq x)
/--
Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')`
to `x + p'`, where `p` and `p'` are submodules of an ambient module.
-/
def quotient_inf_to_sup_quotient (p p' : submodule R M) :
p ⧸ (comap p.subtype (p ⊓ p')) →ₗ[R] _ ⧸ (comap (p ⊔ p').subtype p') := by exact
(comap p.subtype (p ⊓ p')).liftq
((comap (p ⊔ p').subtype p').mkq.comp (of_le le_sup_left)) begin
rw [ker_comp, of_le, comap_cod_restrict, ker_mkq, map_comap_subtype],
exact comap_mono (inf_le_inf_right _ le_sup_left) end
/--
Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism.
-/
noncomputable def quotient_inf_equiv_sup_quotient (p p' : submodule R M) :
(p ⧸ (comap p.subtype (p ⊓ p'))) ≃ₗ[R] _ ⧸ (comap (p ⊔ p').subtype p') := by exact
linear_equiv.of_bijective (quotient_inf_to_sup_quotient p p')
⟨begin
rw [← ker_eq_bot, quotient_inf_to_sup_quotient, ker_liftq_eq_bot],
rw [ker_comp, ker_mkq],
exact λ ⟨x, hx1⟩ hx2, ⟨hx1, hx2⟩
end,
begin
rw [← range_eq_top, quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'],
rintros ⟨x, hx⟩, rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩,
use [⟨y, hy⟩], apply (submodule.quotient.eq _).2,
change y - (y + z) ∈ p',
rwa [sub_add_eq_sub_sub, sub_self, zero_sub, neg_mem_iff]
end⟩
@[simp] lemma coe_quotient_inf_to_sup_quotient (p p' : submodule R M) :
⇑(quotient_inf_to_sup_quotient p p') = quotient_inf_equiv_sup_quotient p p' := rfl
@[simp] lemma quotient_inf_equiv_sup_quotient_apply_mk (p p' : submodule R M) (x : p) :
quotient_inf_equiv_sup_quotient p p' (submodule.quotient.mk x) =
submodule.quotient.mk (of_le (le_sup_left : p ≤ p ⊔ p') x) :=
rfl
lemma quotient_inf_equiv_sup_quotient_symm_apply_left (p p' : submodule R M)
(x : p ⊔ p') (hx : (x:M) ∈ p) :
(quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) =
submodule.quotient.mk ⟨x, hx⟩ :=
(linear_equiv.symm_apply_eq _).2 $ by simp [of_le_apply]
@[simp] lemma quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff {p p' : submodule R M}
{x : p ⊔ p'} :
(quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) = 0 ↔ (x:M) ∈ p' :=
(linear_equiv.symm_apply_eq _).trans $ by simp [of_le_apply]
lemma quotient_inf_equiv_sup_quotient_symm_apply_right (p p' : submodule R M) {x : p ⊔ p'}
(hx : (x:M) ∈ p') :
(quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) = 0 :=
quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff.2 hx
end isomorphism_laws
end linear_map
/-! The third isomorphism theorem for modules. -/
namespace submodule
variables (S T : submodule R M) (h : S ≤ T)
/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/
def quotient_quotient_equiv_quotient_aux (h : S ≤ T) :
(M ⧸ S) ⧸ (T.map S.mkq) →ₗ[R] M ⧸ T := by exact
liftq _ (mapq S T linear_map.id h)
(by { rintro _ ⟨x, hx, rfl⟩, rw [linear_map.mem_ker, mkq_apply, mapq_apply],
exact (quotient.mk_eq_zero _).mpr hx })
@[simp] lemma quotient_quotient_equiv_quotient_aux_mk (x : M ⧸ S) :
quotient_quotient_equiv_quotient_aux S T h (quotient.mk x) = mapq S T linear_map.id h x :=
liftq_apply _ _ _
@[simp] lemma quotient_quotient_equiv_quotient_aux_mk_mk (x : M) :
quotient_quotient_equiv_quotient_aux S T h (quotient.mk (quotient.mk x)) = quotient.mk x :=
by rw [quotient_quotient_equiv_quotient_aux_mk, mapq_apply, linear_map.id_apply]
/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`. -/
def quotient_quotient_equiv_quotient :
((M ⧸ S) ⧸ (T.map S.mkq)) ≃ₗ[R] M ⧸ T :=
{ to_fun := quotient_quotient_equiv_quotient_aux S T h,
inv_fun := mapq _ _ (mkq S) (le_comap_map _ _),
left_inv := λ x, quotient.induction_on' x $ λ x, quotient.induction_on' x $ λ x, by simp,
right_inv := λ x, quotient.induction_on' x $ λ x, by simp,
.. quotient_quotient_equiv_quotient_aux S T h }
/-- Corollary of the third isomorphism theorem: `[S : T] [M : S] = [M : T]` -/
lemma card_quotient_mul_card_quotient (S T : submodule R M) (hST : T ≤ S)
[decidable_pred (λ x, x ∈ S.map T.mkq)] [fintype (M ⧸ S)] [fintype (M ⧸ T)] :
fintype.card (S.map T.mkq) * fintype.card (M ⧸ S) = fintype.card (M ⧸ T) :=
by rw [submodule.card_eq_card_quotient_mul_card (map T.mkq S),
fintype.card_eq.mpr ⟨(quotient_quotient_equiv_quotient T S hST).to_equiv⟩]
end submodule