Create a gist now

Instantly share code, notes, and snippets.

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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment