Last active
March 23, 2023 11:55
-
-
Save myuon/d75edfbb5ef11fbd1075 to your computer and use it in GitHub Desktop.
Yoneda Lemma
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
definition (in Category) Iso where | |
"Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))" | |
definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where | |
"𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)" | |
record 'c setmap = | |
setdom :: "'c set" | |
setcod :: "'c set" | |
setfunction :: "'c ⇒ 'c" | |
definition setmap where | |
"setmap f ≡ (∀x. x∈setdom f ⟶ setfunction f x ∈ setcod f)" | |
definition setmap_eq where | |
"setmap_eq f g ≡ setmap f & setmap g & setdom f = setdom g & setcod f = setcod g & (∀ x ∈ setdom f. setfunction f x = setfunction g x)" | |
definition Set where | |
"Set ≡ ⦇ | |
Obj = UNIV, | |
Arr = {f. setmap f}, | |
Dom = setdom, | |
Cod = setcod, | |
Id = (λX. ⦇ setdom = X, setcod = X, setfunction = λx. x ⦈), | |
comp = (λg f. ⦇ setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x) ⦈), | |
eq = setmap_eq | |
⦈" | |
lemma Set_category: "Category Set" | |
proof (auto simp add: Category_def Set_def) | |
fix X :: "'a set" | |
show "setmap ⦇setdom = X, setcod = X, setfunction = λx. x⦈" by (simp add: setmap_def) | |
next | |
fix f g :: "'a setmap" | |
assume a: "setmap f" "setmap g" "setcod f = setdom g" | |
show "setmap ⦇setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x)⦈" | |
apply (simp add: setmap_def) | |
using a(1) a(3) a(2) apply (auto simp add: setmap_def) | |
done | |
next | |
show "equiv (Collect setmap) {(x, y). setmap_eq x y}" | |
apply (rule equivI) | |
apply (rule refl_onI, auto simp add: setmap_eq_def) | |
apply (rule symI, auto) | |
apply (simp add: transp_trans [symmetric], rule transpI, auto) | |
done | |
next | |
fix f :: "'a setmap" | |
assume a: "setmap f" | |
thus "setmap_eq ⦇setdom = setdom f, setcod = setcod f, setfunction = setfunction f⦈ f" | |
by (simp add: setmap_eq_def setmap_def) | |
next | |
fix f g h :: "'a setmap" | |
assume a: "setmap f" "setmap g" "setmap h" "setcod f = setdom g" "setcod g = setdom h" | |
show "setmap_eq | |
⦇setdom = setdom f, setcod = setcod h, setfunction = λx. setfunction h (setfunction g (setfunction f x))⦈ | |
⦇setdom = setdom f, setcod = setcod h, setfunction = λx. setfunction h (setfunction g (setfunction f x))⦈" | |
apply (simp add: setmap_eq_def setmap_def) | |
using a apply (simp add: setmap_def) | |
done | |
next | |
fix f g h i :: "'a setmap" | |
assume a: "setmap f" "setmap g" "setmap h" "setmap i" "setmap_eq f g" "setmap_eq h i" "setcod h = setdom f" | |
show "setmap_eq | |
⦇setdom = setdom h, setcod = setcod f, setfunction = λx. setfunction f (setfunction h x)⦈ | |
⦇setdom = setdom i, setcod = setcod g, setfunction = λx. setfunction g (setfunction i x)⦈" | |
proof (auto simp add: setmap_eq_def setmap_def) | |
fix x | |
{ | |
assume "x ∈ setdom h" | |
hence "setfunction h x ∈ setcod h" | |
using a(3) by (simp add: setmap_def) | |
thus "setfunction f (setfunction h x) ∈ setcod f" | |
using a(1) by (simp add: a(7) setmap_def) | |
} | |
{ | |
assume "x ∈ setdom i" | |
hence "setfunction i x ∈ setdom g" | |
using a by (simp add: setmap_def setmap_eq_def) | |
thus "setfunction g (setfunction i x) ∈ setcod g" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
{ | |
assume "x ∈ setdom h" thus "x ∈ setdom i" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
{ | |
assume "x ∈ setdom i" thus "x ∈ setdom h" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
{ | |
assume "x ∈ setcod f" thus "x ∈ setcod g" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
{ | |
assume "x ∈ setcod g" thus "x ∈ setcod f" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
{ | |
assume "x ∈ setdom h" thus "setfunction f (setfunction h x) = setfunction g (setfunction i x)" | |
using a by (simp add: setmap_def setmap_eq_def) | |
} | |
qed | |
qed | |
record ('o,'a,'c,'o2,'a2,'d) Functor = | |
domCat :: "('o,'a,'c) Category_scheme" | |
codCat :: "('o2,'a2,'d) Category_scheme" | |
fobj :: "'o ⇒ 'o2" | |
fmap :: "'a ⇒ 'a2" | |
locale Functor = | |
fixes F :: "('o,'a,'c,'o2,'a2,'d,'f) Functor_scheme" (structure) | |
assumes dom_category: "Category (domCat F)" | |
and cod_category: "Category (codCat F)" | |
and obj_mapping: "X ∈ Obj (domCat F) ⟹ fobj F X ∈ Obj (codCat F)" | |
and arr_mapping: "f ∈ Hom[domCat F][A,B] ⟹ fmap F f ∈ Hom[codCat F][fobj F A,fobj F B]" | |
and preserve_id: "X ∈ Obj (domCat F) ⟹ fmap F (Id (domCat F) X) ≈[codCat F] Id (codCat F) (fobj F X)" | |
and preserve_comp: | |
"⟦ f ∈ Arr (domCat F); g ∈ Arr (domCat F); Cod (domCat F) f = Dom (domCat F) g ⟧ | |
⟹ fmap F (g ∘[domCat F] f) ≈[codCat F] fmap F g ∘[codCat F] fmap F f" | |
abbreviation Functor_type ("Functor' _ : _ ⟶ _" [81] 90) where | |
"Functor' F : 𝒞 ⟶ 𝒟 ≡ Functor F & domCat F = 𝒞 & codCat F = 𝒟" | |
lemma FunctorE: "Functor' F : 𝒞 ⟶ 𝒟 ⟹ | |
(Category 𝒞 ⟹ | |
Category 𝒟 ⟹ | |
(X ∈ Obj 𝒞 ⟹ fobj F X ∈ Obj 𝒟) ⟹ | |
(f ∈ Hom[𝒞][A,B] ⟹ fmap F f ∈ Hom[𝒟][fobj F A,fobj F B]) ⟹ thesis) ⟹ thesis" | |
by (auto simp add: Functor_def) | |
record ('o,'a,'c,'o2,'a2,'d,'f,'f2) Nat = | |
domFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor" | |
codFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor" | |
component :: "'o ⇒ 'a2" | |
locale Nat = | |
fixes η :: "('o,'a,'c,'o2,'a2,'d,'f,'f2,'n) Nat_scheme" | |
assumes same_dom: "domCat (domFunctor η) = domCat (codFunctor η)" | |
and same_cod: "codCat (domFunctor η) = codCat (codFunctor η)" | |
and dom_functor: "Functor' (domFunctor η) : domCat (domFunctor η) ⟶ codCat (domFunctor η)" | |
and cod_functor: "Functor' (codFunctor η) : domCat (codFunctor η) ⟶ codCat (codFunctor η)" | |
and component_mapping: "X ∈ Obj (domCat (domFunctor η)) | |
⟹ component η X ∈ Hom[codCat (domFunctor η)][fobj (domFunctor η) X, fobj (codFunctor η) X]" | |
and naturality: "⟦ f ∈ Hom[domCat (domFunctor η)][A,B]; A ∈ Obj (domCat (domFunctor η)); B ∈ Obj (domCat (domFunctor η)) ⟧ | |
⟹ (component η B ∘[codCat (domFunctor η)] fmap (domFunctor η) f) ≈[codCat (domFunctor η)] | |
(fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η A)" | |
abbreviation Nat_type ("Nat' _ : _ ⟶ _" [81] 90) where | |
"Nat' η : F ⟶ G ≡ Nat η & Nat.domFunctor η = F & Nat.codFunctor η = G" | |
lemma NatE: "Nat' η : F ⟶ G ⟹ | |
(Functor' F : domCat F ⟶ codCat F ⟹ | |
Functor' G : domCat G ⟶ codCat G ⟹ | |
domCat F = domCat G ⟹ codCat F = codCat G ⟹ | |
(X ∈ Obj (domCat F) ⟹ component η X ∈ Hom[codCat F][fobj F X,fobj G X]) ⟹ | |
(f ∈ Hom[domCat F][A,B] ⟹ A ∈ Obj (domCat F) ⟹ B ∈ Obj (domCat F) ⟹ (component η B ∘[codCat F] fmap F f) ≈[codCat F] (fmap G f ∘[codCat F] component η A)) ⟹ | |
thesis) ⟹ thesis" | |
by (auto simp add: Nat_def) | |
lemma NatE_naturality: | |
"⟦ Nat' η : F ⟶ G; f ∈ Hom[domCat F][A,B]; A ∈ Obj (domCat F); B ∈ Obj (domCat F) ⟧ ⟹ (component η B ∘[codCat F] fmap F f) ≈[codCat F] (fmap G f ∘[codCat F] component η A)" | |
by (rule NatE, auto) | |
lemma NatI: | |
assumes "Functor' F : 𝒞 ⟶ 𝒟" "Functor' G : 𝒞 ⟶ 𝒟" "domFunctor η = F" "codFunctor η = G" | |
and "⋀X. X ∈ Obj 𝒞 ⟹ component η X ∈ Hom[𝒟][fobj F X,fobj G X]" | |
and "⋀f A B. ⟦ f ∈ Hom[𝒞][A,B]; A ∈ Obj 𝒞; B ∈ Obj 𝒞 ⟧ | |
⟹ ((component η B ∘[𝒟] fmap F f) ≈[𝒟] fmap G f ∘[𝒟] component η A)" | |
shows "Nat' η : F ⟶ G" | |
by (rule, auto simp add: Nat_def assms) | |
definition idNat where | |
"idNat F ≡ ⦇ domFunctor = F, codFunctor = F, component = λX. Id (codCat F) (fobj F X) ⦈" | |
lemma idNat_is_Nat: | |
assumes "Functor' F : 𝒞 ⟶ 𝒟" | |
shows "Nat' (idNat F) : F ⟶ F" | |
proof (simp add: Nat_def idNat_def, auto simp add: assms) | |
have D_cat: "Category 𝒟" by (rule FunctorE [OF assms], simp) | |
{ | |
fix X | |
assume "X ∈ Obj 𝒞" | |
then have FX_in: "fobj F X ∈ Obj 𝒟" | |
by (metis assms Functor.obj_mapping) | |
show "id⇘𝒟⇙ fobj F X ∈ Hom[𝒟][fobj F X,fobj F X]" | |
apply (rule CategoryE [OF D_cat]) | |
using FX_in by auto | |
} | |
{ | |
fix f A B | |
assume "f ∈ Hom[𝒞][A,B]" | |
then have Ff_in: "fmap F f ∈ Hom[𝒟][fobj F A, fobj F B]" | |
by (metis assms Functor.arr_mapping) | |
show "((id⇘𝒟⇙ fobj F B) ∘[𝒟] fmap F f) ≈[𝒟] (fmap F f ∘[𝒟] (id⇘𝒟⇙ fobj F A))" (is "?L ≈[_] ?R") | |
proof- | |
have "?L ≈[𝒟] fmap F f" | |
by (rule CategoryE_left_id, rule D_cat, rule Ff_in) | |
moreover have "fmap F f ≈[𝒟] ?R" | |
using CategoryE_right_id [OF D_cat Ff_in] | |
by (rule Category.eq_sym [OF D_cat]) | |
ultimately | |
show ?thesis by (rule Category.eq_trans [OF D_cat]) | |
qed | |
} | |
qed | |
definition compNat ("_ ∘[Nat] _") where | |
"compNat η ε ≡ ⦇ | |
domFunctor = Nat.domFunctor ε, codFunctor = Nat.codFunctor η, | |
component = λX. component η X ∘[codCat (Nat.domFunctor η)] component ε X | |
⦈" | |
lemma compNat_nat: | |
assumes η_nat: "Nat' η : G ⟶ H" | |
and ε_nat: "Nat' ε : F ⟶ G" | |
shows "Nat' (η ∘[Nat] ε) : F ⟶ H" | |
apply (rule NatI) | |
apply (rule NatE [OF ε_nat], simp) | |
apply (rule NatE [OF η_nat], simp) | |
apply (simp add: compNat_def, simp add: ε_nat) | |
apply (simp add: compNat_def, simp add: η_nat) | |
apply (simp add: compNat_def, simp add: assms) | |
proof- | |
have codG_cat: "Category (codCat G)" | |
apply (rule NatE [OF η_nat]) | |
apply (metis FunctorE) | |
done | |
have codH_cat: "Category (codCat H)" | |
apply (rule NatE [OF η_nat]) | |
apply (metis FunctorE) | |
done | |
have F_functor: "Functor' F : domCat F ⟶ codCat F" | |
by (rule NatE [OF ε_nat], simp) | |
have G_functor: "Functor' G : domCat F ⟶ codCat F" | |
by (rule NatE [OF ε_nat], simp) | |
have H_functor: "Functor' H : domCat G ⟶ codCat G" | |
by (rule NatE [OF η_nat], simp) | |
have codGH: "codCat G = codCat H" | |
by (rule NatE [OF η_nat], auto) | |
{ | |
fix X | |
assume X_in: "X ∈ Obj (domCat G)" | |
have 1: "component η X ∈ Hom[codCat H][fobj G X,fobj H X]" | |
apply (rule NatE [OF η_nat]) | |
using X_in by auto | |
have 2: "component ε X ∈ Hom[codCat G][fobj F X,fobj G X]" | |
apply (rule NatE [OF ε_nat]) | |
using X_in by auto | |
show "(component η X ∘[codCat G] component ε X) ∈ Hom[codCat G][fobj F X,fobj H X]" | |
apply (rule NatE [OF η_nat], simp) | |
by (metis CategoryE codG_cat 1 2) | |
} | |
{ | |
fix f A B | |
assume f_in: "f ∈ Hom[domCat G][A,B]" | |
and A_in: "A ∈ Obj (domCat G)" | |
and B_in: "B ∈ Obj (domCat G)" | |
show "(component (η ∘[Nat] ε) B ∘[codCat G] fmap F f) ≈[codCat G] (fmap H f ∘[codCat G] component (η ∘[Nat] ε) A)" (is "?L ≈[_] ?R") | |
proof- | |
have 1: "component η B ∈ Hom[codCat G][fobj G B, fobj H B]" | |
apply (rule NatE [OF η_nat]) using B_in by auto | |
have 11: "component η A ∈ Hom[codCat G][fobj G A, fobj H A]" | |
apply (rule NatE [OF η_nat]) using A_in by auto | |
have 2: "component ε B ∈ Hom[codCat G][fobj F B, fobj G B]" | |
apply (rule NatE [OF ε_nat]) using B_in by auto | |
have 21: "component ε A ∈ Hom[codCat G][fobj F A, fobj G A]" | |
apply (rule NatE [OF ε_nat]) using A_in by auto | |
have 3: "fmap F f ∈ Hom[codCat G][fobj F A, fobj F B]" | |
apply (rule NatE [OF ε_nat], simp) | |
apply (rule FunctorE [OF F_functor]) | |
using f_in by auto | |
have 4: "fmap G f ∈ Hom[codCat G][fobj G A, fobj G B]" | |
apply (rule NatE [OF ε_nat], simp) | |
apply (rule FunctorE [OF G_functor]) | |
using f_in by auto | |
have 41: "fmap G f ∈ Hom[codCat H][fobj G A, fobj G B]" | |
apply (rule NatE [OF η_nat]) | |
using 4 by auto | |
have 5: "fmap H f ∈ Hom[codCat H][fobj H A, fobj H B]" | |
apply (rule NatE [OF η_nat], simp) | |
apply (rule FunctorE [OF H_functor]) | |
using f_in by auto | |
have "?L ≈[codCat G] (component η B ∘[codCat G] component ε B) ∘[codCat G] fmap F f" | |
apply (simp add: compNat_def η_nat) | |
apply (rule CategoryE_refl [OF codG_cat CategoryE_comp_exist [OF codG_cat 3 CategoryE_comp_exist [OF codG_cat 2 1]]]) | |
done | |
moreover have "… ≈[codCat G] component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)" | |
apply (rule CategoryE [OF codG_cat]) | |
using 1 2 3 by auto | |
ultimately | |
have a: "?L ≈[codCat G] component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)" | |
by (rule Category.eq_trans [OF codG_cat]) | |
have "… ≈[codCat G] component η B ∘[codCat G] (fmap G f ∘[codCat G] component ε A)" | |
apply (rule CategoryE_eq_comp [OF codG_cat 1 1]) | |
apply (rule CategoryE_comp_exist [OF codG_cat 3 2]) | |
apply (rule CategoryE_comp_exist [OF codG_cat 21 4]) | |
apply (rule CategoryE_refl [OF codG_cat 1]) | |
defer | |
using CategoryE_comp_exist [OF codG_cat 3 2] 1 apply (simp add: hom_def) | |
proof- | |
have 1: "codCat F = codCat G" by (rule NatE [OF ε_nat], auto) | |
have 2: "domCat F = domCat G" by (rule NatE [OF ε_nat], auto) | |
show "(component ε B ∘[codCat G] fmap F f) ≈[codCat G] (fmap G f ∘[codCat G] component ε A)" | |
apply (simp add: 1 [symmetric]) | |
apply (rule NatE_naturality [OF ε_nat]) | |
using f_in A_in B_in by (auto simp add: 2) | |
qed | |
moreover have "… ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A" | |
by (metis "1" "21" "4" Category.eq_sym CategoryE_assoc codG_cat) | |
ultimately | |
have b: "(component η B ∘[codCat G] (component ε B ∘[codCat G] fmap F f)) ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A" | |
by (rule Category.eq_trans [OF codG_cat]) | |
have "… ≈[codCat G] (fmap H f ∘[codCat G] component η A) ∘[codCat G] component ε A" | |
apply (rule CategoryE_eq_comp [OF codG_cat]) | |
apply (rule CategoryE_comp_exist [OF codG_cat 4 1]) | |
apply (rule CategoryE_comp_exist [OF codG_cat 11]) using 5 apply (simp add: codGH) | |
apply (rule 21, rule 21) | |
apply (rule NatE_naturality [OF η_nat f_in A_in B_in]) | |
apply (rule CategoryE_refl [OF codG_cat 21]) | |
using CategoryE_comp_exist [OF codG_cat 4 1] 21 apply (simp add: hom_def) | |
done | |
moreover have "… ≈[codCat G] fmap H f ∘[codCat G] (component η A ∘[codCat G] component ε A)" | |
using CategoryE_assoc codG_cat by (metis "11" "21" "5" H_functor) | |
ultimately | |
have c: "((component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A) ≈[codCat G] fmap H f ∘[codCat G] (component η A ∘[codCat G] component ε A)" | |
by (rule Category.eq_trans [OF codG_cat]) | |
have d: "… ≈[codCat G] ?R" | |
apply (simp add: compNat_def η_nat) | |
apply (rule CategoryE_refl [OF codG_cat CategoryE_comp_exist [OF codG_cat CategoryE_comp_exist [OF codG_cat 21 11]]]) | |
using 5 by (simp add: codGH) | |
show ?thesis | |
proof- | |
have 1: "?L ≈[codCat G] (component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A" by (rule Category.eq_trans [OF codG_cat a b]) | |
have 2: "((component η B ∘[codCat G] fmap G f) ∘[codCat G] component ε A) ≈[codCat G] ?R" by (rule Category.eq_trans [OF codG_cat c d]) | |
show ?thesis by (rule Category.eq_trans [OF codG_cat 1 2]) | |
qed | |
qed | |
} | |
qed | |
definition nat_eq where | |
"nat_eq η ε ≡ (∀X ∈ Obj (domCat (domFunctor η)). component η X = component ε X)" | |
definition FunCat where | |
"FunCat 𝒞 𝒟 = ⦇ | |
Obj = {F. Functor' F : 𝒞 ⟶ 𝒟}, | |
Arr = {η. ∃F∈{F. Functor' F : 𝒞 ⟶ 𝒟}. ∃G∈{F. Functor' F : 𝒞 ⟶ 𝒟}. Nat' η : F ⟶ G}, | |
Dom = domFunctor, | |
Cod = codFunctor, | |
Id = idNat, | |
comp = compNat, | |
eq = nat_eq | |
⦈" | |
lemma | |
assumes "Category 𝒞" "Category 𝒟" | |
shows "Category (FunCat 𝒞 𝒟)" | |
apply (unfold Category_def) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
theory Category | |
imports Main | |
begin | |
no_notation Fun.comp (infixl "∘" 55) | |
record ('o,'a) Category = | |
Obj :: "'o set" | |
Arr :: "'a set" | |
Dom :: "'a ⇒ 'o" ("domı _" [80] 90) | |
Cod :: "'a ⇒ 'o" ("codı _" [80] 90) | |
Id :: "'o ⇒ 'a" ("idı _" [80] 90) | |
comp :: "'a ⇒ 'a ⇒ 'a" (infixr "∘ı" 60) | |
locale Category = | |
fixes 𝒞 :: "('o,'a,'c) Category_scheme" (structure) | |
assumes dom_obj [intro]: "f ∈ Arr 𝒞 ⟹ dom f ∈ Obj 𝒞" | |
and cod_obj [intro]: "f ∈ Arr 𝒞 ⟹ cod f ∈ Obj 𝒞" | |
and id_exist [intro]: "X ∈ Obj 𝒞 ⟹ id X ∈ Arr 𝒞 & dom (id X) = X & cod (id X) = X" | |
and comp_exist [intro]: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; cod f = dom g ⟧ | |
⟹ g ∘ f ∈ Arr 𝒞 & dom (g ∘ f) = dom f & cod (g ∘ f) = cod g" | |
and left_id [simp]: "f ∈ Arr 𝒞 ⟹ id (cod f) ∘ f = f" | |
and right_id [simp]: "f ∈ Arr 𝒞 ⟹ f ∘ id (dom f) = f" | |
and assoc [iff]: "⟦ f ∈ Arr 𝒞; g ∈ Arr 𝒞; h ∈ Arr 𝒞; cod f = dom g; cod g = dom h ⟧ | |
⟹ (h ∘ g) ∘ f = h ∘ (g ∘ f)" | |
begin | |
abbreviation Hom ("_ → _" [70] 100) where | |
"Hom A B ≡ {f ∈ Arr 𝒞. dom f = A & cod f = B}" | |
lemma arr_type [simp]: | |
assumes "f ∈ Arr 𝒞" shows "f : (dom f) → (cod f)" | |
by (metis (mono_tags, lifting) assms mem_Collect_eq) | |
lemma id_type [simp]: | |
assumes "X ∈ Obj 𝒞" shows "id X : X → X" | |
using assms id_exist by auto | |
lemma comp_hom [simp]: | |
assumes "f : A → B" and "g : B → C" | |
shows "g ∘ f : A → C" | |
using assms comp_exist by auto | |
lemma assoc_hom [simp]: | |
assumes "f : A → B" and "g : B → C" and "h : C → D" | |
shows "(h ∘ g) ∘ f = h ∘ (g ∘ f)" | |
by (metis (mono_tags, lifting) assms assoc mem_Collect_eq) | |
end | |
abbreviation comp_category ("_ ∘[_] _" [60] 100) where | |
"f ∘[𝒞] g ≡ comp 𝒞 f g" | |
abbreviation hom_category ("_ -[_]→ _" [70] 100) where | |
"a -[𝒞]→ b ≡ Category.Hom 𝒞 a b" | |
definition opposite ("_ {^op}" 100) where | |
"opposite 𝒞 ≡ ⦇ | |
Obj = Obj 𝒞, | |
Arr = Arr 𝒞, | |
Dom = Cod 𝒞, | |
Cod = Dom 𝒞, | |
Id = Id 𝒞, | |
comp = (λf g. comp 𝒞 g f) | |
⦈" | |
lemma opposite_category: | |
assumes "Category 𝒞" | |
shows "Category (𝒞 {^op})" | |
unfolding opposite_def Category_def | |
by (auto simp add: assms Category.cod_obj Category.dom_obj | |
Category.id_exist Category.comp_exist | |
Category.right_id Category.left_id Category.assoc) | |
definition (in Category) Iso where | |
"Iso f g ≡ f ∘ g = id (dom g) & g ∘ f = id (dom f)" | |
definition (in Category) Iso_on_objects ("IsoObj _ _") where | |
"IsoObj A B ≡ ∃f∈Arr 𝒞. ∃g∈Arr 𝒞. (f : A → B) & (g : B → A) & Iso f g" | |
definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where | |
"𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. (f : A -[𝒞]→ B) & (g : B -[𝒞]→ A) & Category.Iso 𝒞 f g)" | |
record 'c setmap = | |
setdom :: "'c set" | |
setcod :: "'c set" | |
setfunction :: "'c ⇒ 'c" | |
definition setmap where | |
"setmap f ≡ (∀x. x∈setdom f ⟶ setfunction f x ∈ setcod f)" | |
axiomatization where | |
setmap_eq : "⟦ setmap f; setmap g; setdom f = setdom g; setcod f = setcod g; ∀x∈setdom f. setfunction f x = setfunction g x ⟧ | |
⟹ f = g" | |
definition Set where | |
"Set ≡ ⦇ | |
Obj = UNIV, | |
Arr = {f. setmap f}, | |
Dom = setdom, | |
Cod = setcod, | |
Id = (λX. ⦇ setdom = X, setcod = X, setfunction = λx. x ⦈), | |
comp = (λg f. ⦇ setdom = setdom f, setcod = setcod g, setfunction = λx. setfunction g (setfunction f x) ⦈) | |
⦈" | |
lemma Set_category: "Category Set" | |
unfolding Set_def Category_def | |
apply (simp add: setmap_eq) | |
by (auto simp add: setmap_def) | |
record ('o,'a,'c,'o2,'a2,'d) Functor = | |
domCat :: "('o,'a,'c) Category_scheme" | |
codCat :: "('o2,'a2,'d) Category_scheme" | |
fobj :: "'o ⇒ 'o2" | |
fmap :: "'a ⇒ 'a2" | |
locale Functor = | |
fixes F :: "('o,'a,'c,'o2,'a2,'d,'f) Functor_scheme" (structure) | |
assumes fdom_category [intro]: "Category (domCat F)" | |
and fcod_category [intro]: "Category (codCat F)" | |
and fobj_mapping [intro]: "X ∈ Obj (domCat F) ⟹ fobj F X ∈ Obj (codCat F)" | |
and fmap_mapping [intro]: "f ∈ Arr (domCat F) ⟹ fmap F f ∈ Arr (codCat F) | |
& Dom (codCat F) (fmap F f) = fobj F (Dom (domCat F) f) | |
& Cod (codCat F) (fmap F f) = fobj F (Cod (domCat F) f)" | |
and preserve_id [simp]: "X ∈ Obj (domCat F) ⟹ fmap F (Id (domCat F) X) = Id (codCat F) (fobj F X)" | |
and covariant [simp]: | |
"⟦ f ∈ Arr (domCat F); g ∈ Arr (domCat F); Cod (domCat F) f = Dom (domCat F) g ⟧ | |
⟹ fmap F (g ∘[domCat F] f) = fmap F g ∘[codCat F] fmap F f" | |
begin | |
lemma fmap_mapping_hom: | |
assumes "f : a -[domCat F]→ b" | |
shows "fmap F f : fobj F a -[codCat F]→ fobj F b" | |
using fmap_mapping [of f] assms by auto | |
lemma fmap_type: | |
assumes "f ∈ Arr (domCat F)" | |
shows "fmap F f : fobj F (Dom (domCat F) f) -[codCat F]→ fobj F (Cod (domCat F) f)" | |
using Category.arr_type assms fmap_mapping by auto | |
end | |
abbreviation Functor_type ("Functor' _ : _ ⟶ _" [81] 90) where | |
"Functor' F : 𝒞 ⟶ 𝒟 ≡ Functor F & domCat F = 𝒞 & codCat F = 𝒟" | |
record ('o,'a,'c,'o2,'a2,'d,'f,'f2) Nat = | |
domFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor" | |
codFunctor :: "('o,'a,'c,'o2,'a2,'d) Functor" | |
component :: "'o ⇒ 'a2" | |
locale Nat = | |
fixes η :: "('o,'a,'c,'o2,'a2,'d,'f,'f2,'n) Nat_scheme" | |
assumes dom_functor [intro]: "Functor' (domFunctor η) : domCat (domFunctor η) ⟶ codCat (domFunctor η)" | |
and cod_functor [intro]: "Functor' (codFunctor η) : domCat (codFunctor η) ⟶ codCat (codFunctor η)" | |
and same_dom [intro]: "domCat (domFunctor η) = domCat (codFunctor η)" | |
and same_cod [intro]: "codCat (domFunctor η) = codCat (codFunctor η)" | |
and component_mapping [intro]: "X ∈ Obj (domCat (domFunctor η)) | |
⟹ component η X : fobj (domFunctor η) X -[codCat (domFunctor η)]→ fobj (codFunctor η) X" | |
and naturality [simp]: | |
"f ∈ Arr (domCat (domFunctor η)) | |
⟹ (component η (Cod (domCat (domFunctor η)) f) ∘[codCat (domFunctor η)] fmap (domFunctor η) f) | |
= (fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η (Dom (domCat (domFunctor η)) f))" | |
begin | |
lemma domFunctor_category [intro]: | |
assumes "Nat η" | |
shows "Category (domCat (domFunctor η)) & Category (codCat (domFunctor η))" | |
by (metis assms Nat.dom_functor Functor.fdom_category Functor.fcod_category) | |
lemma codFunctor_category [intro]: | |
assumes "Nat η" | |
shows "Category (domCat (codFunctor η)) & Category (codCat (codFunctor η))" | |
by (metis assms Nat.cod_functor Functor.fdom_category Functor.fcod_category) | |
lemma naturality_hom [intro]: | |
assumes "f ∈ Arr (domCat (domFunctor η))" | |
shows "⟦ a ∈ Obj (domCat (domFunctor η)); b ∈ Obj (domCat (domFunctor η)); f : a -[domCat (domFunctor η)]→ b ⟧ | |
⟹ (component η b ∘[codCat (domFunctor η)] fmap (domFunctor η) f) | |
= (fmap (codFunctor η) f ∘[codCat (domFunctor η)] component η a)" | |
by auto | |
end | |
abbreviation Nat_type ("Nat' _ : _ ⟶ _" [81] 90) where | |
"Nat' η : F ⟶ G ≡ Nat η & Nat.domFunctor η = F & Nat.codFunctor η = G" | |
axiomatization where | |
nat_eq [iff]: "⟦ Functor' F: 𝒞 ⟶ 𝒟; Functor' G: 𝒞 ⟶ 𝒟; Nat' η: F ⟶ G; Nat' ε: F ⟶ G; (∀X∈Obj 𝒞. component η X = component ε X) ⟧ | |
⟹ η = ε" | |
definition idNat where | |
"idNat F ≡ ⦇ domFunctor = F, codFunctor = F, component = λX. Id (codCat F) (fobj F X) ⦈" | |
lemma idNat_nat: | |
assumes "Functor F" | |
shows "Nat' (idNat F) : F ⟶ F" | |
unfolding idNat_def Nat_def apply (auto simp add: assms) | |
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms) | |
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms) | |
apply (metis Category.id_exist Functor.fcod_category Functor.fobj_mapping assms) | |
proof- | |
fix f | |
assume f_in: "f ∈ Arr (domCat F)" | |
have codF_cat: "Category (codCat F)" using assms Functor.fcod_category by auto | |
have Ff_type: "fmap F f : fobj F (dom⇘domCat F⇙ f) -[codCat F]→ fobj F (cod⇘domCat F⇙ f)" | |
using Functor.fmap_type [of F f] assms f_in by auto | |
show "((id⇘codCat F⇙ fobj F (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) = fmap F f ∘[codCat F] id⇘codCat F⇙ fobj F (dom⇘domCat F⇙ f)" | |
proof- | |
have "((id⇘codCat F⇙ fobj F (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) = fmap F f" | |
using Category.left_id codF_cat Ff_type by (metis (mono_tags, lifting) mem_Collect_eq) | |
also have "… = fmap F f ∘[codCat F] id⇘codCat F⇙ fobj F (dom⇘domCat F⇙ f)" | |
using Category.right_id codF_cat Ff_type by (metis (mono_tags, lifting) mem_Collect_eq) | |
finally show ?thesis by auto | |
qed | |
qed | |
definition compNat ("Nat'[_ ∘ _]") where | |
"compNat η ε ≡ ⦇ | |
domFunctor = Nat.domFunctor ε, codFunctor = Nat.codFunctor η, | |
component = λX. Category.comp (codCat (Nat.domFunctor η)) (component η X) (component ε X) | |
⦈" | |
lemma compNat_nat: | |
assumes η_nat: "Nat' η : G ⟶ H" | |
and ε_nat: "Nat' ε : F ⟶ G" | |
shows "Nat' (compNat η ε) : F ⟶ H" | |
unfolding compNat_def | |
apply (auto simp add: Nat_def η_nat ε_nat) | |
using Nat.dom_functor ε_nat apply fastforce | |
using Nat.cod_functor η_nat apply fastforce | |
using Nat.same_dom [of η] η_nat Nat.same_dom [of ε] ε_nat apply fastforce | |
using Nat.same_cod [of η] η_nat Nat.same_cod [of ε] ε_nat apply fastforce | |
proof - | |
def 𝒞 ≡ "domCat F" | |
def 𝒟 ≡ "codCat F" | |
have F_functor: "Functor' F : 𝒞 ⟶ 𝒟" using Nat.dom_functor [of ε] by (auto simp add: ε_nat 𝒞_def 𝒟_def) | |
have G_functor: "Functor' G : 𝒞 ⟶ 𝒟" using Nat.same_dom [of ε] Nat.same_cod [of ε] ε_nat by (metis Nat.dom_functor 𝒞_def 𝒟_def η_nat) | |
have H_functor: "Functor' H : 𝒞 ⟶ 𝒟" using Nat.dom_functor [of η] by (metis G_functor Nat.cod_functor Nat.same_cod Nat.same_dom η_nat) | |
have C_cat: "Category 𝒞" by (metis Functor.fdom_category F_functor) | |
have D_cat: "Category 𝒟" by (metis Functor.fcod_category F_functor) | |
{ | |
fix X | |
assume X_in: "X ∈ Obj (domCat F)" | |
have ηεX_type: "(component η X ∘[codCat G] component ε X) : fobj F X -[codCat F]→ fobj H X" | |
using X_in Nat.component_mapping [of η] Nat.component_mapping [of ε] | |
apply (auto simp add: η_nat ε_nat) | |
apply (auto simp add: G_functor F_functor) | |
by (auto simp add: D_cat Category.comp_exist) | |
show "(component η X ∘[codCat G] component ε X) ∈ Arr (codCat F)" using ηεX_type by auto | |
show "dom⇘codCat F⇙ (component η X ∘[codCat G] component ε X) = fobj F X" using ηεX_type by auto | |
show "cod⇘codCat F⇙ (component η X ∘[codCat G] component ε X) = fobj H X" using ηεX_type by auto | |
} | |
{ | |
fix f | |
assume f_in: "f ∈ Arr (domCat F)" | |
show "((component η (cod⇘domCat F⇙ f) ∘[codCat G] component ε (cod⇘domCat F⇙ f)) ∘[codCat F] fmap F f) = | |
(fmap H f ∘[codCat F] (component η (dom⇘domCat F⇙ f) ∘[codCat G] component ε (dom⇘domCat F⇙ f)))" | |
proof (auto simp add: F_functor G_functor) | |
have 1: "component η (cod⇘𝒞⇙ f) : fobj G (cod⇘𝒞⇙ f) -[𝒟]→ fobj H (cod⇘𝒞⇙ f)" | |
using Nat.component_mapping [of η] η_nat f_in apply (simp add: F_functor G_functor) | |
using C_cat Category.cod_obj by fastforce | |
have 2: "component ε (cod⇘𝒞⇙ f) : fobj F (cod⇘𝒞⇙ f) -[𝒟]→ fobj G (cod⇘𝒞⇙ f)" | |
using Nat.component_mapping [of ε] ε_nat f_in apply (simp add: F_functor G_functor) | |
using C_cat Category.cod_obj by fastforce | |
have 3: "fmap F f : fobj F (dom⇘𝒞⇙ f) -[𝒟]→ fobj F (cod⇘𝒞⇙ f)" | |
using Functor.fmap_type [of F f] f_in by (simp add: F_functor) | |
have 4: "component ε (dom⇘𝒞⇙ f) : fobj F (dom⇘𝒞⇙ f) -[𝒟]→ fobj G (dom⇘𝒞⇙ f)" | |
using Nat.component_mapping [of ε] ε_nat f_in apply (simp add: F_functor G_functor) | |
using C_cat Category.dom_obj by fastforce | |
have 5: "fmap G f : fobj G (dom⇘𝒞⇙ f) -[𝒟]→ fobj G (cod⇘𝒞⇙ f)" | |
using Functor.fmap_type [of G f] f_in by (simp add: F_functor G_functor) | |
have 6: "component η (dom⇘𝒞⇙ f) : fobj G (dom⇘𝒞⇙ f) -[𝒟]→ fobj H (dom⇘𝒞⇙ f)" | |
using Nat.component_mapping [of η] η_nat f_in apply (simp add: F_functor G_functor) | |
using C_cat Category.dom_obj by fastforce | |
have 7: "fmap H f : fobj H (dom⇘𝒞⇙ f) -[𝒟]→ fobj H (cod⇘𝒞⇙ f)" | |
using Functor.fmap_type [of H f] f_in by (simp add: F_functor H_functor) | |
have "((component η (cod⇘𝒞⇙ f) ∘[𝒟] component ε (cod⇘𝒞⇙ f)) ∘[𝒟] fmap F f) | |
= component η (cod⇘𝒞⇙ f) ∘[𝒟] (component ε (cod⇘𝒞⇙ f) ∘[𝒟] fmap F f)" | |
using Category.assoc [OF D_cat] 1 2 3 by auto | |
also have "… = component η (cod⇘𝒞⇙ f) ∘[𝒟] (fmap G f ∘[𝒟] component ε (dom⇘𝒞⇙ f))" | |
using Nat.naturality [of ε f] f_in by (simp add: ε_nat F_functor) | |
also have "… = (component η (cod⇘𝒞⇙ f) ∘[𝒟] fmap G f) ∘[𝒟] component ε (dom⇘𝒞⇙ f)" | |
using Category.assoc [OF D_cat] 1 4 5 by auto | |
also have "… = (fmap H f ∘[𝒟] component η (dom⇘𝒞⇙ f)) ∘[𝒟] component ε (dom⇘𝒞⇙ f)" | |
using Nat.naturality [of η f] f_in by (simp add: η_nat F_functor G_functor) | |
also have "… = fmap H f ∘[𝒟] (component η (dom⇘𝒞⇙ f) ∘[𝒟] component ε (dom⇘𝒞⇙ f))" | |
using Category.assoc [OF D_cat] 4 6 7 by auto | |
finally | |
show "((component η (cod⇘𝒞⇙ f) ∘[𝒟] component ε (cod⇘𝒞⇙ f)) ∘[𝒟] fmap F f) = | |
fmap H f ∘[𝒟] (component η (dom⇘𝒞⇙ f) ∘[𝒟] component ε (dom⇘𝒞⇙ f))" | |
by auto | |
qed | |
} | |
qed | |
definition FunCat where | |
"FunCat 𝒞 𝒟 = ⦇ | |
Obj = {F. Functor' F : 𝒞 ⟶ 𝒟}, | |
Arr = {η. ∃F∈{F. Functor' F : 𝒞 ⟶ 𝒟}. ∃G∈{F. Functor' F : 𝒞 ⟶ 𝒟}. Nat' η : F ⟶ G}, | |
Dom = domFunctor, | |
Cod = codFunctor, | |
Id = idNat, | |
comp = compNat | |
⦈" | |
lemma FunCat_category: | |
assumes C_cat: "Category 𝒞" and D_cat: "Category 𝒟" | |
shows "Category (FunCat 𝒞 𝒟)" (is "Category ?FC") | |
proof | |
fix f | |
assume f_in: "f ∈ Arr ?FC" | |
show "dom⇘FunCat 𝒞 𝒟⇙ f ∈ Obj (FunCat 𝒞 𝒟)" using f_in unfolding FunCat_def by auto | |
show "cod⇘FunCat 𝒞 𝒟⇙ f ∈ Obj (FunCat 𝒞 𝒟)" using f_in unfolding FunCat_def by auto | |
next | |
fix F | |
assume F_in: "F ∈ Obj ?FC" | |
show "id⇘FunCat 𝒞 𝒟⇙ F ∈ Arr (FunCat 𝒞 𝒟) ∧ dom⇘FunCat 𝒞 𝒟⇙ id⇘FunCat 𝒞 𝒟⇙ F = F ∧ cod⇘FunCat 𝒞 𝒟⇙ id⇘FunCat 𝒞 𝒟⇙ F = F" | |
using F_in unfolding FunCat_def by (auto simp add: idNat_nat [of F]) | |
next | |
fix f g | |
assume 0: "f ∈ Arr ?FC" "g ∈ Arr ?FC" "cod⇘FunCat 𝒞 𝒟⇙ f = dom⇘FunCat 𝒞 𝒟⇙ g" | |
then obtain F G H where | |
F_functor: "(Functor' F : 𝒞 ⟶ 𝒟)" and G_functor: "(Functor' G : 𝒞 ⟶ 𝒟)" and H_functor: "(Functor' H : 𝒞 ⟶ 𝒟)" and | |
f_nat: "(Nat' f : F ⟶ G)" and g_nat: "(Nat' g : G ⟶ H)" | |
unfolding FunCat_def by auto | |
show "((g ∘[?FC] f) ∈ Arr ?FC) ∧ (dom⇘?FC⇙ (g ∘[?FC] f) = dom⇘?FC⇙ f) ∧ (cod⇘?FC⇙ (g ∘[?FC] f) = cod⇘?FC⇙ g)" | |
using compNat_nat [OF g_nat f_nat] unfolding compNat_def apply simp | |
unfolding FunCat_def apply simp | |
by (auto simp add: compNat_def f_nat g_nat F_functor G_functor H_functor) | |
next | |
fix f | |
assume f_in: "f ∈ Arr ?FC" | |
hence f_nat: "∃F∈Obj ?FC. ∃G∈Obj ?FC. Nat' f : F ⟶ G" unfolding FunCat_def by auto | |
then obtain F G where | |
FG: "Functor' F : 𝒞 ⟶ 𝒟" "Functor' G : 𝒞 ⟶ 𝒟" "Nat' f : F ⟶ G" | |
unfolding FunCat_def by auto | |
show "((id⇘?FC⇙ (cod⇘?FC⇙ f)) ∘[?FC] f) = f" | |
unfolding FunCat_def apply auto | |
proof (rule_tac nat_eq [of F 𝒞 𝒟 G] , auto simp add: FG) | |
show "Category.Nat Nat[idNat G ∘ f]" using compNat_nat [of _ G G f F] FG idNat_nat [of G] by auto | |
show "domFunctor Nat[idNat G ∘ f] = F" unfolding compNat_def by (auto simp add: FG) | |
show "codFunctor Nat[idNat G ∘ f] = G" unfolding compNat_def idNat_def by auto | |
{ | |
fix X | |
assume X_in: "X ∈ Obj 𝒞" | |
show "component Nat[idNat G ∘ f] X = component f X" | |
unfolding compNat_def idNat_def | |
proof (auto simp add: FG) | |
have "component f X : fobj F X -[𝒟]→ fobj G X" using Nat.component_mapping [of f X] FG X_in by fastforce | |
thus "((id⇘𝒟⇙ fobj G X) ∘[𝒟] component f X) = component f X" using Category.left_id [OF D_cat] by fastforce | |
qed | |
} | |
qed | |
show "(f ∘[?FC] id⇘?FC⇙ dom⇘?FC⇙ f) = f" | |
unfolding FunCat_def apply simp | |
proof (rule_tac nat_eq , auto simp add: FG) | |
show "Category.Nat Nat[f ∘ idNat F]" using compNat_nat [of f F G _ F] idNat_nat FG by auto | |
show "domFunctor Nat[f ∘ idNat F] = F" unfolding compNat_def idNat_def by auto | |
show "codFunctor Nat[f ∘ idNat F] = G" unfolding compNat_def by (auto simp add: FG) | |
{ | |
fix X | |
assume X_in: "X ∈ Obj 𝒞" | |
show "component Nat[f ∘ idNat F] X = component f X" | |
unfolding compNat_def idNat_def | |
proof (auto simp add: FG) | |
have "component f X : fobj F X -[𝒟]→ fobj G X" using Nat.component_mapping [of f X] FG X_in by fastforce | |
thus "(component f X ∘[𝒟] (id⇘𝒟⇙ fobj F X)) = component f X" using Category.right_id [OF D_cat] by fastforce | |
qed | |
} | |
qed | |
next | |
fix f g h | |
assume "f ∈ Arr ?FC" "g ∈ Arr ?FC" "h ∈ Arr ?FC" "cod⇘FunCat 𝒞 𝒟⇙ f = dom⇘FunCat 𝒞 𝒟⇙ g" "cod⇘FunCat 𝒞 𝒟⇙ g = dom⇘FunCat 𝒞 𝒟⇙ h" | |
then obtain F G H I where | |
FGHI: "Functor' F: 𝒞 ⟶ 𝒟" "Functor' G: 𝒞 ⟶ 𝒟" "Functor' H: 𝒞 ⟶ 𝒟" "Functor' I: 𝒞 ⟶ 𝒟" and | |
fgh_nat: "Nat' f : F ⟶ G" "Nat' g : G ⟶ H" "Nat' h : H ⟶ I" | |
unfolding FunCat_def by auto | |
have 1: "Nat' ((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) : F ⟶ I" | |
unfolding FunCat_def by (auto simp add: compNat_nat fgh_nat) | |
have 2: "Nat' (h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)) : F ⟶ I" | |
unfolding FunCat_def by (auto simp add: compNat_nat fgh_nat) | |
show "((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) = h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)" | |
apply (rule_tac nat_eq [of F 𝒞 𝒟 I]) | |
apply (auto simp add: FGHI(1) FGHI(4)) | |
apply (auto simp add: 1 2) | |
proof- | |
fix X | |
assume X_in: "X ∈ Obj 𝒞" | |
show "component ((h ∘[FunCat 𝒞 𝒟] g) ∘[FunCat 𝒞 𝒟] f) X = component (h ∘[FunCat 𝒞 𝒟] (g ∘[FunCat 𝒞 𝒟] f)) X" | |
unfolding FunCat_def apply simp | |
unfolding compNat_def apply simp | |
proof (simp add: fgh_nat FGHI) | |
have 1: "component h X : fobj H X -[𝒟]→ fobj I X" using fgh_nat(3) Nat.component_mapping [of h X] X_in FGHI by auto | |
have 2: "component g X : fobj G X -[𝒟]→ fobj H X" using fgh_nat(2) Nat.component_mapping [of g X] X_in FGHI by auto | |
have 3: "component f X : fobj F X -[𝒟]→ fobj G X" using fgh_nat(1) Nat.component_mapping [of f X] X_in FGHI by auto | |
show "((component h X ∘[𝒟] component g X) ∘[𝒟] component f X) = component h X ∘[𝒟] (component g X ∘[𝒟] component f X)" | |
using Category.assoc [OF D_cat] 1 2 3 by auto | |
qed | |
qed | |
qed | |
definition Presheaf ("PSh(_)") where | |
"PSh(𝒞) ≡ FunCat (𝒞 {^op}) Set" | |
definition contraHom ("Hom{_}[-,_]") where | |
"Hom{𝒞}[-,r] ≡ ⦇ | |
domCat = 𝒞 {^op}, | |
codCat = Set, | |
fobj = λx. Category.Hom 𝒞 x r, | |
fmap = λf. ⦇ setdom = Category.Hom 𝒞 (Cod 𝒞 f) r, setcod = Category.Hom 𝒞 (Dom 𝒞 f) r, setfunction = λu. u ∘[𝒞] f ⦈ | |
⦈" | |
lemma contraHom_functor: | |
assumes C_cat: "Category 𝒞" and r_in: "r ∈ Obj 𝒞" | |
shows "Functor' Hom{𝒞}[-,r] : 𝒞 {^op} ⟶ Set" | |
unfolding Functor_def contraHom_def apply simp | |
apply (auto simp add: C_cat opposite_category) | |
apply (auto simp add: Set_category) | |
proof - | |
fix X assume "X ∈ Obj (𝒞 {^op})" show "Category.Hom 𝒞 X r ∈ Obj Set" unfolding Set_def by auto | |
next | |
fix f assume "f ∈ Arr (𝒞 {^op})" | |
thus "⦇setdom = Category.Hom 𝒞 (cod⇘𝒞⇙ f) r, setcod = Category.Hom 𝒞 (dom⇘𝒞⇙ f) r, setfunction = λu. u ∘[𝒞] f⦈ ∈ Arr Set" | |
unfolding Set_def setmap_def opposite_def by (auto simp add: Category.comp_exist C_cat) | |
next | |
fix f x | |
assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ dom⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈" | |
show "x ∈ Arr 𝒞" using assm unfolding Set_def by auto | |
show "dom⇘𝒞⇙ x = dom⇘𝒞 {^op}⇙ f" using assm unfolding opposite_def Set_def by auto | |
show "cod⇘𝒞⇙ x = r" using assm unfolding Set_def by auto | |
next | |
fix f x | |
assume "f ∈ Arr (𝒞 {^op})" "x ∈ Arr 𝒞" "dom⇘𝒞⇙ x = dom⇘𝒞 {^op}⇙ f" "r = cod⇘𝒞⇙ x" | |
thus "x ∈ dom⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setfunction = λu. u ∘[𝒞] f⦈" | |
unfolding Set_def opposite_def by auto | |
next | |
fix f x | |
assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ cod⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈" | |
show "x ∈ Arr 𝒞" using assm unfolding Set_def by auto | |
show "dom⇘𝒞⇙ x = cod⇘𝒞 {^op}⇙ f" using assm unfolding Set_def opposite_def by auto | |
show "cod⇘𝒞⇙ x = r" using assm unfolding Set_def opposite_def by auto | |
next | |
fix f x | |
assume assm: "f ∈ Arr (𝒞 {^op})" "x ∈ Arr 𝒞" "dom⇘𝒞⇙ x = cod⇘𝒞 {^op}⇙ f" "r = cod⇘𝒞⇙ x" | |
show "x ∈ cod⇘Set⇙ ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ cod⇘𝒞⇙ x, setfunction = λu. u ∘[𝒞] f⦈" | |
using assm unfolding Set_def opposite_def by auto | |
next | |
fix X | |
assume "X ∈ Obj (𝒞 {^op})" | |
thus "⦇setdom = (cod⇘𝒞⇙ (id⇘𝒞 {^op}⇙ X)) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ (id⇘𝒞 {^op}⇙ X)) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] (id⇘𝒞 {^op}⇙ X)⦈ = id⇘Set⇙ (X -[𝒞]→ r)" | |
apply (rule_tac setmap_eq) | |
apply (auto simp add: opposite_def setmap_def) | |
apply (auto simp add: C_cat Category.id_exist Category.right_id Category.left_id) | |
by (auto simp add: Set_def) | |
next | |
fix f g | |
assume "f ∈ Arr (𝒞 {^op})" "g ∈ Arr (𝒞 {^op})" "cod⇘𝒞 {^op}⇙ f = dom⇘𝒞 {^op}⇙ g" | |
thus "⦇setdom = (cod⇘𝒞⇙ (g ∘[𝒞 {^op}] f)) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ (g ∘[𝒞 {^op}] f)) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] (g ∘[𝒞 {^op}] f)⦈ = | |
⦇setdom = (cod⇘𝒞⇙ g) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ g) -[𝒞]→ r, | |
setfunction = λu. u ∘[𝒞] g⦈ ∘[Set] ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = (dom⇘𝒞⇙ f) -[𝒞]→ r, setfunction = λu. u ∘[𝒞] f⦈" | |
unfolding Set_def opposite_def | |
apply (rule_tac setmap_eq) | |
apply (auto simp add: setmap_def) | |
by (auto simp add: C_cat Category.assoc Category.comp_exist) | |
qed | |
definition contraHomNat ("HomNat{_}[-,_]") where | |
"HomNat{𝒞}[-,f] ≡ ⦇ | |
domFunctor = Hom{𝒞}[-,Dom 𝒞 f], | |
codFunctor = Hom{𝒞}[-,Cod 𝒞 f], | |
component = λx. ⦇ setdom = Category.Hom 𝒞 x (Dom 𝒞 f), setcod = Category.Hom 𝒞 x (Cod 𝒞 f), setfunction = λu. f ∘[𝒞] u ⦈ | |
⦈" | |
lemma contraHomNat_nat: | |
assumes C_cat: "Category 𝒞" "f ∈ Arr 𝒞" | |
shows "Nat' HomNat{𝒞}[-,f] : Hom{𝒞}[-,Dom 𝒞 f] ⟶ Hom{𝒞}[-,Cod 𝒞 f]" | |
unfolding Nat_def contraHomNat_def | |
apply (auto simp add: contraHom_functor assms Category.dom_obj Category.cod_obj) | |
proof - | |
fix X | |
assume "X ∈ Obj (𝒞 {^op})" thus "⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈ ∈ Arr Set" | |
unfolding Set_def setmap_def by (auto simp add: assms Category.comp_exist) | |
next | |
fix X x | |
assume "X ∈ Obj (𝒞 {^op})" "x ∈ dom⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈" | |
thus "x ∈ fobj Hom{𝒞}[-,dom⇘𝒞⇙ f] X" unfolding opposite_def Set_def contraHom_def by auto | |
next | |
fix X x | |
assume "X ∈ Obj (𝒞 {^op})" "x ∈ fobj Hom{𝒞}[-,dom⇘𝒞⇙ f] X" | |
thus "x ∈ dom⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈" | |
unfolding opposite_def contraHom_def Set_def by auto | |
next | |
fix X x | |
assume "X ∈ Obj (𝒞 {^op})" "x ∈ cod⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈" | |
thus "x ∈ fobj Hom{𝒞}[-,cod⇘𝒞⇙ f] X" | |
unfolding opposite_def contraHom_def Set_def by auto | |
next | |
fix X x | |
assume "X ∈ Obj (𝒞 {^op})" "x ∈ fobj Hom{𝒞}[-,cod⇘𝒞⇙ f] X" | |
thus "x ∈ cod⇘Set⇙ ⦇setdom = X -[𝒞]→ dom⇘𝒞⇙ f, setcod = X -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈" | |
unfolding opposite_def contraHom_def Set_def by auto | |
next | |
fix fa | |
assume "fa ∈ Arr (𝒞 {^op})" | |
thus "(⦇setdom = (cod⇘𝒞 {^op}⇙ fa) -[𝒞]→ dom⇘𝒞⇙ f, setcod = (cod⇘𝒞 {^op}⇙ fa) -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈ | |
∘[Set] (fmap Hom{𝒞}[-,dom⇘𝒞⇙ f] fa)) = | |
fmap Hom{𝒞}[-,cod⇘𝒞⇙ f] fa | |
∘[Set] ⦇setdom = (dom⇘𝒞 {^op}⇙ fa) -[𝒞]→ dom⇘𝒞⇙ f, setcod = (dom⇘𝒞 {^op}⇙ fa) -[𝒞]→ cod⇘𝒞⇙ f, setfunction = comp_category f 𝒞⦈" | |
apply (rule_tac setmap_eq) | |
unfolding setmap_def opposite_def Set_def contraHom_def | |
apply (auto simp add: assms Category.comp_exist) | |
apply (auto simp add: assms Category.assoc) | |
done | |
qed | |
lemma setmap_functor_fmap: | |
assumes "Functor' F : 𝒞 ⟶ Set" "f ∈ Arr 𝒞" | |
shows "setmap (fmap F f)" | |
using assms Functor.fmap_type unfolding Set_def by fastforce | |
lemma setmap_nat_component: | |
assumes "Nat η" "Functor' (domFunctor η) : 𝒞 ⟶ Set" "X ∈ Obj 𝒞" | |
shows "setmap (component η X)" | |
using assms Nat.component_mapping unfolding Set_def by fastforce | |
definition yoneda where | |
"yoneda 𝒞 ≡ ⦇ | |
domCat = 𝒞, | |
codCat = PSh(𝒞), | |
fobj = contraHom 𝒞, | |
fmap = contraHomNat 𝒞 | |
⦈" | |
lemma yoneda_functor: | |
assumes "Category 𝒞" | |
shows "Functor' (yoneda 𝒞) : 𝒞 ⟶ PSh(𝒞)" | |
unfolding Functor_def apply auto | |
unfolding yoneda_def Presheaf_def | |
apply (auto simp add: assms FunCat_category opposite_category Set_category) | |
apply (auto simp add: assms FunCat_def contraHom_functor contraHomNat_nat) | |
apply (auto simp add: assms Category.dom_obj Category.cod_obj FunCat_def contraHom_functor) | |
proof- | |
fix X | |
assume "X ∈ Obj 𝒞" thus "HomNat{𝒞}[-,id⇘𝒞⇙ X] = idNat Hom{𝒞}[-,X]" | |
apply (rule_tac nat_eq) | |
apply (auto simp add: assms Category.id_exist Nat.dom_functor contraHomNat_nat) | |
apply (auto simp add: assms contraHom_functor idNat_nat) | |
proof - | |
fix Xa | |
assume "X ∈ Obj 𝒞" "Xa ∈ Obj (𝒞 {^op})" | |
thus "component HomNat{𝒞}[-,id⇘𝒞⇙ X] Xa = component (idNat Hom{𝒞}[-,X]) Xa" | |
unfolding contraHomNat_def apply auto | |
unfolding idNat_def apply auto | |
unfolding contraHom_def apply auto | |
apply (auto simp add: assms Category.id_exist) | |
apply (rule setmap_eq) | |
by (auto simp add: setmap_def Set_def assms Category.left_id Category.right_id) | |
qed | |
next | |
fix f g | |
assume fg: "f ∈ Arr 𝒞" "g ∈ Arr 𝒞" "cod⇘𝒞⇙ f = dom⇘𝒞⇙ g" | |
hence gf:"(g ∘[𝒞] f) ∈ Arr 𝒞" by (auto simp add: assms Category.comp_exist) | |
let ?Cop = "𝒞 {^op}" | |
show "HomNat{𝒞}[-,g ∘[𝒞] f] = Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]]" (is "?L = ?R") | |
apply (rule_tac nat_eq [of _ ?Cop Set _ ?L ?R] , auto) | |
apply (auto simp add: contraHomNat_nat fg assms Category.comp_exist) | |
apply (auto simp add: contraHom_functor Category.dom_obj Category.cod_obj fg assms) | |
apply (auto simp add: compNat_nat contraHomNat_nat fg assms) | |
proof - | |
fix X | |
assume X_in: "X ∈ Obj (𝒞 {^op})" | |
show "component HomNat{𝒞}[-,g ∘[𝒞] f] X = component Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]] X" (is "?L = ?R") | |
proof - | |
have "setmap ?L" | |
using setmap_nat_component [OF _ _ X_in] contraHom_functor [OF assms] contraHomNat_nat [OF assms gf] | |
using Category.cod_obj [OF assms gf] Nat.dom_functor Nat.same_cod Nat.same_dom by metis | |
moreover have "setmap ?R" | |
using setmap_nat_component [OF _ _ X_in] contraHom_functor [OF assms] contraHomNat_nat [OF assms] fg | |
using Category.dom_obj [OF assms fg(1)] compNat_nat by metis | |
moreover have "setdom ?L = setdom ?R" | |
proof- | |
have 0: "setdom ?L = X -[𝒞]→ (dom⇘𝒞⇙ (g ∘[𝒞] f))" | |
unfolding contraHomNat_def by auto | |
have "setdom ?R = setdom (component HomNat{𝒞}[-,g] X ∘[codCat (domFunctor HomNat{𝒞}[-,g])] component HomNat{𝒞}[-,f] X)" | |
unfolding compNat_def by auto | |
also have "… = setdom (component HomNat{𝒞}[-,g] X ∘[Set] component HomNat{𝒞}[-,f] X)" | |
unfolding contraHomNat_def contraHom_functor fg X_in by (simp add: contraHom_def) | |
also have "… = setdom (component HomNat{𝒞}[-,f] X)" | |
unfolding Set_def by auto | |
also have "… = X -[𝒞]→ (dom⇘𝒞⇙ f)" | |
unfolding contraHomNat_def by auto | |
finally | |
show ?thesis using 0 assms Category.comp_exist fg by fastforce | |
qed | |
moreover have "setcod ?L = setcod ?R" | |
proof- | |
have 0: "setcod ?L = X -[𝒞]→ (cod⇘𝒞⇙ (g ∘[𝒞] f))" | |
unfolding contraHomNat_def by auto | |
have "setcod ?R = setcod (component HomNat{𝒞}[-,g] X ∘[codCat (domFunctor HomNat{𝒞}[-,g])] component HomNat{𝒞}[-,f] X)" | |
unfolding compNat_def by auto | |
also have "… = setcod (component HomNat{𝒞}[-,g] X ∘[Set] component HomNat{𝒞}[-,f] X)" | |
unfolding contraHomNat_def contraHom_functor fg X_in by (simp add: contraHom_def) | |
also have "… = setcod (component HomNat{𝒞}[-,g] X)" | |
unfolding Set_def by auto | |
also have "… = X -[𝒞]→ (cod⇘𝒞⇙ g)" | |
unfolding contraHomNat_def by auto | |
finally | |
show ?thesis using 0 assms Category.comp_exist fg by fastforce | |
qed | |
moreover have "∀f∈setdom ?L. setfunction ?L f = setfunction ?R f" | |
proof | |
fix fa | |
assume "fa ∈ setdom (component HomNat{𝒞}[-,g ∘[𝒞] f] X)" | |
hence "fa : X -[𝒞]→ (Dom 𝒞 f)" | |
unfolding contraHomNat_def by (auto simp add: assms fg Category.comp_exist) | |
thus "setfunction (component HomNat{𝒞}[-,g ∘[𝒞] f] X) fa = setfunction (component Nat[HomNat{𝒞}[-,g] ∘ HomNat{𝒞}[-,f]] X) fa" | |
unfolding compNat_def contraHomNat_def contraHom_def Set_def | |
by (auto simp add: assms Category.assoc fg) | |
qed | |
ultimately | |
show ?thesis using setmap_eq [of ?L ?R] by auto | |
qed | |
qed | |
qed | |
abbreviation arrow (infixr "→" 80) where | |
"A → B ≡ {f. ∀x∈A. f x ∈ B}" | |
definition Bijective ("_ ≅ _") where | |
"A ≅ B ≡ ∃f ∈ A → B. ∃g ∈ B → A. (∀x ∈ A. g (f x) = x) & (∀y ∈ B. f (g y) = y)" | |
definition nat_to_obj where | |
"nat_to_obj 𝒞 F r ≡ λα. setfunction (component α r) (Id 𝒞 r)" | |
lemma nat_to_obj_arrow: | |
assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞" | |
shows "nat_to_obj 𝒞 F r : Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F → fobj F r" | |
proof | |
show "∀α∈(fobj (yoneda 𝒞) r -[PSh(𝒞)]→ F). nat_to_obj 𝒞 F r α ∈ fobj F r" | |
proof | |
fix α | |
assume "α ∈ fobj (yoneda 𝒞) r -[PSh(𝒞)]→ F" | |
hence "Nat' α : fobj (yoneda 𝒞) r ⟶ F" | |
unfolding Presheaf_def FunCat_def by auto | |
hence "component α r : Category.Hom 𝒞 r r -[Set]→ fobj F r" | |
proof - | |
have r_in: "r ∈ Obj (𝒞 {^op})" | |
unfolding opposite_def by (auto simp add: assms(3)) | |
assume α_nat: "Nat' α : fobj (yoneda 𝒞) r ⟶ F" | |
hence "Functor' (domFunctor α) : 𝒞 {^op} ⟶ Set" | |
unfolding yoneda_def | |
using contraHom_functor [of 𝒞 r] assms by auto | |
hence "component α r : fobj (domFunctor α) r -[Set]→ fobj (codFunctor α) r" | |
using Nat.component_mapping [of α r] α_nat r_in by auto | |
thus ?thesis | |
using α_nat yoneda_def [of 𝒞] contraHom_def [of 𝒞 r] by auto | |
qed | |
thus "nat_to_obj 𝒞 F r α ∈ fobj F r" | |
unfolding nat_to_obj_def Set_def setmap_def | |
using assms(1) assms (3) Category.id_exist [of 𝒞 r] | |
by auto | |
qed | |
qed | |
definition obj_to_nat where | |
"obj_to_nat 𝒞 F r ≡ λx. ⦇ | |
domFunctor = (fobj (yoneda 𝒞) r), | |
codFunctor = F, | |
component = λd. ⦇ setdom = fobj (fobj (yoneda 𝒞) r) d, setcod = fobj F d | |
, setfunction = λu. setfunction (fmap F u) x ⦈ | |
⦈" | |
lemma obj_to_nat_arrow: | |
assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞" | |
shows "obj_to_nat 𝒞 F r : fobj F r → Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F" | |
proof auto | |
fix x | |
assume x_in: "x ∈ fobj F r" | |
have nat: "Nat' (obj_to_nat 𝒞 F r x) : (fobj (yoneda 𝒞) r) ⟶ F" | |
proof | |
show "Category.Nat (obj_to_nat 𝒞 F r x)" (is "Category.Nat ?f") | |
proof | |
have 1: "Functor' (fobj (yoneda 𝒞) r) : 𝒞 {^op} ⟶ Set" | |
unfolding yoneda_def using contraHom_functor [of 𝒞 r] assms by auto | |
have 2: "Functor' F : 𝒞 {^op} ⟶ Set" using assms(2) unfolding Presheaf_def FunCat_def by auto | |
thus "Functor' (domFunctor ?f) : domCat (domFunctor ?f) ⟶ codCat (domFunctor ?f)" | |
unfolding obj_to_nat_def apply auto | |
using assms(2) unfolding Presheaf_def FunCat_def yoneda_def | |
using contraHom_functor [of 𝒞 r] assms by auto | |
show "Functor' (codFunctor ?f) : domCat (codFunctor ?f) ⟶ codCat (codFunctor ?f)" | |
unfolding obj_to_nat_def using assms(2) unfolding Presheaf_def FunCat_def by auto | |
show "domCat (domFunctor ?f) = domCat (codFunctor ?f)" | |
unfolding obj_to_nat_def using 1 2 by auto | |
show "codCat (domFunctor ?f) = codCat (codFunctor ?f)" | |
unfolding obj_to_nat_def using 1 2 by auto | |
fix xa | |
assume xa_in: "xa ∈ Obj (domCat (domFunctor ?f))" | |
show "component ?f xa ∈ fobj (domFunctor ?f) xa -[codCat (domFunctor ?f)]→ fobj (codFunctor ?f) xa" | |
apply (auto simp add: obj_to_nat_def 1) | |
unfolding Set_def apply auto | |
unfolding yoneda_def apply auto | |
unfolding contraHom_def apply auto | |
proof (unfold setmap_def , auto) | |
fix xb | |
assume xb_assm: "xb ∈ Arr 𝒞" "xa = dom⇘𝒞⇙ xb" "r = cod⇘𝒞⇙ xb" | |
hence "xb : r -[𝒞 {^op}]→ xa" | |
unfolding opposite_def by auto | |
hence Fxb_type: "fmap F xb : fobj F r -[Set]→ fobj F xa" | |
using Functor.fmap_mapping [of F xb] 2 by auto | |
hence "setmap (fmap F xb)" | |
unfolding Set_def by auto | |
thus "setfunction (fmap F xb) x ∈ fobj F (dom⇘𝒞⇙ xb)" | |
unfolding setmap_def using x_in xb_assm Fxb_type | |
unfolding Set_def by auto | |
qed | |
next | |
have 1: "Functor' (fobj (yoneda 𝒞) r) : 𝒞 {^op} ⟶ Set" | |
unfolding yoneda_def using contraHom_functor [of 𝒞 r] assms by auto | |
have 2: "Functor' F : 𝒞 {^op} ⟶ Set" using assms(2) unfolding Presheaf_def FunCat_def by auto | |
fix f | |
assume "f ∈ Arr (domCat (domFunctor ?f))" | |
hence f_in: "f : (cod⇘𝒞⇙ f) -[𝒞 {^op}]→ (dom⇘𝒞⇙ f)" | |
using contraHom_functor [of 𝒞 r] assms | |
unfolding opposite_def obj_to_nat_def yoneda_def | |
by auto | |
show "(component ?f (cod⇘domCat (domFunctor ?f)⇙ f) ∘[codCat (domFunctor ?f)] fmap (domFunctor ?f) f) = | |
(fmap (codFunctor ?f) f ∘[codCat (domFunctor ?f)] component ?f (dom⇘domCat (domFunctor ?f)⇙ f))" | |
apply (auto simp add: obj_to_nat_def 1 opposite_def) | |
unfolding yoneda_def apply auto | |
unfolding contraHom_def apply auto | |
proof (rule setmap_eq , auto simp add: Set_def) | |
show "setmap ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = fobj F (dom⇘𝒞⇙ f), | |
setfunction = λxa. setfunction (fmap F (xa ∘[𝒞] f)) x⦈" | |
unfolding setmap_def | |
proof auto | |
fix xa | |
assume "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa" | |
hence "(f ∘[𝒞 {^op}] xa) : r -[𝒞 {^op}]→ (dom⇘𝒞⇙ f)" | |
using f_in unfolding opposite_def by (auto simp add: Category.comp_exist assms(1)) | |
hence "fmap F (f ∘[𝒞 {^op}] xa) : fobj F r -[Set]→ fobj F (dom⇘𝒞⇙ f)" | |
using Functor.fmap_mapping 2 by fastforce | |
thus "setfunction (fmap F (xa ∘[𝒞] f)) x ∈ fobj F (dom⇘𝒞⇙ f)" | |
unfolding opposite_def Set_def setmap_def using x_in by auto | |
qed | |
show "setmap ⦇setdom = (cod⇘𝒞⇙ f) -[𝒞]→ r, setcod = setcod (fmap F f), | |
setfunction = λxa. setfunction (fmap F f) (setfunction (fmap F xa) x)⦈" | |
unfolding setmap_def | |
proof auto | |
fix xa | |
assume xa_assms: "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa" | |
hence "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)" "fmap F xa : fobj F r -[Set]→ fobj F (dom⇘𝒞⇙ xa)" | |
using Functor.fmap_mapping 2 f_in apply fastforce | |
using Functor.fmap_mapping [of F xa] 2 xa_assms unfolding opposite_def by auto | |
thus "setfunction (fmap F f) (setfunction (fmap F xa) x) ∈ setcod (fmap F f)" | |
unfolding Set_def setmap_def using x_in xa_assms by auto | |
qed | |
next | |
have Ff_type: "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)" | |
using f_in Functor.fmap_type 2 unfolding opposite_def by fastforce | |
fix x | |
assume "x ∈ fobj F (dom⇘𝒞⇙ f)" thus "x ∈ setcod (fmap F f)" | |
using Ff_type unfolding Set_def by auto | |
next | |
have Ff_type: "fmap F f : fobj F (cod⇘𝒞⇙ f) -[Set]→ fobj F (dom⇘𝒞⇙ f)" | |
using f_in Functor.fmap_type 2 unfolding opposite_def by fastforce | |
fix x | |
assume "x ∈ setcod (fmap F f)" thus "x ∈ fobj F (dom⇘𝒞⇙ f)" | |
using Ff_type unfolding Set_def by auto | |
next | |
fix xa | |
assume xa_assms: "xa ∈ Arr 𝒞" "dom⇘𝒞⇙ xa = cod⇘𝒞⇙ f" "r = cod⇘𝒞⇙ xa" | |
have "setfunction (fmap F (f ∘[𝒞 {^op}] xa)) x = setfunction (fmap F f) (setfunction (fmap F xa) x)" (is "?L = ?R") | |
proof- | |
have "?L = setfunction (fmap F f ∘[Set] fmap F xa) x" | |
using Functor.covariant [of F xa f] 2 f_in xa_assms | |
by (metis (no_types, lifting) Category.Category.select_convs(2) Category.Category.select_convs(3) Category.Category.select_convs(4) mem_Collect_eq opposite_def) | |
also have "… = ?R" | |
unfolding Set_def by auto | |
finally show ?thesis by simp | |
qed | |
thus "setfunction (fmap F (xa ∘[𝒞] f)) x = setfunction (fmap F f) (setfunction (fmap F xa) x)" | |
unfolding opposite_def by auto | |
qed | |
qed | |
show "domFunctor (obj_to_nat 𝒞 F r x) = fobj (yoneda 𝒞) r ∧ codFunctor (obj_to_nat 𝒞 F r x) = F" | |
unfolding obj_to_nat_def by auto | |
qed | |
show "obj_to_nat 𝒞 F r x ∈ Arr PSh(𝒞)" | |
unfolding Presheaf_def FunCat_def apply auto | |
using nat apply auto | |
unfolding yoneda_def apply auto | |
using contraHom_functor [OF assms(1) assms(3)] apply auto | |
using assms(2) unfolding Presheaf_def FunCat_def apply auto | |
done | |
show "dom⇘PSh 𝒞⇙ obj_to_nat 𝒞 F r x = fobj (yoneda 𝒞) r" | |
unfolding obj_to_nat_def Presheaf_def FunCat_def by auto | |
show "cod⇘PSh 𝒞⇙ obj_to_nat 𝒞 F r x = F" | |
unfolding obj_to_nat_def Presheaf_def FunCat_def by auto | |
qed | |
lemma YonedaLemma: | |
assumes "Category 𝒞" "F ∈ Obj PSh(𝒞)" "r ∈ Obj 𝒞" | |
shows "(Category.Hom (PSh(𝒞)) (fobj (yoneda 𝒞) r) F) ≅ (fobj F r)" | |
unfolding Bijective_def | |
proof - | |
let ?f = "nat_to_obj 𝒞 F r" | |
let ?g = "obj_to_nat 𝒞 F r" | |
let ?Cop = "𝒞 {^op}" | |
have "?f ∈ (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F) → fobj F r" | |
using nat_to_obj_arrow assms by fastforce | |
moreover have "?g ∈ fobj F r → (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F)" | |
using obj_to_nat_arrow assms by fastforce | |
moreover have "∀x∈fobj (yoneda 𝒞) r -[PSh 𝒞]→ F. ?g (?f x) = x" (is "∀x∈?yoneda -[_]→ _. _") | |
apply auto | |
proof (rule nat_eq [of ?yoneda ?Cop Set F]) | |
fix x | |
assume 1: "x ∈ Arr PSh 𝒞" "dom⇘PSh 𝒞⇙ x = fobj (yoneda 𝒞) r" "F = cod⇘PSh 𝒞⇙ x" | |
hence x_arrow: "x : fobj (yoneda 𝒞) r -[PSh 𝒞]→ F" by auto | |
hence x_nat: "Nat' x : fobj (yoneda 𝒞) r ⟶ F" | |
unfolding Presheaf_def FunCat_def by auto | |
show "Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set" | |
unfolding yoneda_def by (auto simp add: contraHom_functor assms) | |
show "Functor' F : 𝒞 {^op} ⟶ Set" | |
using assms(2) unfolding Presheaf_def FunCat_def by auto | |
show "Nat' obj_to_nat 𝒞 (cod⇘PSh 𝒞⇙ x) r (nat_to_obj 𝒞 (cod⇘PSh 𝒞⇙ x) r x) : fobj (yoneda 𝒞) r ⟶ F" | |
using nat_to_obj_arrow [OF assms] obj_to_nat_arrow [OF assms] x_arrow | |
unfolding Presheaf_def FunCat_def by auto | |
show "Nat' x : fobj (yoneda 𝒞) r ⟶ F" by fact | |
show "∀X∈Obj (𝒞 {^op}). component (obj_to_nat 𝒞 (cod⇘PSh 𝒞⇙ x) r (nat_to_obj 𝒞 (cod⇘PSh 𝒞⇙ x) r x)) X = component x X" | |
apply (auto simp add: `F = cod⇘PSh 𝒞⇙ x` [symmetric]) | |
proof (rule_tac setmap_eq) | |
fix X assume X_in: "X ∈ Obj (𝒞 {^op})" | |
have 2: "nat_to_obj 𝒞 F r x ∈ fobj F r" | |
using nat_to_obj_arrow [OF assms] | |
using x_arrow by auto | |
have "Nat (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x))" | |
using obj_to_nat_arrow [OF assms] 2 unfolding Presheaf_def FunCat_def by auto | |
moreover have "Functor' (domFunctor (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x))) : 𝒞 {^op} ⟶ Set" | |
unfolding obj_to_nat_def yoneda_def using contraHom_functor [OF assms(1) assms(3)] by auto | |
ultimately | |
show "setmap (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X)" | |
using setmap_nat_component [OF _ _ X_in] by auto | |
show "setmap (component x X)" | |
using setmap_nat_component [OF _ _ X_in] x_nat unfolding yoneda_def | |
by (metis `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` yoneda_def) | |
show "setdom (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) = setdom (component x X)" | |
unfolding obj_to_nat_def nat_to_obj_def apply simp | |
using Nat.component_mapping [of x X] apply (simp add: x_nat) | |
by (simp add: `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` Set_def X_in) | |
show "setcod (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) = setcod (component x X)" | |
unfolding obj_to_nat_def nat_to_obj_def apply simp | |
using Nat.component_mapping [of x X] apply (simp add: x_nat) | |
by (simp add: `Functor' fobj (yoneda 𝒞) r : 𝒞 {^op} ⟶ Set` Set_def X_in) | |
show "∀xa∈setdom (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X). | |
setfunction (component (obj_to_nat 𝒞 F r (nat_to_obj 𝒞 F r x)) X) xa = | |
setfunction (component x X) xa" | |
unfolding obj_to_nat_def nat_to_obj_def yoneda_def apply simp | |
unfolding contraHom_def | |
proof auto | |
fix xa assume xa_assms: "xa ∈ Arr 𝒞" "X = dom⇘𝒞⇙ xa" "r = cod⇘𝒞⇙ xa" | |
have "(fmap F xa ∘[Set] component x r) = component x X ∘[Set] fmap (fobj (yoneda 𝒞) r) xa" | |
using Nat.naturality [of x xa] x_nat apply auto | |
unfolding yoneda_def apply simp unfolding contraHom_def apply simp | |
unfolding opposite_def by (auto simp add: xa_assms) | |
hence 2: "setfunction (fmap F xa) (setfunction (component x r) (id⇘𝒞⇙ r)) | |
= setfunction (component x X) (setfunction (fmap (fobj (yoneda 𝒞) r) xa) (id⇘𝒞⇙ r))" | |
unfolding Set_def apply auto by metis | |
show "setfunction (fmap F xa) (setfunction (component x (cod⇘𝒞⇙ xa)) (id⇘𝒞⇙ cod⇘𝒞⇙ xa)) = | |
setfunction (component x (dom⇘𝒞⇙ xa)) xa" | |
apply (auto simp add: xa_assms(2) [symmetric] xa_assms(3) [symmetric]) | |
apply (auto simp add: 2) | |
unfolding yoneda_def apply simp | |
unfolding contraHom_def apply simp | |
using Category.left_id [OF assms(1) xa_assms(1)] xa_assms(3) by auto | |
qed | |
qed | |
qed | |
moreover have "∀y∈fobj F r. ?f (?g y) = y" | |
apply auto | |
unfolding nat_to_obj_def obj_to_nat_def apply simp | |
using Functor.preserve_id [of F r] assms | |
unfolding Presheaf_def FunCat_def opposite_def apply auto | |
unfolding Set_def by simp | |
ultimately | |
show "∃f∈(fobj (yoneda 𝒞) r -[PSh 𝒞]→ F) → fobj F r. ∃g∈fobj F r → (fobj (yoneda 𝒞) r -[PSh 𝒞]→ F). | |
(∀x∈fobj (yoneda 𝒞) r -[PSh 𝒞]→ F. g (f x) = x) ∧ (∀y∈fobj F r. f (g y) = y)" | |
by auto | |
qed | |
end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment