src/EpicMonic_ch2_1.v

   1 Generalizable All Variables.
   2 Require Import Notations.
   3 Require Import Categories_ch1_3.
   4 Require Import Functors_ch1_4.
   5 Require Import Isomorphisms_ch1_5.
   6
   7 (******************************************************************************)
   8 (* Chapter 2.1: Epic and Monic morphisms                                      *)
   9 (******************************************************************************)
  10
  11 (* Definition 2.1a *)
  12 Class Monic `{C:Category}{a b:C}(f:a~>b) : Prop :=
  13   monic : forall c (g1 g2:c~>a), g1>>>f ~~ g2>>>f -> g1~~g2.
  14 Implicit Arguments monic [ C a b Ob Hom ].
  15
  16 (* Definition 2.1b *)
  17 Class Epic `{C:Category}{a b:C}(f:a~>b) : Prop :=
  18   epic : forall c (g1 g2:b~>c), f>>>g1 ~~ f>>>g2 -> g1~~g2.
  19 Implicit Arguments epic [ C a b Ob Hom ].
  20
  21 (* Proposition 2.6 *)
  22 Instance iso_epic `(i:Isomorphic) : Epic #i.
  23   simpl; unfold Epic; intros.
  24   setoid_rewrite <- left_identity.
  25   setoid_rewrite <- iso_comp2.
  26   setoid_rewrite associativity.
  27   setoid_rewrite H; reflexivity.
  28   Qed.
  29
  30 (* Proposition 2.6 *)
  31 Instance iso_monic `(i:Isomorphic) : Monic #i.
  32   simpl; unfold Monic; intros.
  33   setoid_rewrite <- right_identity.
  34   setoid_rewrite <- iso_comp1.
  35   setoid_rewrite <- associativity.
  36   setoid_rewrite H; reflexivity.
  37   Qed.
  38
  39 (* a BiMorphism is an epic monic *)
  40 Class BiMorphism `{C:Category}{a b:C}(f:a~>b) : Prop :=
  41 { bimorphism_epic  :> Epic  f
  42 ; bimorphism_monic :> Monic f
  43 }.
  44 Coercion bimorphism_epic  : BiMorphism >-> Epic.
  45 Coercion bimorphism_monic : BiMorphism >-> Monic.
  46
  47 Class EndoMorphism `{C:Category}(A:C) :=
  48   endo : A ~> A.
  49
  50 Class AutoMorphism `{C:Category}(A:C) : Type :=
  51 { auto_endo1 : EndoMorphism A
  52 ; auto_endo2 : EndoMorphism A
  53 ; auto_iso   : Isomorphism  (@endo _ _ _ _ auto_endo1) (@endo _ _ _ _ auto_endo2)
  54 }.
  55
  56 (*Class Balanced `{C:Category} : Prop :=
  57   balanced : forall (a b:C)(f:a~>b), BiMorphism f -> Isomorphism f.*)
  58