Library Exercise_4_1_1_14

Require Import Utf8.
Require Import Graph GraphCategory Category CategoryIsomorphisms SetCategory.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.1.1.14

Problem

Suppose that G = (V, A, src, tgt) and G' = (V', A', src', tgt') are graphs and that f : (f0, f1) : G G' is a graph homomorphism (as in Definition 3.3.3.1). If f0 : V V' and f1 : A A' are isomorphisms in Set, does this imply that f is an isomorphism in Grph? If so, why; and if not, show a counterexample (where f0 and f1 are isomorphisms but f is not).

Let Grph := CategoryOfGraph's.
Local Ltac t :=
repeat match goal with
| _reflexivity
| _intro
| [ H := _ |- _ ] ⇒ subst H
| [ H : IsomorphismOf _ |- _ ] ⇒ destruct H
| _progress (simpl in *; fg_equal)
| [ H : _ |- _ ] ⇒ rewrite H
| [ H0 : x, ?f (?g x) = x,
H1 : x, ?g (?f x) = x |- ?g ?y = ?z ] ⇒
cut (g (f (g y)) = g (f z));
[ let H := fresh in
intro H;
repeat rewrite H1 in H;
exact H
| rewrite H0;
apply f_equal ]
end.

Lemma Exercise_4_1_1_14
(G G' : Grph)
(f : Morphism Grph G G')
(f0 := OnVertices' f)
(f1 := OnArrows' f)
: IsomorphismOf (C := CategoryOfTypes) f0
→ IsomorphismOf (C := CategoryOfTypes) f1
→ IsomorphismOf (C := Grph) f.
intros i0 i1.
eexists {| OnVertices' := (Inverse i0);
OnArrows' := (Inverse i1) |};
apply Graph'Homomorphism_Eq; simpl;
abstract (
subst f0 f1;
destruct i0, i1;
simpl in *;
fg_equal;
intuition
).
Grab Existential Variables.
abstract (pose proof (TargetCommutes' f); pose proof (SourceCommutes' f); t).
abstract (pose proof (TargetCommutes' f); pose proof (SourceCommutes' f); t).
Defined.
End Exercise_4_1_1_14.