Lemmas on Epic and Monic for Exercise of Category Theory.

EpicMonicExercise.v

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.