Library CategoryMorphisms


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category.
Require Import Notations.

Set Implicit Arguments.

Generalizable All Variables.

Category Morphisms

Section category_morphisms.
  Context `(C : @Category obj).

  Local Open Scope morphism_scope.

Quoting Wikipedia,
In category theory, an epimorphism (also called an epic morphism or, colloquially, an epi) is a morphism f : X Y which is right-cancellative in the sense that, for all morphisms g, g' : Y Z, g f = g' f g = g'
Epimorphisms are analogues of surjective functions, but they are not exactly the same. The dual of an epimorphism is a monomorphism (i.e. an epimorphism in a category C is a monomorphism in the dual category C op).

  Definition IsEpimorphism x y (m : C.(Morphism) x y) : Prop :=
     z (m1 m2 : C.(Morphism) y z), m1 m = m2 m
      m1 = m2.
  Definition IsMonomorphism x y (m : C.(Morphism) x y) : Prop :=
     z (m1 m2 : C.(Morphism) z x), m m1 = m m2
      m1 = m2.

  Section properties.
    Lemma IdentityIsEpimorphism x : IsEpimorphism _ _ (Identity x).
      repeat intro; autorewrite with category in *; trivial.
    Qed.

    Lemma IdentityIsMonomorphism x : IsMonomorphism _ _ (Identity x).
      repeat intro; autorewrite with category in *; trivial.
    Qed.

    Lemma EpimorphismComposition s d d' m0 m1 :
      IsEpimorphism _ _ m0
      → IsEpimorphism _ _ m1
      → IsEpimorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
      repeat intro.
      repeat match goal with | [ H : _ |- _ ] ⇒ rewrite <- Associativity in H end.
      intuition.
    Qed.

    Lemma MonomorphismComposition s d d' m0 m1 :
      IsMonomorphism _ _ m0
      → IsMonomorphism _ _ m1
      → IsMonomorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
      repeat intro.
      repeat match goal with | [ H : _ |- _ ] ⇒ rewrite Associativity in H end.
      intuition.
    Qed.
  End properties.
End category_morphisms.

Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : category.
Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : morphism.

Arguments IsEpimorphism {obj} [C x y] m.
Arguments IsMonomorphism {obj} [C x y] m.

Section AssociativityComposition.
  Context `(C : @Category obj).
  Variables o0 o1 o2 o3 o4 : C.

  Local Open Scope morphism_scope.

  Lemma compose4associativity_helper
        (a : Morphism C o3 o4) (b : Morphism C o2 o3)
        (c : Morphism C o1 o2) (d : Morphism C o0 o1) :
    (a b) (c d) = a ((b c) d).
    repeat rewrite Associativity; reflexivity.
  Qed.
End AssociativityComposition.

Ltac compose4associativity' a b c d :=
  transitivity (a ((b c) d))%morphism;
  try solve [ apply compose4associativity_helper ].
Ltac compose4associativity :=
  match goal with
    | [ |- ((?a ?b) (?c ?d))%morphism = _ ] ⇒ compose4associativity' a b c d
    | [ |- _ = ((?a ?b) (?c ?d))%morphism ] ⇒ compose4associativity' a b c d
  end.