Theory Yoneda

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

section ‹Yonedas Lemma›

theory Yoneda
imports HomFunctors NatTrans
begin

subsection ‹The Sandwich Natural Transformation›

locale Yoneda = "functor" + into_set +
  assumes "TERM (AA :: ('o,'a,'m)category_scheme)"
  fixes sandwich :: "['o,'a,'o]  'a set_arrow"  ("σ'(_,_')")
  defines "sandwich A a  (λBOb. 
  set_dom=Hom A B,
  set_func=(λfHom A B. set_func (F𝖺 f) a),
  set_cod=F𝗈 B
  )"
  fixes unsandwich :: "['o,'o  'a set_arrow]  'a" ("σ'(_,_')")
  defines "unsandwich A u  set_func (u A) (Id A)"

lemma (in Yoneda) F_into_set: 
  "Functor F : AA  Set"
proof-
  from F_axioms have "Functor F : AA  BB" by intro_locales
  thus ?thesis
    by (simp only: BB_Set)
qed


lemma (in Yoneda) F_comp_func:
  assumes 1: "A  Ob" and 2: "B  Ob" and 3: "C  Ob"
  and 4: "g  Hom A B" and 5: "f  Hom B C"
  shows "set_func (F𝖺 (f  g)) = compose (F𝗈 A) (set_func (F𝖺 f)) (set_func (F𝖺 g))"
proof-
  from 4 and 5 
  have 7: "Cod g = Dom f" 
    and 8: "g  Ar" 
    and 9: "f  Ar"
    and 10: "Dom g = A"
    by (simp_all add: hom_def)
  from F_preserves_dom and 8 and 10
  have 11: "set_dom (F𝖺 g) = F𝗈 A"
    by (simp add: preserves_dom_def BB_Set Set_def) auto
  from F_preserves_comp and 7 and 8 and 9
  have "F𝖺 (f  g) = (F𝖺 f) BB(F𝖺 g)"
    by (simp add: preserves_comp_def)
  hence "set_func (F𝖺 (f  g))  = set_func ((F𝖺 f)  (F𝖺 g))"
    by (simp add: BB_Set Set_def)
  also have " = compose (F𝗈 A) (set_func (F𝖺 f)) (set_func (F𝖺 g))"
    by (simp add: set_comp_def 11)
  finally show ?thesis .
qed

lemma (in Yoneda) sandwich_funcset:
  assumes A: "A  Ob"
  and "a  F𝗈 A"
  shows  "σ(A,a) : Ob  ar Set"
proof (rule funcsetI)
  fix B
  assume B: "B  Ob"
  thus "σ(A,a) B  ar Set"
  proof (simp add: Set_def sandwich_def set_cat_def)
    show "set_arrow U 
      set_dom = Hom A B, 
      set_func = λfHom A B. set_func (F𝖺 f) a, 
      set_cod = F𝗈 B"
    proof (simp add: set_arrow_def, intro conjI)
      show "Hom A B  U" and "F𝗈 B  U"
        by (simp_all add: U_def)
      show "(λfHom A B. set_func (F𝖺 f) a)  Hom A B  F𝗈 B"
      proof (rule funcsetI, simp)
        fix f
        assume f: "f  Hom A B"
        with A B have "F𝖺 f  HomBB(F𝗈 A) (F𝗈 B)"
          by (rule functors_preserve_homsets)
        hence "F𝖺 f  ar Set" 
          and "set_dom (F𝖺 f) = (F𝗈 A)"
          and "set_cod (F𝖺 f) = (F𝗈 B)"
          by (simp_all add: hom_def BB_Set Set_def)
        hence "set_func (F𝖺 f) : (F𝗈 A)  (F𝗈 B)"
          by (simp add: Set_def set_cat_def set_arrow_def)
        thus "set_func (F𝖺 f) a  F𝗈 B"
          using a  F𝗈 A
          by (rule funcset_mem)
      qed
    qed
  qed
qed


lemma (in Yoneda) sandwich_type:
  assumes A: "A  Ob" and B: "B  Ob"
  and "a  F𝗈 A"
  shows "σ(A,a) B  hom Set (Hom A B) (F𝗈 B)"
proof-
  have "σ(A,a)  Ob  ArSet⇙"
    using A and a  F𝗈 A by (rule sandwich_funcset)
  hence "σ(A,a) B  ar Set"
    using B by (rule funcset_mem)
  thus ?thesis
    using B by (simp add: sandwich_def hom_def Set_def)
qed


