push pushHEADmaster

1 files changed, 188 insertions, 0 deletions

diff --git a/four.v b/four.v
new file mode 100644
index 0000000..c47bf16
--- /dev/null
+++ b/four.v
@@ -0,0 +1,188 @@
+Require Import Utf8.
+Require Import AbGroup Setoid.
+
+(* 
+           g       h        j
+        B------>C------>D------>E
+        |       |       |       ∩
+       b|      c|      d|      e|
+        v       |       v       |
+        v       v       v       v
+        B'----->C'----->D'----->E'
+           g'      h'      j'
+
+  If 1/ the diagram is commutative,
+     2/ (g, h, j) and (g', h', j') are exact,
+     3/ b and d are epimorphisms,
+     4/ e is monomorphism,
+  Then
+     c is an epimorphism.
+*)
+
+Lemma four_1 :
+  ∀ (B C D E B' C' D' E' : AbGroup)
+     (g : HomGr B C) (h : HomGr C D) (j : HomGr D E)
+     (g' : HomGr B' C') (h' : HomGr C' D') (j' : HomGr D' E')
+     (b : HomGr B B') (c : HomGr C C')
+     (d : HomGr D D') (e : HomGr E E'),
+  diagram_commutes g b c g'
+  → diagram_commutes h c d h'
+  → diagram_commutes j d e j'
+  → exact_sequence [g; h; j]
+  → exact_sequence [g'; h'; j']
+  → is_epi b ∧ is_epi d ∧ is_mono e
+  → is_epi c.
+Proof.
+intros * Hcgg' Hchh' Hcjj' s s' (Heb & Hed & Hme).
+unfold is_epi.
+enough
+  (∀ T (g₁ g₂ : HomGr C' T),
+   (∀ z, z ∈ C → (Happ g₁ (Happ c z) = Happ g₂ (Happ c z))%G)
+   → ∀ z', z' ∈ C' → (Happ g₁ z' = Happ g₂ z')%G). {
+  now intros T g₁ g₂ H1; apply H.
+}
+intros * Hgc * Hz'.
+assert (H : ∃ t, t ∈ D ∧ (Happ d t = Happ h' z')%G). {
+  apply epi_is_surj; [ easy | now apply h' ].
+}
+destruct H as (t & Ht & Hdt).
+move t after z'; move Ht after Hz'.
+assert (H : ∃ z, z ∈ C ∧ (Happ h z = t)%G). {
+  assert (H : t ∈ Ker j). {
+    split; [ easy | ].
+    assert (H : (Happ e (Happ j t) = 0)%G). {
+      rewrite Hcjj'.
+
+      etransitivity; [ apply Happ_compat | ]; [ | apply Hdt | ]; cycle 1.
+      -assert (H : Happ h' z' ∈ Im h') by (exists z'; easy).
+       now apply s' in H; simpl in H.
+      -now apply d.
+    }
+    specialize (mono_is_inj Hme) as H1.
+    apply H1; [ now apply j | apply E | now rewrite Hzero ].
+  }
+  apply s in H.
+  destruct H as (z & Hz & Hhz).
+  now exists z.
+}
+destruct H as (z & Hz & Hhz).
+move z after t; move Hz after Ht.
+assert (H : Happ c z - z' ∈ Ker h'). {
+  split.
+  -apply C'; [ now apply c | now apply C' ].
+  -rewrite Hadditive; [ | now apply c | now apply C' ].
+   rewrite Hopp; [ | easy ].
+   rewrite <- Hchh'.
+   apply gr_sub_move_r.
+   rewrite gr_add_0_l.
+   etransitivity; [ apply Happ_compat | ]; [ | apply Hhz | ]; try easy.
+   now apply h.
+}
+apply s' in H.
+destruct H as (y' & Hy' & Hgy').
+move y' after z'; move Hy' before Hz'.
+assert (H : ∃ y, y ∈ B ∧ (Happ b y = y')%G) by now apply epi_is_surj.
+destruct H as (y & Hy & Hby).
+move y after z; move Hy before Hz.
+specialize (Hgc (z - Happ g y)) as H1.
+assert (H : z - Happ g y ∈ C). {
+  apply C; [ easy | now apply C, g ].
+}
+specialize (H1 H); clear H.
+assert (H : (Happ c (z - Happ g y) = z')%G). {
+  rewrite Hadditive; [ | easy | now apply C, g ].
+  rewrite Hopp; [ | now apply g ].
+  apply gr_sub_move_r.
+  apply gr_sub_move_l.
+  rewrite <- Hgy'.
+  rewrite Hcgg'.
+  apply g'; [ easy | now symmetry ].
+}
+symmetry in H.
+etransitivity; [ apply Happ_compat | ]; [ | apply H | ]; cycle 1.
+-rewrite H1.
+ apply g₂; [ | easy ].
+ apply c, C; [ easy | now apply C, g ].
+-easy.
+Qed.
+
+(*
+            f      g       h
+        A------>B------>C------>D
+        |       ∩       |       ∩
+       a|      b|      c|      d|
+        v       |       |       |
+        v       v       v       v
+        A'----->B'----->C'----->D'
+           f'      g'      h'
+
+  If 1/ the diagram is commutative,
+     2/ (f, g, h) and (f', g', h') are exact,
+     3/ b and d are monomorphisms,
+     4/ a is epimorphism,
+  Then
+     c is an monomorphism.
+*)
+
+Lemma four_2 :
+  ∀ (A B C D A' B' C' D' : AbGroup)
+     (f : HomGr A B) (g : HomGr B C) (h : HomGr C D)
+     (f' : HomGr A' B') (g' : HomGr B' C') (h' : HomGr C' D')
+     (a : HomGr A A') (b : HomGr B B')
+     (c : HomGr C C') (d : HomGr D D'),
+  diagram_commutes f a b f'
+  → diagram_commutes g b c g'
+  → diagram_commutes h c d h'
+  → exact_sequence [f; g; h]
+  → exact_sequence [f'; g'; h']
+  → is_mono b ∧ is_mono d ∧ is_epi a
+  → is_mono c.
+Proof.
+intros * Hcff' Hcgg' Hchh' s s' (Hmb & Hmd & Hea).
+intros T g₁ g₂ Hcg u Hu.
+specialize (Hcg u Hu) as H.
+assert (H1 :( Happ c (Happ g₁ u - Happ g₂ u) = 0)%G). {
+  rewrite Hadditive; [ | now apply g₁ | now apply C, g₂ ].
+  rewrite Hopp; [ | now apply g₂ ].
+  now rewrite H, gr_add_opp_r.
+}
+clear H.
+symmetry; rewrite <- gr_add_0_r; symmetry.
+apply gr_sub_move_l.
+set (z := Happ g₁ u - Happ g₂ u) in H1 |-*.
+assert (Hz : z ∈ C) by (apply C; [ now apply g₁ | now apply C, g₂ ]).
+move Hz before z.
+generalize H1; intros H2.
+apply (Happ_compat _ _ h') in H2; [ | now apply c ].
+rewrite <- Hchh', Hzero in H2.
+assert (H3 : z ∈ Ker h). {
+  split; [ easy | ].
+  apply (mono_is_inj Hmd); [ now apply h | apply D | now rewrite Hzero ].
+}
+apply s in H3.
+destruct H3 as (y & Hy & Hgy).
+generalize Hgy; intros H3.
+apply (Happ_compat _ _ c) in H3; [ | now apply g ].
+rewrite Hcgg', H1 in H3.
+assert (H4 : Happ b y ∈ Ker g') by (split; [ now apply b | easy ]).
+apply s' in H4.
+destruct H4 as (x' & Hx' & Hfx').
+assert (H : ∃ x, x ∈ A ∧ (Happ a x = x')%G) by now apply epi_is_surj.
+destruct H as (x & Hx & Hax).
+assert (H4 : (Happ f' (Happ a x) = Happ b y)%G). {
+  etransitivity; [ apply Happ_compat | ]; [ | apply Hax | ]; try easy.
+  now apply a.
+}
+rewrite <- Hcff' in H4.
+apply mono_is_inj in H4; [ | easy | now apply f | easy ].
+assert (H5 : (Happ g (Happ f x) = z)%G). {
+  etransitivity; [ apply Happ_compat | ]; [ | apply H4 | ]; try easy.
+  now apply f.
+}
+rewrite <- H5.
+assert (H : Happ f x ∈ Im f) by now exists x.
+apply s in H.
+now destruct H.
+Qed.
+
+