Library CategoryIsomorphisms


Require Import Setoid Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import Classes.RelationClasses Morphisms.
Require Export Category CategoryMorphisms.
Require Import Notations Common.

Set Implicit Arguments.

Generalizable All Variables.

Category Isomorphisms


Section category_isomorphisms.
  Context `(C : @Category obj).
  Local Open Scope morphism_scope.

  Definition IsInverseOf1 s d (m : C.(Morphism) s d) (m' : C.(Morphism) d s) : Prop
    := m' m = Identity s.
  Definition IsInverseOf2 s d (m : C.(Morphism) s d) (m' : C.(Morphism) d s) : Prop
    := m m' = Identity d.

  Global Arguments IsInverseOf1 / _ _ _ _.
  Global Arguments IsInverseOf2 / _ _ _ _.

  Definition IsInverseOf {s d} (m : C.(Morphism) s d) (m' : C.(Morphism) d s) : Prop
    := Eval simpl in @IsInverseOf1 s d m m' @IsInverseOf2 s d m m'.

  Lemma IsInverseOf_sym s d m m' : @IsInverseOf s d m m' → @IsInverseOf d s m' m.
    firstorder.
  Qed.

  Section IsomorphismOf.
    Record IsomorphismOf {s d : C} (m : C.(Morphism) s d) :=
      {
        IsomorphismOf_Morphism :> C.(Morphism) s d := m;
        Inverse : C.(Morphism) d s;
        LeftInverse : Inverse m = Identity s;
        RightInverse : m Inverse = Identity d
      }.

    Existing Class IsomorphismOf.

    Hint Resolve RightInverse LeftInverse : category.
    Hint Resolve RightInverse LeftInverse : morphism.

    Definition IsomorphismOf_sig2 {s d} (m : C.(Morphism) s d) (i : IsomorphismOf m)
    : { m' | m' m = Identity s & m m' = Identity d }.
       (Inverse i);
      [ apply LeftInverse | apply RightInverse ].
    Defined.

    Definition IsomorphismOf_sig {s d : C} (m : C.(Morphism) s d)
      := { m' | m' m = Identity s & m m' = Identity d }.

    Global Identity Coercion Isomorphism_sig : IsomorphismOf_sig >-> sig2.

    Global Instance sig2_IsomorphismOf {s d : C}
           (m : C.(Morphism) s d)
           (i : IsomorphismOf_sig m)
    : @IsomorphismOf s d m.
    Proof.
       (proj1_sig i);
      [ apply (proj2_sig i) | apply (proj3_sig i) ].
    Defined.

    Global Coercion IsomorphismOf_sig2 : IsomorphismOf >-> sig2.
    Global Coercion sig2_IsomorphismOf : IsomorphismOf_sig >-> IsomorphismOf.

    Global Instance IsomorphismOf_Identity (c : C) : IsomorphismOf (Identity c).
    Proof.
       (Identity _); auto with morphism.
    Defined.

    Global Instance InverseOf {s d : C} (m : C.(Morphism) s d) (i : IsomorphismOf m)
    : IsomorphismOf (Inverse i).
    Proof.
       (i : Morphism C _ _); auto with morphism.
    Defined.

    Global Instance ComposeIsomorphismOf {s d d'}
           {m1 : C.(Morphism) d d'}
           {m2 : C.(Morphism) s d}
           (i1 : IsomorphismOf m1)
           (i2 : IsomorphismOf m2)
    : IsomorphismOf (m1 m2).
    Proof.
       (Inverse i2 Inverse i1);
      abstract (
          simpl; compose4associativity;
          destruct i1, i2; simpl;
          repeat (rewrite_hyp; autorewrite with morphism);
          trivial
        ).
    Defined.
  End IsomorphismOf.

  Section Isomorphism.
    Record Isomorphism (s d : C) :=
      {
        Isomorphism_Morphism : C.(Morphism) s d;
        Isomorphism_Of :> IsomorphismOf Isomorphism_Morphism
      }.

    Global Existing Instance Isomorphism_Of.

    Global Coercion Build_Isomorphism : IsomorphismOf >-> Isomorphism.
  End Isomorphism.

  Infix "≅" := (Isomorphism) (at level 70) : category_scope.
  Infix "≅" := (Isomorphism) (at level 70) : type_scope.

  Section IsIsomorphism.
    Definition IsIsomorphism {s d : C} (m : C.(Morphism) s d) : Prop :=
       m', IsInverseOf m m'.

    Lemma IsomrphismOf_IsIsomorphism {s d : C} (m : C.(Morphism) s d)
    : IsomorphismOf m
      → IsIsomorphism m.
      intro i; hnf.
       (Inverse i);
        destruct i; simpl;
        split;
        assumption.
    Qed.

    Lemma IsIsomorphism_IsomorphismOf {s d : C} (m : C.(Morphism) s d)
    : IsIsomorphism m _ : IsomorphismOf m, True.
      intros [ ? [ ? ? ] ].
      repeat esplit; eassumption.
    Qed.
  End IsIsomorphism.

  Section Isomorphic.
    Definition Isomorphic (s d : C) : Prop :=
       (m : C.(Morphism) s d) (m' : C.(Morphism) d s), IsInverseOf m m'.

    Local Infix "≅" := (Isomorphic) (at level 70).
    Local Infix "≅" := (Isomorphic) (at level 70) : type_scope.

    Lemma Isomrphism_Isomorphic s d : Isomorphism s ds d.
      intro i; destruct i as [ m i ].
       m.
      apply IsomrphismOf_IsIsomorphism; assumption.
    Qed.

    Lemma Isomorphic_Isomorphism s d : s d _ : Isomorphism s d, True.
      intros [ ? [ ? [ ? ? ] ] ];
      repeat esplit; eassumption.
    Qed.

    Local Ltac t_iso' := intros;
      repeat match goal with
               | [ i : Isomorphic _ _ |- _ ] ⇒
                 destruct (Isomorphic_Isomorphism i) as [ ? [] ] ; clear i
               | [ |- Isomorphic _ _ ] ⇒
                 apply Isomrphism_Isomorphic
             end.

    Local Ltac t_iso:= t_iso';
      repeat match goal with
               | [ i : Isomorphism _ _ |- _ ] ⇒ unique_pose (Isomorphism_Of i);
                                                try clear i
               | [ |- Isomorphism _ _ ] ⇒ eapply Build_Isomorphism
             end.

    Hint Resolve @IsomorphismOf_Identity @InverseOf
         @ComposeIsomorphismOf : category.
    Hint Resolve @IsomorphismOf_Identity @InverseOf
         @ComposeIsomorphismOf : morphism.
    Local Hint Extern 1 ⇒ eassumption.

    Lemma Isomorphic_refl c : c c.
      t_iso.
      apply IsomorphismOf_Identity.
    Qed.

    Lemma Isomorphic_sym s d : s dd s.
      t_iso.
      eauto with morphism.
    Qed.

    Lemma Isomorphic_trans s d d' : s dd d's d'.
      t_iso.
      apply @ComposeIsomorphismOf;
        eauto with morphism.
    Qed.

    Global Add Parametric Relation : _ Isomorphic
      reflexivity proved by Isomorphic_refl
      symmetry proved by Isomorphic_sym
      transitivity proved by Isomorphic_trans
        as Isomorphic_rel.
  End Isomorphic.

  Lemma iso_is_epi s d (m : _ s d) : IsIsomorphism mIsEpimorphism (C := C) m.
    destruct 1 as [ x [ i0 i1 ] ]; intros z m1 m2 e.
    transitivity (m1 (m x)); [ rewrite_hyp; autorewrite with morphism | ];
    trivial.
    transitivity (m2 (m x)); [ repeat rewrite <- Associativity | ];
    rewrite_hyp; autorewrite with morphism; trivial.
  Qed.

  Lemma iso_is_mono s d (m : _ s d) : IsIsomorphism mIsMonomorphism (C := C) m.
    destruct 1 as [ x [ i0 i1 ] ]; intros z m1 m2 e.
    transitivity ((x m) m1); [ rewrite_hyp; autorewrite with morphism | ];
    trivial.
    transitivity ((x m) m2); [ repeat rewrite Associativity | ];
    rewrite_hyp; autorewrite with morphism; trivial.
  Qed.
End category_isomorphisms.

Section identity_composition_lemmas.
  Context `(C : @Category objC).

  Local Open Scope morphism_scope.

  Lemma pre_compose_identity
        a b c
        (x : Morphism C a b)
        (y : Morphism C b a)
        (z : Morphism C _ _)
        (w : Morphism C c a)
        (H : y x = Identity _)
  : z = x wy z = w.
    intro H1.
    subst.
    rewrite <- Associativity.
    rewrite H.
    autorewrite with morphism.
    reflexivity.
  Qed.

  Lemma post_compose_identity
        a b c
        (x : Morphism C a b)
        (y : Morphism C b a)
        (z : Morphism C _ _)
        (w : Morphism C b c)
        (H : x y = Identity _)
  : z = w xz y = w.
    intro H1.
    subst.
    rewrite Associativity.
    rewrite H.
    autorewrite with morphism.
    reflexivity.
  Qed.

  Corollary pre_compose_identity2
            a b
            (x : Morphism C a b)
            (y : Morphism C b a)
            (z : Morphism C _ _)
            (H : y x = Identity _)
  : z = xy z = Identity _.
  intros; subst; assumption.
  Qed.

  Corollary post_compose_identity2
            a b
            (x : Morphism C a b)
            (y : Morphism C b a)
            (z : Morphism C _ _)
            (H : x y = Identity _)
  : z = xz y = Identity _.
  intros; subst; assumption.
  Qed.
