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 ≡ (λB∈Ob. ⦇
  set_dom=Hom A B,
  set_func=(λf∈Hom 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 = λf∈Hom 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 "(λf∈Hom 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 ∈ Hom⇘BB⇙ (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 → Ar⇘Set⇙"
    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) ∈ Hom⇘BB⇙ (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)) = 
    (λg∈Hom 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)) =
    (λg∈Hom 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 " … = (λg∈Hom 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)) =
    (λg∈Hom 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 "∀B∈Ob. σ(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 "∀B∈Ob. ∀C∈Ob. ∀f∈Hom 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 ∈ Ob⇘BB⇙" 
    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 = (λf∈Hom 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: "(λf∈Hom A B. (set_func (F⇘𝖺⇙ f)) (set_func (u A) (Id A))) 
    = (λf∈Hom 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 "(∀X∈Ob. ∀Y∈Ob. ∀f∈Hom 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: "(λf∈Hom A B. (set_func ((F⇘𝖺⇙ f) ⊙ (u A)) (Id A))) 
    = (λf∈Hom 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 "(λf∈Hom A B. (set_func ((u B) ⊙ (Hom(A,_))⇘𝖺⇙ f)) (Id A))
    = (λf∈Hom 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 "… = (λf∈Hom 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: 
    "(λf∈Hom A B. (set_func ((u B) ⊙ (Hom(A,_))⇘𝖺⇙ f)) (Id A))
    = (λf∈Hom 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 ⟷ (∀y∈B. ∃x∈A. 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 ∧ (∀y∈B. ∃x∈A. f(x)=y) ∧ (∀x∈A. 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