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
|
(* Five lemma *)
Require Import Utf8.
Require Import AbGroup Setoid.
Require Import four.
Theorem is_iso_is_epi : ∀ A B (f : HomGr A B), is_iso f → is_epi f.
Proof.
intros * (g & Hgf & Hfg) C * Hgg * Hy.
specialize (Hfg y Hy) as H1.
etransitivity.
-apply g₁; [ easy | symmetry; apply H1 ].
-rewrite Hgg; [ | now apply g ].
apply g₂; [ now apply f, g | easy ].
Qed.
Theorem is_iso_is_mono : ∀ A B (f : HomGr A B), is_iso f → is_mono f.
Proof.
intros * (g & Hgf & Hfg) C * Hgg * Hz.
specialize (Hgg z Hz) as H1.
apply (Happ_compat _ _ g) in H1; [ | now apply f, g₁ ].
rewrite Hgf in H1; [ | now apply g₁ ].
rewrite Hgf in H1; [ | now apply g₂ ].
easy.
Qed.
Theorem epi_mono_is_iso : ∀ A B (f : HomGr A B),
Decidable_Membership * Choice
→ is_epi f → is_mono f → is_iso f.
Proof.
intros * (mem_dec, choice) He Hm.
unfold is_iso.
specialize (epi_is_surj He) as H1.
specialize (mono_is_inj Hm) as H2.
assert (H3 : ∀ y, ∃ t, y ∈ B → t ∈ A ∧ (Happ f t = y)%G). {
intros y.
specialize (H1 y).
specialize (mem_dec B y) as [H3| H3]; [ | now exists 0 ].
specialize (H1 H3) as (x & Hx & Hfx).
exists x; intros H; easy.
}
specialize (choice _ _ _ H3) as (g & Hg).
assert (Hmc : ∀ x : gr_set B, x ∈ B → g x ∈ A). {
intros y Hy.
now specialize (Hg _ Hy).
}
assert (Hac : ∀ x y, x ∈ B → (x = y)%G → (g x = g y)%G). {
intros y1 y2 Hy1 Hyy.
assert (Hy2 : y2 ∈ B) by now apply (gr_mem_compat _ y1).
specialize (Hg _ Hy1) as H; destruct H as (Hgy1, Hfgy1).
specialize (Hg _ Hy2) as H; destruct H as (Hgy2, Hfgy2).
move Hgy2 before Hgy1.
rewrite Hyy in Hfgy1 at 2.
rewrite <- Hfgy2 in Hfgy1.
now apply H2.
}
assert (Had : ∀ x y, x ∈ B → y ∈ B → (g (x + y) = g x + g y)%G). {
intros y1 y2 Hy1 Hy2.
specialize (Hg _ Hy1) as H; destruct H as (Hg1, Hfg1).
specialize (Hg _ Hy2) as H; destruct H as (Hg2, Hfg2).
move Hg2 before Hg1.
apply H2; [ now apply Hmc, B | now apply A | ].
rewrite Hadditive; [ | easy | easy ].
rewrite Hfg1, Hfg2.
now apply Hg, B.
}
set (hv :=
{| Happ := g;
Hmem_compat := Hmc;
Happ_compat := Hac;
Hadditive := Had |}).
exists hv; simpl.
split.
-intros x Hx.
apply H2; [ now apply Hmc, f | easy | ].
now apply Hg, f.
-intros y Hy.
now apply Hg.
Qed.
Lemma five :
∀ (A B C D E A' B' C' D' E' : AbGroup)
(f : HomGr A B) (g : HomGr B C) (h : HomGr C D) (j : HomGr D E)
(f' : HomGr A' B') (g' : HomGr B' C')
(h' : HomGr C' D') (j' : HomGr D' E')
(a : HomGr A A') (b : HomGr B B') (c : HomGr C C')
(d : HomGr D D') (e : HomGr E E'),
Decidable_Membership * Choice
→ diagram_commutes f a b f'
→ diagram_commutes g b c g'
→ diagram_commutes h c d h'
→ diagram_commutes j d e j'
→ exact_sequence [f; g; h; j]
→ exact_sequence [f'; g'; h'; j']
→ is_epi a ∧ is_iso b ∧ is_iso d ∧ is_mono e
→ is_iso c.
Proof.
intros * dc.
intros Hcff' Hcgg' Hchh' Hcjj' s s' (Hea & Hib & Hid & Hme).
specialize (four_1 B C D E B' C' D' E') as H1.
specialize (H1 g h j g' h' j' b c d e).
specialize (H1 Hcgg' Hchh' Hcjj').
assert (H : exact_sequence [g; h; j]) by apply s.
specialize (H1 H); clear H.
assert (H : exact_sequence [g'; h'; j']) by apply s'.
specialize (H1 H); clear H.
assert (H : is_epi b ∧ is_epi d ∧ is_mono e). {
split; [ | split ]; [ | | easy ]; now apply is_iso_is_epi.
}
specialize (H1 H); clear H.
specialize (four_2 A B C D A' B' C' D') as H2.
specialize (H2 f g h f' g' h' a b c d).
specialize (H2 Hcff' Hcgg' Hchh').
assert (H : exact_sequence [f; g; h]) by now destruct s as (t & u & v).
specialize (H2 H); clear H.
assert (H : exact_sequence [f'; g'; h']) by now destruct s' as (t & u & v).
specialize (H2 H); clear H.
assert (H : is_mono b ∧ is_mono d ∧ is_epi a). {
split; [ | split ]; [ | | easy ]; now apply is_iso_is_mono.
}
specialize (H2 H); clear H.
now apply epi_mono_is_iso.
Qed.
Check five.
|