End identity_composition_lemmas.

Hint Resolve @RightInverse @LeftInverse
     @IsomorphismOf_Identity @ComposeIsomorphismOf : category.
Hint Resolve @RightInverse @LeftInverse
     @IsomorphismOf_Identity @ComposeIsomorphismOf : morphism.

Notation "i -1" := (Inverse i) : morphism_scope.


Infix "≅" := (@Isomorphism _ _) : category_scope.

Arguments IsomorphismOf {_ C} [s d] m.
Arguments IsIsomorphism {_ C} [s d] m.

Ltac eapply_by_compose H :=
  match goal with
    | [ |- @eq (@Morphism ?obj ?mor ?C) _ _ ] ⇒ eapply (H obj mor C)
    | [ |- @Compose ?obj ?mor ?C _ _ _ _ _ = _ ] ⇒ eapply (H obj mor C)
    | [ |- _ = @Compose ?obj ?mor ?C _ _ _ _ _ ] ⇒ eapply (H obj mor C)
    | _eapply H
    | [ C : @Category ?obj ?mor |- _ ] ⇒ eapply (H obj mor C)
    | [ C : ?T |- _ ] ⇒ match eval hnf in T with | @Category ?obj ?moreapply (H obj mor C) end
  end.

Ltac solve_isomorphism := destruct_hypotheses;
  solve [ eauto ] ||
    match goal with
      | [ _ : Compose ?x ?x' = Identity _ |- IsIsomorphism ?x ] ⇒ solve [ x'; hnf; eauto ]
      | [ _ : Compose ?x ?x' = Identity _ |- Isomorphism ?x ] ⇒ solve [ x'; hnf; eauto ]
      | [ _ : Compose ?x ?x' = Identity _ |- IsomorphismOf ?x ] ⇒ solve [ x'; hnf; eauto ]
      | [ _ : Compose ?x ?x' = Identity _ |- context[Compose ?x _ = Identity _] ] ⇒ solve [ try x'; hnf; eauto ]
    end.

Ltac post_compose_to_identity :=
  eapply_by_compose @iso_is_epi;
  [ | repeat rewrite AssociativityNoEvar by noEvar; find_composition_to_identity; rewrite RightIdentity ];
  [ solve_isomorphism | ].
Ltac pre_compose_to_identity :=
  eapply_by_compose @iso_is_mono;
  [ | repeat rewrite <- AssociativityNoEvar by noEvar; find_composition_to_identity; rewrite LeftIdentity ];
  [ solve_isomorphism | ].