Library Functor


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

Functors


Section Functors.
  Context `(C : @Category objC).
  Context `(D : @Category objD).

  Local Open Scope morphism_scope.

Quoting from the lecture notes for 18.705, Commutative Algebra:
A map of categories is known as a functor. Namely, given categories C and C', a (covariant) functor F : C C' is a rule that assigns to each object A of C an object F A of C' and to each map m : A B of C a map F m : F A F B of C' preserving composition and identity; that is,
  • F (m' m) = (F m') (F m) for maps m : A B and m' : B C of C, and
  • F (id A) = id (F A) for any object A of C, where id A is the identity morphism of A.
  Record Functor :=
    {
      ObjectOf :> objCobjD;
      MorphismOf : s d, C.(Morphism) s d
                               → D.(Morphism) (ObjectOf s) (ObjectOf d);
      FCompositionOf : s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
                          MorphismOf _ _ (m2 m1)
                          = (MorphismOf _ _ m2) (MorphismOf _ _ m1);
      FIdentityOf : x, MorphismOf _ _ (Identity x)
                              = Identity (ObjectOf x)
    }.
End Functors.

Delimit Scope functor_scope with functor.
Bind Scope functor_scope with Functor.

Create HintDb functor discriminated.

Arguments ObjectOf {objC C objD D} F c : simpl nomatch, rename.
Arguments MorphismOf {objC} [C] {objD} [D] F [s d] m : simpl nomatch, rename.

Arguments FCompositionOf [objC C objD D] F _ _ _ _ _ : rename.
Arguments FIdentityOf [objC C objD D] F _ : rename.

Hint Resolve @FCompositionOf @FIdentityOf : category.
Hint Resolve @FCompositionOf @FIdentityOf : functor.
Hint Rewrite @FIdentityOf : category.
Hint Rewrite @FIdentityOf : functor.

Section Functors_Equal.
  Lemma Functor_Eq objC C objD D :
     (F G : @Functor objC C objD D),
      ( x, ObjectOf F x = ObjectOf G x)
      → ( H : ( x, ObjectOf F x = ObjectOf G x),
           s d m, match H s in (_ = y) return y ~> G d with
                          | eq_reflmatch H d in (_ = y) return F s ~> y with
                                         | eq_reflMorphismOf F (s := s) (d := d) m
                                       end
                        end
                        = MorphismOf G (s := s) (d := d) m)
      → F = G.
    intros.
    assert (H' : ObjectOf F = ObjectOf G)
      by (apply functional_extensionality_dep; assumption);
      pose F as F'; pose G as G';
      destruct F, G;
      simpl in *;
      intuition.
    assert (match H' in (_ = y) return s d : objC, (s ~> d) y s ~> y d with
              | eq_reflMorphismOf F'
            end
            = MorphismOf G');
      [ repeat (apply functional_extensionality_dep; intro); subst_body; simpl in ×
      | ].
    - rewrite <- (H0 H).
      clear.
      subst.
      repeat match goal with
               | [ |- appcontext[match ?f ?x with __ end] ] ⇒ generalize (f x); clear; intros
             end.
      repeat match goal with
               | [ H : ?x = ?x |- _ ] ⇒ assert (H = eq_refl) by apply ProofIrrelevance.proof_irrelevance;
                                        subst H
             end.
      reflexivity.
    - subst_body.
      simpl in ×.
      repeat subst.
      f_equal;
        apply ProofIrrelevance.proof_irrelevance.
  Qed.

  Lemma Functor_Eq_by_JMeq objC C objD D :
     (F G : @Functor objC C objD D),
      ( x, ObjectOf F x = ObjectOf G x)
      → (ObjectOf F = ObjectOf G
          → s d m, MorphismOf F (s := s) (d := d) m
                           == MorphismOf G (s := s) (d := d) m)
      → F = G.
    intros.
    assert (H' : ObjectOf F = ObjectOf G)
      by (apply functional_extensionality_dep; assumption);
      pose F as F'; pose G as G';
      destruct F, G;
      simpl in *;
      intuition;
      subst.
    assert (MorphismOf F' = MorphismOf G');
      subst F' G';
      simpl;
      repeat (apply functional_extensionality_dep; intro);
      try solve [ apply JMeq_eq; intuition ];
      simpl in ×.
    subst;
      f_equal; apply ProofIrrelevance.proof_irrelevance.
  Qed.
End Functors_Equal.

Ltac functor_eq :=
  simpl;
  repeat intro;
  simpl;
  apply Functor_Eq;
  intros;
  subst_eq_refl_in_match;
  try easy.

Section FunctorComposition.
  Context `(B : @Category objB).
  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Context `(E : @Category objE).

  Hint Rewrite @FCompositionOf : functor.

  Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
    refine (Build_Functor C E
                          (fun cG (F c))
                          (fun _ _ mG.(MorphismOf) (F.(MorphismOf) m))
                          _
                          _);
    abstract (
        intros; autorewrite with functor; reflexivity
      ).
  Defined.
End FunctorComposition.

Infix "○" := (@ComposeFunctors _ _ _ _ _ _) : functor_scope.

Section IdentityFunctor.
  Context `(C : @Category objC).

There is an identity functor. It does the obvious thing.
  Definition IdentityFunctor : Functor C C.
    refine {| ObjectOf := (fun x x);
      MorphismOf := (fun _ _ x x)
    |};
    abstract t.
  Defined.
End IdentityFunctor.

Section IdentityFunctorLemmas.
  Context `(C : @Category objC).
  Context `(D : @Category objD).

  Lemma LeftIdentityFunctor (F : Functor D C)
  : ComposeFunctors (IdentityFunctor _) F = F.
    functor_eq.
  Qed.

  Lemma RightIdentityFunctor (F : Functor C D)
  : ComposeFunctors F (IdentityFunctor _) = F.
    functor_eq.
  Qed.
End IdentityFunctorLemmas.

Hint Rewrite @LeftIdentityFunctor @RightIdentityFunctor : category.
Hint Immediate @LeftIdentityFunctor @RightIdentityFunctor : category.
Hint Rewrite @LeftIdentityFunctor @RightIdentityFunctor : functor.
Hint Immediate @LeftIdentityFunctor @RightIdentityFunctor : functor.

Section FunctorCompositionLemmas.
  Context `(B : @Category objB).
  Context `(C : @Category objC).
  Context `(D : @Category objD).
  Context `(E : @Category objE).

  Lemma ComposeFunctorsAssociativity
        (F : Functor B C)
        (G : Functor C D)
        (H : Functor D E)
  : ComposeFunctors (ComposeFunctors H G) F
    = ComposeFunctors H (ComposeFunctors G F).
    functor_eq.
   Qed.
End FunctorCompositionLemmas.

Hint Resolve @ComposeFunctorsAssociativity : category.
Hint Resolve @ComposeFunctorsAssociativity : functor.