From 9f5c228d068d5da86db5fb1532ea3ca1b9c11c41 Mon Sep 17 00:00:00 2001 From: itamar Date: Mon, 9 Mar 2026 22:39:37 +0200 Subject: push push --- four.v | 188 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 four.v (limited to 'four.v') 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. + + -- cgit v1.2.3