diff options
Diffstat (limited to 'five.v')
| -rw-r--r-- | five.v | 128 |
1 files changed, 128 insertions, 0 deletions
@@ -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. + |