forked from leanprover-community/mathlib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
composition_series.lean
107 lines (97 loc) · 3.82 KB
/
composition_series.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
import order.jordan_holder
import order.cover
import ring_theory.simple_module
def partial_order.bot_or_top {α : Type*} [partial_order α] (x z : α) :=
∀ ⦃y⦄, x ≤ y → y ≤ z → (y = x ∨ y = z)
lemma covby.bot_or_top {α : Type*} [partial_order α] {x z : α} (hxz : x ⋖ z) :
partial_order.bot_or_top x z := λ y hxy hyz,
begin
cases lt_or_eq_of_le hxy with hxy h,
cases lt_or_eq_of_le hyz with hyz h,
{ exfalso,
exact hxz.2 hxy hyz },
exact or.inr h,
exact or.inl h.symm
end
lemma covby.iff_bot_or_top {α : Type*} [partial_order α] {x z : α} :
x ⋖ z ↔ (x < z ∧ partial_order.bot_or_top x z ) :=
begin
split; intro h,
exact ⟨h.lt, h.bot_or_top⟩,
refine ⟨h.1, _⟩,
intros y hxy hyz,
apply lt_irrefl y,
cases h.2 (le_of_lt hxy) (le_of_lt hyz) with h' h';
rw ←h' at *; assumption
end
lemma covby.sup_eq {α : Type*} [lattice α] {x y z : α} : x ⋖ z → y ⋖ z → x ≠ y → x ⊔ y = z :=
begin
intros hxz hyz hxy,
have hxyz : x ⊔ y ≤ z := sup_le (le_of_lt hxz.lt) (le_of_lt hyz.lt),
cases hxz.bot_or_top le_sup_left hxyz with hx h,
cases hyz.bot_or_top le_sup_right hxyz with hy h,
{ exfalso,
exact hxy (eq.trans hx.symm hy) },
all_goals { exact h },
end
namespace composition_series
open submodule
open lattice
variables {R M : Type*} [ring R] [add_comm_group M] [module R M]
@[simp]
lemma comap_map_subtype (B : submodule R M) (A : submodule R B) :
comap B.subtype (map B.subtype A) = A :=
comap_map_eq_of_injective subtype.coe_injective A
lemma covby_iff_quot_is_simple {A B : submodule R M} (hAB : A ≤ B) :
A ⋖ B ↔ is_simple_module R (B ⧸ comap B.subtype A) :=
begin
rw is_simple_module_iff_is_coatom,
split; intro h,
{ split,
{ intro htop,
rw comap_subtype_eq_top at htop,
rw le_antisymm hAB htop at h,
exact lt_irrefl B h.lt },
{ intros C' hAC',
have hA : A = map B.subtype (comap B.subtype A),
rwa [map_comap_subtype,right_eq_inf],
have hAC : A ≤ map B.subtype C',
{ rw hA,
exact map_mono (le_of_lt hAC') },
cases h.bot_or_top hAC (map_subtype_le B C') with h h,
{ exfalso,
apply ne_of_lt hAC',
rw congr_arg (comap B.subtype) h.symm,
exact comap_map_subtype B C' },
{ rw [←comap_map_subtype B C', h, comap_subtype_self] } } },
{ rw covby.iff_bot_or_top,
split,
{ apply lt_of_le_of_ne hAB,
intro hAB',
apply h.1,
rw hAB',
exact comap_subtype_self B },
{ intros C hAC hCB,
by_cases u : comap B.subtype A < comap B.subtype C,
{ right,
exact le_antisymm hCB (comap_subtype_eq_top.mp $ h.2 _ u) },
{ left,
have eqAC := eq_of_le_of_not_lt (comap_mono hAC) u,
rw [right_eq_inf.mpr hAB, right_eq_inf.mpr hCB, ←map_comap_subtype, ←eqAC, map_comap_subtype] } } }
end
instance jordan_holder_module : jordan_holder_lattice (submodule R M) :=
{ is_maximal := covby,
lt_of_is_maximal := λ x y, covby.lt,
sup_eq_of_is_maximal := λ x y z, covby.sup_eq,
is_maximal_inf_left_of_is_maximal_sup := λ {A B} h₁ h₂, by {
rw covby_iff_quot_is_simple (inf_le_left : A ⊓ B ≤ A),
haveI h := (covby_iff_quot_is_simple (le_sup_right : B ≤ A ⊔ B)).mp h₂,
apply is_simple_module.congr (linear_map.quotient_inf_equiv_sup_quotient A B) },
iso := λ X Y,
nonempty $ (X.2 ⧸ comap X.2.subtype X.1) ≃ₗ[R] (Y.2 ⧸ comap Y.2.subtype Y.1),
iso_symm := λ A B ⟨f⟩, ⟨f.symm⟩,
iso_trans := λ A B C ⟨f⟩ ⟨g⟩, ⟨f.trans g⟩,
second_iso := λ A B h, ⟨by {
rw [sup_comm,inf_comm],
exact (linear_map.quotient_inf_equiv_sup_quotient B A).symm }⟩ }
end composition_series