Instantly share code, notes, and snippets.

# gusmachine/EpicMonicExercise.v Created May 9, 2011

What would you like to do?
Lemmas on Epic and Monic for Exercise of Category Theory.
 Require Export ConCaT.SETOID.Setoid. Require Export ConCaT.CATEGORY_THEORY.CATEGORY.Category. Require Export ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.CatProperty. Set Implicit Arguments. Unset Strict Implicit. Variables C: Category. (* Compositions of epic/monic are also epic/monic. *) (* Useful Lemma not defined in CatProperty *) Lemma ByEpic : forall (a b c:C) (epic_type: Epic a b) (f g: b --> c), Epic_mor epic_type o f =_S Epic_mor epic_type o g -> f =_S g. Proof. intros. assert (HEp1: Epic_mor epic_type o f =_S Epic_mor epic_type o g -> f =_S g) by apply Prf_isEpic. auto. Qed. Lemma ByMonic : forall (a b c:C) (monic_type: Monic a b) (f g: c --> b), f o Monic_mor monic_type =_S g o Monic_mor monic_type -> f =_S g. Proof. intros. assert (HMo1: f o Monic_mor monic_type =_S g o Monic_mor monic_type-> f =_S g) by apply Prf_isMonic. auto. Qed. Section epic_composition. Variables (a b c: C) (epic_type_ab: Epic a b) (epic_type_bc: Epic b c). Let ep_morph_ab := Epic_mor epic_type_ab. Let ep_morph_bc := Epic_mor epic_type_bc. Lemma Epic_law_composed: Epic_law (ep_morph_ab o ep_morph_bc). Proof. unfold Epic_law. intros d g h H1. apply ByEpic with (epic_type := epic_type_bc). fold ep_morph_bc. apply ByEpic with (epic_type := epic_type_ab). fold ep_morph_ab. apply Trans with (y := (ep_morph_ab o ep_morph_bc) o h). (* Trans 1: ep_morph_ab o ep_morph_bc o g =_S (ep_morph_ab o ep_morph_bc) o h *) apply Trans with (y := (ep_morph_ab o ep_morph_bc) o g). apply Ass. exact H1. (* Trans 2: ep_morph_ab o ep_morph_bc) o h =_S ep_morph_ab o ep_morph_bc o h *) apply Ass1. Qed. Canonical Structure Epic_Composed := Build_Epic Epic_law_composed. End epic_composition. Section monic_composition. Variables (a b c: C) (monic_type_ab: Monic a b) (monic_type_bc: Monic b c). Let mo_morph_ab := Monic_mor monic_type_ab. Let mo_morph_bc := Monic_mor monic_type_bc. Lemma Monic_law_composed: Monic_law (mo_morph_bc o mo_morph_ab). Proof. unfold Monic_law. intros d g h H1. apply ByMonic with (monic_type := monic_type_bc). fold mo_morph_bc. apply ByMonic with (monic_type := monic_type_ab). fold mo_morph_ab. apply Trans with (y := g o mo_morph_bc o mo_morph_ab). (* Trans1: (g o mo_morph_bc) o mo_morph_ab =_S g o mo_morph_bc o mo_morph ab *) apply Ass1. (* Trans2: g o mo_morph_bc o mo_morph_ab =_S (h o mo_morph_bc) o mo_morph_ab) *) apply Trans with (y := h o mo_morph_bc o mo_morph_ab). exact H1. apply Ass. Qed. Canonical Structure Monic_Composed := Build_Monic Monic_law_composed. End monic_composition. (* If f ; g is epic, so is g. *) Section Part_Epic. Variables (a b c: C) (f: a --> b) (g: b --> c). Lemma Part_Epic: Epic_law (f o g) -> Epic_law g. Proof. unfold Epic_law. intros HEp_composed d h0 h1 HEp_g. apply HEp_composed. apply Trans with (y := f o g o h0). apply Ass1. apply Trans with (y := f o g o h1). apply Comp_l. apply HEp_g. apply Ass. Qed. (* Canonical Structure Epic_From_Part := Build_Epic Part_Epic. *) End Part_Epic. (* If f ; g is monic, so is f. *) Section Part_Monic. Variables (a b c: C) (f: a --> b) (g: b --> c). Lemma Part_Monic: Monic_law (f o g) -> Monic_law f. Proof. unfold Monic_law. intros HMo_composed d h0 h1 HMo_f. apply HMo_composed. apply Trans with (y := (h0 o f) o g). apply Ass. apply Trans with (y := (h1 o f) o g). apply Comp_r. apply HMo_f. apply Ass1. Qed. End Part_Monic.