push pushHEADmaster

1 files changed, 128 insertions, 0 deletions

diff --git a/five.v b/five.v
new file mode 100644
index 0000000..7bddcc5
--- /dev/null
+++ b/five.v
@@ -0,0 +1,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.
+