lemma (in Yoneda) sandwich_commutes:
  assumes AOb: "A  Ob" and BOb: "B  Ob" and COb: "C  Ob"
  and aFa: "a  F𝗈 A"
  and fBC: "f  Hom B C"
  shows "(F𝖺 f)  (σ(A,a) B) = (σ(A,a) C)  (Hom(A,_)𝖺 f)"
proof-
  from fBC have 1: "f  Ar" and 2: "Dom f = B" and 3: "Cod f = C"
    by (simp_all add: hom_def)
  from BOb have "set_dom ((F𝖺 f)  (σ(A,a) B)) = Hom A B"
    by (simp add: set_comp_def sandwich_def)
  also have " = set_dom ((σ(A,a) C)  (Hom(A,_)𝖺 f))"
    by (simp add: set_comp_def homf_def 1 2)
  finally have set_dom_eq: 
    "set_dom ((F𝖺 f)  (σ(A,a) B)) 
    = set_dom ((σ(A,a) C)  (Hom(A,_)𝖺 f))" .
  from BOb COb fBC have "(F𝖺 f)  HomBB(F𝗈 B) (F𝗈 C)" 
    by (rule functors_preserve_homsets)
  hence "set_cod ((F𝖺 f)  (σ(A,a) B)) = F𝗈 C"
    by (simp add: set_comp_def BB_Set Set_def set_cat_def hom_def)
  also from COb
  have " = set_cod ((σ(A,a) C)  (Hom(A,_)𝖺 f))"
    by (simp add: set_comp_def sandwich_def)
  finally have set_cod_eq:
    "set_cod ((F𝖺 f)  (σ(A,a) B)) 
    = set_cod ((σ(A,a) C)  (Hom(A,_)𝖺 f))" .
  from AOb and BOb and COb and fBC and aFa
  have set_func_lhs: 
    "set_func ((F𝖺 f)  (σ(A,a) B)) = 
    (λgHom A B. set_func (F𝖺 (f  g)) a)"
    apply (simp add:  set_comp_def sandwich_def compose_def)
    apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
    by (simp add: F_comp_func compose_def)
  have "(∙) : Hom B C  Hom A B  Hom A C" ..  
  from this and fBC 
  have opfType: "(∙) f : Hom A B  Hom A C"
    by (rule funcset_mem)
  from 1 and 2
  have "set_func ((σ(A,a) C)  (Hom(A,_)𝖺 f)) =
    (λgHom A B. set_func (σ(A,a) C) (f  g))"
    apply (simp add: set_comp_def homf_def)
    apply (simp add: compose_def)
    apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
    by auto
  also from COb and opfType 
  have "  = (λgHom A B. set_func (F𝖺 (f  g)) a)"
    apply (simp add: sandwich_def)
    apply (rule extensionalityI, rule restrict_extensional, rule restrict_extensional)
    by (simp add:Pi_def)
  finally have set_func_rhs:
    "set_func ((σ(A,a) C)  (Hom(A,_)𝖺 f)) =
    (λgHom A B. set_func (F𝖺 (f  g)) a)" .
  from set_func_lhs and set_func_rhs have
    "set_func ((F𝖺 f)  (σ(A,a) B))
    = set_func ((σ(A,a) C)  (Hom(A,_)𝖺 f))"
    by simp
  with set_dom_eq and set_cod_eq show ?thesis
    by simp
qed


lemma (in Yoneda) sandwich_natural:
  assumes "A  Ob"
  and "a  F𝗈 A"
  shows "σ(A,a) : Hom(A,_)  F in Func(AA,Set)"
proof (intro natural_transformation.intro natural_transformation_axioms.intro two_cats.intro)
  show "category AA" ..
  show "category Set" 
    by (simp only: Set_def)(rule set_cat_cat)
  show "Functor Hom(A,_) : AA  Set"
    by (rule homf_into_set)
  show "Functor F : AA  Set"
    by (rule F_into_set)
  show "BOb. σ(A,a) B  hom Set (Hom(A,_)𝗈 B) (F𝗈 B)"
    using assms by (auto simp add: homf_def intro: sandwich_type)
  show "σ(A,a) : Ob  ar Set"
    using assms by (rule sandwich_funcset)
  show "σ(A,a)  extensional (Ob)"
    unfolding sandwich_def by (rule restrict_extensional)
  show "BOb. COb. fHom B C.
    comp Set (F 𝖺 f) (σ(A,a) B) = comp Set (σ(A,a) C) (Hom(A,_)𝖺 f)"
    using assms by (auto simp add: Set_def intro: sandwich_commutes)
qed


subsection ‹Sandwich Components are Bijective›

