diff options
Diffstat (limited to 'abgroup.v')
| -rw-r--r-- | abgroup.v | 719 |
1 files changed, 719 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}. + |