Quelle  Functors.thy

(*  Title:       Category theory using Isar and Locales
    Author:      Greg O'Keefe, June, July, August 2003
    License: LGPL

Functors: Define functors and prove a trivial example.
*)

section ‹Functors›

theory Functors
imports Cat
begin

subsection ‹Definitions›

record ('o1,'a1,'o2,'a2) "functor" =
  om :: "'o1 ==> 'o2"
  am :: "'a1 ==> 'a2"

abbreviation
  om_syn  (‹_ _o› [81]) where
  "F_<o> ≡ om F"

abbreviation
  am_syn  (‹_ _a› [81]) where
  "F_<a> ≡ am F"

locale two_cats = AA?: category AA + BB?: category BB
    for AA :: "('o1,'a1,'m1)category_scheme" (structure)
    and BB :: "('o2,'a2,'m2)category_scheme" (structure) + 
  fixes preserves_dom  ::  "('o1,'a1,'o2,'a2)functor ==> bool"
    and preserves_cod  ::  "('o1,'a1,'o2,'a2)functor ==> bool"
    and preserves_id  ::  "('o1,'a1,'o2,'a2)functor ==> bool"
    and preserves_comp  ::  "('o1,'a1,'o2,'a2)functor ==> bool"
  defines "preserves_dom G ≡ ∀f∈Ar. G_<o> (Dom f) = Dom (G_<a> f)"
    and "preserves_cod G ≡ ∀f∈Ar. G_<o> (Cod f) = Cod (G_<a> f)"
    and "preserves_id G ≡ ∀A∈Ob. G_<a> (Id A) = Id (G_<o> A)"
    and "preserves_comp G ≡
      ∀f∈Ar. ∀g∈Ar. Cod f = Dom g ⟶ G_<a> (g ∙ f) = (G_<a> g) ∙ (G_<a> f)"

locale "functor" = two_cats +
  fixes F (structure)
  assumes F_preserves_arrows: "F_<a> : Ar → Ar"
    and F_preserves_objects: "F_<o> : Ob → Ob"
    and F_preserves_dom: "preserves_dom F"
    and F_preserves_cod: "preserves_cod F"
    and F_preserves_id: "preserves_id F"
    and F_preserves_comp: "preserves_comp F"
begin

lemmas F_axioms = F_preserves_arrows F_preserves_objects F_preserves_dom 
  F_preserves_cod F_preserves_id F_preserves_comp

lemmas func_pred_defs = preserves_dom_def preserves_cod_def preserves_id_def preserves_comp_def

end

text ‹This gives us nicer notation for asserting that things are functors.›

abbreviation
  Functor  (‹Functor _ : _ ⟶ _› [81]) where
  "Functor F : AA ⟶ BB ≡ functor AA BB F"


subsection ‹Simple Lemmas›

text ‹For example:›

lemma (in "functor") "Functor F : AA ⟶ BB" ..


lemma functors_preserve_arrows [intro]:
  assumes "Functor F : AA ⟶ BB"
    and "f ∈ ar AA"
  shows "F_<a> f ∈ ar BB"
proof-
  from ‹Functor F : AA ⟶ BB›
  have "F_<a> : ar AA → ar BB"
    by (simp add: functor_def functor_axioms_def)
  from this and ‹f ∈ ar AA›
  show ?thesis by (rule funcset_mem)
qed


lemma (in "functor") functors_preserve_homsets:
  assumes 1: "A ∈ Ob"
  and 2: "B ∈ Ob"
  and 3: "f ∈ Hom A B"
  shows "F_<a> f ∈ Hom (F_<o> A) (F_<o> B)"
proof-
  from 3 
  have 4: "f ∈ Ar" 
    by (simp add: hom_def)
  with F_preserves_arrows 
  have 5: "F_<a> f ∈ Ar" 
    by (rule funcset_mem)
  from 4 and F_preserves_dom 
  have "Dom (F_<a> f) = F_<o> (Dom f)"
    by (simp add: preserves_dom_def)
  also from 3 have "… = F_<o> A"
    by (simp add: hom_def)
  finally have 6: "Dom (F_<a> f) = F_<o> A" .
  from 4 and F_preserves_cod 
  have "Cod (F_<a> f) = F_<o> (Cod f)"
    by (simp add: preserves_cod_def)
  also from 3 have "… = F_<o> B"
    by (simp add: hom_def)
  finally have 7: "Cod (F_<a> f) = F_<o> B" .
  from 5 and 6 and 7
  show ?thesis
    by (simp add: hom_def)
