(*  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"
 java.lang.StringIndexOutOfBoundsException: Range [5, 4) out of bounds for length 31

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

abbreviation
  am_syn  (‹_ _a› [81]) where
 " ≡

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 <sub>smsments_are_iso_iso to
    and "preserves_id G ≡ ∀A∈Ob. G<a> (Id A) = Id (G<o> A)"
    and "preserves_comp G ≡
      ∀f∈Ar. ∀g∈Ar. Cod f = Domguille>Ff ⋆D φ : F f ⋆D F w' →D F f ⋆D w¬"

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</sub>