Library Exercise_4_1_2_28


Require Import Utf8.
Require Import Omega JMeq.
Require Import Common DiscreteCategory NatCategory PathsCategory Graph ComputableCategory CategoryIsomorphisms ChainCategory.

Set Implicit Arguments.

Generalizable All Variables.


Exercise 4.1.2.28

Problem

Let G be the graph depicted
      v₀      e     v₁
      o ----------> o
and let [1] : Ob Cat denote the free category on G (see Example 4.1.2.27). We call [1] the free arrow category. What are its objects? For every pair of objects in [1], write down the hom-set.
  Lemma OneLeOne : 1 1. repeat constructor. Qed.
  Lemma ZeroLeOne : 0 1. repeat constructor. Qed.
  Lemma TwoNotLeOne n : S (S n) 1 → False. omega. Qed.

  Inductive G_Vertex := G_v0 | G_v1.
  Inductive G_Edge : G_VertexG_VertexSet := G_e : G_Edge G_v0 G_v1.

  Definition G : Graph :=
    {|
      Vertex := G_Vertex;
      Edge := G_Edge
    |}.

  Definition FreeArrowCategory := @PathsCategory (Vertex G) (Edge G).

  Lemma E_4_1_2_28_Objects_G : Object FreeArrowCategory = Vertex G. reflexivity. Qed.

Helper lemmas

  Local Ltac t' tac :=
    repeat match goal with
             | _assumption
             | _progress (repeat intro; hnf in *; subst_eq_refl; subst; trivial)
             | _ ⇒ ( eq_refl)
             | [ H : _ |- _ ] ⇒ solve [ inversion H; trivial ]
             | [ H : _ |- _ ] ⇒ solve [ destruct H; trivial ]
             | [ H : _ |- _ ] ⇒ specialize (H eq_refl)
             | [ H : sigT _ |- _ ] ⇒ destruct H
             | [ H : sig _ |- _ ] ⇒ destruct H
             | [ H : context[match ?x with __ end] |- _ ] ⇒ destruct x
             | _progress tac
           end.

  Lemma no_path'
  : m (p : Morphism FreeArrowCategory G_v1 m),
      { Hm : G_v1 = m
      | p = match Hm with
              | eq_reflNoEdges
            end }.
    induction p; t' idtac.
  Qed.
  Lemma destruct_path v v' (p : Morphism FreeArrowCategory v v')
  : { H : v = v' & match H
                         in (_ = y)
                         return (Morphism FreeArrowCategory v y Prop)
                   with
                     | eq_reflλ p0, p0 = NoEdges
                   end p }
    + { v'' : _ & { p' : path _ v v'' & { e : _ | p = AddEdge p' e } } }.
    destruct p.
    - left.
       eq_refl.
      reflexivity.
    - right.
      repeat esplit.
  Defined.

  Local Ltac t'' tac := t' ltac:(idtac;
                                 match goal with
                                   | [ H : _ |- _ ] ⇒ destruct (no_path' H)
                                 end;
                                 tac).

  Local Ltac t :=
    intros;
    hnf in *;
    match goal with
      | [ p : path _ _ _ |- _ ] ⇒ induction p; solve [ t'' idtac ]
      | [ p : path _ _ _ |- _ ] ⇒ destruct p; solve [ t'' idtac ]
      | [ p : path _ _ _ |- _ ] ⇒ destruct (destruct_path p); solve [ t'' idtac ]
    end.

  Lemma one_path'
  : m n (p : Morphism FreeArrowCategory n m)
           (Hn : G_v0 = n)
           (Hm : G_v1 = m),
      p = match Hn with
            | eq_reflmatch Hm with
                           | eq_reflAddEdge NoEdges G_e
                         end
          end.
    induction p;
    repeat match goal with
             | [ d : G_Vertex |- _ ] ⇒ destruct d
             | _progress (t' idtac)
             | _apply f_equal2
             | _t
             | [ d : G_Edge _ _ |- _ ] ⇒ try solve [ apply JMeq_eq; destruct d; reflexivity ]
           end.
  Qed.

  Lemma E_4_1_2_28_Hom_v0_v0
  : m : Morphism FreeArrowCategory G_v0 G_v0, m = NoEdges. Proof. t. Qed.
  Lemma E_4_1_2_28_Hom_v1_v1
  : m : Morphism FreeArrowCategory G_v1 G_v1, m = NoEdges. Proof. t. Qed.
  Lemma E_4_1_2_28_Hom_v1_v0
  : Morphism FreeArrowCategory G_v1 G_v0False. Proof. t. Qed.
  Lemma E_4_1_2_28_Hom_v0_v1
  : m : Morphism FreeArrowCategory G_v0 G_v1, m = AddEdge NoEdges G_e.
  Proof. exact (fun m ⇒ @one_path' _ _ m eq_refl eq_refl). Qed.
End Exercise_4_1_2_28.