lemma (in Yoneda) unsandwich_left_inverse:
  assumes 1: "A  Ob"
  and 2: "a  F𝗈 A"
  shows "σ(A,σ(A,a)) = a"
proof-
  from 1 have "Id A  Hom A A" ..
  with 1 
  have 3: "σ(A,σ(A,a)) = set_func (F𝖺 (Id A)) a"
    by (simp add: sandwich_def homf_def unsandwich_def)
  from F_preserves_id and 1
  have 4: "F𝖺 (Id A) = id Set (F𝗈 A)"
    by (simp add: preserves_id_def BB_Set)
  from F_preserves_objects and 1 
  have "F𝗈 A  ObBB⇙" 
    by (rule funcset_mem)
  hence "F𝗈 A  U"
    by (simp add: BB_Set Set_def set_cat_def)
  with 2
  have 5: "set_func (id Set (F𝗈 A)) a = a"
    by (simp add: Set_def  set_id_def)
  show ?thesis
    by (simp add: 3 4 5)
qed


lemma (in Yoneda) unsandwich_right_inverse:
  assumes 1: "A  Ob"
  and 2: "u : Hom(A,_)  F in Func(AA,Set)"
  shows "σ(A,σ(A,u)) = u"
proof (rule extensionalityI)
  show "σ(A,σ(A,u))  extensional (Ob)"
    by (unfold sandwich_def, rule restrict_extensional)
  from 2 show "u   extensional (Ob)"
    by (simp add: natural_transformation_def natural_transformation_axioms_def)
  fix B
  assume 3: "B  Ob"
  with 1
  have one: "σ(A,σ(A,u)) B = 
    set_dom = Hom A B,
    set_func = (λfHom A B. (set_func (F𝖺 f)) (set_func (u A) (Id A))),
    set_cod = F𝗈 B "
    by (simp add: sandwich_def unsandwich_def)
  from 1 have "Hom(A,_)𝗈 A = Hom A A"
    by (simp add: homf_def)
  with 1 and 2 have "(u A)  hom Set (Hom A A) (F𝗈 A)"
    by (simp add: natural_transformation_def natural_transformation_axioms_def,
      auto)
  hence "set_dom (u A) = Hom A A"
    by (simp add: hom_def Set_def)
  with 1 have applicable: "Id A  set_dom (u A)"
    by (simp)(rule)
  have two: "(λfHom A B. (set_func (F𝖺 f)) (set_func (u A) (Id A))) 
    = (λfHom A B. (set_func ((F𝖺 f)  (u A)) (Id A)))" 
    by (rule extensionalityI,
      rule restrict_extensional, rule restrict_extensional,
      simp add: set_comp_def compose_def applicable)
  from 2
  have "(XOb. YOb. fHom X Y. (F𝖺 f) BB(u X) = (u Y) BB(Hom(A,_)𝖺 f))"
    by (simp add: natural_transformation_def natural_transformation_axioms_def BB_Set)
  with 1 and 3 
  have three: "(λfHom A B. (set_func ((F𝖺 f)  (u A)) (Id A))) 
    = (λfHom A B. (set_func ((u B)  (Hom(A,_))𝖺 f)) (Id A))"
    apply (simp add: BB_Set Set_def)
    apply (rule extensionalityI)
    apply (rule restrict_extensional, rule restrict_extensional)
    by simp
  have "f  Hom A B. set_dom (Hom(A,_)𝖺 f) = Hom A A"
    by (intro ballI, simp add: homf_def hom_def)
  have roolz: "f. f  Hom A B  set_dom (Hom(A,_)𝖺 f) = Hom A A"
    by (simp add: homf_def hom_def)
  from 1 have rooly: "Id A  Hom A A" ..
  have roolx: "f. f  Hom A B  f  Ar"
    by (simp add: hom_def)
  have roolw: "f. f  Hom A B  Id A  Hom A (Dom f)"
  proof-
    fix f
    assume "f  Hom A B"
    hence "Dom f = A" by (simp add: hom_def)
    thus "Id A  Hom A (Dom f)"
      by (simp add: rooly)
  qed
  have annoying: "f. f  Hom A B  Id A = Id (Dom f)"
    by (simp add: hom_def)
  have "(λfHom A B. (set_func ((u B)  (Hom(A,_))𝖺 f)) (Id A))
    = (λfHom A B. (compose (Hom A A) (set_func (u B)) (set_func (Hom(A,_)𝖺 f))) (Id A))"
    apply (rule extensionalityI)
    apply (rule restrict_extensional, rule restrict_extensional)
    by (simp add: compose_def set_comp_def roolz rooly)
  also have " = (λfHom A B. (set_func (u B) f))"
    apply (rule extensionalityI)
    apply (rule restrict_extensional, rule restrict_extensional)
    apply (simp add: compose_def homf_def rooly roolx roolw)
    apply (simp only: annoying)
    apply (simp add: roolx id_right)
    done
  finally have four: 
    "(λfHom A B. (set_func ((u B)  (Hom(A,_))𝖺 f)) (Id A))
    = (λfHom A B. (set_func (u B) f))" .
  from 2 and  3 
  have uBhom: "u B  hom Set (Hom(A,_)𝗈 B) (F𝗈 B)"
    by (simp add: natural_transformation_def natural_transformation_axioms_def)
  with 3 
  have five: "set_dom (u B) = Hom A B"
    by (simp add: hom_def homf_def Set_def set_cat_def)
  from uBhom
  have six: "set_cod (u B) = F𝗈 B" 
    by (simp add: hom_def homf_def Set_def set_cat_def)
  have seven: "restrict (set_func (u B)) (Hom A B) = set_func (u B)"
    apply (rule extensionalityI)
    apply (rule restrict_extensional)
  proof-
    from uBhom have "u B  ar Set"
      by (simp add: hom_def)
    hence almost: "set_func (u B)  extensional (set_dom (u B))"
      by (simp add: Set_def set_cat_def set_arrow_def)
    from almost and five
    show "set_func (u B)  extensional (Hom A B)" 
      by simp
    fix f
    assume "f  Hom A B"
    thus "restrict (set_func (u B)) (Hom A B) f = set_func (u B) f"
      by simp
  qed
  from one and two and three and four and five and six and seven
  show "σ(A,σ(A,u)) B = u B" 
    by simp
