# 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" := 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 | ].