qed
    

lemma functors_preserve_objects [intro]:
  assumes "Functor F : AA ⟶ BB"
    and "A ∈ ob AA"
  shows "F_<o> A ∈ ob BB"
proof-
  from ‹Functor F : AA ⟶ BB›
  have "F_<o> : ob AA → ob BB"
    by (simp add: functor_def functor_axioms_def)
  from this and ‹A ∈ ob AA›
  show ?thesis by (rule funcset_mem)
qed


subsection ‹Identity Functor›

definition
  id_func :: "('o,'a,'m) category_scheme ==> ('o,'a,'o,'a) functor" where
  "id_func CC = (om=(λA∈ob CC. A), am=(λf∈ar CC. f))"

locale one_cat = two_cats +
  assumes endo: "BB = AA"

lemma (in one_cat) id_func_preserves_arrows:
  shows "(id_func AA)_<a> : Ar → Ar"
  by (unfold id_func_def, rule funcsetI, simp)


lemma (in one_cat) id_func_preserves_objects:
  shows "(id_func AA)_<o> : Ob → Ob"
  by (unfold id_func_def, rule funcsetI, simp)


lemma (in one_cat) id_func_preserves_dom:
  shows  "preserves_dom (id_func AA)"
unfolding preserves_dom_def endo
proof
  fix f
  assume f: "f ∈ Ar"
  hence lhs: "(id_func AA)_<o> (Dom f) = Dom f"
    by (simp add: id_func_def) auto
  have "(id_func AA)_<a> f = f"
    using f by (simp add: id_func_def)
  hence rhs: "Dom (id_func AA)_<a> f = Dom f"
    by simp
  from lhs and rhs show "(id_func AA)_<o> (Dom f) = Dom (id_func AA)_<a> f"
    by simp
qed

lemma (in one_cat) id_func_preserves_cod:
  "preserves_cod (id_func AA)"
apply (unfold preserves_cod_def, simp only: endo)
proof
  fix f
  assume f: "f ∈ Ar"
  hence lhs: "(id_func AA)_<o> (Cod f) = Cod f"
    by (simp add: id_func_def) auto
  have "(id_func AA)_<a> f = f"
    using f by (simp add: id_func_def)
  hence rhs: "Cod (id_func AA)_<a> f = Cod f"
    by simp
  from lhs and rhs show "(id_func AA)_<o> (Cod f) = Cod (id_func AA)_<a> f"
    by simp
qed


lemma (in one_cat) id_func_preserves_id:
  "preserves_id (id_func AA)"
unfolding preserves_id_def endo
proof
  fix A
  assume A: "A ∈ Ob"
  hence lhs: "(id_func AA)_<a> (Id A) = Id A"
    by (simp add: id_func_def) auto
  have "(id_func AA)_<o> A = A"
    using A by (simp add: id_func_def)
  hence rhs: "Id ((id_func AA)_<o> A) = Id A"
    by simp
  from lhs and rhs show "(id_func AA)_<a> (Id A) = Id ((id_func AA)_<o> A)"
    by simp
qed


lemma (in one_cat) id_func_preserves_comp:
  "preserves_comp (id_func AA)"
unfolding preserves_comp_def endo
proof (intro ballI impI)
  fix f and g
  assume f: "f ∈ Ar" and g: "g ∈ Ar" and "Cod f = Dom g"
  then have "g ∙ f ∈ Ar" ..
  hence lhs: "(id_func AA)_<a> (g ∙ f) = g ∙ f"
    by (simp add: id_func_def)
  have id_f: "(id_func AA)_<a> f = f"
    using f by (simp add: id_func_def)
  have id_g: "(id_func AA)_<a> g = g"
    using g by (simp add: id_func_def)
  hence rhs: "(id_func AA)_<a> g ∙ (id_func AA)_<a> f = g ∙ f"
    by (simp add: id_f id_g)
  from lhs and rhs 
  show "(id_func AA)_<a> (g ∙ f) = (id_func AA)_<a> g ∙ (id_func AA)_<a> f"
    by simp
qed

theorem (in one_cat) id_func_functor:
  "Functor (id_func AA) : AA ⟶ AA"
proof-
  from id_func_preserves_arrows
    and id_func_preserves_objects
    and id_func_preserves_dom
    and id_func_preserves_cod
    and id_func_preserves_id
    and id_func_preserves_comp
  show ?thesis
    by unfold_locales (simp_all add: endo preserves_dom_def
      preserves_cod_def preserves_id_def preserves_comp_def)
qed

end