qed


text ‹In order to state the lemma, we must rectify a curious
omission from the Isabelle/HOL library. They define the idea of
injectivity on a given set, but surjectivity is only defined relative
to the entire universe of the target type.›

definition
  surj_on :: "['a  'b, 'a set, 'b set]  bool" where
  "surj_on f A B  (yB. xA. f(x)=y)"

definition
  bij_on :: "['a  'b, 'a set, 'b set]  bool" where
  "bij_on f A B  inj_on f A & surj_on f A B"

definition
  equinumerous :: "['a set, 'b set]  bool"  (infix "" 40) where
  "equinumerous A B  (f. bij_betw f A B)"

lemma bij_betw_eq:
  "bij_betw f A B 
    inj_on f A  (yB. xA. f(x)=y)  (xA. f x  B)"
unfolding bij_betw_def by auto

theorem (in Yoneda) Yoneda:
  assumes 1: "A  Ob"
  shows "F𝗈 A  {u. u : Hom(A,_)  F in Func(AA,Set)}"
unfolding equinumerous_def bij_betw_eq inj_on_def
proof (intro exI conjI bexI ballI impI)
  ― ‹Sandwich is injective›
  fix x and y
  assume 2: "x  F𝗈 A" and 3: "y  F𝗈 A"
  and 4: "σ(A,x) = σ(A,y)"
  hence "σ(A,σ(A,x)) = σ(A,σ(A,y))"
    by simp
  with unsandwich_left_inverse
  show "x = y"
    by (simp add: 1 2 3)
next
  ― ‹Sandwich covers F A›
  fix u
  assume "u  {y. y : Hom(A,_)  F in Func (AA,Set)}"
  hence 2: "u : Hom(A,_)  F in Func (AA,Set)"
    by simp
  with 1 show "σ(A,σ(A,u)) = u"
    by (rule unsandwich_right_inverse)
  ― ‹Sandwich is into F A› (* there is really similar reasoning elsewhere*)
  from 1 and 2 
  have "u A  hom Set (Hom A A) (F𝗈 A)"
    by (simp add: natural_transformation_def natural_transformation_axioms_def homf_def)
  hence "u A  ar Set" and "dom Set (u A) = Hom A A" and "cod Set (u A) = F𝗈 A"
    by (simp_all add: hom_def)
  hence uAfuncset: "set_func (u A) : (Hom A A)  (F𝗈 A)"
    by (simp add: Set_def set_cat_def set_arrow_def)
  from 1 have "Id A  Hom A A" ..
  with uAfuncset 
  show "σ(A,u)  F𝗈 A"
    by (simp add: unsandwich_def, rule funcset_mem)
next
  fix x
  assume "x  F𝗈 A"
  with 1 have "σ(A,x) : Hom(A,_)  F in Func (AA,Set)"
    by (rule sandwich_natural)
  thus "σ(A,x)  {y. y : Hom(A,_)  F in Func (AA,Set)}"
    by simp
qed

end