src/EpicMonic_ch2_1.v

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