Library Exercise_4_1_1_13


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

Set Implicit Arguments.

Generalizable All Variables.

Exercise 4.1.1.13

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 f is an isomorphism in Grph, does this imply that f0 : V V' and f1 : A A' are isomorphisms in Set? If so, why; and if not, show a counterexample (where f is an isomorphism but either f0 or f1 is not).

  Let Grph := CategoryOfGraph's.

  Lemma Exercise_4_1_1_13
        (G G' : Grph)
        (f : Morphism Grph G G')
        (f0 := OnVertices' f)
        (f1 := OnArrows' f)
  : IsomorphismOf (C := Grph) fIsomorphismOf (C := CategoryOfTypes) f0 × IsomorphismOf (C := CategoryOfTypes) f1.
    intro i.
    split;
      [ ( (OnVertices' (Inverse i)))
      | ( (OnArrows' (Inverse i))) ];
      abstract (
          subst f0 f1;
          destruct i as [ i_f i_inv i_left i_right ];
          simpl;
          inversion i_left;
          inversion i_right;
          subst i_f;
          reflexivity
        ).
  Defined.
End Exercise_4_1_1_13.