Library Exercise_4_4_1_1


Require Import Utf8.
Require Import FunctionalExtensionality JMeq EqdepFacts.
Require Import Graph PathsCategory ChainCategory UnderlyingGraph Graph PathsFunctor Morphism.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.4.1.1

Problem

Note: This is an out-dated version of the problem statement, which requires that the maps be injective as graph homomorphisms, rather than just injective on edges.
Let [2] denote the linear order graph of length 2 (see Exercise 4.1.1.8 and Proposition 4.1.2.6), and let Loop denote the unique graph having one vertex and one arrow (pictured in Diagram (3.15)).
(a) Find an injective graph homomorphism f : [2] Paths(Loop).
(b) The graph [2] has 6 paths, so Paths([2]) has 6 arrows. What are the images of these arrows under the graph homomorphism Paths(f) : Paths([2]) Paths(Paths(Loop))?

  Definition Loop : Graph := {| Vertex := unit; Edge := (fun _ _ unit) |}.
  Inductive LinearOrder2Graph_Vertex := Zero | One | Two.
  Inductive LinearOrder2Graph_Edge
  : LinearOrder2Graph_VertexLinearOrder2Graph_VertexSet :=
  | Zero_One : LinearOrder2Graph_Edge Zero One
  | One_Two : LinearOrder2Graph_Edge One Two.
  Definition LinearOrder2Graph : Graph
    := {| Vertex := LinearOrder2Graph_Vertex;
          Edge := LinearOrder2Graph_Edge |}.
  Fixpoint nth_edge_in_loop (n : ) : path (fun _ _unit) tt tt
    := match n with
         | ONoEdges
         | S n'AddEdge (nth_edge_in_loop n') tt
       end.
  Definition f (n m : ) : GraphHomomorphism LinearOrder2Graph (PathsFunctor Loop)
    := Build_GraphHomomorphism LinearOrder2Graph
                               (PathsFunctor Loop)
                               (fun _tt)
                               (fun src tgt
                                  match src, tgt with
                                    | Zero, One
                                      (fun _nth_edge_in_loop n)
                                    | One, Two
                                      (fun _nth_edge_in_loop m)
                                    | _, _fun xNoEdges
                                  end).

  Lemma Exercise_4_4_1_1_a_vert n m
  : is_injective (OnVertices (f n m)) → False.
    subst_body; clear; simpl.
    intro H.
    specialize (H One Two eq_refl).
    inversion H.
  Qed.
  Lemma nth_edge_in_loop_injective
  : is_injective nth_edge_in_loop.
    intro x; induction x;
    intro y; induction y;
    intuition;
    match goal with
      | [ H : _ |- _ ] ⇒ try solve [ inversion H; firstorder ]
    end.
  Qed.
  Definition f' n m := GraphHomomorphismToGraph'Homomorphism (f n m).
  Lemma Exercise_4_4_1_1_a_edges n m
  : m nis_injective (OnArrows' (f' n m)).
    subst_body; clear; simpl.
    intro.
    assert (n m) by intuition.
    intros x y.
    destruct_head_hnf @sigT;
    destruct_head_hnf @prod;
    destruct_head_hnf @LinearOrder2Graph_Edge;
    simpl in *;
    repeat intro;
    try reflexivity;
    repeat match goal with
             | [ H : @eq (sigT _) _ _ |- _ ] ⇒
               apply EqdepFacts.eq_sigT_eq_dep in H;
                 apply eq_dep_JMeq in H;
                 apply JMeq_eq in H
             | [ H : _ = _ |- _ ] ⇒ apply nth_edge_in_loop_injective in H
           end;
    firstorder.
  Qed.
  Definition Paths2 := PathsFunctor LinearOrder2Graph.
  Definition Paths2Path0 : Edge Paths2 Zero Zero
    := NoEdges.
  Definition Paths2Path1 : Edge Paths2 One One
    := NoEdges.
  Definition Paths2Path2 : Edge Paths2 Two Two
    := NoEdges.
  Definition Paths2Path3 : Edge Paths2 Zero One
    := AddEdge NoEdges Zero_One.
  Definition Paths2Path4 : Edge Paths2 One Two
    := AddEdge NoEdges One_Two.
  Definition Paths2Path5 : Edge Paths2 Zero Two
    := AddEdge (AddEdge NoEdges Zero_One) One_Two.

  Section part_b.
    Local Notation "[ a , .. , b ]" := (AddEdge .. (AddEdge NoEdges a) .. b).
    Local Notation "[]" := NoEdges.

    Variables n m : .

    Local Notation "'Paths_f' a" := ((MorphismOf PathsFunctor (f n m)) a) (at level 10).
    Local Notation "a ~> b" := (Edge _ a b).
    Local Notation "a ~~> b" := (path _ a b).

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path0.

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path1.

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path2.

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path3.

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path4.

    Eval simpl in OnEdges (MorphismOf PathsFunctor (f n m)) _ _ Paths2Path5.
  End part_b.
End Exercise_4_4_1_1.