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.