diff options
| -rw-r--r-- | abgroup.v | 719 | ||||
| -rw-r--r-- | five.v | 128 | ||||
| -rw-r--r-- | four.v | 188 | ||||
| -rw-r--r-- | snake.v | 836 |
4 files changed, 1871 insertions, 0 deletions
diff --git a/abgroup.v b/abgroup.v new file mode 100644 index 0000000..8825e33 --- /dev/null +++ b/abgroup.v @@ -0,0 +1,719 @@ +(* Abelian groups and Homomorphisms *) + +Require Import Utf8. +Require Import Setoid Morphisms. + +Reserved Notation "x '∈' S" (at level 60). +Reserved Notation "x '≡' y" (at level 70). + +(* Abelian Groups. + + Notes: + + -sets in groups are predicates (naive theory of sets); a value of type + gr_set is not necessarily in the group set. To be in the group set, it + must satisfy the predicate gr_mem, which is later syntaxified by the + usual symbol ∈. This allows to create subgroups by changing gr_mem. + + -group sets are setoids: there is a specific equality (gr_eq) which is + compatible with membership (gr_mem_compat), addition (gr_add_compat), + and opposite (gr_opp_compat). This allows to define quotient groups, + for example in cokernets, by changing this equality. +*) + +Record AbGroup := + { (* data *) + gr_set : Type; + gr_mem : gr_set → Prop where "x ∈ G" := (gr_mem x); + gr_eq : gr_set → gr_set → Prop where "x ≡ y" := (gr_eq x y); + gr_zero : gr_set where "0" := (gr_zero); + gr_add : gr_set → gr_set → gr_set where "x + y" := (gr_add x y); + gr_opp : gr_set → gr_set where "- x" := (gr_opp x); + (* properties *) + gr_zero_mem : 0 ∈ G; + gr_add_mem : ∀ x y, x ∈ G → y ∈ G → x + y ∈ G; + gr_add_0_l : ∀ x, 0 + x ≡ x; + gr_add_assoc : ∀ x y z, (x + y) + z ≡ x + (y + z); + gr_opp_mem : ∀ x, x ∈ G → - x ∈ G; + gr_add_opp_r : ∀ x, x + (- x) ≡ 0; + gr_add_comm : ∀ x y, x + y ≡ y + x; + gr_equiv : Equivalence gr_eq; + gr_mem_compat : ∀ x y, x ≡ y → x ∈ G → y ∈ G; + gr_add_compat : ∀ x y x' y', x ≡ y → x' ≡ y' → x + x' ≡ y + y'; + gr_opp_compat : ∀ x y, x ≡ y → - x ≡ - y }. + +(* coq stuff: implicit and renamed arguments *) + +Arguments gr_eq [_]. +Arguments gr_zero [_]. +Arguments gr_add [_]. +Arguments gr_opp [_]. +Arguments gr_zero_mem G : rename. +Arguments gr_add_mem G : rename. +Arguments gr_add_0_l G : rename. +Arguments gr_add_assoc G : rename. +Arguments gr_opp_mem G : rename. +Arguments gr_add_opp_r G : rename. +Arguments gr_add_comm G : rename. +Arguments gr_equiv G : rename. +Arguments gr_mem_compat G : rename. +Arguments gr_add_compat G : rename. +Arguments gr_opp_compat G : rename. + +(* syntaxes for expressions for groups elements and sets *) + +Delimit Scope group_scope with G. + +Notation "0" := (gr_zero) : group_scope. +Notation "a = b" := (gr_eq a b) : group_scope. +Notation "a ≠ b" := (¬ gr_eq a b) : group_scope. +Notation "a + b" := (gr_add a b) : group_scope. +Notation "a - b" := (gr_add a (gr_opp b)) : group_scope. +Notation "- a" := (gr_opp a) : group_scope. + +Notation "x '∈' S" := (gr_mem S x) (at level 60). +Notation "x '∉' S" := (¬ gr_mem S x) (at level 60). + +Open Scope group_scope. + +(* Homomorphism between groups *) + +Record HomGr (A B : AbGroup) := + { Happ : gr_set A → gr_set B; + Hmem_compat : ∀ x, x ∈ A → Happ x ∈ B; + Happ_compat : ∀ x y, x ∈ A → (x = y)%G → (Happ x = Happ y)%G; + Hadditive : ∀ x y, + x ∈ A → y ∈ A → (Happ (x + y) = Happ x + Happ y)%G }. + +(* coq stuff: implicit and renamed arguments *) + +Arguments Happ [A] [B]. +Arguments Hmem_compat _ _ f : rename. +Arguments Happ_compat _ _ f : rename. +Arguments Hadditive _ _ f : rename. + +(* Equality (gr_eq) of groups elements is an equivalence relation *) + +Instance gr_eq_rel {G} : Equivalence (@gr_eq G). +Proof. apply gr_equiv. Qed. + +(* Coq "Morphisms": they allow to use "rewrite" in expressions containing + opposites (-), additions (+) and memberships (∈) *) + +Instance gr_opp_morph {G} : Proper (@gr_eq G ==> @gr_eq G) (@gr_opp G). +Proof. +intros x y Hxy. +now apply gr_opp_compat. +Qed. + +Instance gr_add_morph {G} : + Proper (@gr_eq G ==> @gr_eq G ==> @gr_eq G) (@gr_add G). +Proof. +intros x y Hxy x' y' Hxy'. +now apply gr_add_compat. +Qed. + +Instance gr_mem_morph {G} : Proper (@gr_eq G ==> iff) (@gr_mem G). +Proof. +intros x y Hxy. +split; intros H. +-eapply gr_mem_compat; [ apply Hxy | easy ]. +-eapply gr_mem_compat; [ symmetry; apply Hxy | easy ]. +Qed. + +(* +Instance gr_app_morph {G H f} : Proper (@gr_eq G ==> @gr_eq H) (Happ f). +Proof. +intros x y Hxy. +apply Happ_compat; [ | easy ]. +... +blocked: we have to prove x ∈ G but it is not possible to +have this hypothesis in Proper +*) + +(* Miscellaneous theorems in groups *) + +Theorem gr_add_0_r : ∀ G (x : gr_set G), (x + 0 = x)%G. +Proof. +intros. +rewrite gr_add_comm. +apply gr_add_0_l. +Qed. + +Theorem gr_add_opp_l : ∀ G (x : gr_set G), (- x + x = 0)%G. +Proof. +intros. +rewrite gr_add_comm. +apply gr_add_opp_r. +Qed. + +Theorem gr_opp_zero : ∀ G, (- 0 = @gr_zero G)%G. +Proof. +intros. +rewrite <- gr_add_0_l. +apply gr_add_opp_r. +Qed. + +Theorem gr_sub_0_r : ∀ G (x : gr_set G), (x - 0 = x)%G. +Proof. +intros. +symmetry; rewrite <- gr_add_0_r at 1. +apply gr_add_compat; [ easy | now rewrite gr_opp_zero ]. +Qed. + +Theorem gr_sub_move_r : ∀ G (x y z : gr_set G), + (x - y = z)%G ↔ (x = z + y)%G. +Proof. +intros. +split; intros Hxyz. +-now rewrite <- Hxyz, gr_add_assoc, gr_add_opp_l, gr_add_0_r. +-now rewrite Hxyz, gr_add_assoc, gr_add_opp_r, gr_add_0_r. +Qed. + +Theorem gr_sub_move_l : ∀ G (x y z : gr_set G), + (x - y = z)%G ↔ (x = y + z)%G. +Proof. +intros. +split; intros Hxyz. +-now rewrite <- Hxyz, gr_add_comm, gr_add_assoc, gr_add_opp_l, gr_add_0_r. +-now rewrite Hxyz, gr_add_comm, <- gr_add_assoc, gr_add_opp_l, gr_add_0_l. +Qed. + +Theorem gr_opp_add_distr : ∀ G (x y : gr_set G), (- (x + y) = - x - y)%G. +Proof. +intros *. +symmetry. +apply gr_sub_move_r. +rewrite <- gr_add_0_l. +apply gr_sub_move_r. +symmetry; rewrite gr_add_assoc. +symmetry. +apply gr_sub_move_r. +rewrite gr_add_0_l. +apply gr_opp_compat, gr_add_comm. +Qed. + +Theorem gr_opp_involutive : ∀ G (x : gr_set G), (- - x = x)%G. +Proof. +intros. +transitivity (- - x + (- x + x))%G. +-rewrite <- gr_add_0_r at 1. + apply gr_add_compat; [ easy | ]. + now rewrite gr_add_opp_l. +-now rewrite <- gr_add_assoc, gr_add_opp_l, gr_add_0_l. +Qed. + +Theorem gr_eq_opp_l : ∀ G (x y : gr_set G), (- x = y)%G ↔ (x = - y)%G. +Proof. +intros. +split; intros Hxy. +-rewrite <- Hxy; symmetry; apply gr_opp_involutive. +-rewrite Hxy; apply gr_opp_involutive. +Qed. + +(* Theorems on homomorphisms *) + +Theorem Hzero : ∀ A B (f : HomGr A B), (Happ f 0 = 0)%G. +Proof. +intros. +assert (H1 : (@gr_zero A + 0 = 0)%G) by apply A. +assert (H2 : (Happ f 0 + Happ f 0 = Happ f 0)%G). { + rewrite <- Hadditive; [ | apply A | apply A ]. + apply f; [ apply A; apply A | apply A ]. +} +assert (H3 : (Happ f 0 + Happ f 0 - Happ f 0 = Happ f 0 - Happ f 0)%G). { + apply gr_add_compat; [ apply H2 | easy ]. +} +assert (H4 : (Happ f 0 + Happ f 0 - Happ f 0 = 0)%G). { + rewrite H3; apply gr_add_opp_r. +} +rewrite <- H4. +now rewrite gr_add_assoc, gr_add_opp_r, gr_add_0_r. +Qed. + +Theorem Hopp : ∀ A B (f : HomGr A B) x, + x ∈ A → (Happ f (- x) = - Happ f x)%G. +Proof. +intros * Hx. +assert (H2 : (Happ f (x - x) = Happ f 0)%G). { + apply Happ_compat; [ now apply A, A | apply A ]. +} +assert (H3 : (Happ f x + Happ f (- x) = Happ f 0)%G). { + rewrite <- H2. + symmetry; apply Hadditive; [ easy | now apply A ]. +} +assert (H4 : (Happ f x + Happ f (- x) = 0)%G). { + rewrite H3; apply Hzero. +} +symmetry; rewrite <- gr_add_0_l. +apply gr_sub_move_l. +now symmetry. +Qed. + +(* Images *) + +Theorem Im_zero_mem {G H} : ∀ (f : HomGr G H), + ∃ a : gr_set G, a ∈ G ∧ (Happ f a = 0)%G. +Proof. +intros. +exists 0%G. +split; [ apply gr_zero_mem | apply Hzero ]. +Qed. + +Theorem Im_add_mem {G H} : ∀ f (x y : gr_set H), + (∃ a : gr_set G, a ∈ G ∧ (Happ f a = x)%G) + → (∃ a : gr_set G, a ∈ G ∧ (Happ f a = y)%G) + → ∃ a : gr_set G, a ∈ G ∧ (Happ f a = x + y)%G. +Proof. +intros f y y' (x & Hxg & Hx) (x' & Hx'g & Hx'). +exists (gr_add x x'). +split; [ now apply G | ]. +rewrite Hadditive; [ | easy | easy ]. +now apply gr_add_compat. +Qed. + +Theorem Im_opp_mem {G H} : ∀ (f : HomGr G H) (x : gr_set H), + (∃ a : gr_set G, a ∈ G ∧ (Happ f a = x)%G) + → ∃ a : gr_set G, a ∈ G ∧ (Happ f a = - x)%G. +Proof. +intros f x (y & Hy & Hyx). +exists (gr_opp y). +split; [ now apply gr_opp_mem | ]. +rewrite <- Hyx. +now apply Hopp. +Qed. + +Theorem Im_mem_compat {G H} : ∀ f (x y : gr_set H), + (x = y)%G + → (∃ a, a ∈ G ∧ (Happ f a = x)%G) + → ∃ a, a ∈ G ∧ (Happ f a = y)%G. +intros * Hxy (z & Hz & Hfz). +exists z. +split; [ easy | now rewrite Hfz ]. +Qed. + +Definition Im {G H : AbGroup} (f : HomGr G H) := + {| gr_set := gr_set H; + gr_zero := gr_zero; + gr_eq := @gr_eq H; + gr_mem := λ b, ∃ a, a ∈ G ∧ (Happ f a = b)%G; + gr_add := @gr_add H; + gr_opp := @gr_opp H; + gr_zero_mem := Im_zero_mem f; + gr_add_mem := Im_add_mem f; + gr_add_0_l := gr_add_0_l H; + gr_add_assoc := gr_add_assoc H; + gr_opp_mem := Im_opp_mem f; + gr_add_opp_r := gr_add_opp_r H; + gr_add_comm := gr_add_comm H; + gr_equiv := gr_equiv H; + gr_mem_compat := Im_mem_compat f; + gr_add_compat := gr_add_compat H; + gr_opp_compat := gr_opp_compat H |}. + +(* Kernels *) + +Theorem Ker_zero_mem {G H} : ∀ (f : HomGr G H), 0%G ∈ G ∧ (Happ f 0 = 0)%G. +Proof. +intros f. +split; [ apply gr_zero_mem | apply Hzero ]. +Qed. + +Theorem Ker_add_mem {G H} : ∀ (f : HomGr G H) (x y : gr_set G), + x ∈ G ∧ (Happ f x = 0)%G + → y ∈ G ∧ (Happ f y = 0)%G → (x + y)%G ∈ G ∧ (Happ f (x + y) = 0)%G. +Proof. +intros f x x' (Hx, Hfx) (Hx', Hfx'). +split; [ now apply gr_add_mem | ]. +rewrite Hadditive; [ | easy | easy ]. +rewrite Hfx, Hfx'. +apply gr_add_0_r. +Qed. + +Theorem Ker_opp_mem {G H} : ∀ (f : HomGr G H) (x : gr_set G), + x ∈ G ∧ (Happ f x = 0)%G → (- x)%G ∈ G ∧ (Happ f (- x) = 0)%G. +Proof. +intros f x (Hx & Hfx). +split; [ now apply gr_opp_mem | ]. +rewrite Hopp; [ | easy ]. +rewrite Hfx. +apply gr_opp_zero. +Qed. + +Theorem Ker_mem_compat {G H} : ∀ (f : HomGr G H) x y, + (x = y)%G → x ∈ G ∧ (Happ f x = 0)%G → y ∈ G ∧ (Happ f y = 0)%G. +Proof. +intros * Hxy (ax, Hx). +split. +-eapply gr_mem_compat; [ apply Hxy | easy ]. +-rewrite <- Hx. + apply f; [ | easy ]. + now rewrite <- Hxy. +Qed. + +Definition Ker {G H : AbGroup} (f : HomGr G H) := + {| gr_set := gr_set G; + gr_zero := gr_zero; + gr_eq := @gr_eq G; + gr_mem := λ a, a ∈ G ∧ (Happ f a = gr_zero)%G; + gr_add := @gr_add G; + gr_opp := @gr_opp G; + gr_zero_mem := Ker_zero_mem f; + gr_add_mem := Ker_add_mem f; + gr_add_0_l := gr_add_0_l G; + gr_add_assoc := gr_add_assoc G; + gr_opp_mem := Ker_opp_mem f; + gr_add_opp_r := gr_add_opp_r G; + gr_add_comm := gr_add_comm G; + gr_equiv := gr_equiv G; + gr_mem_compat := Ker_mem_compat f; + gr_add_compat := gr_add_compat G; + gr_opp_compat := gr_opp_compat G |}. + +(* Cokernels + + x ∈ Coker f ↔ x ∈ H/Im f + quotient group is H with setoid, i.e. set with its own equality *) + +Definition Coker_eq {G H} (f : HomGr G H) x y := (x - y)%G ∈ Im f. + +Theorem Coker_add_0_l {G H} : ∀ (f : HomGr G H) x, Coker_eq f (0 + x)%G x. +Proof. +intros. +unfold Coker_eq. +exists 0%G. +split; [ apply gr_zero_mem | ]. +rewrite gr_add_0_l, gr_add_opp_r. +simpl; apply Hzero. +Qed. + +Theorem Coker_add_assoc {G H} : ∀ (f : HomGr G H) x y z, + Coker_eq f (x + y + z)%G (x + (y + z))%G. +Proof. +intros. +unfold Coker_eq. +exists 0%G. +split; [ apply gr_zero_mem | ]. +rewrite Hzero. +symmetry; simpl. +apply gr_sub_move_r. +rewrite gr_add_0_l. +apply gr_add_assoc. +Qed. + +Theorem Coker_add_opp_r {G H} : ∀ (f : HomGr G H) x, Coker_eq f (x - x)%G 0%G. +Proof. +intros. +exists 0%G. +split; [ apply gr_zero_mem | ]. +now rewrite Hzero, gr_add_opp_r, gr_sub_0_r. +Qed. + +Theorem Coker_add_comm {G H} : ∀ (f : HomGr G H) x y, + Coker_eq f (x + y)%G (y + x)%G. +Proof. +intros. +exists 0%G. +split; [ apply gr_zero_mem | ]. +rewrite Hzero. +symmetry. +simpl; apply gr_sub_move_l. +now rewrite gr_add_0_r, gr_add_comm. +Qed. + +Theorem Coker_eq_refl {G H} (f : HomGr G H) : Reflexive (Coker_eq f). +Proof. +intros x. +exists 0%G. +split; [ apply gr_zero_mem | ]. +rewrite gr_add_opp_r. +simpl; apply Hzero. +Qed. + +Theorem Coker_eq_symm {G H} (f : HomGr G H) : Symmetric (Coker_eq f). +Proof. +intros x y Hxy. +destruct Hxy as (z & Hz & Hfz). +exists (- z)%G. +split; [ now apply gr_opp_mem | ]. +rewrite Hopp; [ | easy ]. +rewrite Hfz. +simpl; rewrite gr_opp_add_distr, gr_add_comm. +apply gr_add_compat; [ | easy ]. +apply gr_opp_involutive. +Qed. + +Theorem Coker_eq_trans {G H} (f : HomGr G H) : Transitive (Coker_eq f). +Proof. +intros x y z Hxy Hyz. +simpl in Hxy, Hyz. +destruct Hxy as (t & Ht & Hft). +destruct Hyz as (u & Hu & Hfu). +exists (t + u)%G. +split; [ now apply gr_add_mem | ]. +rewrite Hadditive; [ | easy | easy ]. +rewrite Hft, Hfu. +simpl; rewrite gr_add_assoc. +apply gr_add_compat; [ easy | ]. +now rewrite <- gr_add_assoc, gr_add_opp_l, gr_add_0_l. +Qed. + +Theorem Coker_equiv {G H} : ∀ (f : HomGr G H), Equivalence (Coker_eq f). +Proof. +intros. +unfold Coker_eq; split. +-apply Coker_eq_refl. +-apply Coker_eq_symm. +-apply Coker_eq_trans. +Qed. + +Add Parametric Relation {G H} {f : HomGr G H} : (gr_set (Im f)) (Coker_eq f) + reflexivity proved by (Coker_eq_refl f) + symmetry proved by (Coker_eq_symm f) + transitivity proved by (Coker_eq_trans f) + as gr_cokereq_rel. + +Theorem Coker_mem_compat {G H} : ∀ (f : HomGr G H) x y, + Coker_eq f x y → x ∈ H → y ∈ H. +Proof. +intros * Heq Hx. +destruct Heq as (z & Hz & Hfz). +apply gr_mem_compat with (x := (x - Happ f z)%G). +-rewrite Hfz. + simpl; apply gr_sub_move_r. + now rewrite gr_add_comm, gr_add_assoc, gr_add_opp_l, gr_add_0_r. +-simpl; apply gr_add_mem; [ easy | ]. + apply gr_opp_mem. + now apply f. +Qed. + +Theorem Coker_add_compat {G H} : ∀ (f : HomGr G H) x y x' y', + Coker_eq f x y → Coker_eq f x' y' → Coker_eq f (x + x')%G (y + y')%G. +Proof. +intros f x y x' y' (z & Hz & Hfz) (z' & Hz' & Hfz'). +exists (z + z')%G. +split. +-now apply gr_add_mem. +-rewrite Hadditive; [ | easy | easy ]. + rewrite Hfz, Hfz'; simpl. + rewrite gr_add_assoc; symmetry. + rewrite gr_add_assoc; symmetry. + apply gr_add_compat; [ easy | ]. + rewrite gr_add_comm, gr_add_assoc. + apply gr_add_compat; [ easy | ]. + rewrite gr_add_comm; symmetry. + apply gr_opp_add_distr. +Qed. + +Theorem Coker_opp_compat {G H} :∀ (f : HomGr G H) x y, + Coker_eq f x y → Coker_eq f (- x)%G (- y)%G. +Proof. +intros * (z & Hz & Hfz). +unfold Coker_eq; simpl. +exists (- z)%G. +split; [ now apply gr_opp_mem | ]. +rewrite Hopp; [ | easy ]. +rewrite Hfz. +simpl; apply gr_opp_add_distr. +Qed. + +Definition Coker {G H : AbGroup} (f : HomGr G H) := + {| gr_set := gr_set H; + gr_zero := gr_zero; + gr_eq := Coker_eq f; + gr_mem := gr_mem H; + gr_add := @gr_add H; + gr_opp := @gr_opp H; + gr_zero_mem := @gr_zero_mem H; + gr_add_mem := @gr_add_mem H; + gr_add_0_l := Coker_add_0_l f; + gr_add_assoc := Coker_add_assoc f; + gr_opp_mem := gr_opp_mem H; + gr_add_opp_r := Coker_add_opp_r f; + gr_add_comm := Coker_add_comm f; + gr_equiv := Coker_equiv f; + gr_mem_compat := Coker_mem_compat f; + gr_add_compat := Coker_add_compat f; + gr_opp_compat := Coker_opp_compat f |}. + +(* Exact sequences *) + +Inductive sequence {A : AbGroup} := + | SeqEnd : sequence + | Seq : ∀ {B} (f : HomGr A B), @sequence B → sequence. + +Notation "A ⊂ B" := (∀ a, a ∈ A → a ∈ B) (at level 60). +Notation "A == B" := (A ⊂ B ∧ B ⊂ A) (at level 60). + +Fixpoint exact_sequence {A : AbGroup} (S : sequence) := + match S with + | SeqEnd => True + | Seq f S' => + match S' with + | SeqEnd => True + | Seq g S'' => Im f == Ker g ∧ exact_sequence S' + end + end. + +Delimit Scope seq_scope with S. + +Notation "[ ]" := SeqEnd (format "[ ]") : seq_scope. +Notation "[ x ]" := (Seq x SeqEnd) : seq_scope. +Notation "[ x ; y ; .. ; z ]" := (Seq x (Seq y .. (Seq z SeqEnd) ..)) : seq_scope. + +Arguments exact_sequence _ S%S. + +(* + f + A------>B + | | + g| |h + | | + v v + C------>D + k +*) + +Definition diagram_commutes {A B C D} + (f : HomGr A B) (g : HomGr A C) (h : HomGr B D) (k : HomGr C D) := + ∀ x, (Happ h (Happ f x) = Happ k (Happ g x))%G. + +(* The trivial group *) + +Theorem Gr1_add_0_l : ∀ x : True, I = x. +Proof. now destruct x. Qed. + +Definition Gr1 := + {| gr_set := True; + gr_mem _ := True; + gr_eq := eq; + gr_zero := I; + gr_add _ _ := I; + gr_opp x := x; + gr_zero_mem := I; + gr_add_mem _ _ _ _ := I; + gr_add_0_l := Gr1_add_0_l; + gr_add_assoc _ _ _ := eq_refl; + gr_opp_mem _ H := H; + gr_add_opp_r _ := eq_refl; + gr_add_comm _ _ := eq_refl; + gr_equiv := eq_equivalence; + gr_mem_compat _ _ _ _ := I; + gr_add_compat _ _ _ _ _ _ := eq_refl; + gr_opp_compat _ _ H := H |}. + +(* *) + +Definition is_mono {A B} (f : HomGr A B) := + ∀ C (g₁ g₂ : HomGr C A), + (∀ z, z ∈ C → (Happ f (Happ g₁ z) = Happ f (Happ g₂ z))%G) + → (∀ z, z ∈ C → (Happ g₁ z = Happ g₂ z)%G). + +Definition is_epi {A B} (f : HomGr A B) := + ∀ C (g₁ g₂ : HomGr B C), + (∀ x, x ∈ A → (Happ g₁ (Happ f x) = Happ g₂ (Happ f x))%G) + → (∀ y, y ∈ B → (Happ g₁ y = Happ g₂ y)%G). + +Definition is_iso {A B} (f : HomGr A B) := + ∃ g : HomGr B A, + (∀ x, x ∈ A → (Happ g (Happ f x) = x)%G) ∧ + (∀ y, y ∈ B → (Happ f (Happ g y) = y)%G). + +(* epimorphism is surjective and monomorphism is injective *) + +Theorem epi_is_surj : ∀ {A B} {f : HomGr A B}, + is_epi f + → ∀ y, y ∈ B → ∃ t, t ∈ A ∧ (Happ f t = y)%G. +Proof. +intros * Hed y Hy. +(* type gr_set B → gr_set (Coker f) *) +set (v y1 := let _ : gr_set B := y1 in y1 : gr_set (Coker f)). +assert (Hmc : ∀ y1, y1 ∈ B → v y1 ∈ B) by easy. +assert (Hac : ∀ y1 y2, y1 ∈ B → (y1 = y2)%G → (v y1 = v y2)%G). { + intros * Hy1 Hyy. + exists 0; split; [ apply A | ]. + now unfold v; simpl; rewrite Hzero, Hyy, gr_add_opp_r. +} +assert (Had : ∀ y1 y2, y1 ∈ B → y2 ∈ B → (v (y1 + y2) = v y1 + v y2)%G). { + intros * Hy1 Hy2. + exists 0; split; [ apply A | now unfold v; rewrite Hzero, gr_add_opp_r ]. +} +set (hv := + {| Happ := v; + Hmem_compat := Hmc; + Happ_compat := Hac; + Hadditive := Had |}). +assert (Hmc₀ : ∀ y1, y1 ∈ B → 0 ∈ Coker f) by (intros; apply B). +assert (Hac₀ : ∀ y1 y2, y1 ∈ B → (y1 = y2)%G → (@gr_zero (Coker f) = 0)%G). { + intros * Hy1 Hyy. + simpl; unfold Coker_eq; simpl. + exists 0; split; [ apply A | now rewrite Hzero, gr_add_opp_r ]. +} +assert (Had₀ : ∀ y1 y2, y1 ∈ B → y2 ∈ B → (@gr_zero (Coker f) = 0 + 0)%G). { + intros * Hy1 Hy2. + simpl; unfold Coker_eq; simpl. + exists 0; split; [ apply A | now rewrite Hzero, gr_add_0_r, gr_sub_0_r ]. +} +set (hw := + {| Happ _ := 0; + Hmem_compat := Hmc₀; + Happ_compat := Hac₀; + Hadditive := Had₀ |}). +specialize (Hed (Coker f) hv hw) as H1. +assert (H : ∀ x, x ∈ A → (Happ hv (Happ f x) = Happ hw (Happ f x))%G). { + intros x Hx. + simpl; unfold v; unfold Coker_eq; simpl. + exists x; split; [ easy | now rewrite gr_sub_0_r ]. +} +specialize (H1 H y Hy); clear H. +simpl in H1; unfold Coker_eq in H1; simpl in H1. +destruct H1 as (x & Hx). +rewrite gr_sub_0_r in Hx. +now exists x. +Qed. + +Theorem mono_is_inj : ∀ {A B} {f : HomGr A B}, + is_mono f + → ∀ x1 x2, x1 ∈ A → x2 ∈ A → (Happ f x1 = Happ f x2)%G → (x1 = x2)%G. +Proof. +intros * Hf * Hx1 Hx2 Hxx. +(* morphism identity from Ker f to A *) +set (v x := let _ : gr_set (Ker f) := x in x : gr_set A). +assert (Hmc : ∀ x, x ∈ Ker f → v x ∈ A) by (intros x Hx; apply Hx). +set (hv := + {| Happ := v; + Hmem_compat := Hmc; + Happ_compat _ _ _ H := H; + Hadditive _ _ _ _ := reflexivity _ |}). +(* morphism null from Ker f to A *) +set (hw := + {| Happ x := let _ : gr_set (Ker f) := x in 0 : gr_set A; + Hmem_compat _ _ := gr_zero_mem A; + Happ_compat _ _ _ _ := reflexivity _; + Hadditive _ _ _ _ := symmetry (gr_add_0_r _ _) |}). +specialize (Hf (Ker f) hv hw) as H1. +assert (H : ∀ z, z ∈ Ker f → (Happ f (Happ hv z) = Happ f (Happ hw z))%G). { + intros z (Hz, Hfz). + unfold hv, hw, v; simpl. + now rewrite Hfz, Hzero. +} +specialize (H1 H (x1 - x2)); clear H. +assert (H : x1 - x2 ∈ Ker f). { + split. + -apply A; [ easy | now apply A ]. + -rewrite Hadditive; [ | easy | now apply A ]. + rewrite Hopp; [ | easy ]. + now rewrite Hxx, gr_add_opp_r. +} +specialize (H1 H); clear H. +unfold hv, hw, v in H1; simpl in H1. +apply gr_sub_move_r in H1. +now rewrite gr_add_0_l in H1. +Qed. + +(* We sometimes need these axioms *) + +Definition Choice := ∀ {A B} {R : A → B → Prop}, + (∀ x : A, ∃ y : B, R x y) → ∃ f : A → B, ∀ x : A, R x (f x). +Definition Decidable_Membership := ∀ G x, {x ∈ G} + {x ∉ G}. + @@ -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. + @@ -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. + + @@ -0,0 +1,836 @@ +(* Snake lemma *) + +Require Import Utf8. +Require Import Classes.RelationClasses. +Require Import Setoid. + +Require Import AbGroup. + +(* Functor HomGr A B → HomGr (KerA) (KerB) *) + +Theorem KK_mem_compat {A B A' B'} : ∀ (a : HomGr A A') (b : HomGr B B') f f', + diagram_commutes f a b f' + → ∀ x : gr_set (Ker a), x ∈ Ker a → Happ f x ∈ Ker b. +intros * Hc * (Hx & Hax). +split; [ now apply f | ]. +rewrite Hc, <- (Hzero _ _ f'). +apply f'; [ apply a, Hx | easy ]. +Qed. + +Theorem KK_app_compat {A B A'} : ∀ (f : HomGr A B) (a : HomGr A A'), + ∀ x y : gr_set (Ker a), x ∈ Ker a → (x = y)%G → (Happ f x = Happ f y)%G. +Proof. +intros * Hx Hxy. +simpl in Hx. +now apply f. +Qed. + +Theorem KK_additive {A B A'} : ∀ (f : HomGr A B) (a : HomGr A A'), + ∀ x y : gr_set (Ker a), + x ∈ Ker a → y ∈ Ker a → (Happ f (x + y) = Happ f x + Happ f y)%G. +Proof. +intros * Hx Hx'; simpl in Hx, Hx'. +now apply f. +Qed. + +Definition HomGr_Ker_Ker {A B A' B'} + {f : HomGr A B} {f' : HomGr A' B'} (a : HomGr A A') (b : HomGr B B') + (Hc : diagram_commutes f a b f') := + {| Happ (x : gr_set (Ker a)) := Happ f x : gr_set (Ker b); + Hmem_compat := KK_mem_compat a b f f' Hc; + Happ_compat := KK_app_compat f a; + Hadditive := KK_additive f a |}. + +(* Functor f:HomGr A B → g:HomGr B C → HomGr (CoKer f) (Coker g) *) + +Theorem CC_mem_compat {A B A' B'} : + ∀ (f' : HomGr A' B') (a : HomGr A A') (b : HomGr B B'), + ∀ x : gr_set (Coker a), x ∈ Coker a → Happ f' x ∈ Coker b. +Proof. +intros * Hx. +now apply f'. +Qed. + +Theorem CC_app_compat {A B A' B'} : + ∀ (f : HomGr A B) (f' : HomGr A' B') (a : HomGr A A') (b : HomGr B B'), + diagram_commutes f a b f' + → ∀ x y : gr_set (Coker a), + x ∈ Coker a + → (x = y)%G + → @gr_eq (Coker b) (Happ f' x) (Happ f' y)%G. +Proof. +intros * Hc * Hx Hxy. +assert (Hy : y ∈ Coker a) by now apply (gr_mem_compat _ x). +simpl in Hx, x, y, Hxy; simpl. +destruct Hxy as (z & Hz & Haz). +simpl; unfold Coker_eq; simpl. +exists (Happ f z). +split; [ now apply f | ]. +rewrite Hc. +transitivity (Happ f' (x - y)%G). +-apply Happ_compat; [ now apply a | easy ]. +-rewrite Hadditive; [ | easy | ]. + +apply gr_add_compat; [ easy | now apply Hopp ]. + +now apply A'. +Qed. + +Theorem CC_additive {A B A' B'} : + ∀ (f' : HomGr A' B') (a : HomGr A A') (b : HomGr B B'), + ∀ x y : gr_set (Coker a), + x ∈ Coker a + → y ∈ Coker a + → @gr_eq (Coker b) (Happ f' (x + y))%G (Happ f' x + Happ f' y)%G. +Proof. +intros * Hx Hy; simpl in Hx, Hy. +exists 0%G. +split; [ apply B | ]. +rewrite Hzero; symmetry. +simpl; apply gr_sub_move_r. +rewrite gr_add_0_l. +now apply Hadditive. +Qed. + +Definition HomGr_Coker_Coker {A B A' B'} + {f : HomGr A B} {f' : HomGr A' B'} (a : HomGr A A') (b : HomGr B B') + (Hc : diagram_commutes f a b f') := + {| Happ (x : gr_set (Coker a)) := Happ f' x : gr_set (Coker b); + Hmem_compat := CC_mem_compat f' a b; + Happ_compat := CC_app_compat f f' a b Hc; + Hadditive := CC_additive f' a b |}. + +Theorem g_is_surj {B C C' g} (c : HomGr C C') {cz : HomGr C Gr1} : + Decidable_Membership + → Im g == Ker cz + → ∀ x : gr_set (Ker c), ∃ y, x ∈ C → y ∈ B ∧ (Happ g y = x)%G. +Proof. +intros * mem_dec sg x. +destruct (mem_dec C x) as [H2| H2]; [ | now exists 0%G ]. +enough (H : x ∈ Im g). { + simpl in H. + destruct H as (y & Hy & Hyx). + now exists y. +} +apply sg. +split; [ easy | ]. +now destruct (Happ cz x). +Qed. + +Theorem f'_is_inj {A' B'} {f' : HomGr A' B'} {za' : HomGr Gr1 A'} : + Im za' == Ker f' + → ∀ x y, x ∈ A' → y ∈ A' → (Happ f' x = Happ f' y)%G → (x = y)%G. +Proof. +intros * sf' * Hx Hy Hxy. +assert (H2 : (Happ f' x - Happ f' y = 0)%G). { + apply gr_sub_move_r. + now rewrite gr_add_0_l. +} +assert (H3 : (Happ f' (x - y) = 0)%G). { + rewrite Hadditive; [ | easy | now apply A' ]. + rewrite Hxy, Hopp; [ | easy ]. + apply gr_add_opp_r. +} +assert (H4 : (x - y)%G ∈ Ker f'). { + split; [ | apply H3 ]. + apply A'; [ easy | now apply A' ]. +} +apply sf' in H4. +simpl in H4. +destruct H4 as (z & _ & H4). +destruct z. +assert (H5 : (x - y = 0)%G). { + rewrite <- H4. + apply Hzero. +} +apply gr_sub_move_r in H5. +rewrite H5. +apply gr_add_0_l. +Qed. + +Theorem f'c_is_inj + {A A' B'} {f' : HomGr A' B'} {a : HomGr A A'} {za' : HomGr Gr1 A'} : + Im za' == Ker f' + → ∀ x y, x ∈ Coker a → y ∈ Coker a → + (Happ f' x = Happ f' y)%G → (x = y)%G. +Proof. +intros * sf' * Hx Hy Hxy. +simpl; unfold Coker_eq; simpl. +exists 0; split; [ apply A | ]. +eapply (f'_is_inj sf'); [ apply a, A | | ]. +-apply A'; [ easy | now apply A' ]. +-transitivity (Happ f' 0). + +apply f'; [ apply a, A | apply Hzero ]. + +rewrite Hzero; symmetry. + rewrite Hadditive; [ | easy | now apply A' ]. + rewrite Hxy, Hopp; [ | easy ]. + apply gr_add_opp_r. +Qed. + +Definition g₁_prop {B C C'} g (c : HomGr C C') g₁ := + ∀ x : gr_set (Ker c), x ∈ C → g₁ x ∈ B ∧ (Happ g (g₁ x) = x)%G. + +Definition f'₁_prop + {A A' B C B' C'} (a : HomGr A A') (b : HomGr B B') {c : HomGr C C'} + (f' : HomGr A' B') g₁ f'₁ := + ∀ x : gr_set B', + (∃ x1 : gr_set (Ker c), x1 ∈ Ker c ∧ (x = Happ b (g₁ x1))%G) + → f'₁ x ∈ Coker a ∧ (Happ f' (f'₁ x) = x)%G. + +Theorem g₁_in_B : ∀ {B C C' g} {c : HomGr C C'} {g₁}, + g₁_prop g c g₁ → ∀ x, x ∈ C → g₁ x ∈ B. +Proof. +intros * Hg₁ * Hx. +now specialize (Hg₁ x Hx) as H. +Qed. + +Theorem exists_B'_to_Coker_a : ∀ {A A' B B' C C' g f'} + {g' : HomGr B' C'} (a : HomGr A A') {b : HomGr B B'} {c : HomGr C C'} {g₁}, + Decidable_Membership + → Im f' == Ker g' + → g₁_prop g c g₁ + → diagram_commutes g b c g' + → ∀ y', ∃ z', + (∃ x, x ∈ Ker c ∧ (y' = Happ b (g₁ x))%G) + → z' ∈ Coker a ∧ (Happ f' z' = y')%G. +Proof. +intros * mem_dec sg' Hg₁ Hcgg' *. +destruct (mem_dec (Im b) y') as [Hy'| Hy']. +-destruct (mem_dec (Im f') y') as [(z' & Hz' & Hfz')| Hfy']. + +exists z'; now intros (x' & Hx' & Hyx'). + +exists 0%G; intros (x' & Hx' & Hyx'). + exfalso; apply Hfy', sg'; simpl. + split. + *destruct Hy' as (y & Hy & Hby). + eapply B'; [ apply Hby | now apply b ]. + *transitivity (Happ g' (Happ b (g₁ x'))). + --apply Happ_compat; [ | easy ]. + destruct Hy' as (y & Hy & Hby). + eapply B'; [ apply Hby | now apply b ]. + --rewrite <- Hcgg'. + destruct Hx' as (Hx', Hcx'). + specialize (Hg₁ x' Hx') as H2. + destruct H2 as (Hgx', Hggx'). + transitivity (Happ c x'); [ | easy ]. + apply c; [ now apply g, (g₁_in_B Hg₁) | easy ]. +-exists 0%G; intros (x' & Hx' & Hyx'). + exfalso; apply Hy'. + exists (g₁ x'). + split; [ apply (g₁_in_B Hg₁); now simpl in Hx' | ]. + now symmetry. +Qed. + +Theorem d_mem_compat + {A A' B B' C C'} {a : HomGr A A'} {b : HomGr B B'} {c : HomGr C C'} + {f' : HomGr A' B'} {g₁ f'₁} : + let d := λ x, f'₁ (Happ b (g₁ x)) in + f'₁_prop a b f' g₁ f'₁ + → ∀ x, x ∈ Ker c → d x ∈ Coker a. +Proof. +intros * Hf'₁ * Hx. +apply Hf'₁. +now exists x. +Qed. + +Theorem d_app_compat + {A A' B B' C C'} {a : HomGr A A'} {b : HomGr B B'} {c : HomGr C C'} + {f : HomGr A B} {g : HomGr B C} {f' : HomGr A' B'} {g' : HomGr B' C'} + {za' : HomGr Gr1 A'} {g₁ f'₁} : + diagram_commutes f a b f' + → diagram_commutes g b c g' + → Im f == Ker g + → Im za' == Ker f' + → Im f' == Ker g' + → g₁_prop g c g₁ + → f'₁_prop a b f' g₁ f'₁ + → let d := λ x, f'₁ (Happ b (g₁ x)) in + ∀ x1 x2, x1 ∈ Ker c → (x1 = x2)%G → (d x1 = d x2)%G. +Proof. +intros * Hcff' Hcgg' sf sf' sg' Hg₁ Hf'₁ * Hx1 Hxx. +assert (Hx2 : x2 ∈ Ker c) by now apply (gr_mem_compat _ x1). +assert (Hgy1 : (Happ g (g₁ x1) = x1)%G) by apply Hg₁, Hx1. +assert (Hgy2 : (Happ g (g₁ x2) = x2)%G) by apply Hg₁, Hx2. +assert (Hgb1 : (Happ g' (Happ b (g₁ x1)) = 0)%G). { + rewrite <- Hcgg'. + etransitivity; [ | apply Hx1 ]. + apply c; [ apply g, Hg₁, Hx1 | apply Hgy1 ]. +} +assert (Hgb2 : (Happ g' (Happ b (g₁ x2)) = 0)%G). { + rewrite <- Hcgg'. + etransitivity; [ | apply Hx2 ]. + apply c; [ apply g, Hg₁, Hx2 | apply Hgy2 ]. +} +assert (H1 : Happ b (g₁ x1) ∈ Im f'). { + apply sg'; split; [ apply b, (g₁_in_B Hg₁), Hx1 | easy ]. +} +assert (H2 : Happ b (g₁ x2) ∈ Im f'). { + apply sg'; split; [ apply b, (g₁_in_B Hg₁), Hx2 | easy ]. +} +destruct H1 as (z'1 & Hz'1 & Hfz'1). +destruct H2 as (z'2 & Hz'2 & Hfz'2). +move z'2 before z'1; move Hz'2 before Hz'1. +assert (H3 : (Happ f' (z'1 - z'2) = Happ b (g₁ x1 - g₁ x2))%G). { + rewrite Hadditive; [ | easy | now apply A' ]. + rewrite Hadditive. + -apply gr_add_compat; [ apply Hfz'1 | ]. + rewrite Hopp; [ | easy ]. + rewrite Hopp; [ | apply Hg₁, Hx2 ]. + now rewrite Hfz'2. + -apply (g₁_in_B Hg₁), Hx1. + -apply B, (g₁_in_B Hg₁), Hx2. +} +assert (H4 : g₁ x1 - g₁ x2 ∈ Im f). { + apply sf. + split. + -apply B; [ apply (g₁_in_B Hg₁), Hx1 | apply B, (g₁_in_B Hg₁), Hx2 ]. + -rewrite Hadditive; [ | apply Hg₁, Hx1 | apply B, Hg₁, Hx2 ]. + rewrite Hopp; [ | apply Hg₁, Hx2 ]. + apply gr_sub_move_r. + now rewrite Hgy1, Hgy2, gr_add_0_l. +} +destruct H4 as (z & Hz & Hfz). +assert (H4 : (z'1 - z'2 = Happ a z)%G). { + apply (f'_is_inj sf'); [ | now apply a | ]. + -apply A'; [ easy | now apply A' ]. + -rewrite <- Hcff', H3. + apply b; [ | now symmetry ]. + apply B; [ apply (g₁_in_B Hg₁), Hx1 | apply B, (g₁_in_B Hg₁), Hx2 ]. +} +assert (H6 : z'1 - z'2 ∈ Im a). { + exists z; split; [ easy | now symmetry ]. +} +assert (Hdx2 : (d x2 = z'2)%G). { + simpl; unfold Coker_eq; simpl. + exists 0. + split; [ apply A | ]. + rewrite Hzero; symmetry. + apply gr_sub_move_r; symmetry. + rewrite gr_add_0_l. + apply (f'_is_inj sf'); [ easy | now apply Hf'₁; exists x2 | ]. + rewrite Hfz'2; symmetry. + now apply Hf'₁; exists x2. +} +assert (Hdx1 : (d x1 = z'1)%G). { + simpl; unfold Coker_eq; simpl. + exists 0. + split; [ apply A | ]. + rewrite Hzero; symmetry. + apply gr_sub_move_r; symmetry. + rewrite gr_add_0_l. + apply (f'_is_inj sf'); [ easy | now apply Hf'₁; exists x1 | ]. + rewrite Hfz'1. + now symmetry; apply Hf'₁; exists x1. +} +assert (Hzz' : @gr_eq (@Coker A A' a) z'1 z'2). { + destruct H6 as (zz & Hzz & Hazz). + simpl; unfold Coker_eq; simpl. + now exists zz; split. +} +now rewrite Hdx1, Hzz'; symmetry. +Qed. + +Theorem d_additive + {A A' B B' C C'} {f : HomGr A B} {g : HomGr B C} {f' : HomGr A' B'} + {a : HomGr A A'} {b : HomGr B B'} {c : HomGr C C'} {za' : HomGr Gr1 A'} + {g₁ f'₁} : + diagram_commutes f a b f' + → Im f == Ker g + → Im za' == Ker f' + → g₁_prop g c g₁ + → f'₁_prop a b f' g₁ f'₁ + → let d := λ x, f'₁ (Happ b (g₁ x)) in + ∀ x1 x2, x1 ∈ Ker c → x2 ∈ Ker c → (d (x1 + x2) = d x1 + d x2)%G. +Proof. +intros * Hcff' sf sf' Hg₁ Hf'₁ * Hx1 Hx2. +set (x3 := (x1 + x2)%G). +set (y1 := g₁ x1). +set (y2 := g₁ x2). +set (y3 := g₁ x3). +set (z1 := d x1). +set (z2 := d x2). +set (z3 := d x3). +assert (H1 : (Happ g y1 = x1)%G) by now apply Hg₁; simpl in Hx1. +assert (H2 : (Happ g y2 = x2)%G) by now apply Hg₁; simpl in Hx2. +assert (H3 : (Happ g (y1 + y2)%G = x3)%G). { + rewrite Hadditive; [ now rewrite H1, H2 | | ]. + -apply (g₁_in_B Hg₁), Hx1. + -apply (g₁_in_B Hg₁), Hx2. +} +assert (Hy1 : y1 ∈ B) by apply (g₁_in_B Hg₁), Hx1. +assert (Hy2 : y2 ∈ B) by apply (g₁_in_B Hg₁), Hx2. +assert (Hy3 : y3 ∈ B) by (apply (g₁_in_B Hg₁), C; [ apply Hx1 | apply Hx2 ]). +assert (H4 : (y1 + y2 - y3)%G ∈ Ker g). { + split; [ now apply B; apply B | ]. + rewrite Hadditive; [ | now apply B | now apply B ]. + symmetry; apply gr_sub_move_r. + rewrite gr_add_0_l, Hopp; [ | easy ]. + rewrite gr_opp_involutive, H3. + apply Hg₁, C; [ apply Hx1 | apply Hx2 ]. +} +assert (Hfx1 : (Happ f' z1 = Happ b y1)%G). { + now apply Hf'₁; exists x1. +} +assert (Hfx2 : (Happ f' z2 = Happ b y2)%G). { + now apply Hf'₁; exists x2. +} +assert (Hfx3 : (Happ f' z3 = Happ b y3)%G). { + unfold z3, y3. + apply Hf'₁. + exists x3. + split; [ now apply (Ker c)| easy ]. +} +assert + (Hfzzz : + (Happ f' (z1 + z2 - z3) = Happ b y1 + Happ b y2 - Happ b y3)%G). { + assert (Hz1A' : z1 ∈ A' ∧ z2 ∈ A' ∧ z3 ∈ A'). { + assert (H : z1 ∈ A' ∧ z2 ∈ A'). { + split. + -now apply Hf'₁; exists x1. + -now apply Hf'₁; exists x2. + } + split; [ easy | ]. + split; [ easy | ]. + unfold z3. + apply Hf'₁. + exists x3; split; [ now apply (Ker c) | easy ]. + } + simpl; rewrite Hadditive; [ | now apply A' | now apply A' ]. + apply gr_add_compat. + -rewrite Hadditive; [ now apply gr_add_compat | easy | easy ]. + -rewrite Hopp; [ now apply gr_opp_compat | easy ]. +} +apply sf in H4. +destruct H4 as (z & Hz & Hzf). +assert (Hfz : (Happ f' (z1 + z2 - z3) = Happ f' (Happ a z))%G). { + rewrite Hfzzz. + etransitivity. + -apply gr_add_compat; [ now symmetry; apply b | now symmetry; apply Hopp ]. + -rewrite <- Hadditive; [ | now apply B | now apply B ]. + rewrite <- Hcff'. + apply b; [ | now apply B; apply B ]. + rewrite <- Hzf. + now apply f. +} +apply (f'_is_inj sf') in Hfz; [ | | now apply a ]. +-simpl; unfold Coker_eq; simpl. + exists (- z). + split; [ now apply A | ]. + rewrite Hopp; [ | easy ]. + rewrite <- Hfz. + symmetry; rewrite gr_add_comm. + rewrite gr_opp_add_distr. + apply gr_eq_opp_l. + rewrite gr_opp_add_distr. + simpl; apply gr_add_compat; [ | easy ]. + rewrite gr_opp_add_distr. + now do 2 rewrite gr_opp_involutive. +-apply A'. + +apply A'; [ now apply Hf'₁; exists x1 | now apply Hf'₁; exists x2 ]. + +apply A'. + apply Hf'₁; exists x3. + split; [ now apply (Ker c) | easy ]. +Qed. + +(* Ker a → Ker b → Ker c *) + +Theorem exact_sequence_1 {A B C A' B' C'} : + ∀ (f : HomGr A B) (g : HomGr B C) (f' : HomGr A' B') (g' : HomGr B' C') + (a : HomGr A A') (b : HomGr B B') (c : HomGr C C') (za' : HomGr Gr1 A') + (Hcff' : diagram_commutes f a b f') (Hcgg' : diagram_commutes g b c g'), + Im f == Ker g + → Im za' == Ker f' + → Im (HomGr_Ker_Ker a b Hcff') == Ker (HomGr_Ker_Ker b c Hcgg'). +Proof. +intros * sf sf'. +split. ++intros y (x & (Hx & Hax) & Hxy). + split; [ split | ]. + *eapply B; [ apply Hxy | now apply f ]. + *transitivity (Happ b (Happ f x)). + --apply b; [ | now symmetry ]. + eapply gr_mem_compat; [ apply Hxy | now apply f ]. + --rewrite Hcff'. + transitivity (Happ f' (@gr_zero A')); [ | apply Hzero ]. + apply f'; [ now apply a | easy ]. + *now apply sf; exists x. ++intros y ((Hy & Hby) & Hgy). + assert (H : y ∈ Im f) by now apply sf; split. + destruct H as (x & Hx & Hxy). + exists x; split; [ | easy ]. + split; [ easy | ]. + specialize (proj2 sf' (Happ a x)) as H1. + assert (H3 : Happ a x ∈ Ker f'). { + split; [ now apply a | ]. + rewrite <- Hcff'. + transitivity (Happ b y); [ | easy ]. + apply b; [ now apply f | easy ]. + } + specialize (H1 H3). + destruct H1 as (z & _ & Hzz). + rewrite <- Hzz. + destruct z. + apply Hzero. +Qed. + +(* Ker b → Ker c → CoKer a *) + +Theorem exact_sequence_2 {A B C A' B' C'} : + ∀ (f : HomGr A B) (g : HomGr B C) (f' : HomGr A' B') (g' : HomGr B' C') + (a : HomGr A A') (b : HomGr B B') (c : HomGr C C') (za' : HomGr Gr1 A') + (g₁ : gr_set (Ker c) → gr_set B) (f'₁ : gr_set B' → gr_set (Coker a)) + (sf : Im f == Ker g) (sf' : Im za' == Ker f') + (Hcff' : diagram_commutes f a b f') + (Hcgg' : diagram_commutes g b c g') + (Hg₁ : g₁_prop g c g₁) (Hf'₁ : f'₁_prop a b f' g₁ f'₁), + let d := λ x : gr_set (Ker c), f'₁ (Happ b (g₁ x)) in + ∀ (dm : HomGr (Ker c) (Coker a)), Happ dm = d + → Im (HomGr_Ker_Ker b c Hcgg') == Ker dm. +Proof. +intros *. +intros sf sf' Hcff' Hcgg' Hg₁ Hf'₁ d. +intros * Hd. +split. +-intros x (y & (Hy & Hay) & Hyx). + split; [ split | ]. + +eapply C; [ apply Hyx | now apply g ]. + +specialize (Hcgg' y) as H1. + transitivity (Happ c (Happ g y)). + *eapply c; [ | now apply C ]. + eapply C; [ apply Hyx | now apply g ]. + *rewrite H1. + transitivity (Happ g' (@gr_zero B')); [ | apply Hzero ]. + apply g'; [ now apply b | easy ]. + +simpl in Hyx. + assert (Hgy : Happ g y ∈ Ker c). { + split; [ now apply g | ]. + rewrite Hcgg'. + etransitivity; [ | apply Hzero ]. + apply g'; [ now apply b | easy ]. + } + assert (Hxk : x ∈ Ker c). { + assert (Hx : x ∈ C). { + eapply gr_mem_compat; [ apply Hyx | now apply g ]. + } + split; [ easy | ]. + etransitivity; [ | apply Hgy ]. + apply c; [ easy | now symmetry ]. + } + assert (Hyk : g₁ x - y ∈ Ker g). { + split. + -apply B; [ apply (g₁_in_B Hg₁), Hxk | now apply B ]. + -rewrite Hadditive; [ | apply (g₁_in_B Hg₁), Hxk | now apply B ]. + etransitivity. + *apply gr_add_compat; [ apply Hg₁, Hxk | ]. + now simpl; apply Hopp. + *apply gr_sub_move_r; rewrite <- Hyx. + symmetry; apply gr_add_0_l. + } + apply sf in Hyk. + destruct Hyk as (z & Hz & Haz). + assert (Hdx : (d x = Happ a z)%G). { + apply (f'c_is_inj sf'); [ | now apply a | ]. + -now apply (d_mem_compat Hf'₁). + -etransitivity; [ apply Hf'₁; now exists x | ]. + rewrite <- Hcff'; symmetry. + etransitivity. + +apply Happ_compat; [ apply Hmem_compat, Hz | apply Haz ]. + +rewrite Hadditive; [ | apply (g₁_in_B Hg₁), Hxk | now apply B ]. + etransitivity. + *apply gr_add_compat; [ easy | now simpl; apply Hopp ]. + *etransitivity. + --apply gr_add_compat; [ easy | apply gr_opp_compat, Hay ]. + --rewrite gr_sub_0_r. + apply b; [ apply (g₁_in_B Hg₁), Hxk | easy ]. + } + rewrite Hd. + simpl; rewrite Hdx. + exists z; split; [ easy | ]. + now simpl; rewrite gr_sub_0_r. +-intros x (Hx & z & Hz & Haz). + rewrite Hd in Haz. + simpl in x, Haz. + move z before x; move Hz before Hx. + rewrite gr_sub_0_r in Haz. + enough (∃ y, (y ∈ B ∧ (Happ b y = 0)%G) ∧ (Happ g y = x)%G) by easy. + apply (Happ_compat _ _ f') in Haz; [ | now apply a ]. + rewrite <- Hcff' in Haz. + exists (g₁ x - Happ f z). + split; [ split | ]. + +apply B; [ apply Hg₁, Hx | now apply B, f ]. + +rewrite Hadditive; [ | apply Hg₁, Hx | now apply B, f ]. + etransitivity. + *apply gr_add_compat; [ easy | now apply Hopp, f ]. + *apply gr_sub_move_r; rewrite gr_add_0_l; symmetry. + now rewrite Haz; apply Hf'₁; exists x. + +rewrite Hadditive; [ | apply Hg₁, Hx | now apply B, f ]. + *etransitivity. + --apply gr_add_compat; [ easy | now apply Hopp, f ]. + --apply gr_sub_move_l. + etransitivity; [ apply Hg₁, Hx | ]. + rewrite <- gr_add_0_l at 1. + apply gr_add_compat; [ | easy ]. + enough (H1 : Happ f z ∈ Ker g) by now simpl in H1. + now apply sf; exists z. +Qed. + +Theorem exact_sequence_3 {A B C A' B' C'} : + ∀ (f : HomGr A B) (g : HomGr B C) (f' : HomGr A' B') (g' : HomGr B' C') + (a : HomGr A A') (b : HomGr B B') (c : HomGr C C') (za' : HomGr Gr1 A') + (Hcff' : diagram_commutes f a b f') + (Hcgg' : diagram_commutes g b c g') + (sf : Im f == Ker g) (sf' : Im za' == Ker f') (sg' : Im f' == Ker g') + (g₁ : gr_set (Ker c) → gr_set B) + (f'₁ : gr_set B' → gr_set (Coker a)) + (Hg₁ : g₁_prop g c g₁) + (Hf'₁ : f'₁_prop a b f' g₁ f'₁), + let d := λ x : gr_set (Ker c), f'₁ (Happ b (g₁ x)) in + ∀ (dm : HomGr (Ker c) (Coker a)), Happ dm = d → + Im dm == Ker (HomGr_Coker_Coker a b Hcff'). +Proof. +intros *. +intros Hcgg' sf sf' sg' * Hg₁ Hf'₁ * Hdm. +split. +-intros z' Hz'. + destruct Hz' as (x & Hx & z & Hz & Haz). + move z before x. + rewrite Hdm in Haz. + simpl in Haz. + assert (Hz' : z' ∈ A'). { + apply gr_mem_compat with (x := d x - Happ a z). + -transitivity (d x - (d x - z')); simpl. + +apply gr_add_compat; [ easy | now apply gr_opp_compat ]. + +apply gr_sub_move_l. + rewrite gr_add_assoc; symmetry. + etransitivity; [ | apply gr_add_0_r ]. + apply gr_add_compat; [ easy | ]. + apply gr_add_opp_l. + -apply A'; [ now apply Hf'₁; exists x | now apply A', a ]. + } + simpl; split; [ easy | ]. + unfold Coker_eq; simpl. + enough (H : ∃ y, y ∈ B ∧ (Happ b y = Happ f' z')%G). { + destruct H as (y & Hy & Hby). + exists y. + split; [ easy | now rewrite gr_sub_0_r ]. + } + simpl in z'. + exists (g₁ x - Happ f z). + split. + +apply B; [ apply Hg₁, Hx | now apply B, f ]. + +apply (Happ_compat _ _ f') in Haz; [ | now apply a ]. + rewrite Hadditive; [ | apply Hg₁, Hx | now apply B, f ]. + etransitivity. + *apply gr_add_compat; [ easy | now apply Hopp, f ]. + *etransitivity. + --apply gr_add_compat; [ easy | ]. + apply gr_opp_compat, Hcff'. + --apply gr_sub_move_r. + etransitivity; [ now symmetry; apply Hf'₁; exists x | ]. + fold (d x). + apply gr_sub_move_l. + etransitivity. + ++apply gr_add_compat; [ easy | now symmetry; apply Hopp ]. + ++rewrite <- Hadditive; [ now symmetry | | now apply A' ]. + now apply Hf'₁; exists x. +-intros z' (Hz' & y & Hy & Hby). + simpl in z', Hz', Hby. + rewrite gr_sub_0_r in Hby. + simpl; unfold Coker_eq; simpl. + rewrite Hdm. + enough (H : + ∃ x, x ∈ C ∧ (Happ c x = 0)%G ∧ + ∃ z, z ∈ A ∧ (Happ a z = d x - z')%G). { + destruct H as (x & Hx). + now exists x. + } + exists (Happ g y). + split; [ now apply g | ]. + split. + +rewrite Hcgg'. + etransitivity. + *apply Happ_compat; [ now apply b | apply Hby ]. + *assert (H : Happ f' z' ∈ Im f') by now exists z'. + now apply sg' in H; simpl in H. + +assert (H : g₁ (Happ g y) - y ∈ Ker g). { + split. + -apply B; [ now apply Hg₁, g | now apply B ]. + -rewrite Hadditive; [ | now apply Hg₁, g | now apply B ]. + rewrite <- gr_add_opp_r. + apply gr_add_compat; [ now apply Hg₁, g | now apply Hopp ]. + } + apply sf in H. + destruct H as (z & Hz & Hfz). + exists z; split; [ easy | ]. + apply (Happ_compat _ _ b) in Hfz; [ | now apply f ]. + rewrite Hadditive in Hfz; [ | now apply Hg₁, g | now apply B ]. + rewrite Hcff' in Hfz. + *apply (f'_is_inj sf'); [ now apply a | | ]. + --apply A'; [ | now apply A' ]. + apply Hf'₁. + exists (Happ g y); split; [ | easy ]. + split; [ now apply g | ]. + rewrite Hcgg'. + etransitivity. + ++apply Happ_compat; [ now apply b | apply Hby ]. + ++assert (H : Happ f' z' ∈ Im f') by (exists z'; easy). + now apply sg' in H; simpl in H. + --rewrite Hfz. + symmetry; simpl; rewrite Hadditive; [ | | now apply A' ]. + ++apply gr_add_compat. + **apply Hf'₁. + exists (Happ g y); split; [ | easy ]. + split; [ now apply g | ]. + rewrite Hcgg'. + etransitivity. + ---apply Happ_compat; [ now apply b | apply Hby ]. + ---assert (H : Happ f' z' ∈ Im f') by (exists z'; easy). + now apply sg' in H; simpl in H. + **rewrite Hopp; [ | easy ]. + rewrite Hopp; [ | easy ]. + apply gr_opp_compat. + now symmetry. + ++apply Hf'₁; exists (Happ g y); split; [ | easy ]. + split; [ now apply g | ]. + rewrite Hcgg'. + etransitivity. + **apply Happ_compat; [ now apply b | apply Hby ]. + **assert (H : Happ f' z' ∈ Im f') by (exists z'; easy). + now apply sg' in H; simpl in H. +Qed. + +Theorem exact_sequence_4 {A B C A' B' C'} : + ∀ (f : HomGr A B) (g : HomGr B C) (f' : HomGr A' B') (g' : HomGr B' C') + (a : HomGr A A') (b : HomGr B B') (c : HomGr C C') + (Hcff' : diagram_commutes f a b f') + (Hcgg' : diagram_commutes g b c g') + (sg' : Im f' == Ker g') + (g₁ : gr_set (Ker c) → gr_set B) + (Hg₁ : g₁_prop g c g₁), + Im (HomGr_Coker_Coker a b Hcff') == Ker (HomGr_Coker_Coker b c Hcgg'). +Proof. +intros. +split. +-simpl. + intros y' (z' & Hz' & y & Hy & Hby). + simpl in Hby. + assert (Hb' : y' ∈ B'). { + symmetry in Hby. + apply gr_sub_move_r in Hby. + rewrite gr_add_comm in Hby. + apply gr_sub_move_r in Hby. + rewrite <- Hby. + apply B'; [ now apply f' | now apply B', b ]. + } + split; [ easy | ]. + unfold Coker_eq; simpl. + enough (H : ∃ x, x ∈ C ∧ (Happ c x = Happ g' y')%G). { + destruct H as (x & Hx & Hcx). + exists x; split; [ easy | ]. + rewrite Hcx; symmetry. + apply gr_sub_0_r. + } + exists (- Happ g y). + split; [ now apply C, g | ]. + rewrite Hopp, Hcgg'; [ | now apply g ]. + apply gr_eq_opp_l. + rewrite <- Hopp; [ | easy ]. + symmetry. + transitivity (Happ g' (Happ f' z' - y')). + +rewrite Hadditive; [ | now apply f' | now apply B' ]. + rewrite <- gr_add_0_l at 1. + apply gr_add_compat; [ | easy ]. + symmetry. + assert (H : Happ f' z' ∈ Im f') by (exists z'; easy). + now apply sg' in H; simpl in H. + +apply g'; [ | now symmetry ]. + apply B'; [ now apply f' | now apply B' ]. +-simpl; intros y' (Hy' & x & Hx & Hcx). + simpl in Hcx; rewrite gr_sub_0_r in Hcx. + unfold Coker_eq; simpl. + enough (H : ∃ y z', y ∈ B ∧ z' ∈ A' ∧ (Happ b y = Happ f' z' - y')%G). { + destruct H as (y & z' & Hz' & Hy & Hby). + exists z'; split; [ easy | ]. + now exists y. + } + assert (Hby : y' - Happ b (g₁ x) ∈ Ker g'). { + split. + -apply B'; [ easy | now apply B', b, Hg₁ ]. + -rewrite Hadditive; [ | easy | now apply B', b, Hg₁ ]. + rewrite <- Hcx, Hopp; [ | now apply b, Hg₁ ]. + rewrite <- Hcgg'. + etransitivity; [ | apply gr_add_opp_r ]. + apply gr_add_compat; [ easy | ]. + apply gr_opp_compat. + apply Happ_compat; [ now apply g, Hg₁ | now apply Hg₁ ]. + } + apply sg' in Hby. + destruct Hby as (z' & Hz' & Hfz'). + exists (- g₁ x), z'. + split; [ now apply B, Hg₁ | ]. + split; [ easy | ]. + rewrite Hfz', gr_add_comm, <- gr_add_assoc, gr_add_opp_l, gr_add_0_l. + now apply Hopp, Hg₁. +Qed. + +(* + f g cz + A------>B------>C------>0 + | | | + a| b| c| + | | | + v v v + 0----->A'----->B'----->C' + za' f' g' + + If the diagram is commutative, + and (f, g, cz) and (za', f', g') are exact sequences, + Then + there exists a morphism d from Ker c to Coker a, such that + Ker a→Ker b→Ker c→Coker a→Coker b→Coker c is an exact sequence. +*) + +Lemma snake : + ∀ (A B C A' B' C' : AbGroup) + (f : HomGr A B) (g : HomGr B C) + (f' : HomGr A' B') (g' : HomGr B' C') + (a : HomGr A A') (b : HomGr B B') (c : HomGr C C') + (cz : HomGr C Gr1) (za' : HomGr Gr1 A'), + Decidable_Membership * Choice + → diagram_commutes f a b f' + → diagram_commutes g b c g' + → exact_sequence [f; g; cz] + → exact_sequence [za'; f'; g'] + → ∃ (fk : HomGr (Ker a) (Ker b)) (gk : HomGr (Ker b) (Ker c)) + (fk' : HomGr (Coker a) (Coker b)) (gk' : HomGr (Coker b) (Coker c)), + ∃ (d : HomGr (Ker c) (Coker a)), + exact_sequence (Seq fk (Seq gk (Seq d (Seq fk' (Seq gk' SeqEnd))))). +Proof. +intros *. +intros (mem_dec, choice) Hcff' Hcgg' s s'. +exists (HomGr_Ker_Ker a b Hcff'). +exists (HomGr_Ker_Ker b c Hcgg'). +exists (HomGr_Coker_Coker a b Hcff'). +exists (HomGr_Coker_Coker b c Hcgg'). +destruct s as (sf & sg & _). +destruct s' as (sf' & sg' & _). +specialize (g_is_surj c mem_dec sg) as H1. +specialize (choice _ _ _ H1) as H; destruct H as (g₁, Hg₁). +specialize (exists_B'_to_Coker_a a mem_dec sg' Hg₁ Hcgg') as H2. +specialize (choice _ _ _ H2) as H; destruct H as (f'₁, Hf'₁). +fold (g₁_prop g c g₁) in Hg₁. +fold (f'₁_prop a b f' g₁ f'₁) in Hf'₁. +move f'₁ before g₁. +clear H1 H2. +set (d := λ x, f'₁ (Happ b (g₁ x))). +set + (dm := + {| Happ := d; + Hmem_compat := d_mem_compat Hf'₁; + Happ_compat := d_app_compat Hcff' Hcgg' sf sf' sg' Hg₁ Hf'₁; + Hadditive := d_additive Hcff' sf sf' Hg₁ Hf'₁ |}). +exists dm. +split; [ now eapply exact_sequence_1 | ]. +split; [ now eapply exact_sequence_2; try easy | ]. +split; [ now eapply exact_sequence_3; try easy | ]. +split; [ eapply exact_sequence_4; try easy; apply Hg₁ | easy ]. +Qed. + +Check snake. |