Theory SetsCat
chapter "The Category of Small Sets"
theory SetsCat
imports Category3.SetCat Category3.CategoryWithPullbacks Category3.CartesianClosedCategory
Category3.EquivalenceOfCategories Category3.Colimit Universe
begin
text‹
In this section we consider the category of small sets and functions between
them as an exemplifying instance of the pattern we propose for working with large categories
in HOL. We define a locale ‹sets_cat›, which axiomatizes a category with terminal object,
such that each object determines a ``small'' set (the set of its global elements),
there is an object corresponding to any externally given small set, and such that
the hom-sets between objects are in bijection with the small extensional functions
between sets of global elements. We show that this locale characterizes the category
of small sets and functions, in the sense that, for a fixed notion of smallness,
any two interpretations of the ‹sets_cat› locale are equivalent as categories.
We then proceed to derive various familiar properties of a category of sets; assuming
in each case that the notion of ``smallness'' satisfies suitable conditions as defined
in the theory ‹Smallness›, and that the collection of all arrows of the
category satisfies suitable closure conditions as defined in the theory
‹Universe›. In particular, we show if the collection of arrows
forms a ``universe'', then the category is well-pointed, small-complete and small co-complete,
cartesian closed, has a subobject classifier and a natural numbers object,
and splits all epimorphisms.
›
section "Basic Definitions and Properties"
text‹
We will describe the category of small sets and functions as a certain kind of category
with terminal object, which has been equipped with a notion of ``smallness'' that
specifies what sets will correspond to objects in the category.
›
locale sets_cat_base =
smallness sml +
category_with_terminal_object C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
sublocale embedding ‹Collect arr› .
text‹
Every object in the category determines a set: its set of global elements
(we make an arbitrary choice of terminal object).
›
abbreviation Set
where "Set ≡ hom 𝟭⇧?"
text‹
Every arrow in the category determines an extensional function between
sets of global elements.
›
definition Fun
where "Fun f x ≡ if x ∈ Set (dom f) then f ⋅ x else null"
abbreviation Hom
where "Hom a b ≡ (Set a → Set b) ∩ {F. ∀x. x ∉ Set a ⟶ F x = null}"
lemma Fun_in_Hom:
assumes "«f : a → b»"
shows "Fun f ∈ Hom a b"
using assms Fun_def by auto
lemma Set_some_terminal:
shows "Set some_terminal = {some_terminal}"
using ide_in_hom terminal_def terminal_some_terminal by auto
lemma Fun_some_terminator:
assumes "ide a"
shows "Fun 𝗍⇧?[a] = (λx. if x ∈ Set a then 𝟭⇧? else null)"
unfolding Fun_def
using assms elementary_category_with_terminal_object.trm_naturality
elementary_category_with_terminal_object.trm_one
extends_to_elementary_category_with_terminal_object
by fastforce
text‹
The following function will allow us to obtain an object corresponding to an
externally given set. The set of global elements of the object is to be
equipollent with the given set. We give the definition here, but of course
it will be necessary to prove that this function actually does produce such
an object under suitable conditions.
›
definition mkide :: "'a set ⇒ 'U"
where "mkide A ≡ SOME a. ide a ∧ Set a ≈ A"
end
text‹
The following locale states our axioms for the category of small sets and functions.
The axioms assert: (1) that the set of global elements of every object is small;
(2) that the mapping from hom-sets to extensional functions between small sets
of global elements is injective and surjective; and (3) that the category is ``replete''
in the sense that for every small set of arrows of the category there exists an object
whose set of elements is equipollent with it.
›
locale sets_cat =
sets_cat_base sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55) +
assumes small_Set: "ide a ⟹ small (Set a)"
and inj_Fun: "⟦ide a; ide b⟧ ⟹ inj_on Fun (hom a b)"
and surj_Fun: "⟦ide a; ide b⟧ ⟹ Hom a b ⊆ Fun ` (hom a b)"
and repleteness_ax: "⟦small A; A ⊆ Collect arr⟧ ⟹ ∃a. ide a ∧ Set a ≈ A"
begin
text‹
It is convenient to extend the repleteness property to apply to any small set,
at any type, which happens to have an embedding into the collection of arrows of
the category.
›
lemma repleteness:
assumes "small A" and "embeds A"
shows "∃a. ide a ∧ Set a ≈ A"
by (metis assms(1,2) eqpoll_trans inj_on_image_eqpoll_self repleteness_ax small_image_iff)
text‹
We obtain a pair of inverse comparison maps between an externally given small set ‹A›
and the set of global elements of the object ‹mkide a› corresponding to it.
The map ‹IN› encodes each element of ‹A› as a global element of ‹mkide A›.
The inverse map ‹OUT› decodes global elements of ‹mkide A› to the corresponding
elements of ‹A›.
We will need to pay attention to these comparison maps when relating notions internal
to the category to notions external to it. However, when working completely internally
to the category these maps do not appear at all.
›
definition OUT :: "'a set ⇒ 'U ⇒ 'a"
where "OUT A ≡ SOME F. bij_betw F (Set (mkide A)) A"
abbreviation IN :: "'a set ⇒ 'a ⇒ 'U"
where "IN A ≡ inv_into (Set (mkide A)) (OUT A)"
text‹
The following is the main fact that allows us to produce objects of the category.
It states that, given any small set ‹A› for which there is some embedding into the
collection of arrows of the category, there exists a corresponding object ‹mkide A›
whose set of global elements is equipollent to ‹A›.
›
lemma ide_mkide:
assumes "small A" and "embeds A"
shows [intro]: "ide (mkide A)"
and "Set (mkide A) ≈ A"
proof -
have "ide (mkide A) ∧ Set (mkide A) ≈ A"
using assms repleteness mkide_def someI_ex
by (metis (lifting) HOL.ext)
thus "ide (mkide A)" and "Set (mkide A) ≈ A"
using assms by auto
qed
lemma bij_OUT:
assumes "small A" and "embeds A"
shows "bij_betw (OUT A) (Set (mkide A)) A"
unfolding OUT_def
using assms ide_mkide(2) someI_ex [of "λF. bij_betw F (Set (mkide A)) A"] eqpoll_def
by blast
lemma bij_IN:
assumes "small A" and "embeds A"
shows "bij_betw (IN A) A (Set (mkide A))"
using assms bij_OUT bij_betw_inv_into by blast
lemma OUT_elem_of:
assumes "small A" and "embeds A" and "«x : 𝟭⇧? → mkide A»"
shows "OUT A x ∈ A"
by (metis CollectI assms(1,2,3) bij_betw_apply bij_OUT)
lemma IN_in_hom:
assumes "small A" and "embeds A" and "x ∈ A" and "a = mkide A"
shows "«IN A x : 𝟭⇧? → a»"
by (metis (mono_tags, lifting) Ball_Collect assms(1,2,3,4) bij_betw_def bij_OUT
inv_into_into set_eq_subset)
lemma IN_OUT:
assumes "small A" and "embeds A"
shows "x ∈ Set (mkide A) ⟹ IN A (OUT A x) = x"
using assms bij_OUT(1)
by (metis bij_betw_inv_into_left)
lemma OUT_IN:
assumes "small A" and "embeds A"
shows "x ∈ A ⟹ OUT A (IN A x) = x"
using assms bij_OUT(1)
by (metis bij_betw_inv_into_right)
lemma Fun_IN:
assumes "small A" and "embeds A" and "y ∈ A"
shows "Fun (IN A y) = (λx. if x = 𝟭⇧? then IN A y else null)"
proof
fix x
show "Fun (IN A y) x = (if x = 𝟭⇧? then IN A y else null)"
proof (cases "x ∈ Set 𝟭⇧?")
case False
show ?thesis
using False Fun_def
by (metis IN_in_hom Set_some_terminal assms(1,2,3) in_homE singleton_iff)
next
case True
have x: "x = 𝟭⇧?"
using True Set_some_terminal by blast
have "Fun (IN A y) x = IN A y ⋅ 𝟭⇧?"
using Fun_def dom_eqI ide_some_terminal ext x by auto
also have "... = (if x = 𝟭⇧? then IN A y else null)"
by (metis (lifting) HOL.ext IN_in_hom assms(1,2,3) comp_arr_dom in_homE x)
finally show ?thesis by blast
qed
qed
text‹
The following function enables us to obtain an arrow of the category by specifying
an extensional function between sets of global objects.
›
definition mkarr :: "'U ⇒ 'U ⇒ ('U ⇒ 'U) ⇒ 'U"
where "mkarr a b F ≡ if ide a ∧ ide b ∧ F ∈ Hom a b
then SOME f. «f : a → b» ∧ Fun f = F
else null"
lemma mkarr_in_hom [intro]:
assumes "ide a" and "ide b" and "F ∈ Hom a b"
shows "«mkarr a b F : a → b»"
proof -
have "∃f. «f : a → b» ∧ Fun f = F"
using assms surj_Fun [of a b] by blast
thus ?thesis
unfolding mkarr_def
using assms someI_ex [of "λf. «f : a → b» ∧ Fun f = F"] by auto
qed
lemma arr_mkarr [intro, simp]:
assumes "ide a" and "ide b" and "F ∈ Hom a b"
shows "arr (mkarr a b F)"
using assms mkarr_in_hom by blast
lemma arr_mkarrD [dest]:
assumes "arr (mkarr a b F)"
shows "ide a" and "ide b" and "F ∈ Hom a b"
by (metis (lifting) assms mkarr_def not_arr_null)+
lemma arr_mkarrE [elim]:
assumes "arr (mkarr a b F)"
and "⟦ide a; ide b; F ∈ Hom a b⟧ ⟹ T"
shows T
using assms by auto
lemma dom_mkarr [simp]:
assumes "arr (mkarr a b F)"
shows "dom (mkarr a b F) = a"
by (meson arr_mkarrE assms in_homE mkarr_in_hom)
lemma cod_mkarr [simp]:
assumes "arr (mkarr a b F)"
shows "cod (mkarr a b F) = b"
by (meson arr_mkarrE assms in_homE mkarr_in_hom)
lemma Fun_mkarr [simp]:
assumes "arr (mkarr a b F)"
shows "Fun (mkarr a b F) = F"
proof -
have "∃f. «f : a → b» ∧ Fun f = F"
using assms surj_Fun [of a b] by blast
thus ?thesis
unfolding mkarr_def
using assms someI_ex [of "λf. «f : a → b» ∧ Fun f = F"] by auto
qed
lemma mkarr_Fun:
assumes "«f : a → b»"
shows "mkarr a b (Fun f) = f"
proof -
have "«mkarr a b (Fun f) : a → b» ∧ Fun (mkarr a b (Fun f)) = Fun f"
by (metis (lifting) Fun_in_Hom Fun_mkarr assms ide_cod ide_dom in_homE mkarr_in_hom)
thus ?thesis
using assms inj_Fun inj_onD [of Fun "hom a b" "mkarr a b (Fun f)" f]
by blast
qed
text‹
The locale assumptions ensure that, for any two objects ‹a› and ‹b›,
there is a bijection between the hom-set ‹hom a b› and the set ‹Hom a b›
of extensional functions from ‹Set a› to ‹Set b›.
›
lemma bij_Fun:
assumes "ide a" and "ide b"
shows "bij_betw Fun (hom a b) (Hom a b)"
and "bij_betw (mkarr a b) (Hom a b) (hom a b)"
proof -
have 1: "Fun ∈ hom a b → Hom a b"
using Fun_in_Hom by blast
have 2: "mkarr a b ∈ Hom a b → hom a b"
using assms mkarr_in_hom by auto
have 3: "⋀F. F ∈ Hom a b ⟹ Fun (mkarr a b F) = F"
using Fun_mkarr assms(1,2) mkarr_in_hom by auto
have 4: "⋀f. f ∈ hom a b ⟹ mkarr a b (Fun f) = f"
using assms mkarr_Fun by auto
show "bij_betw Fun (hom a b) (Hom a b)"
using 1 2 3 4
by (intro bij_betwI) auto
show "bij_betw (mkarr a b) (Hom a b) (hom a b)"
using 1 2 3 4
by (intro bij_betwI) auto
qed
lemma arr_eqI:
assumes "par t u" and "Fun t = Fun u"
shows "t = u"
using assms by (metis (lifting) arr_iff_in_hom mkarr_Fun)
lemma arr_eqI':
assumes "in_hom f a b" and "in_hom g a b"
and "⋀x. in_hom x 𝟭⇧? a ⟹ f ⋅ x = g ⋅ x"
shows "f = g"
using assms arr_eqI [of f g] in_homE Fun_def by fastforce
lemma Fun_arr:
assumes "«f : a → b»"
shows "Fun f = (λx. if x ∈ Set a then f ⋅ x else null)"
using assms Fun_def by auto
lemma Fun_ide:
assumes "ide a"
shows "Fun a = (λx. if x ∈ Set a then x else null)"
by (metis (lifting) CollectD CollectI assms comp_cod_arr in_homE ide_char Fun_def)
lemma Fun_comp:
assumes "seq t u"
shows "Fun (t ⋅ u) = Fun t ∘ Fun u"
unfolding Fun_def
using assms comp_assoc by force
lemma mkarr_comp:
assumes "seq g f"
shows "mkarr (dom f) (cod g) (Fun g ∘ Fun f) = g ⋅ f"
by (metis (lifting) Fun_comp assms cod_comp dom_comp in_homI mkarr_Fun)
lemma comp_mkarr:
assumes "arr (mkarr a b F)" and "arr (mkarr b c G)"
shows "mkarr b c G ⋅ mkarr a b F = mkarr a c (G ∘ F)"
using assms Fun_mkarr mkarr_comp [of "mkarr b c G" "mkarr a b F"] by simp
lemma app_mkarr:
assumes "in_hom (mkarr a b F) a b" and "in_hom x 𝟭⇧? a"
shows "mkarr a b F ⋅ x = F x"
using assms Fun_mkarr
by (metis Fun_def in_homE mem_Collect_eq)
lemma ide_as_mkarr:
assumes "ide a"
shows "mkarr a a (λx. if x ∈ Set a then x else null) = a"
using assms Fun_ide Fun_mkarr
by (intro arr_eqI) auto
text‹
An object ‹a› is terminal if and only if its set of global elements ‹Set a›
is a singleton set.
›
lemma terminal_char:
shows "terminal a ⟷ ide a ∧ (∃!x. x ∈ Set a)"
proof
show "terminal a ⟹ ide a ∧ (∃!x. x ∈ Set a)"
using terminal_def terminal_some_terminal by auto
assume a: "ide a ∧ (∃!x. x ∈ Set a)"
show "terminal a"
proof
show "ide a"
using a by blast
show "⋀b. ide b ⟹ ∃!f. «f : b → a»"
proof -
fix b
assume b: "ide b"
have "«mkarr b a (λx. if x ∈ Set b then THE y. y ∈ Set a else null) : b → a»"
using a b theI [of "λy. y ∈ Set a"]
by (intro mkarr_in_hom) fastforce+
moreover have "⋀t u. ⟦«t : b → a»; «u : b → a»⟧ ⟹ t = u"
using a Fun_def by (intro arr_eqI) fastforce+
ultimately show "∃!f. «f : b → a»" by blast
qed
qed
qed
text‹
An object ‹a› is initial if and only if its set of global elements ‹Set a›
is the empty set, except in the degenerate situation in which every object
is both an initial and a terminal object.
›
lemma initial_char:
shows "initial a ⟷ ide a ∧ (Set a = {} ∨ (∀b. ide b ⟶ terminal b))"
proof -
have "∀b. ide b ⟶ terminal b ⟹ ∀b. ide b ⟶ initial b"
by (simp add: initialI terminal_def)
moreover have "∃b. ide b ∧ ¬ terminal b ⟹ ∀a. initial a ⟷ ide a ∧ Set a = {}"
proof -
assume 1: "∃b. ide b ∧ ¬ terminal b"
obtain b where b: "ide b ∧ ¬ terminal b"
using 1 by blast
show "∀a. initial a ⟷ ide a ∧ Set a = {}"
proof (intro allI iffI conjI)
fix a
assume a: "initial a"
show "ide a"
using a initial_def by blast
show "Set a = {}"
proof (cases "Set b = {}")
case True
show ?thesis
using a b True by blast
next
case False
have "Set a ≠ {} ⟹ ¬ (∃!f. «f : a → b»)"
proof -
assume 2: "Set a ≠ {}"
obtain x y where 3: "x ∈ Set b ∧ y ∈ Set b ∧ x ≠ y"
using b False terminal_char by auto
show ?thesis
proof -
have "«mkarr a b (λz. if z ∈ Set a then x else null) : a → b»"
using ‹ide a› b 3 by auto
moreover have "«mkarr a b (λz. if z ∈ Set a then y else null) : a → b»"
using ‹ide a› b 3 by auto
moreover have "mkarr a b (λz. if z ∈ Set a then x else null) ≠
mkarr a b (λz. if z ∈ Set a then y else null)"
by (metis (full_types, lifting) 2 3 Fun_mkarr arrI calculation(2) ex_in_conv)
ultimately show ?thesis by auto
qed
qed
thus ?thesis
using a b initial_def by auto
qed
next
fix a
assume a: "ide a ∧ Set a = {}"
show "initial a"
proof -
have "⋀b. ide b ⟹ ∃!f. «f : a → b»"
proof -
fix b
assume b: "ide b"
have "«mkarr a b (λ_. null) : a → b»"
by (simp add: a b mkarr_in_hom)
moreover have "⋀f g. ⟦«f : a → b»; «g : a → b»⟧ ⟹ f = g"
using a arr_eqI' by fastforce
ultimately show "∃!f. «f : a → b»" by blast
qed
thus ?thesis
using a initial_def by blast
qed
qed
qed
ultimately show ?thesis
by (metis initial_def)
qed
text‹
An arrow is a monomorphism if and only if the corresponding function is injective.
›
lemma mono_char:
shows "mono f ⟷ arr f ∧ inj_on (Fun f) (Set (dom f))"
proof
assume f: "mono f"
have "arr f"
using f mono_implies_arr by simp
moreover have "inj_on (Fun f) (Set (dom f))"
by (intro inj_onI)
(metis Fun_def calculation f in_homE mem_Collect_eq mono_cancel seqI)
ultimately show "arr f ∧ inj_on (Fun f) (Set (dom f))" by blast
next
assume f: "arr f ∧ inj_on (Fun f) (Set (dom f))"
show "mono f"
proof
show "arr f"
using f by blast
fix g h
assume seq: "seq f g" and eq: "f ⋅ g = f ⋅ h"
show "g = h"
proof (intro arr_eqI)
show par: "par g h"
by (metis dom_comp eq seq seqE)
show "Fun g = Fun h"
proof -
have "⋀x. x ∈ Set (dom g) ⟹ Fun g x = Fun h x"
proof -
fix x
assume x: "x ∈ Set (dom g)"
have "f ⋅ (g ⋅ x) = f ⋅ (h ⋅ x)"
using eq by (metis comp_assoc)
moreover have "g ⋅ x ∈ Set (dom f) ∧ h ⋅ x ∈ Set (dom f)"
by (metis seq par comp_in_homI in_homI mem_Collect_eq seq seqE x)
ultimately have "g ⋅ x = h ⋅ x"
using f inj_on_def [of "Fun f" "Set (dom f)"] Fun_def by auto
thus "Fun g x = Fun h x"
using par Fun_def by presburger
qed
thus ?thesis
using par Fun_def by force
qed
qed
qed
qed
text‹
An arrow is a retraction if and only if the corresponding function is surjective.
›
lemma retraction_char:
shows "retraction f ⟷ arr f ∧ Fun f ` Set (dom f) = Set (cod f)"
proof (intro iffI conjI)
assume f: "retraction f"
show 1: "arr f"
using f by blast
obtain g where g: "f ⋅ g = cod f"
using f by blast
show "Fun f ` Set (dom f) = Set (cod f)"
proof
show "Fun f ` Set (dom f) ⊆ Set (cod f)"
using ‹arr f› Fun_def by auto
show "Set (cod f) ⊆ Fun f ` Set (dom f)"
proof -
have "Set (cod f) ⊆ Fun f ` Fun g ` Set (cod f)"
proof -
have "Set (cod f) ⊆ Fun (cod f) ` Set (cod f)"
using 1 Fun_ide by auto
also have "... = (Fun f ∘ Fun g) ` Set (cod f)"
using 1 g Fun_comp
by (metis (no_types, lifting) arr_cod)
also have "... = Fun f ` Fun g ` Set (cod f)"
by (metis image_comp)
finally show ?thesis by blast
qed
also have "... ⊆ Fun f ` Set (dom f)"
proof -
have "«g : cod f → dom f»"
using g
by (metis 1 arr_iff_in_hom ide_cod ide_compE seqE)
thus ?thesis
using Fun_def by auto
qed
finally show ?thesis by blast
qed
qed
next
assume f: "arr f ∧ Fun f ` Set (dom f) = Set (cod f)"
let ?G = "λy. if y ∈ Set (cod f) then inv_into (Set (dom f)) (Fun f) y else null"
let ?g = "mkarr (cod f) (dom f) ?G"
have "f ⋅ ?g = cod f"
proof (intro arr_eqI)
have seq: "seq f ?g"
proof
show "«f : dom f → cod f»"
using f by blast
show "«?g : cod f → dom f»"
proof (intro mkarr_in_hom)
show "ide (cod f)" and "ide (dom f)"
using f by auto
show "?G ∈ (Set (cod f) → Set (dom f)) ∩ {F. ∀x. x ∉ Set (cod f) ⟶ F x = null}"
proof
show "?G ∈ Set (cod f) → Set (dom f)"
proof
fix x
assume x: "x ∈ Set (cod f)"
show "?G x ∈ Set (dom f)"
by (metis f inv_into_into x)
qed
show "?G ∈ {F. ∀x. x ∉ Set (cod f) ⟶ F x = null}"
using f by auto
qed
qed
qed
thus par: "par (f ⋅ ?g) (cod f)" by auto
show "Fun (f ⋅ ?g) = Fun (cod f)"
proof -
have "Fun (f ⋅ ?g) = Fun f ∘ ?G"
using par Fun_comp Fun_mkarr by fastforce
also have "... = Fun (cod f)"
proof
fix y
show "(Fun f ∘ ?G) y = Fun (cod f) y"
proof (cases "y ∈ Set (cod f)")
case False
show ?thesis
using False Fun_def dom_cod by auto
next
case True
show ?thesis
proof -
have "Fun f (inv_into (Set (dom f)) (Fun f) y) = y"
by (metis (no_types) True f f_inv_into_f)
thus ?thesis
using Fun_ide True f by force
qed
qed
qed
finally show ?thesis by blast
qed
qed
thus "retraction f"
by (metis (lifting) f ide_cod retraction_def)
qed
text‹
An arrow is a isomorphism if and only if the corresponding function is a bijection.
›
lemma iso_char:
shows "iso f ⟷ arr f ∧ bij_betw (Fun f) (Set (dom f)) (Set (cod f))"
using retraction_char mono_char bij_betw_def
by (metis (no_types, lifting) iso_iff_mono_and_retraction)
lemma isomorphic_char:
shows "isomorphic a b ⟷ ide a ∧ ide b ∧ Set a ≈ Set b"
proof
assume 1: "isomorphic a b"
show "ide a ∧ ide b ∧ Set a ≈ Set b"
using 1 isomorphic_def iso_char eqpoll_def [of "Set a" "Set b"] by auto
next
assume 1: "ide a ∧ ide b ∧ Set a ≈ Set b"
obtain F where F: "bij_betw F (Set a) (Set b)"
using 1 eqpoll_def by blast
let ?F' = "λx. if x ∈ Set a then F x else null"
let ?f = "mkarr a b (λx. if x ∈ Set a then F x else null)"
have f: "«?f : a → b»"
proof
show "ide a" and "ide b"
using 1 by auto
show "(λx. if x ∈ Set a then F x else null) ∈ Hom a b"
using F Pi_mem bij_betw_imp_funcset by fastforce
qed
moreover have "bij_betw (Fun ?f) (Set a) (Set b)"
using F Fun_mkarr arrI bij_betw_cong f
apply (unfold bij_betw_def)
by (auto simp add: inj_on_def)
ultimately have "iso ?f ∧ dom ?f = a ∧ cod ?f = b"
using iso_char Fun_mkarr by auto
thus "isomorphic a b"
using isomorphicI by force
qed
end
section "Categoricity"
text‹
The following is a kind of ``categoricity in power'' result which states that,
for a fixed notion of smallness, if ‹C› and ‹D› are ``sets categories'' whose collections
of arrows are equipollent, then in fact ‹C› and ‹D› are equivalent categories.
›
lemma categoricity:
assumes "sets_cat sml C" and "sets_cat sml D"
and "Collect (partial_composition.arr C) ≈ Collect (partial_composition.arr D)"
shows "equivalent_categories C D"
proof
interpret smallness sml
using assms(1) sets_cat_def sets_cat_base_def by blast
interpret C: sets_cat sml C
using assms(1) by blast
interpret D: sets_cat sml D
using assms(2) by blast
have D_embeds_C_Set: "⋀a. C.ide a ⟹ D.embeds (C.Set a)"
using assms(3) D.embeds_subset [of "Collect C.arr"]
by (metis (no_types, lifting) Collect_mono bij_betw_def C.in_homE eqpoll_def)
let ?F⇩o = "λa. D.mkide (C.Set a)"
have F⇩o: "⋀a. C.ide a ⟹ D.ide (?F⇩o a)"
by (simp add: C.small_Set D.ide_mkide(1) D_embeds_C_Set)
have bij_OUT: "⋀a. C.ide a ⟹ bij_betw (D.OUT (C.Set a)) (D.Set (?F⇩o a)) (C.Set a)"
by (simp add: C.small_Set D.bij_OUT(1) D_embeds_C_Set)
let ?F⇩F⇩u⇩n = "λf. λx. if x ∈ D.Set (?F⇩o (C.dom f))
then (D.IN (C.Set (C.cod f)) ∘ C.Fun f ∘ D.OUT (C.Set (C.dom f))) x
else D.null"
have F⇩F⇩u⇩n: "⋀f. C.arr f ⟹ ?F⇩F⇩u⇩n f ∈ D.Hom (?F⇩o (C.dom f)) (?F⇩o (C.cod f))"
proof
fix f
assume f: "C.arr f"
show "?F⇩F⇩u⇩n f ∈ {F. ∀x. x ∉ D.Set (?F⇩o (C.dom f)) ⟶ F x = D.null}"
by simp
show "?F⇩F⇩u⇩n f ∈ D.Set (?F⇩o (C.dom f)) → D.Set (?F⇩o (C.cod f))"
proof
fix x
assume x: "x ∈ D.Set (?F⇩o (C.dom f))"
show "?F⇩F⇩u⇩n f x ∈ D.Set (D.mkide (C.Set (C.cod f)))"
proof -
have "D.in_hom (D.IN (C.Set (C.cod f)) (C f (D.OUT (C.Set (C.dom f)) x)))
D.some_terminal (D.mkide (C.Set (C.cod f)))"
proof -
have "«C f (D.OUT (C.Set (C.dom f)) x) : 𝟭⇧? → C.cod f»"
using x f C.ide_dom bij_betwE bij_OUT by blast
moreover have "small (C.Set (C.cod f))"
using C.small_Set f by force
moreover have "D.embeds (C.Set (C.cod f))"
by (simp add: D_embeds_C_Set f)
ultimately show ?thesis
using x f D.bij_IN [of "C.Set (C.cod f)"] bij_betwE by auto
qed
moreover have "«D.OUT (C.Set (C.dom f)) x : 𝟭⇧? → C.dom f»"
using x f C.ide_dom bij_betwE bij_OUT by blast
ultimately show ?thesis
using x f C.Fun_def by force
qed
qed
qed
let ?F = "λf. if C.arr f then D.mkarr (?F⇩o (C.dom f)) (?F⇩o (C.cod f)) (?F⇩F⇩u⇩n f) else D.null"
interpret "functor" C D ?F
proof
show "⋀f. ¬ C.arr f ⟹ ?F f = D.null"
by simp
show arrF: "⋀f. C.arr f ⟹ D.arr (?F f)"
using F⇩o F⇩F⇩u⇩n by auto
show domF: "⋀f. C.arr f ⟹ D.dom (?F f) = ?F (C.dom f)"
proof -
fix f
assume f: "C.arr f"
have "D.dom (?F f) = D.mkide (C.Set (C.dom f))"
using f arrF by auto
also have "... = ?F (C.dom f)"
proof -
have "?F⇩F⇩u⇩n (C.dom f) =
(λx. if x ∈ D.Set (D.mkide (C.Set (C.dom f))) then x else D.null)"
proof
fix x
have "x ∈ D.Set (D.mkide (C.Set (C.dom f))) ⟹
«D.OUT (C.Set (C.dom f)) x : 𝟭⇧? → C.dom f»"
using f C.ide_dom bij_betwE bij_OUT by blast
thus "?F⇩F⇩u⇩n (C.dom f) x =
(if x ∈ D.Set (D.mkide (C.Set (C.dom f))) then x else D.null)"
using f C.ide_dom bij_betwE bij_OUT arrF F⇩o C.Fun_ide
D.IN_OUT [of "C.Set (C.dom f)" x]
by (auto simp add: C.small_Set D_embeds_C_Set)
qed
moreover have "D.mkide (C.Set (C.dom f)) =
D.mkarr (D.mkide (C.Set (C.dom f))) (D.mkide (C.Set (C.dom f)))
(λx. if D.in_hom x D.some_terminal (D.mkide (C.Set (C.dom f)))
then x else D.null)"
using f arrF F⇩o D.ide_as_mkarr by auto
ultimately show ?thesis
using f by auto
qed
finally show "D.dom (?F f) = ?F (C.dom f)" by blast
qed
show codF: "⋀f. C.arr f ⟹ D.cod (?F f) = ?F (C.cod f)"
proof -
fix f
assume f: "C.arr f"
have "D.cod (?F f) = D.mkide (C.Set (C.cod f))"
using f arrF by auto
also have "... = ?F (C.cod f)"
proof -
have "?F⇩F⇩u⇩n (C.cod f) =
(λx. if x ∈ D.Set (D.mkide (C.Set (C.cod f))) then x else D.null)"
proof
fix x
have "x ∈ D.Set (D.mkide (C.Set (C.cod f))) ⟹
«D.OUT (C.Set (C.cod f)) x : 𝟭⇧? → C.cod f»"
using f C.ide_cod bij_betwE bij_OUT by blast
thus "?F⇩F⇩u⇩n (C.cod f) x =
(if x ∈ D.Set (D.mkide (C.Set (C.cod f))) then x else D.null)"
using f C.ide_cod bij_betwE bij_OUT arrF F⇩o C.Fun_ide
D.IN_OUT [of "C.Set (C.cod f)" x]
by (auto simp add: C.small_Set D_embeds_C_Set)
qed
moreover have "D.mkide (C.Set (C.cod f)) =
D.mkarr (D.mkide (C.Set (C.cod f))) (D.mkide (C.Set (C.cod f)))
(λx. if D.in_hom x D.some_terminal (D.mkide (C.Set (C.cod f)))
then x else D.null)"
using f arrF F⇩o D.ide_as_mkarr [of "D.mkide (C.Set (C.cod f))"] by auto
ultimately show ?thesis
using f by auto
qed
finally show "D.cod (?F f) = ?F (C.cod f)" by blast
qed
fix f g
assume seq: "C.seq g f"
have f: "C.arr f" and g: "C.arr g"
using seq by auto
show "?F (C g f) = D (?F g) (?F f)"
proof (intro D.arr_eqI [of "?F (C g f)"])
show par: "D.par (?F (C g f)) (D (?F g) (?F f))"
proof (intro conjI)
show 1: "D.arr (?F (C g f))"
using seq arrF [of "C g f"] by fastforce
show 2: "D.arr (D (?F g) (?F f))"
using seq arrF domF codF by (intro D.seqI) auto
show "D.dom (?F (C g f)) = D.dom (D (?F g) (?F f))"
using 1 2 by fastforce
show "D.cod (?F (C g f)) = D.cod (D (?F g) (?F f))"
using 1 2 by fastforce
qed
show "D.Fun (?F (C g f)) = D.Fun (D (?F g) (?F f))"
proof -
have "D.Fun (D (?F g) (?F f)) = D.Fun (?F g) ∘ D.Fun (?F f)"
using seq par D.Fun_comp [of "?F g" "?F f"] by fastforce
also have "... = ?F⇩F⇩u⇩n g ∘ ?F⇩F⇩u⇩n f"
using f g arrF D.Fun_mkarr by auto
also have "... = D.Fun (?F (C g f))"
proof
fix x
show "(?F⇩F⇩u⇩n g ∘ ?F⇩F⇩u⇩n f) x = D.Fun (?F (C g f)) x"
proof (cases "x ∈ D.Set (D.mkide (C.Set (C.dom f)))")
case False
show ?thesis
using False f par by auto
next
case True
have 1: "«D.OUT (C.Set (C.dom f)) x : 𝟭⇧? → C.dom f»"
using True D.OUT_elem_of [of "C.Set (C.dom f)" x]
C.ide_dom C.small_Set D_embeds_C_Set f
by blast
have "(?F⇩F⇩u⇩n g ∘ ?F⇩F⇩u⇩n f) x =
D.IN (C.Set (C.cod g))
(C.Fun g
(D.OUT (C.Set (C.dom g))
(D.IN (C.Set (C.cod f))
(C.Fun f
(D.OUT (C.Set (C.dom f)) x)))))"
proof -
have "D.in_hom (D.IN (C.Set (C.cod f)) (C f (D.OUT (C.Set (C.dom f)) x)))
D.some_terminal (D.mkide (C.Set (C.dom g)))"
using True f seq 1 C.ide_cod C.small_Set D_embeds_C_Set
by (intro D.IN_in_hom) auto
thus ?thesis
using True 1 C.Fun_def by auto
qed
also have "... =
D.IN (C.Set (C.cod g))
(C.Fun g
(C.Fun f
(D.OUT (C.Set (C.dom f)) x)))"
using True 1 seq f g C.small_Set D_embeds_C_Set C.Fun_def D.Fun_def
D.OUT_IN [of "C.Set (C.dom g)" "C f (D.OUT (C.Set (C.dom f)) x)"]
by auto[1] (metis C.comp_in_homI' C.in_homE C.seqE)
also have "... = ?F⇩F⇩u⇩n (C g f) x"
using True seq 1 C.comp_assoc C.Fun_def D.Fun_def
by auto[1] fastforce
also have "... = D.Fun (?F (C g f)) x"
using True par seq D.Fun_mkarr D.app_mkarr D.in_homI by force
finally show ?thesis by blast
qed
qed
finally show ?thesis by simp
qed
qed
qed
interpret F: fully_faithful_and_essentially_surjective_functor C D ?F
proof
show "⋀f f'. ⟦C.par f f'; ?F f = ?F f'⟧ ⟹ f = f'"
proof -
fix f f'
assume par: "C.par f f'"
assume eq: "?F f = ?F f'"
show "f = f'"
proof (intro C.arr_eqI' [of f])
show f: "«f : C.dom f → C.cod f»"
using par by blast
show f': "«f' : C.dom f → C.cod f»"
using par by auto
show "⋀x. «x : 𝟭⇧? → C.dom f» ⟹ C f x = C f' x"
proof -
fix x
assume x: "«x : 𝟭⇧? → C.dom f»"
have fx: "«C f x : 𝟭⇧? → C.cod f» ∧ C.ide (C.dom f) ∧ C.ide (C.cod f)"
by (metis (no_types) C.arrI C.comp_in_homI C.ide_cod C.seqE f x)
have f'x: "«C f' x : 𝟭⇧? → C.cod f'» ∧ C.ide (C.dom f') ∧ C.ide (C.cod f')"
by (metis (no_types) C.arrI C.comp_in_homI C.ide_cod C.seqE f' x par)
have 1: "D.in_hom (D.IN (C.Set (C.dom f)) x)
D.some_terminal (D.mkide (C.Set (C.dom f)))"
by (metis C.ide_dom C.small_Set D.IN_in_hom D_embeds_C_Set mem_Collect_eq
par x)
have "C f x = C.Fun f x"
using C.Fun_def x by auto
also have "... = D.OUT (C.Set (C.cod f))
(D.IN (C.Set (C.cod f))
(C.Fun f
(D.OUT (C.Set (C.dom f))
(D.IN (C.Set (C.dom f)) x))))"
by (simp add: fx C.small_Set D.OUT_IN D_embeds_C_Set x C.Fun_def)
also have "... = D.OUT (C.Set (C.cod f)) (?F⇩F⇩u⇩n f (D.IN (C.Set (C.dom f)) x))"
using par 1 by auto
also have "... =
D.OUT (C.Set (C.cod f)) (D.Fun (?F f) (D.IN (C.Set (C.dom f)) x))"
proof -
have "D.arr (?F f)"
using f by blast
thus ?thesis
using x f par by auto
qed
also have "... =
D.OUT (C.Set (C.cod f)) (D.Fun (?F f') (D.IN (C.Set (C.dom f)) x))"
using eq by simp
also have "... = D.OUT (C.Set (C.cod f)) (?F⇩F⇩u⇩n f' (D.IN (C.Set (C.dom f)) x))"
proof -
have "D.arr (?F f')"
using f' by blast
thus ?thesis
using x f par by auto
qed
also have "... = D.OUT (C.Set (C.cod f'))
(D.IN (C.Set (C.cod f'))
(C.Fun f'
(D.OUT (C.Set (C.dom f'))
(D.IN (C.Set (C.dom f')) x))))"
using par 1 by auto
also have "... = C.Fun f' x"
by (metis f'x C.small_Set D.OUT_IN D_embeds_C_Set mem_Collect_eq par x C.Fun_def)
also have "... = C f' x"
using C.Fun_def x par by auto
finally show "C f x = C f' x" by blast
qed
qed
qed
have *: "⋀a. C.ide a ⟹ ?F a = ?F⇩o a"
proof -
fix a
assume a: "C.ide a"
show "?F a = ?F⇩o a"
proof -
have "(λx. if D.in_hom x D.some_terminal (D.mkide (C.Set a))
then (D.IN (C.Set (C.cod a)) ∘ C.Fun a ∘ D.OUT (C.Set (C.dom a))) x
else D.null) =
(λx. if D.in_hom x D.some_terminal (D.mkide (C.Set a)) then x else D.null)"
proof
fix x
show "(if D.in_hom x D.some_terminal (D.mkide (C.Set a))
then (D.IN (C.Set (C.cod a)) ∘ C.Fun a ∘ D.OUT (C.Set (C.dom a))) x
else D.null) =
(if D.in_hom x D.some_terminal (D.mkide (C.Set a)) then x else D.null)"
using a C.Fun_ide D.IN_OUT [of "C.Set a"] C.small_Set D_embeds_C_Set
apply auto[1]
by (metis (lifting) D.OUT_elem_of mem_Collect_eq)
qed
thus ?thesis
using a D.ide_as_mkarr F⇩o by auto
qed
qed
show "⋀a b g. ⟦C.ide a; C.ide b; D.in_hom g (?F a) (?F b)⟧
⟹ ∃h. «h : a → b» ∧ ?F h = g"
proof -
fix a b g
assume a: "C.ide a" and b: "C.ide b" and g: "D.in_hom g (?F a) (?F b)"
have "?F a = ?F⇩o a"
using a * by blast
have dom_g: "D.dom g = ?F⇩o a"
using a g * by auto
have cod_g: "D.cod g = ?F⇩o b"
using b g * by auto
have Fun_g: "D.Fun g ∈ D.Hom (?F⇩o a) (?F⇩o b)"
using g D.Fun_in_Hom dom_g cod_g by blast
let ?H = "λx. if x ∈ C.Set a
then (D.OUT (C.Set b) ∘ D.Fun g ∘ D.IN (C.Set a)) x
else C.null"
have H: "?H ∈ C.Hom a b"
proof
show "?H ∈ C.Set a → C.Set b"
proof
fix x
assume x: "x ∈ C.Set a"
show "?H x ∈ C.Set b"
proof -
have "?H x = D.OUT (C.Set b) (D.Fun g (D.IN (C.Set a) x))"
using x by simp
moreover have "... ∈ C.Set b"
proof -
have "D.IN (C.Set a) x ∈ D.Set (?F⇩o a)"
by (metis (lifting) a bij_betw_iff_bijections bij_betw_inv_into bij_OUT x)
hence "D.Fun g (D.IN (C.Set a) x) ∈ D.Set (?F⇩o b)"
using Fun_g by blast
thus ?thesis
using b C.small_Set D_embeds_C_Set bij_OUT bij_betw_apply D.Fun_def
by fastforce
qed
ultimately show ?thesis by auto
qed
qed
show "?H ∈ {F. ∀x. x ∉ C.Set a ⟶ F x = C.null}" by simp
qed
let ?h = "C.mkarr a b ?H"
have h: "«?h : a → b»"
using a b H by blast
moreover have "?F ?h = g"
proof (intro D.arr_eqI)
have Fh: "D.in_hom (?F ?h) (?F⇩o a) (?F⇩o b)"
proof -
have "D.in_hom (?F ?h) (?F a) (?F b)"
using h preserves_hom by blast
moreover have "?F a = ?F⇩o a ∧ ?F b = ?F⇩o b"
using a b * by auto
ultimately show ?thesis by simp
qed
show par: "D.par (?F ?h) g"
using Fh h g cod_g dom_g D.in_homE by auto
show "D.Fun (?F ?h) = D.Fun g"
proof
fix x
show "D.Fun (?F ?h) x = D.Fun g x"
proof (cases "x ∈ D.Set (?F⇩o a)")
case False
show ?thesis
using False par D.Fun_def by auto
next
case True
have "D.Fun (?F ?h) x = ?F⇩F⇩u⇩n ?h x"
using True h Fh D.Fun_def D.app_mkarr by auto
also have "... = (if x ∈ D.Set (?F⇩o a)
then (D.IN (C.Set b) ∘ C.Fun ?h ∘ D.OUT (C.Set a)) x
else D.null)"
using h by auto
also have "... = D.IN (C.Set b) (?H (D.OUT (C.Set a) x))"
using True h C.app_mkarr by auto
also have "... = D.IN (C.Set b)
(D.OUT (C.Set b)
(D.Fun g
(D.IN (C.Set a)
(D.OUT (C.Set a) x))))"
proof -
have "D.OUT (C.Set a) x ∈ C.Set a"
using True a bij_betw_apply bij_OUT by force
thus ?thesis by simp
qed
also have "... = D.Fun g x"
using True a b g D.IN_OUT [of "C.Set a" x] D.IN_OUT [of "C.Set b" "D.Fun g x"]
C.small_Set D_embeds_C_Set dom_g cod_g D.Fun_def
by auto
finally show ?thesis by blast
qed
qed
qed
ultimately show "∃h. «h : a → b» ∧ ?F h = g" by blast
qed
show "⋀b. D.ide b ⟹ ∃a. C.ide a ∧ D.isomorphic (?F a) b"
proof -
fix b
assume b: "D.ide b"
let ?a = "C.mkide (D.Set b)"
have 1: "C.ide ?a ∧ C.Set ?a ≈ D.Set b"
proof -
have "∃ι. C.is_embedding_of ι (D.Set b)"
by (metis (no_types, lifting) D.in_homE Set.basic_monos(6) assms(3)
bij_betw_def bij_betw_inv_into eqpoll_def image_mono inj_on_subset)
thus ?thesis
using b C.ide_mkide [of "D.Set b"] D.small_Set by force
qed
have "D.Set (?F ?a) ≈ D.Set b"
proof -
have "⋀a. C.ide a ⟹ D.Set (?F a) ≈ C.Set a"
using * C.small_Set D_embeds_C_Set D.ide_mkide(2) by fastforce
thus ?thesis
using 1 eqpoll_trans by blast
qed
moreover have "⋀a. C.ide a ⟹ D.isomorphic (?F a) b ⟷ D.Set (?F a) ≈ D.Set b"
using D.isomorphic_char b preserves_ide by force
ultimately show "∃a. C.ide a ∧ D.isomorphic (?F a) b"
using 1 by blast
qed
qed
show "equivalence_functor C D ?F"
using F.is_equivalence_functor by blast
qed
section "Well-Pointedness"
context sets_cat
begin
lemma is_well_pointed:
assumes "par f g" and "⋀x. x ∈ Set (dom f) ⟹ f ⋅ x = g ⋅ x"
shows "f = g"
by (metis CollectI arr_eqI' assms(1,2) in_homI)
end
section "Epis Split"
text‹
In this section we assume that smallness encompasses sets of arbitrary finite cardinality,
and that the category has at least two arrows, so that we can show the existence of an
object with two global elements.
If this fails to be the case, then the situation is somewhat pathological and not very
interesting.
›
locale sets_cat_with_bool =
sets_cat sml C +
small_finite sml
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55) +
assumes embeds_bool_ax: "embeds (UNIV :: bool set)"
begin
definition two ("❙𝟮")
where "two ≡ mkide {True, False}"
lemma ide_two [intro, simp]:
shows "ide two"
and "bij_betw (IN {True, False}) UNIV (Set two)"
and "bij_betw (OUT {True, False}) (Set two) UNIV"
using two_def ide_mkide embeds_bool_ax small_finite UNIV_bool
finite.simps insert_commute infinite_imp_nonempty finite.emptyI
bij_IN [of "{True, False}"] bij_OUT [of "{True, False}"]
by metis+
definition tt
where "tt ≡ IN {True, False} True"
definition ff
where "ff ≡ IN {True, False} False"
lemma tt_in_hom [intro]:
shows "«tt : 𝟭⇧? → ❙𝟮»"
using bij_betwE tt_def by force
lemma ff_in_hom [intro]:
shows "«ff : 𝟭⇧? → ❙𝟮»"
using bij_betwE ff_def by force
lemma tt_simps [simp]:
shows "arr tt" and "dom tt = 𝟭⇧?" and "cod tt = ❙𝟮"
using tt_in_hom by blast+
lemma ff_simps [simp]:
shows "arr ff" and "dom ff = 𝟭⇧?" and "cod ff = ❙𝟮"
using ff_in_hom by blast+
lemma Fun_tt:
shows "Fun tt = (λx. if x ∈ Set 𝟭⇧? then tt else null)"
unfolding Fun_def
using tt_def
by (metis Set_some_terminal comp_arr_dom emptyE insertE tt_simps(1,2))
lemma Fun_ff:
shows "Fun ff = (λx. if x ∈ Set 𝟭⇧? then ff else null)"
unfolding Fun_def
using ff_def
by (metis Set_some_terminal comp_arr_dom emptyE insertE ff_simps(1,2))
lemma mono_tt:
shows "mono tt"
using Fun_tt mono_char
by (metis point_is_mono terminal_some_terminal tt_simps(1,2))
lemma mono_ff:
shows "mono ff"
using Fun_ff mono_char
by (metis point_is_mono terminal_some_terminal ff_simps(1,2))
lemma tt_ne_ff:
shows "tt ≠ ff"
using tt_def ff_def two_def
by (metis bij_betw_inv_into_right ide_two(3) iso_tuple_UNIV_I)
lemma Set_two:
shows "Set ❙𝟮 = {tt, ff}"
proof -
have "Set ❙𝟮 = IN {True, False} ` UNIV"
using bij_betw_imp_surj_on by blast
thus ?thesis
using tt_def ff_def
by (simp add: UNIV_bool insert_commute)
qed
text‹
In the present context, an arrow is epi if and only if the corresponding function
is surjective. It follows that every epimorphism splits.
›
lemma epi_char⇩S⇩C⇩B:
shows "epi f ⟷ arr f ∧ Fun f ` Set (dom f) = Set (cod f)"
proof
show "arr f ∧ Fun f ` Set (dom f) = Set (cod f) ⟹ epi f"
using retraction_char retraction_is_epi by presburger
assume f: "epi f"
show "arr f ∧ Fun f ` Set (dom f) = Set (cod f)"
proof (intro conjI)
show "arr f"
using epi_implies_arr f by blast
show "Fun f ` Set (dom f) = Set (cod f)"
proof
show "Fun f ` Set (dom f) ⊆ Set (cod f)"
using ‹arr f› Fun_def by auto
show "Set (cod f) ⊆ Fun f ` Set (dom f)"
proof
fix y
assume y: "y ∈ Set (cod f)"
have "y ∉ Fun f ` Set (dom f) ⟹ False"
proof -
assume 1: "y ∉ Fun f ` Set (dom f)"
let ?G = "λz. if z ∈ Set (cod f) then if z = y then tt else ff else null"
let ?G' = "λz. if z ∈ Set (cod f) then ff else null"
let ?g = "mkarr (cod f) ❙𝟮 ?G"
let ?g' = "mkarr (cod f) ❙𝟮 ?G'"
have g: "«?g : cod f → ❙𝟮»"
using f epi_implies_arr ide_two
by (intro mkarr_in_hom) auto
have g': "«?g' : cod f → ❙𝟮»"
using f epi_implies_arr ide_two
by (intro mkarr_in_hom) auto
have "?g ≠ ?g'"
proof -
have "?g ⋅ y ≠ ?g' ⋅ y"
using app_mkarr g g' tt_ne_ff y by auto
thus ?thesis by auto
qed
moreover have "?g ⋅ f = ?g' ⋅ f"
proof -
have "?G ∘ Fun f = ?G' ∘ Fun f"
proof
fix x
show "(?G ∘ Fun f) x = (?G' ∘ Fun f) x"
using 1 tt_ne_ff Fun_def by auto
qed
thus ?thesis
using f g g' Fun_mkarr ‹arr f› in_homI Fun_comp
by (intro arr_eqI) auto
qed
ultimately show False
using f g g' ‹arr f› epi_cancel by blast
qed
thus "y ∈ Fun f ` Set (dom f)" by blast
qed
qed
qed
qed
corollary epis_split:
assumes "epi e"
shows "∃m. e ⋅ m = cod e"
using assms epi_char⇩S⇩C⇩B retraction_char
by (meson ide_compE retraction_def)
end
section "Equalizers"
text‹
In this section we show that the category of small sets and functions has equalizers
of parallel pairs of arrows. This is our first example of a general pattern that we
will apply repeatedly in the sequel to other categorical constructions.
Given a parallel pair ‹f›, ‹g› of arrows in a category of sets, we know that the
global elements of the domain of the equalizer will be in bijection with the set ‹E›
of global elements ‹x› of ‹dom f› such that ‹f ⋅ x = g ⋅ x›. So, we obtain this set,
which in this case happens already to be a small subset of the set of arrows of the
category, and we obtain the corresponding object ‹mkide E›, which will be the domain
of the equalizer. This part of the proof uses the smallness of ‹E› and the fact that
it embeds in (actually, is a subset of) the set of arrows of the category.
Once we have shown the existence of the object ‹mkide E›, we can apply ‹mkarr› to the
inclusion of ‹Set (mkide e)› in ‹Set (dom f)› to obtain the equalizing arrow itself.
Showing that this arrow has the necessary universal property requires reasoning about
the comparison maps between ‹E› and ‹Set (mkide e)›, but once that has been accomplished
we are left simply with a universal property that does not mention these maps.
The construction and proofs here are simpler than for the other constructions we will
consider, because the set ‹E› to which we apply ‹mkide› is already a subset of the
collection of arrows of the category -- in particular it is at the same type.
This means that the smallness and embedding property required for the application
of ‹mkide› holds automatically, without any further assumptions.
In general, though, a set to which we wish to apply ‹mkide› will not be a subset of
the set of arrows, nor will it even be at the same type, so it will be necessary
to reason about an encoding that embeds the elements of this set into the set of
arrows of the category.
›
locale equalizers_in_sets_cat =
sets_cat
begin
abbreviation Dom_equ
where "Dom_equ f g ≡ {x. x ∈ Set (dom f) ∧ f ⋅ x = g ⋅ x}"
definition dom_equ
where "dom_equ f g ≡ mkide (Dom_equ f g)"
abbreviation Equ
where "Equ f g ≡ λx. if x ∈ Set (dom_equ f g) then OUT (Dom_equ f g) x else null"
definition equ
where "equ f g ≡ mkarr (dom_equ f g) (dom f) (Equ f g)"
text‹
It is useful to include convenience facts about ‹OUT› and ‹IN› in the following,
so that we can avoid having to deal with the smallness and embedding conditions
elsewhere.
›
lemma ide_dom_equ:
assumes "par f g"
shows "ide (dom_equ f g)"
and "bij_betw (OUT (Dom_equ f g)) (Set (dom_equ f g)) (Dom_equ f g)"
and "bij_betw (IN (Dom_equ f g)) (Dom_equ f g) (Set (dom_equ f g))"
and "⋀x. x ∈ Set (dom_equ f g) ⟹ OUT (Dom_equ f g) x ∈ Set (dom f)"
and "⋀y. y ∈ Dom_equ f g ⟹ IN (Dom_equ f g) y ∈ Set (dom_equ f g)"
and "⋀x. x ∈ Set (dom_equ f g) ⟹ IN (Dom_equ f g) (OUT (Dom_equ f g) x) = x"
and "⋀y. y ∈ Dom_equ f g ⟹ OUT (Dom_equ f g) (IN (Dom_equ f g) y) = y"
proof -
have 1: "small (Dom_equ f g)"
by (metis (full_types) assms ide_dom small_Collect small_Set)
have 2: "embeds (Dom_equ f g)"
by (metis (no_types, lifting) Collect_mono arrI image_ident mem_Collect_eq
subset_image_inj)
show "ide (dom_equ f g)"
by (unfold dom_equ_def, intro ide_mkide) fact+
show 3: "bij_betw (OUT (Dom_equ f g)) (Set (dom_equ f g)) (Dom_equ f g)"
unfolding dom_equ_def
using assms ide_mkide bij_OUT 1 2 by auto
show 4: "bij_betw (IN (Dom_equ f g)) (Dom_equ f g) (Set (dom_equ f g))"
unfolding dom_equ_def
using assms ide_mkide bij_OUT bij_IN 1 2 by fastforce
show "⋀x. x ∈ Set (dom_equ f g) ⟹ OUT (Dom_equ f g) x ∈ Set (dom f)"
by (metis (no_types, lifting) 3 CollectD bij_betw_apply)
show "⋀y. y ∈ Dom_equ f g ⟹ IN (Dom_equ f g) y ∈ Set (dom_equ f g)"
by (metis (no_types, lifting) 4 bij_betw_apply)
show "⋀x. x ∈ Set (dom_equ f g) ⟹ IN (Dom_equ f g) (OUT (Dom_equ f g) x) = x"
using 1 2 IN_OUT dom_equ_def by auto
show "⋀y. y ∈ Dom_equ f g ⟹ OUT (Dom_equ f g) (IN (Dom_equ f g) y) = y"
using 1 2 OUT_IN by force
qed
lemma Equ_in_Hom [intro]:
assumes "par f g"
shows "Equ f g ∈ Hom (dom_equ f g) (dom f)"
proof
show "Equ f g ∈ Set (dom_equ f g) → Set (dom f)"
using assms ide_dom_equ(4) by auto
show "Equ f g ∈ {F. ∀x. x ∉ Set (dom_equ f g) ⟶ F x = null}"
by simp
qed
lemma equ_in_hom [intro, simp]:
assumes "par f g"
shows "«equ f g : dom_equ f g → dom f»"
using assms ide_dom_equ Equ_in_Hom
unfolding equ_def
by (intro mkarr_in_hom) auto
lemma equ_simps [simp]:
assumes "par f g"
shows "arr (equ f g)" and "dom (equ f g) = dom_equ f g" and "cod (equ f g) = dom f"
using assms equ_in_hom by blast+
lemma Fun_equ:
assumes "par f g"
shows "Fun (equ f g) = Equ f g"
proof -
have "arr (equ f g)"
using assms by auto
thus ?thesis
unfolding equ_def
using assms Fun_mkarr by auto
qed
lemma equ_equalizes:
assumes "par f g"
shows "f ⋅ equ f g = g ⋅ equ f g"
proof (intro arr_eqI [of "f ⋅ equ f g"])
show par: "par (f ⋅ equ f g) (g ⋅ equ f g)"
using assms by auto
show "Fun (f ⋅ equ f g) = Fun (g ⋅ equ f g)"
proof
fix x
show "Fun (f ⋅ equ f g) x = Fun (g ⋅ equ f g) x"
proof (cases "x ∈ Set (dom_equ f g)")
case False
show ?thesis
using assms False Fun_equ Fun_def by simp
next
case True
show ?thesis
proof -
have "Fun (f ⋅ equ f g) x = Fun f (Fun (equ f g) x)"
using assms Fun_comp comp_in_homI equ_in_hom comp_assoc by auto
also have "... = Fun f (OUT (Dom_equ f g) x)"
using assms True Fun_equ by simp
also have "... = f ⋅ (OUT (Dom_equ f g) x)"
using Fun_def True assms ide_dom_equ(4) by simp
also have "... = g ⋅ (OUT (Dom_equ f g) x)"
using assms True ide_dom_equ(2) [of f g] bij_betw_apply by force
also have "... = Fun g (Fun (equ f g) x)"
using assms True Fun_def Fun_equ ide_dom_equ by simp
also have "... = Fun (g ⋅ equ f g) x"
using assms Fun_comp comp_in_homI equ_in_hom comp_assoc by auto
finally show ?thesis by blast
qed
qed
qed
qed
lemma equ_is_equalizer:
assumes "par f g"
shows "has_as_equalizer f g (equ f g)"
proof
show "par f g" by fact
show 0: "seq f (equ f g)"
using assms by auto
show "f ⋅ equ f g = g ⋅ equ f g"
using assms equ_equalizes by blast
show "⋀e'. ⟦seq f e'; f ⋅ e' = g ⋅ e'⟧ ⟹ ∃!h. equ f g ⋅ h = e'"
proof -
fix e'
assume seq: "seq f e'" and eq: "f ⋅ e' = g ⋅ e'"
let ?H = "λx. if x ∈ Set (dom e') then IN (Dom_equ f g) (e' ⋅ x) else null"
have H: "?H ∈ Hom (dom e') (dom_equ f g)"
proof
show "?H ∈ {F. ∀x. x ∉ Set (dom e') ⟶ F x = null}" by simp
show "?H ∈ Set (dom e') → Set (dom_equ f g)"
proof
fix x
assume x: "x ∈ Set (dom e')"
have "?H x = IN (Dom_equ f g) (e' ⋅ x)"
using x by simp
moreover have "... ∈ Set (dom_equ f g)"
using assms seq x ide_dom_equ(5)
by (metis (mono_tags, lifting) CollectD CollectI arr_iff_in_hom
comp_in_homI eq local.comp_assoc seqE)
ultimately show "?H x ∈ Set (dom_equ f g)" by auto
qed
qed
let ?h = "mkarr (dom e') (dom_equ f g) ?H"
have h: "«?h : dom e' → dom_equ f g»"
using assms H seq ide_dom_equ
by (intro mkarr_in_hom) auto
have *: "equ f g ⋅ ?h = e'"
proof (intro arr_eqI' [of "equ f g ⋅ ?h"])
show 1: "«equ f g ⋅ ?h : dom e' → dom f»"
using assms h by blast
show e': "«e' : dom e' → dom f»"
by (metis arr_iff_in_hom seq seqE)
show "⋀x. «x : 𝟭⇧? → dom e'» ⟹ (equ f g ⋅ ?h) ⋅ x = e' ⋅ x"
proof -
fix x
assume x: "«x : 𝟭⇧? → dom e'»"
have "(equ f g ⋅ ?h) ⋅ x = equ f g ⋅ ?h ⋅ x"
using comp_assoc by blast
also have "... = equ f g ⋅ ?H x"
using app_mkarr h x by presburger
also have "... = OUT (Dom_equ f g) (IN (Dom_equ f g) (e' ⋅ x))"
proof -
have "?H x ∈ Set (dom_equ f g)"
using 1 x by blast
thus ?thesis
using assms x equ_in_hom app_mkarr
by (simp add: assms equ_def)
qed
also have "... = e' ⋅ x"
proof -
have "e' ⋅ x ∈ Dom_equ f g"
by (metis (mono_tags, lifting) e' comp_in_homI eq comp_assoc
mem_Collect_eq x)
thus ?thesis
using assms ide_dom_equ(7) [of f g "e' ⋅ x"] by blast
qed
finally show "(equ f g ⋅ ?h) ⋅ x = e' ⋅ x" by blast
qed
qed
moreover have "⋀h'. equ f g ⋅ h' = e' ⟹ h' = ?h"
proof -
fix h'
assume h': "equ f g ⋅ h' = e'"
show "h' = ?h"
proof (intro arr_eqI' [of h' _ _ ?h])
show 1: "«h' : dom e' → dom_equ f g»"
by (metis arr_iff_in_hom assms comp_in_homE equ_simps(2) h' in_homE seq)
show "«?h : dom e' → dom_equ f g»"
using h by blast
show "⋀x. «x : 𝟭⇧? → dom e'» ⟹ h' ⋅ x = ?h ⋅ x"
proof -
fix x
assume x: "«x : 𝟭⇧? → dom e'»"
have 3: "h' ⋅ x = IN (Dom_equ f g) (Equ f g (h' ⋅ x))"
using assms h' x 1 seq eq ide_dom_equ(6) comp_in_homI in_homI
by auto
also have 4: "... = IN (Dom_equ f g) (Fun (equ f g) (h' ⋅ x))"
using assms Fun_equ [of f g]
by (metis (lifting))
also have 5: "... = IN (Dom_equ f g) (equ f g ⋅ (h' ⋅ x))"
using Fun_def
by (metis (no_types, lifting) x CollectI comp_in_homI
dom_comp h' in_homI seq seqE)
also have "... = IN (Dom_equ f g) ((equ f g ⋅ h') ⋅ x)"
using comp_assoc by simp
also have "... = IN (Dom_equ f g) ((equ f g ⋅ ?h) ⋅ x)"
using h h' eq "*" by argo
also have "... = IN (Dom_equ f g) (equ f g ⋅ (?h ⋅ x))"
using comp_assoc by simp
also have "... = IN (Dom_equ f g) (Fun (equ f g) (?h ⋅ x))"
using x Fun_def app_mkarr h h' comp_assoc 3 4 5 by auto
also have "... = IN (Dom_equ f g) (Equ f g (?h ⋅ x))"
using assms Fun_equ by (metis (lifting))
also have "... = ?h ⋅ x"
using assms x ide_dom_equ(6) h by auto
finally show "h' ⋅ x = ?h ⋅ x" by blast
qed
qed
qed
ultimately show "∃!h. equ f g ⋅ h = e'" by auto
qed
qed
lemma has_equalizers:
assumes "par f g"
shows "∃e. has_as_equalizer f g e"
using assms equ_is_equalizer by blast
end
subsection "Exported Notions"
text‹
As we don't want to clutter the @{locale sets_cat} locale with auxiliary definitions and
facts that no longer need to be used once we have completed the equalizer construction,
we have carried out the construction in a separate locale and we now transfer
to the @{locale sets_cat} locale only those definitions and facts that we would like to export.
In general, we will need to export the objects and arrows mentioned by the
universal property together with the associated infrastructure for establishing the
types of expressions that use them.
We will also need to export facts that allow us to externalize these arrows
as functions between sets of global elements, and we will need facts that give
the types and inverse relationship between the comparison maps.
›
context sets_cat
begin
interpretation Equ: equalizers_in_sets_cat sml C ..
abbreviation equ
where "equ ≡ Equ.equ"
abbreviation Equ
where "Equ f g ≡ {x. x ∈ Set (dom f) ∧ f ⋅ x = g ⋅ x}"
lemma equalizer_comparison_map_props:
assumes "par f g"
shows "bij_betw (OUT (Equ f g)) (Set (dom (equ f g))) (Equ f g)"
and "bij_betw (IN (Equ f g)) (Equ f g) (Set (dom (equ f g)))"
and "⋀x. x ∈ Set (dom (equ f g)) ⟹ OUT (Equ f g) x ∈ Set (dom f)"
and "⋀y. y ∈ Equ f g ⟹ IN (Equ f g) y ∈ Set (dom (equ f g))"
and "⋀x. x ∈ Set (dom (equ f g)) ⟹ IN (Equ f g) (OUT (Equ f g) x) = x"
and "⋀y. y ∈ Equ f g ⟹ OUT (Equ f g) (IN (Equ f g) y) = y"
using assms Equ.ide_dom_equ [of f g] Equ.equ_simps(2) [of f g] by auto
lemma equ_is_equalizer:
assumes "par f g"
shows "has_as_equalizer f g (equ f g)"
using assms Equ.equ_is_equalizer by blast
lemma Fun_equ:
assumes "par f g"
shows "Fun (equ f g) = (λx. if x ∈ Set (dom (equ f g))
then OUT {x. x ∈ Set (dom f) ∧ f ⋅ x = g ⋅ x} x
else null)"
using assms Equ.Fun_equ by auto
lemma has_equalizers:
assumes "par f g"
shows "∃e. has_as_equalizer f g e"
using assms Equ.has_equalizers by blast
end
section "Binary Products"
text‹
In this section we show that the category of small sets and functions has binary products.
We follow the same pattern as for equalizers, except that now the set to which we would
like to apply ‹mkide› to obtain a product object will consist of pairs of arrows,
rather than individual arrows. This means that we will need to assume the existence of
a pairing function that embeds the set of pairs of arrows of the category back into the
original set of arrows. Once again, in showing that the construction makes sense we will
need to reason about comparison maps, but once this is done we will be left simply with a
universal property which does not mention these maps. After that, we only have to work
with the comparison maps when relating notions internal to the category to notions
external to it.
›
text‹
The following locale specializes @{locale sets_cat} by adding the assumption that there exists
a suitable pairing function. In addition, we need to assume that the smallness notion
being used is respected by pairing.
›
locale sets_cat_with_pairing =
sets_cat sml C +
small_product sml +
pairing ‹Collect arr›
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
text‹
As previously, we carry out the details of the construction in an auxiliary locale
and later transfer to the @{locale sets_cat} locale only those things that we want to export.
›
locale products_in_sets_cat =
sets_cat_with_pairing sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
lemma small_product_set:
assumes "ide a" and "ide b"
shows "small (Set a × Set b)"
using assms small_Set by fastforce
lemma embeds_product_sets:
assumes "ide a" and "ide b"
shows "embeds (Set a × Set b)"
proof -
have "Set a × Set b ⊆ Collect arr × Collect arr"
using assms small_Set by auto
thus ?thesis
using assms embeds_pairs
by (meson image_mono inj_on_subset subset_trans)
qed
text‹
We define the product of two objects as the object determined by the cartesian
product of their sets of elements.
›
definition prod⇩o
where "prod⇩o a b ≡ mkide (Set a × Set b)"
lemma ide_prod⇩o:
assumes "ide a" and "ide b"
shows "ide (prod⇩o a b)"
and "bij_betw (OUT (Set a × Set b)) (Set (prod⇩o a b)) (Set a × Set b)"
and "bij_betw (IN (Set a × Set b)) (Set a × Set b) (Set (prod⇩o a b))"
and "⋀x. x ∈ Set (prod⇩o a b) ⟹ OUT (Set a × Set b) x ∈ Set a × Set b"
and "⋀y. y ∈ Set a × Set b ⟹ IN (Set a × Set b) y ∈ Set (prod⇩o a b)"
and "⋀x. x ∈ Set (prod⇩o a b) ⟹ IN (Set a × Set b) (OUT (Set a × Set b) x) = x"
and "⋀y. y ∈ Set a × Set b ⟹ OUT (Set a × Set b) (IN (Set a × Set b) y) = y"
proof -
have 1: "small (Set a × Set b)"
using assms ide_char small_Set small_product by metis
moreover have 2: "is_embedding_of some_pairing (Set a × Set b)"
proof -
have "Set a × Set b ⊆ Collect arr × Collect arr"
using assms ide_char small_Set by blast
thus ?thesis
using assms some_pairing_is_embedding
by (meson image_mono inj_on_subset subset_trans)
qed
ultimately show "ide (prod⇩o a b)"
and 3: "bij_betw (OUT (Set a × Set b)) (Set (prod⇩o a b)) (Set a × Set b)"
unfolding prod⇩o_def
using assms ide_mkide bij_OUT by blast+
show 4: "bij_betw (IN (Set a × Set b)) (Set a × Set b) (Set (prod⇩o a b))"
using ‹bij_betw (OUT (Set a × Set b)) (Set (prod⇩o a b)) (Set a × Set b)›
bij_betw_inv_into prod⇩o_def
by auto
show "⋀x. x ∈ Set (prod⇩o a b) ⟹ OUT (Set a × Set b) x ∈ Set a × Set b"
using 3 bij_betwE by blast
show "⋀y. y ∈ Set a × Set b ⟹ IN (Set a × Set b) y ∈ Set (prod⇩o a b)"
using 4 bij_betwE by blast
show "⋀x. x ∈ Set (prod⇩o a b) ⟹ IN (Set a × Set b) (OUT (Set a × Set b) x) = x"
using 1 2 IN_OUT prod⇩o_def by auto
show "⋀y. y ∈ Set a × Set b ⟹ OUT (Set a × Set b) (IN (Set a × Set b) y) = y"
by (metis "1" "2" OUT_IN)
qed
text‹
We next define the projection arrows from a product object in terms of the projection
functions on the underlying cartesian product of sets.
›
abbreviation P⇩0 :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "P⇩0 a b ≡ λx. if x ∈ Set (prod⇩o a b) then snd (OUT (Set a × Set b) x) else null"
abbreviation P⇩1 :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "P⇩1 a b ≡ λx. if x ∈ Set (prod⇩o a b) then fst (OUT (Set a × Set b) x) else null"
lemma P⇩0_in_Hom:
assumes "ide a" and "ide b"
shows "P⇩0 a b ∈ Hom (prod⇩o a b) b"
proof
show "P⇩0 a b ∈ Set (prod⇩o a b) → Set b"
proof
fix x
assume x: "x ∈ Set (prod⇩o a b)"
have "OUT (Set a × Set b) x ∈ Set a × Set b"
using assms x bij_betwE ide_prod⇩o(2) by blast
thus "P⇩0 a b x ∈ Set b"
using assms x by force
qed
show "P⇩0 a b ∈ {F. ∀x. x ∉ Set (prod⇩o a b) ⟶ F x = null}"
by simp
qed
lemma P⇩1_in_Hom:
assumes "ide a" and "ide b"
shows "P⇩1 a b ∈ Hom (prod⇩o a b) a"
proof
show "P⇩1 a b ∈ Set (prod⇩o a b) → Set a"
proof
fix x
assume x: "x ∈ Set (prod⇩o a b)"
have "OUT (Set a × Set b) x ∈ Set a × Set b"
using assms x bij_betwE ide_prod⇩o(2) by blast
thus "P⇩1 a b x ∈ Set a"
using assms x by force
qed
show "P⇩1 a b ∈ {F. ∀x. x ∉ Set (prod⇩o a b) ⟶ F x = null}"
by simp
qed
definition pr⇩0 :: "'U ⇒ 'U ⇒ 'U"
where "pr⇩0 a b ≡ mkarr (prod⇩o a b) b (P⇩0 a b)"
definition pr⇩1 :: "'U ⇒ 'U ⇒ 'U"
where "pr⇩1 a b ≡ mkarr (prod⇩o a b) a (P⇩1 a b)"
lemma pr_in_hom [intro]:
assumes "ide a" and "ide b"
shows "in_hom (pr⇩1 a b) (prod⇩o a b) a"
and "in_hom (pr⇩0 a b) (prod⇩o a b) b"
using assms pr⇩0_def pr⇩1_def mkarr_in_hom ide_prod⇩o P⇩0_in_Hom P⇩1_in_Hom by auto
lemma pr_simps [simp]:
assumes "ide a" and "ide b"
shows "arr (pr⇩0 a b)" and "dom (pr⇩0 a b) = prod⇩o a b" and "cod (pr⇩0 a b) = b"
and "arr (pr⇩1 a b)" and "dom (pr⇩1 a b) = prod⇩o a b" and "cod (pr⇩1 a b) = a"
using assms pr_in_hom by blast+
lemma Fun_pr:
assumes "ide a" and "ide b"
shows "Fun (pr⇩1 a b) = P⇩1 a b"
and "Fun (pr⇩0 a b) = P⇩0 a b"
using assms Fun_mkarr pr⇩0_def pr⇩1_def pr_simps(1,4) by presburger+
text‹
Tupling of arrows is also defined in terms of the underlying cartesian product.
›
definition Tuple :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "Tuple f g ≡ (λx. if x ∈ Set (dom f)
then IN (Set (cod f) × Set (cod g)) (Fun f x, Fun g x)
else null)"
definition tuple :: "'U ⇒ 'U ⇒ 'U"
where "tuple f g ≡ mkarr (dom f) (prod⇩o (cod f) (cod g)) (Tuple f g)"
lemma tuple_in_hom [intro]:
assumes "«f : c → a»" and "«g : c → b»"
shows "«tuple f g : c → prod⇩o a b»"
proof -
have "Tuple f g ∈ Set c → Set (prod⇩o a b)"
proof
fix x
assume x: "x ∈ Set c"
have "bij_betw (IN (Set a × Set b)) (Set a × Set b) (Set (mkide (Set a × Set b)))"
using assms embeds_pairs ide_prod⇩o(2) prod⇩o_def
by (metis ide_cod ide_prod⇩o(3) in_homE)
thus "Tuple f g x ∈ Set (prod⇩o a b)"
unfolding Tuple_def prod⇩o_def Fun_def
using assms x bij_betw_apply in_homE small_Set
by auto fastforce
qed
moreover have "⋀x. x ∉ Set c ⟹ Tuple f g x = null"
unfolding Tuple_def
using assms by auto
ultimately show ?thesis
unfolding tuple_def
using assms mkarr_in_hom ide_prod⇩o(1) by fastforce
qed
lemma tuple_simps [simp]:
assumes "span f g"
shows "arr (tuple f g)"
and "dom (tuple f g) = dom f"
and "cod (tuple f g) = prod⇩o (cod f) (cod g)"
using assms
by (metis assms in_homE in_homI tuple_in_hom)+
text‹
In verifying the equations required for a categorical product, we unfortunately
do have to fuss with the comparison maps.
›
lemma comp_pr_tuple:
assumes "span f g"
shows "pr⇩1 (cod f) (cod g) ⋅ tuple f g = f"
and "pr⇩0 (cod f) (cod g) ⋅ tuple f g = g"
proof -
let ?c = "dom f" and ?a = "cod f" and ?b = "cod g"
show "pr⇩1 ?a ?b ⋅ tuple f g = f"
proof -
have "pr⇩1 ?a ?b ⋅ tuple f g =
mkarr (prod⇩o ?a ?b) ?a (P⇩1 ?a ?b) ⋅ mkarr ?c (prod⇩o ?a ?b) (Tuple f g)"
unfolding pr⇩1_def tuple_def Tuple_def
using assms by auto
also have "... = mkarr ?c ?a (P⇩1 ?a ?b ∘ Tuple f g)"
using assms comp_mkarr
by (metis (lifting) calculation ide_cod pr_simps(4,5) seqE seqI tuple_simps(1,3))
also have "... = mkarr ?c ?a
(λx. if x ∈ Set ?c
then fst (OUT (Set ?a × Set ?b)
(IN (Set ?a × Set ?b) (Fun f x, Fun g x)))
else null)"
proof -
have "(P⇩1 ?a ?b ∘ Tuple f g) =
(λx. if «x : 𝟭⇧? → ?c»
then fst (OUT (Set ?a × Set ?b)
(IN (Set ?a × Set ?b) (Fun f x, Fun g x)))
else null)"
using assms ide_prod⇩o(3) [of ?a ?b] bij_betw_apply Tuple_def Fun_def by fastforce
thus ?thesis by simp
qed
also have "... = mkarr ?c ?a (λx. if x ∈ Set ?c then fst (Fun f x, Fun g x) else null)"
proof -
have "⋀x. x ∈ Set ?c ⟹
OUT (Set ?a × Set ?b) (IN (Set ?a × Set ?b) (Fun f x, Fun g x)) =
(Fun f x, Fun g x)"
using assms OUT_IN [of "Set ?a × Set ?b"] small_product_set embeds_product_sets
Fun_def
by auto
thus ?thesis
by (metis (lifting))
qed
also have "... = mkarr ?c ?a (λx. if x ∈ Set ?c then Fun f x else null)"
using assms by (metis (lifting) fst_eqD)
also have "... = f"
proof -
have "Fun f = (λx. if x ∈ Set ?c then Fun f x else null)"
unfolding Fun_def by meson
thus ?thesis
by (metis (no_types, lifting) arr_iff_in_hom assms mkarr_Fun)
qed
finally show ?thesis by simp
qed
show "pr⇩0 ?a ?b ⋅ tuple f g = g"
proof -
have "pr⇩0 ?a ?b ⋅ tuple f g =
mkarr (prod⇩o ?a ?b) ?b (P⇩0 ?a ?b) ⋅ mkarr ?c (prod⇩o ?a ?b) (Tuple f g)"
unfolding pr⇩0_def tuple_def Tuple_def
using assms comp_mkarr by auto
also have "... = mkarr ?c ?b (P⇩0 ?a ?b ∘ Tuple f g)"
using assms comp_mkarr
by (metis (lifting) calculation ide_cod seqE seqI pr_simps(1,2) tuple_simps(1,3))
also have "... = mkarr ?c ?b
(λx. if x ∈ Set ?c
then snd (OUT (Set ?a × Set ?b)
(IN (Set ?a × Set ?b) (Fun f x, Fun g x)))
else null)"
proof -
have "(P⇩0 ?a ?b ∘ Tuple f g) =
(λx. if x ∈ Set ?c
then snd (OUT (Set ?a × Set ?b)
(IN (Set ?a × Set ?b) (Fun f x, Fun g x)))
else null)"
using assms ide_prod⇩o(3) [of ?a ?b] bij_betw_apply Tuple_def Fun_def by fastforce
thus ?thesis by simp
qed
also have "... = mkarr ?c ?b (λx. if x ∈ Set ?c then snd (Fun f x, Fun g x) else null)"
proof -
have "⋀x. x ∈ Set ?c ⟹
OUT (Set ?a × Set ?b) (IN (Set ?a × Set ?b) (Fun f x, Fun g x)) =
(Fun f x, Fun g x)"
using assms OUT_IN [of "Set ?a × Set ?b"] small_product_set embeds_product_sets
Fun_def
by auto
thus ?thesis
by (metis (lifting))
qed
also have "... = mkarr ?c ?b (λx. if x ∈ Set ?c then Fun g x else null)"
using assms by (metis (lifting) snd_eqD)
also have "... = g"
proof -
have "Fun g = (λx. if x ∈ Set ?c then Fun g x else null)"
unfolding Fun_def by (metis assms)
thus ?thesis
by (metis (no_types, lifting) arr_iff_in_hom assms mkarr_Fun)
qed
finally show ?thesis by simp
qed
qed
lemma Fun_tuple:
assumes "span f g"
shows "Fun (tuple f g) =
(λx. if x ∈ Set (dom f)
then IN (Set (cod f) × Set (cod g)) (Fun f x, Fun g x)
else null)"
using tuple_def Tuple_def Fun_mkarr assms tuple_simps(1) by presburger
lemma binary_product_pr:
assumes "ide a" and "ide b"
shows "binary_product C a b (pr⇩1 a b) (pr⇩0 a b)"
proof
show "has_as_binary_product a b (pr⇩1 a b) (pr⇩0 a b)"
proof
show 1: "span (pr⇩1 a b) (pr⇩0 a b)"
using assms by auto
show "cod (pr⇩1 a b) = a"
using assms by auto
show "cod (pr⇩0 a b) = b"
using assms by auto
fix x f g
assume f: "«f : x → a»" and g: "«g : x → b»"
let ?H = "λz. if z ∈ Set x then IN (Set a × Set b) (Fun f z, Fun g z) else null"
let ?h = "mkarr x (prod⇩o a b) ?H"
have h: "«?h : x → dom (pr⇩1 a b)» ∧ C (pr⇩1 a b) ?h = f ∧ C (pr⇩0 a b) ?h = g"
using assms f g tuple_in_hom [of f x a g b] comp_pr_tuple [of f g]
unfolding tuple_def Tuple_def by auto
moreover have "⋀h'. «h' : x → dom (pr⇩1 a b)» ∧ C (pr⇩1 a b) h' = f ∧
C (pr⇩0 a b) h' = g
⟹ h' = ?h"
proof -
fix h'
assume h': "«h' : x → dom (pr⇩1 a b)» ∧ C (pr⇩1 a b) h' = f ∧ C (pr⇩0 a b) h' = g"
show "h' = ?h"
proof (intro arr_eqI' [of h'])
show "«h' : x → dom (prod⇩o a b)»"
using assms h' ide_prod⇩o(1) by auto
show "«?h : x → dom (prod⇩o a b)»"
using assms h ide_prod⇩o(1) by auto
show "⋀z. «z : 𝟭⇧? → x» ⟹ h' ⋅ z = ?h ⋅ z"
proof -
fix z
assume z: "«z : 𝟭⇧? → x»"
have "h' ⋅ z = Fun h' z"
using h' z Fun_def by auto
also have "... = IN (Set a × Set b) (Fun f z, Fun g z)"
proof -
have "fst (OUT (Set a × Set b) (Fun h' z)) = Fun f z"
proof -
have "Fun f z = Fun (pr⇩1 a b ⋅ h') z"
using h' by force
also have "... = (P⇩1 a b ∘ Fun h') z"
using assms(1-2) f h' Fun_pr(1) Fun_comp arrI by auto
also have "... = fst (OUT (Set a × Set b) (Fun h' z))"
using assms(1,2) h' z Fun_def by auto
finally show ?thesis by simp
qed
moreover have "snd (OUT (Set a × Set b) (Fun h' z)) = Fun g z"
proof -
have "Fun g z = Fun (pr⇩0 a b ⋅ h') z"
using h' by force
also have "... = (P⇩0 a b ∘ Fun h') z"
using assms(1-2) g h' Fun_pr(2) Fun_comp arrI by auto
also have "... = snd (OUT (Set a × Set b) (Fun h' z))"
using assms(1,2) h' z Fun_def by auto
finally show ?thesis by simp
qed
ultimately have "IN (Set a × Set b) (Fun f z, Fun g z) =
IN (Set a × Set b) (OUT (Set a × Set b) (Fun h' z))"
by (metis split_pairs2)
also have "... = Fun h' z"
using assms h' z IN_OUT ‹C h' z = Fun h' z› prod⇩o_def Fun_def
small_product_set [of a b] embeds_product_sets [of a b]
by auto
finally show ?thesis by simp
qed
also have "... = C ?h z"
using app_mkarr assms(1,2) h z by auto
finally show "C h' z = C ?h z" by blast
qed
qed
qed
ultimately show "∃!h. «h : x → dom (pr⇩1 a b)» ∧ C (pr⇩1 a b) h = f ∧
C (pr⇩0 a b) h = g"
by auto
qed
qed
lemma has_binary_products:
shows has_binary_products
using binary_product_pr
by (meson binary_product.has_as_binary_product has_binary_products_def)
end
subsection "Exported Notions"
text‹
We now transfer to the @{locale sets_cat_with_pairing} locale just the things we want to export.
The projections are the main thing; most of the rest is inherited from the
@{locale elementary_category_with_binary_products} locale. We also need to include some
infrastucture for moving in and out of the category and working with the comparison maps.
›
context sets_cat_with_pairing
begin
interpretation Products: products_in_sets_cat ..
abbreviation pr⇩0 :: "'U ⇒ 'U ⇒ 'U"
where "pr⇩0 ≡ Products.pr⇩0"
abbreviation pr⇩1 :: "'U ⇒ 'U ⇒ 'U"
where "pr⇩1 ≡ Products.pr⇩1"
sublocale elementary_category_with_binary_products C pr⇩0 pr⇩1
proof
show "⋀f g. span f g ⟹ ∃!l. C (pr⇩1 (cod f) (cod g)) l = f ∧ C (pr⇩0 (cod f) (cod g)) l = g"
proof -
fix f g
assume fg: "span f g"
interpret binary_product C ‹cod f› ‹cod g› ‹pr⇩1 (cod f) (cod g)› ‹pr⇩0 (cod f) (cod g)›
using fg Products.binary_product_pr ide_cod by blast
show "∃!l. C (pr⇩1 (cod f) (cod g)) l = f ∧ C (pr⇩0 (cod f) (cod g)) l = g"
by (metis (full_types) fg tuple_props(4,5,6))
qed
qed auto
lemma bin_prod_comparison_map_props:
assumes "ide a" and "ide b"
shows "OUT (Set a × Set b) ∈ Set (prod a b) → Set a × Set b"
and "IN (Set a × Set b) ∈ Set a × Set b → Set (prod a b)"
and "⋀x. x ∈ Set (prod a b) ⟹ IN (Set a × Set b) (OUT (Set a × Set b) x) = x"
and "⋀y. y ∈ Set a × Set b ⟹ OUT (Set a × Set b) (IN (Set a × Set b) y) = y"
and "bij_betw (OUT (Set a × Set b)) (Set (prod a b)) (Set a × Set b)"
and "bij_betw (IN (Set a × Set b)) (Set a × Set b) (Set (prod a b))"
using assms Products.ide_prod⇩o [of a b] pr_simps(5) by auto
lemma Fun_pr⇩0:
assumes "ide a" and "ide b"
shows "Fun (pr⇩0 a b) = Products.P⇩0 a b"
using assms Products.Fun_pr(2) by auto[1]
lemma Fun_pr⇩1:
assumes "ide a" and "ide b"
shows "Fun (pr⇩1 a b) = Products.P⇩1 a b"
using assms Products.Fun_pr(1) by auto[1]
lemma Fun_prod:
assumes "«f : a → b»" and "«g : c → d»"
shows "Fun (prod f g) = (λx. if x ∈ Set (prod a c)
then tuple (Fun f (C (pr⇩1 a c) x)) (Fun g (C (pr⇩0 a c) x))
else null)"
proof
fix x
show "Fun (prod f g) x = (if x ∈ Set (prod a c)
then tuple (Fun f (C (pr⇩1 a c) x)) (Fun g (C (pr⇩0 a c) x))
else null)"
proof (cases "x ∈ Set (prod a c)")
case False
show ?thesis
using False
by (metis assms(1,2) in_homE prod_simps(2) Fun_def)
next
case True
show ?thesis
proof -
have "«x : 𝟭⇧? → dom (prod f g)»"
using True assms(1,2) by fastforce
moreover have "«pr⇩1 a c ⋅ x : 𝟭⇧? → dom f» ∧ «pr⇩0 a c ⋅ x : 𝟭⇧? → dom g»"
using assms True
by (intro conjI comp_in_homI) fastforce+
moreover have "prod f g ⋅ x = tuple (f ⋅ pr⇩1 a c ⋅ x) (g ⋅ pr⇩0 a c ⋅ x)"
using assms True prod_tuple tuple_pr_arr
by (metis calculation(2) ide_dom in_homE seqI)
ultimately show ?thesis
using assms True Fun_def by auto
qed
qed
qed
lemma prod_ide_eq:
assumes "ide a" and "ide b"
shows "prod a b = mkide (Set a × Set b)"
using assms(1,2) pr_simps(2) Products.prod⇩o_def by force
lemma tuple_eq:
assumes "«f : x → a»" and "«g : x → b»"
shows "tuple f g = mkarr x (prod a b)
(λz. if z ∈ Set x
then IN (Set a × Set b) (Fun f z, Fun g z)
else null)"
proof -
have "tuple f g = Products.tuple f g"
by (metis Products.comp_pr_tuple(1,2) assms(1,2) in_homE pr_tuple(1,2) universal)
thus ?thesis
unfolding Products.tuple_def Products.Tuple_def
using assms Products.prod⇩o_def prod_ide_eq by fastforce
qed
lemma tuple_point_eq:
assumes "«x : 𝟭⇧? → a»" and "«y : 𝟭⇧? → b»"
shows "tuple x y = IN (Set a × Set b) (x, y)"
proof -
have 1: "tuple x y = mkarr 𝟭⇧? (prod a b)
(λz. if z ∈ Set 𝟭⇧? then IN (Set a × Set b) (x, y) else null)"
proof -
have "⋀z. z ∈ Set 𝟭⇧? ⟹ Fun x z = x ∧ Fun y z = y"
unfolding Fun_def
by (metis assms CollectD comp_arr_dom ide_dom ide_in_hom in_homE some_trm_eqI)
hence "(λz. if z ∈ Set 𝟭⇧? then IN (Set a × Set b) (Fun x z, Fun y z) else null) =
(λz. if z ∈ Set 𝟭⇧? then IN (Set a × Set b) (x, y) else null)"
by fastforce
thus ?thesis
using assms tuple_eq by simp
qed
also have "... = IN (Set a × Set b) (x, y)"
proof -
have "mkarr 𝟭⇧? (prod a b)
(λz. if z ∈ Set 𝟭⇧? then IN (Set a × Set b) (x, y) else null) =
mkarr 𝟭⇧? (prod a b)
(λz. if z ∈ Set 𝟭⇧? then IN (Set a × Set b) (x, y) else null) ⋅ 𝟭⇧?"
by (metis (lifting) assms(1,2) calculation comp_arr_dom dom_mkarr in_homE
tuple_simps(1))
also have "... = IN (Set a × Set b) (x, y)"
using app_mkarr [of "𝟭⇧?" "prod a b" _ "𝟭⇧?"]
by (metis (full_types, lifting) CollectI
assms(1,2) 1 ide_in_hom ide_some_terminal tuple_in_hom)
finally show ?thesis by blast
qed
finally show ?thesis by blast
qed
lemma Fun_tuple:
assumes "span f g"
shows "Fun (tuple f g) =
(λx. if x ∈ Set (dom f)
then IN (Set (cod f) × Set (cod g)) (Fun f x, Fun g x)
else null)"
using assms Fun_mkarr tuple_eq [of f "dom f" "cod f" g "cod g"]
by (metis (lifting) in_homI tuple_simps(1))
end
section "Binary Coproducts"
text‹
In this section we prove the existence of binary coproducts, following the
same approach as for binary products. The required assumptions are slightly
different, because here we need smallness to be preserved by union.
›
locale sets_cat_with_cotupling =
sets_cat_with_bool sml C +
small_sum sml +
pairing ‹Collect arr›
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
locale coproducts_in_sets_cat =
sets_cat_with_cotupling sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
abbreviation Coprod
where "Coprod a b ≡ ({tt} × Set a) ∪ ({ff} × Set b)"
lemma small_Coprod:
assumes "ide a" and "ide b"
shows "small (Coprod a b)"
using assms small_product
by (metis Set_two ide_two(1) small_Set small_insert_iff small_union)
lemma embeds_Coprod:
assumes "ide a" and "ide b"
shows "embeds (Coprod a b)"
proof -
have "Coprod a b ⊆ Collect arr × Collect arr"
using ff_simps(1) tt_simps(1) by blast
thus ?thesis
using embeds_pairs
by (simp add: embeds_subset)
qed
definition coprod⇩o
where "coprod⇩o a b ≡ mkide (Coprod a b)"
lemma ide_coprod⇩o:
assumes "ide a" and "ide b"
shows "ide (coprod⇩o a b)"
and "bij_betw (OUT (Coprod a b)) (Set (coprod⇩o a b)) (Coprod a b)"
and "bij_betw (IN (Coprod a b)) (Coprod a b) (Set (coprod⇩o a b))"
and "⋀x. x ∈ Set (coprod⇩o a b) ⟹ OUT (Coprod a b) x ∈ Coprod a b"
and "⋀y. y ∈ Coprod a b ⟹ IN (Coprod a b) y ∈ Set (coprod⇩o a b)"
and "⋀x. x ∈ Set (coprod⇩o a b) ⟹ IN (Coprod a b) (OUT (Coprod a b) x) = x"
and "⋀y. y ∈ Coprod a b ⟹ OUT (Coprod a b) (IN (Coprod a b) y) = y"
proof -
show "ide (coprod⇩o a b)"
and 1: "bij_betw (OUT (Coprod a b)) (Set (coprod⇩o a b)) (Coprod a b)"
unfolding coprod⇩o_def
using assms ide_mkide(1) bij_OUT small_Coprod embeds_Coprod by metis+
show 2: "bij_betw (IN (Coprod a b)) (Coprod a b) (Set (coprod⇩o a b))"
using 1 bij_betw_inv_into coprod⇩o_def by auto
show "⋀x. x ∈ Set (coprod⇩o a b) ⟹ OUT (Coprod a b) x ∈ Coprod a b"
using 1 bij_betwE by blast
show "⋀y. y ∈ Coprod a b ⟹ IN (Coprod a b) y ∈ Set (coprod⇩o a b)"
using 2 bij_betwE by blast
show "⋀x. x ∈ Set (coprod⇩o a b) ⟹ IN (Coprod a b) (OUT (Coprod a b) x) = x"
using assms small_Coprod embeds_Coprod IN_OUT coprod⇩o_def by metis
show "⋀y. y ∈ Coprod a b ⟹ OUT (Coprod a b) (IN (Coprod a b) y) = y"
using assms small_Coprod embeds_Coprod coprod⇩o_def 1
bij_betw_inv_into_right
[of "OUT (Coprod a b)" "Set (coprod⇩o a b)" "Coprod a b"]
by presburger
qed
abbreviation In⇩0 :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "In⇩0 a b ≡ λx. if x ∈ Set b then IN (Coprod a b) (ff, x) else null"
abbreviation In⇩1 :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "In⇩1 a b ≡ λx. if x ∈ Set a then IN (Coprod a b) (tt, x) else null"
lemma In⇩0_in_Hom:
assumes "ide a" and "ide b"
shows "In⇩0 a b ∈ Hom b (coprod⇩o a b)"
proof
show "In⇩0 a b ∈ {F. ∀x. x ∉ Set b ⟶ F x = null}" by simp
show "In⇩0 a b ∈ Set b → Set (coprod⇩o a b)"
proof
fix x
assume x: "x ∈ Set b"
have "(ff, x) ∈ Coprod a b"
using assms x by blast
thus "In⇩0 a b x ∈ Set (coprod⇩o a b)"
using assms x ide_coprod⇩o(3) bij_betwE ide_coprod⇩o(5) by presburger
qed
qed
lemma In⇩1_in_Hom:
assumes "ide a" and "ide b"
shows "In⇩1 a b ∈ Hom a (coprod⇩o a b)"
proof
show "In⇩1 a b ∈ {F. ∀x. x ∉ Set a ⟶ F x = null}" by simp
show "In⇩1 a b ∈ Set a → Set (coprod⇩o a b)"
proof
fix x
assume x: "x ∈ Set a"
have "(tt, x) ∈ Coprod a b"
using assms x by blast
thus "In⇩1 a b x ∈ Set (coprod⇩o a b)"
using assms x ide_coprod⇩o(3) bij_betwE ide_coprod⇩o(5) by presburger
qed
qed
definition in⇩0 :: "'U ⇒ 'U ⇒ 'U"
where "in⇩0 a b ≡ mkarr b (coprod⇩o a b) (In⇩0 a b)"
definition in⇩1 :: "'U ⇒ 'U ⇒ 'U"
where "in⇩1 a b ≡ mkarr a (coprod⇩o a b) (In⇩1 a b)"
lemma in_in_hom [intro, simp]:
assumes "ide a" and "ide b"
shows "in_hom (in⇩1 a b) a (coprod⇩o a b)"
and "in_hom (in⇩0 a b) b (coprod⇩o a b)"
using assms in⇩0_def in⇩1_def mkarr_in_hom ide_coprod⇩o In⇩0_in_Hom In⇩1_in_Hom by auto
lemma in_simps [simp]:
assumes "ide a" and "ide b"
shows "arr (in⇩0 a b)" and "dom (in⇩0 a b) = b" and "cod (in⇩0 a b) = coprod⇩o a b"
and "arr (in⇩1 a b)" and "dom (in⇩1 a b) = a" and "cod (in⇩1 a b) = coprod⇩o a b"
using assms in_in_hom by blast+
lemma Fun_in:
assumes "ide a" and "ide b"
shows "Fun (in⇩1 a b) = In⇩1 a b"
and "Fun (in⇩0 a b) = In⇩0 a b"
using assms Fun_mkarr in⇩0_def in⇩1_def in_simps(1,4) by presburger+
definition Cotuple :: "'U ⇒ 'U ⇒ 'U ⇒ 'U"
where "Cotuple f g ≡ (λx. if x ∈ Set (coprod⇩o (dom f) (dom g))
then if fst (OUT (Coprod (dom f) (dom g)) x) = tt
then Fun f (snd (OUT (Coprod (dom f) (dom g)) x))
else if fst (OUT (Coprod (dom f) (dom g)) x) = ff
then Fun g (snd (OUT (Coprod (dom f) (dom g)) x))
else null
else null)"
definition cotuple :: "'U ⇒ 'U ⇒ 'U"
where "cotuple f g ≡ mkarr (coprod⇩o (dom f) (dom g)) (cod f) (Cotuple f g)"
lemma cotuple_in_hom [intro, simp]:
assumes "«f : a → c»" and "«g : b → c»"
shows "«cotuple f g : coprod⇩o a b → c»"
proof -
have bij: "bij_betw (OUT (Coprod a b)) (Set (coprod⇩o a b)) (Coprod a b)"
using assms ide_coprod⇩o(2) ide_dom by blast
have "Cotuple f g ∈ Set (coprod⇩o a b) → Set c"
proof
fix x
assume x: "x ∈ Set (coprod⇩o a b)"
have 1: "OUT (Coprod a b) x ∈ Coprod a b"
using x bij bij_betwE by blast
have "fst (OUT (Coprod a b) x) = tt ∨ fst (OUT (Coprod a b) x) = ff"
using 1 by fastforce
moreover have "fst (OUT (Coprod a b) x) = tt ⟹ Cotuple f g x ∈ Set c"
proof -
assume 2: "fst (OUT (Coprod a b) x) = tt"
have "snd (OUT (Coprod a b) x) ∈ Set a"
using 1 2 tt_ne_ff by auto
thus ?thesis
unfolding Cotuple_def
using assms x 2 Fun_in_Hom [of f a c] tt_ne_ff
by auto fastforce
qed
moreover have "fst (OUT (Coprod a b) x) = ff ⟹ Cotuple f g x ∈ Set c"
proof -
assume 2: "fst (OUT (Coprod a b) x) = ff"
have "snd (OUT (Coprod a b) x) ∈ Set b"
using 1 2 tt_ne_ff by auto
thus ?thesis
unfolding Cotuple_def
using assms x 2 Fun_in_Hom [of g b c] tt_ne_ff by auto
qed
ultimately show "Cotuple f g x ∈ Set c" by blast
qed
moreover have "⋀x. x ∉ Set (coprod⇩o a b) ⟹ Cotuple f g x = null"
unfolding Cotuple_def
using assms by auto
ultimately show ?thesis
unfolding cotuple_def
using assms mkarr_in_hom ide_coprod⇩o(1) by fastforce
qed
lemma cotuple_simps [simp]:
assumes "cospan f g"
shows "arr (cotuple f g)"
and "dom (cotuple f g) = coprod⇩o (dom f) (dom g)"
and "cod (cotuple f g) = cod f"
using assms
by (metis assms in_homE in_homI cotuple_in_hom)+
lemma comp_cotuple_in:
assumes "cospan f g"
shows "cotuple f g ⋅ in⇩1 (dom f) (dom g) = f"
and "cotuple f g ⋅ in⇩0 (dom f) (dom g) = g"
proof -
let ?a = "dom f" and ?b = "dom g" and ?c = "cod f"
show "cotuple f g ⋅ in⇩1 (dom f) (dom g) = f"
proof -
have "cotuple f g ⋅ in⇩1 (dom f) (dom g) =
mkarr (coprod⇩o ?a ?b) ?c (Cotuple f g) ⋅ mkarr ?a (coprod⇩o ?a ?b) (In⇩1 ?a ?b)"
unfolding in⇩1_def cotuple_def
using assms by auto
also have "... = mkarr ?a ?c (Cotuple f g ∘ In⇩1 ?a ?b)"
using assms comp_mkarr cotuple_def cotuple_simps(1) ide_dom in⇩1_def in_simps(4)
by presburger
also have "... = mkarr ?a ?c
(λx. if x ∈ Set ?a
then Fun f (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (tt, x))))
else null)"
proof -
have "⋀x. x ∈ Set ?a ⟹
(Cotuple f g ∘ In⇩1 ?a ?b) x =
Fun f (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (tt, x))))"
unfolding Cotuple_def tt_ne_ff
using assms tt_ne_ff ide_coprod⇩o by auto
hence "Cotuple f g ∘ In⇩1 ?a ?b =
(λx. if x ∈ Set ?a
then Fun f (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (tt, x))))
else null)"
unfolding Cotuple_def
by fastforce
thus ?thesis by simp
qed
also have "... = mkarr ?a ?c (λx. if x ∈ Set ?a then Fun f x else null)"
proof -
have "⋀x. x ∈ Set ?a ⟹
Fun f (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (tt, x)))) = Fun f x"
using assms ide_coprod⇩o(7) by auto
thus ?thesis
by meson
qed
also have "... = f"
proof -
have "Fun f = (λx. if x ∈ Set ?a then Fun f x else null)"
unfolding Fun_def by meson
thus ?thesis
by (metis (no_types, lifting) arr_iff_in_hom assms mkarr_Fun)
qed
finally show ?thesis by blast
qed
show "cotuple f g ⋅ in⇩0 (dom f) (dom g) = g"
proof -
have "cotuple f g ⋅ in⇩0 (dom f) (dom g) =
mkarr (coprod⇩o ?a ?b) ?c (Cotuple f g) ⋅ mkarr ?b (coprod⇩o ?a ?b) (In⇩0 ?a ?b)"
unfolding in⇩0_def cotuple_def
using assms by auto
also have "... = mkarr ?b ?c (Cotuple f g ∘ In⇩0 ?a ?b)"
using assms comp_mkarr cotuple_def cotuple_simps(1) ide_dom in⇩0_def in_simps(1)
by presburger
also have "... = mkarr ?b ?c
(λx. if x ∈ Set ?b
then Fun g (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (ff, x))))
else null)"
proof -
have "⋀x. x ∈ Set ?b ⟹
(Cotuple f g ∘ In⇩0 ?a ?b) x =
Fun g (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (ff, x))))"
unfolding Cotuple_def tt_ne_ff
using assms tt_ne_ff ide_coprod⇩o by auto
hence "Cotuple f g ∘ In⇩0 ?a ?b =
(λx. if x ∈ Set ?b
then Fun g (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (ff, x))))
else null)"
unfolding Cotuple_def
by fastforce
thus ?thesis by simp
qed
also have "... = mkarr ?b ?c (λx. if x ∈ Set ?b then Fun g x else null)"
proof -
have "⋀x. x ∈ Set ?b ⟹
Fun g (snd (OUT (Coprod ?a ?b) (IN (Coprod ?a ?b) (ff, x)))) = Fun g x"
using assms ide_coprod⇩o(7) by auto
thus ?thesis
by meson
qed
also have "... = g"
proof -
have "Fun g = (λx. if x ∈ Set ?b then Fun g x else null)"
unfolding Fun_def by meson
thus ?thesis
by (metis (no_types, lifting) arr_iff_in_hom assms mkarr_Fun)
qed
finally show ?thesis by blast
qed
qed
lemma Fun_cotuple:
assumes "cospan f g"
shows "Fun (cotuple f g) =
(λx. if x ∈ Set (coprod⇩o (dom f) (dom g))
then if fst (OUT (Coprod (dom f) (dom g)) x) = tt
then Fun f (snd (OUT (Coprod (dom f) (dom g)) x))
else if fst (OUT (Coprod (dom f) (dom g)) x) = ff
then Fun g (snd (OUT (Coprod (dom f) (dom g)) x))
else null
else null)"
using cotuple_def Cotuple_def Fun_mkarr assms cotuple_simps(1) by presburger
lemma binary_coproduct_in:
assumes "ide a" and "ide b"
shows "binary_product (dual_category.comp C) a b (in⇩1 a b) (in⇩0 a b)"
proof -
have bij: "bij_betw (OUT (Coprod a b)) (Set (coprod⇩o a b)) (Coprod a b)"
using assms ide_coprod⇩o(2) ide_dom by blast
interpret Cop: dual_category C ..
show ?thesis
proof
show "Cop.has_as_binary_product a b (in⇩1 a b) (in⇩0 a b)"
proof
show "Cop.span (in⇩1 a b) (in⇩0 a b)"
using assms(1,2) by force
show "Cop.cod (in⇩1 a b) = a"
using assms(1,2) by fastforce
show "Cop.cod (in⇩0 a b) = b"
using assms(1,2) by fastforce
fix c f g
assume f: "Cop.in_hom f c a" and g: "Cop.in_hom g c b"
show "∃!h. Cop.in_hom h c (Cop.dom (in⇩1 a b)) ∧ in⇩1 a b ⋅⇧o⇧p h = f ∧ in⇩0 a b ⋅⇧o⇧p h = g"
proof
show "Cop.in_hom (cotuple f g) c (Cop.dom (in⇩1 a b)) ∧
in⇩1 a b ⋅⇧o⇧p (cotuple f g) = f ∧ in⇩0 a b ⋅⇧o⇧p (cotuple f g) = g"
proof (intro conjI)
show "Cop.in_hom (cotuple f g) c (Cop.dom (in⇩1 a b))"
using assms(1,2) f g by force
show "in⇩1 a b ⋅⇧o⇧p cotuple f g = f"
using assms(1,2) f g comp_cotuple_in by auto
show "in⇩0 a b ⋅⇧o⇧p cotuple f g = g"
using assms(1,2) f g comp_cotuple_in
by (metis Cop.comp_def Cop.hom_char in_homE)
qed
show "⋀h. Cop.in_hom h c (Cop.dom (in⇩1 a b)) ∧ in⇩1 a b ⋅⇧o⇧p h = f ∧ in⇩0 a b ⋅⇧o⇧p h = g
⟹ h = cotuple f g"
proof -
fix h
assume h: "Cop.in_hom h c (Cop.dom (in⇩1 a b)) ∧
in⇩1 a b ⋅⇧o⇧p h = f ∧ in⇩0 a b ⋅⇧o⇧p h = g"
show "h = cotuple f g"
proof (intro arr_eqI [of h])
show par: "par h (cotuple f g)"
using assms(1,2) h by force
show "Fun h = Fun (cotuple f g)"
proof
fix x
show "Fun h x = Fun (cotuple f g) x"
proof (cases "x ∈ Set (coprod⇩o a b)")
case False
show ?thesis
using False assms(1,2) h par Fun_cotuple [of f g] Fun_def
by (metis (lifting) Cop.cod_char Cop.dom_char Cop.in_homE
in_simps(6) mem_Collect_eq)
next
case True
show ?thesis
proof -
have 2: "OUT (Coprod a b) x ∈ Coprod a b"
using True bij bij_betwE by blast
hence "fst (OUT (Coprod a b) x) = tt ∨ fst (OUT (Coprod a b) x) = ff"
using True bij bij_betwE
unfolding coprod⇩o_def
by auto
moreover have "fst (OUT (Coprod a b) x) = tt ⟹ ?thesis"
proof -
assume 3: "fst (OUT (Coprod a b) x) = tt"
have 4: "snd (OUT (Coprod a b) x) ∈ Set a"
using True 2 3 tt_ne_ff by fastforce
have "Fun (cotuple f g) x = Fun f (snd (OUT (Coprod a b) x))"
using assms 2 3 4 coprod⇩o_def
apply simp
by (metis (lifting) HOL.ext Cop.cod_char Cop.dom_char Cop.in_homE True
Fun_cotuple [of f g] arr_dom_iff_arr f g ide_char)
also have "... = Fun (h ⋅ in⇩1 a b) (snd (OUT (Coprod a b) x))"
using h by auto
also have "... = Fun h (Fun (in⇩1 a b) (snd (OUT (Coprod a b) x)))"
using Cop.arrI Fun_comp f h by force
also have "... = Fun h (IN (Coprod a b) (tt, snd (OUT (Coprod a b) x)))"
using assms 4 Fun_in(1) [of a b] by auto
also have "... = Fun h (IN (Coprod a b) (OUT (Coprod a b) x))"
by (metis "3" surjective_pairing)
also have "... = Fun h x"
using assms True ide_coprod⇩o(6) by presburger
finally show ?thesis by simp
qed
moreover have "fst (OUT (Coprod a b) x) = ff ⟹ ?thesis"
proof -
assume 3: "fst (OUT (Coprod a b) x) = ff"
have 4: "snd (OUT (Coprod a b) x) ∈ Set b"
using True 2 3 tt_ne_ff by fastforce
have "Fun (cotuple f g) x = Fun g (snd (OUT (Coprod a b) x))"
using True assms f g 2 3 4 tt_ne_ff coprod⇩o_def Fun_cotuple [of f g]
apply auto[1]
by (metis (lifting) HOL.ext fst_conv in_homE snd_conv)
also have "... = Fun (h ⋅ in⇩0 a b) (snd (OUT (Coprod a b) x))"
using h by auto
also have "... = Fun h (Fun (in⇩0 a b) (snd (OUT (Coprod a b) x)))"
using Cop.arrI Fun_comp g h by force
also have "... = Fun h (IN (Coprod a b) (ff, snd (OUT (Coprod a b) x)))"
using assms 4 Fun_in(2) [of a b] by auto
also have "... = Fun h (IN (Coprod a b) (OUT (Coprod a b) x))"
by (metis "3" surjective_pairing)
also have "... = Fun h x"
using assms True ide_coprod⇩o(6) by presburger
finally show ?thesis by simp
qed
ultimately show ?thesis by blast
qed
qed
qed
qed
qed
qed
qed
qed
qed
lemma has_binary_coproducts:
shows "category.has_binary_products (dual_category.comp C)"
proof -
interpret Cop: dual_category C ..
show "Cop.has_binary_products"
proof (unfold Cop.has_binary_products_def, intro allI impI, elim conjE)
fix a b
assume a: "Cop.ide a" and b: "Cop.ide b"
interpret binary_product Cop.comp a b ‹in⇩1 a b› ‹in⇩0 a b›
using a b binary_coproduct_in [of a b] Cop.ide_char by blast
show "∃p. Ex (Cop.has_as_binary_product a b p)"
using has_as_binary_product by blast
qed
qed
end
subsection "Exported Notions"
context sets_cat_with_cotupling
begin
interpretation Coproducts: coproducts_in_sets_cat ..
abbreviation in⇩0 :: "'U ⇒ 'U ⇒ 'U"
where "in⇩0 ≡ Coproducts.in⇩0"
abbreviation in⇩1 :: "'U ⇒ 'U ⇒ 'U"
where "in⇩1 ≡ Coproducts.in⇩1"
abbreviation Coprod :: "'U ⇒ 'U ⇒ ('U × 'U) set"
where "Coprod ≡ Coproducts.Coprod"
abbreviation coprod⇩o :: "'U ⇒ 'U ⇒ 'U"
where "coprod⇩o ≡ Coproducts.coprod⇩o"
lemma ide_coprod⇩o:
assumes "ide a" and "ide b"
shows "ide (coprod⇩o a b)"
using assms Coproducts.ide_coprod⇩o by blast
lemma in⇩1_in_hom [intro, simp]:
assumes "ide a" and "ide b"
shows "in_hom (in⇩1 a b) a (coprod⇩o a b)"
using assms Coproducts.in_in_hom by blast
lemma in⇩0_in_hom [intro, simp]:
assumes "ide a" and "ide b"
shows "in_hom (in⇩0 a b) b (coprod⇩o a b)"
using assms Coproducts.in_in_hom by blast
lemma in⇩1_simps [simp]:
assumes "ide a" and "ide b"
shows "arr (in⇩1 a b)" and "dom (in⇩1 a b) = a" and "cod (in⇩1 a b) = coprod⇩o a b"
using assms Coproducts.in_simps by auto
lemma in⇩0_simps [simp]:
assumes "ide a" and "ide b"
shows "arr (in⇩0 a b)" and "dom (in⇩0 a b) = b" and "cod (in⇩0 a b) = coprod⇩o a b"
using assms Coproducts.in_simps by auto
lemma bin_coprod_comparison_map_props:
assumes "ide a" and "ide b"
shows "bij_betw (OUT (Coprod a b)) (Set (coprod⇩o a b)) (Coprod a b)"
and "bij_betw (IN (Coprod a b)) (Coprod a b) (Set (coprod⇩o a b))"
and "⋀x. x ∈ Set (coprod⇩o a b) ⟹ OUT (Coprod a b) x ∈ Coprod a b"
and "⋀y. y ∈ Coprod a b ⟹ IN (Coprod a b) y ∈ Set (coprod⇩o a b)"
and "⋀x. x ∈ Set (coprod⇩o a b) ⟹ IN (Coprod a b) (OUT (Coprod a b) x) = x"
and "⋀y. y ∈ Coprod a b ⟹ OUT (Coprod a b) (IN (Coprod a b) y) = y"
using assms Coproducts.ide_coprod⇩o by auto
lemma Fun_in⇩1:
assumes "ide a" and "ide b"
shows "Fun (in⇩1 a b) = Coproducts.In⇩1 a b"
using assms Coproducts.Fun_in(1) by auto[1]
lemma Fun_in⇩0:
assumes "ide a" and "ide b"
shows "Fun (in⇩0 a b) = Coproducts.In⇩0 a b"
using assms Coproducts.Fun_in(2) by auto[1]
abbreviation cotuple
where "cotuple ≡ Coproducts.cotuple"
lemma cotuple_in_hom [intro, simp]:
assumes "«f : a → c»" and "«g : b → c»"
shows "«cotuple f g : coprod⇩o a b → c»"
using assms Coproducts.cotuple_in_hom by blast
lemma cotuple_simps [simp]:
assumes "cospan f g"
shows "arr (cotuple f g)"
and "dom (cotuple f g) = coprod⇩o (dom f) (dom g)"
and "cod (cotuple f g) = cod f"
using assms Coproducts.cotuple_simps by auto
abbreviation Cotuple
where "Cotuple f g ≡ (λx. if x ∈ Set (coprod⇩o (dom f) (dom g))
then if fst (OUT (Coprod (dom f) (dom g)) x) = tt
then Fun f (snd (OUT (Coprod (dom f) (dom g)) x))
else if fst (OUT (Coprod (dom f) (dom g)) x) = ff
then Fun g (snd (OUT (Coprod (dom f) (dom g)) x))
else null
else null)"
lemma cotuple_eq:
assumes "«f : a → c»" and "«g : b → c»"
shows "cotuple f g = mkarr (coprod⇩o a b) c (Cotuple f g)"
unfolding Coproducts.cotuple_def Coproducts.Cotuple_def
using assms by auto
lemma Fun_cotuple:
assumes "cospan f g"
shows "Fun (cotuple f g) = Cotuple f g"
using assms Coproducts.Fun_cotuple by blast
lemma binary_coproduct_in:
assumes "ide a" and "ide b"
shows "binary_product (dual_category.comp C) a b (in⇩1 a b) (in⇩0 a b)"
using assms Coproducts.binary_coproduct_in by blast
lemma has_binary_coproducts:
shows "category.has_binary_products (dual_category.comp C)"
using Coproducts.has_binary_coproducts by blast
end
section "Small Products"
text‹
In this section we show that the category of small sets and functions has small products.
For this we need to assume that smallness is preserved by the formation of function
spaces.
›
locale sets_cat_with_tupling =
sets_cat sml C +
tupling sml ‹Collect arr› null
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
sublocale sets_cat_with_bool
using embeds_bool
by unfold_locales auto
sublocale sets_cat_with_pairing sml C ..
sublocale sets_cat_with_cotupling ..
end
locale small_products_in_sets_cat =
sets_cat_with_tupling sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
text‹
A product diagram is specified by an extensional function ‹A› from small index set ‹I›
to @{term ‹Collect ide›}, using @{term null} as the default value. An element of the product
is given by an extensional function ‹F› from ‹I› to @{term ‹Collect arr›}, such that
‹F i ∈ Set (A i)› for each ‹i ∈ I›.
›
abbreviation ProdX :: "'a set ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) set"
where "ProdX I A ≡ {F. ∀i. i ∈ I ⟶ F i ∈ Set (A i)} ∩ {F. ∀i. i ∉ I ⟶ F i = null}"
lemma ProdX_empty:
shows "ProdX {} A = {λx. null}"
by auto
definition prodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'U"
where "prodX I A ≡ mkide (ProdX I A)"
lemma small_function_tuple:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "F ∈ ProdX I A"
shows "small_function F" and "range F ⊆ (⋃i∈I. Set (A i)) ∪ {null}"
proof -
have 1: "small ((⋃i∈I. Set (A i)) ∪ {null})"
using assms small_Set by auto
have 2: "⋀F v. ⟦F ∈ ProdX I A; popular_value F v⟧ ⟹ v = null"
proof -
fix F v
assume F: "F ∈ ProdX I A"
assume v: "popular_value F v"
have "(∃i. i ∈ I ∧ v ∈ Set (A i)) ∨ v = null"
using v F popular_value_in_range [of F v] by blast
hence "v ≠ null ⟹ {i. F i = v} ⊆ I"
using F by blast
hence "v ≠ null ⟹ ¬ popular_value F v"
using assms(1) smaller_than_small by blast
thus "v = null"
using v by blast
qed
show 3: "range F ⊆ (⋃i∈I. Set (A i)) ∪ {null}"
using assms(4) by auto
show "small_function F"
proof
show "small (range F)"
using 1 3 smaller_than_small by blast
show "at_most_one_popular_value F"
using assms(4) 2 Uniq_def
by (metis (mono_tags, lifting))
qed
qed
lemma small_ProdX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "small (ProdX I A)"
proof (cases "small (UNIV :: 'U set)")
case True
show ?thesis
using True small_function_tuple smaller_than_small
by (metis large_univ subset_UNIV)
next
case False
have "⋀F. F ∈ ProdX I A ⟹ SF_Dom F ⊆ I"
proof -
fix F
assume F: "F ∈ ProdX I A"
have "popular_value F null"
proof -
have "¬ small (UNIV - I)"
using assms False small_union by fastforce
moreover have "UNIV - I ⊆ {i. F i = null}"
using F by blast
ultimately show ?thesis
using smaller_than_small by blast
qed
thus "SF_Dom F ⊆ I"
using F by auto
qed
hence "ProdX I A ⊆ {f. small_function f ∧ SF_Dom f ⊆ I ∧
range f ⊆ (⋃i∈I. Set (A i)) ∪ {null}}"
using assms small_function_tuple by blast
moreover have 1: "small ((⋃i∈I. Set (A i)) ∪ {null})"
using assms small_Set by auto
ultimately show ?thesis
using assms(1) small_Set small_funcset [of I "(⋃i∈I. Set (A i)) ∪ {null}"]
smaller_than_small
by blast
qed
lemma embeds_ProdX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "embeds (ProdX I A)"
proof -
obtain ι where ι: "is_embedding_of ι SEF"
using embeds_SEF by blast
have "ProdX I A ⊆ SEF"
using assms EF_def small_function_tuple by auto
hence "is_embedding_of ι (ProdX I A)"
using ι by (meson dual_order.trans image_mono inj_on_subset)
thus ?thesis by blast
qed
lemma ide_prodX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "ide (prodX I A)"
and "bij_betw (OUT (ProdX I A)) (Set (prodX I A)) (ProdX I A)"
and "bij_betw (IN (ProdX I A)) (ProdX I A) (Set (prodX I A))"
and "⋀x. x ∈ Set (prodX I A) ⟹ OUT (ProdX I A) x ∈ ProdX I A"
and "⋀y. y ∈ ProdX I A ⟹ IN (ProdX I A) y ∈ Set (prodX I A)"
and "⋀x. x ∈ Set (prodX I A) ⟹ IN (ProdX I A) (OUT (ProdX I A) x) = x"
and "⋀y. y ∈ ProdX I A ⟹ OUT (ProdX I A) (IN (ProdX I A) y) = y"
proof -
have 2: "small ((⋃i∈I. Set (A i)) ∪ {null})"
using assms(1-2) small_Set by auto
have *: "⋀F. F ∈ ProdX I A ⟹ small_function F ∧ range F ⊆ (⋃i∈I. Set (A i)) ∪ {null}"
using assms small_function_tuple by blast
show "ide (prodX I A)"
unfolding prodX_def
using assms small_ProdX embeds_ProdX by auto
show 1: "bij_betw (OUT (ProdX I A)) (Set (prodX I A)) (ProdX I A)"
unfolding prodX_def
using assms small_ProdX embeds_ProdX bij_OUT [of "ProdX I A"] by fastforce
show 2: "bij_betw (IN (ProdX I A)) (ProdX I A) (Set (prodX I A))"
unfolding prodX_def
using assms small_ProdX embeds_ProdX bij_IN [of "ProdX I A"] by fastforce
show "⋀x. x ∈ Set (prodX I A) ⟹ OUT (ProdX I A) x ∈ ProdX I A"
using 1 bij_betwE by blast
show "⋀y. y ∈ ProdX I A ⟹ IN (ProdX I A) y ∈ Set (prodX I A)"
using 2 bij_betwE by blast
show "⋀x. x ∈ Set (prodX I A) ⟹ IN (ProdX I A) (OUT (ProdX I A) x) = x"
proof -
fix x
assume x: "x ∈ Set (prodX I A)"
show "IN (ProdX I A) (OUT (ProdX I A) x) = x"
proof -
have "x = inv_into (Set (prodX I A)) (OUT (ProdX I A)) (OUT (ProdX I A) x)"
using x 1
bij_betw_inv_into_left
[of "OUT (ProdX I A)" "Set (prodX I A)" "ProdX I A"]
by auto
thus ?thesis
by (simp add: prodX_def)
qed
qed
show "⋀y. y ∈ ProdX I A ⟹ OUT (ProdX I A) (IN (ProdX I A) y) = y"
proof -
fix y
assume y: "y ∈ ProdX I A"
show "OUT (ProdX I A) (IN (ProdX I A) y) = y"
using assms(1,2,3) y OUT_IN [of "ProdX I A" y] small_ProdX embeds_ProdX [of I A]
by blast
qed
qed
lemma terminal_prodX_empty:
shows "terminal (prodX {} (A :: 'U ⇒ 'U))"
proof -
let ?I = "{} :: 'U set"
have 1: "{F. ∀i. i ∉ ?I ⟶ F i = null} = {λi. null}"
by auto
have "∃!x. x ∈ Set (prodX ?I A)"
proof -
have "eqpoll (Set (prodX ?I A)) {F. ∀i. i ∉ ?I ⟶ F i = null}"
proof -
have "small {F. ∀i. i ∉ ?I ⟶ F i = null}"
using 1 small_finite by force
moreover have "∃ι. is_embedding_of ι {F. ∀i :: 'U. F i = null}"
proof -
have "is_embedding_of (λ_. 𝟭⇧?) {λi. null}"
using ide_char ide_some_terminal by blast
thus ?thesis
using 1 by auto
qed
ultimately show ?thesis
unfolding prodX_def
using 1 bij_OUT [of "{F. ∀i. i ∉ ?I ⟶ F i = null}"] eqpoll_def
by auto blast
qed
moreover have "∃!x. x ∈ {F. ∀i. i ∉ ?I ⟶ F i = null}"
using 1 by auto
ultimately show ?thesis
by (metis (no_types, lifting) eqpoll_iff_bijections)
qed
thus ?thesis
using terminal_char ide_prodX(1)
by (metis Pi_I empty_subsetI ex_in_conv small_Set smaller_than_small
terminal_some_terminal)
qed
abbreviation PrX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'a ⇒ 'U ⇒ 'U"
where "PrX I A i ≡ λx. if x ∈ Set (prodX I A) then OUT (ProdX I A) x i else null"
definition prX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'a ⇒ 'U"
where "prX I A i ≡ mkarr (prodX I A) (A i) (PrX I A i)"
lemma prX_in_hom [intro, simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "in_hom (prX I A i) (prodX I A) (A i)"
proof (unfold prX_def, intro mkarr_in_hom)
show "ide (prodX I A)"
using assms ide_prodX by blast
show "ide (A i)"
using assms by blast
show "PrX I A i ∈ Hom (prodX I A) (A i)"
proof
show "PrX I A i ∈ Set (prodX I A) → Set (A i)"
proof
fix x
assume x: "x ∈ Set (prodX I A)"
have "OUT (ProdX I A) x ∈ ProdX I A"
using assms(1,2,3) x ide_prodX(2)
bij_betwE [of "OUT (ProdX I A)" "Set (prodX I A)" "ProdX I A"]
by blast
thus "PrX I A i x ∈ Set (A i)"
using assms x by force
qed
show "PrX I A i ∈ {F. ∀x. x ∉ Set (prodX I A) ⟶ F x = null}"
by simp
qed
qed
lemma prX_simps [simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "arr (prX I A i)" and "dom (prX I A i) = prodX I A" and "cod (prX I A i) = A i"
using assms prX_in_hom by blast+
lemma Fun_prX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "Fun (prX I A i) = PrX I A i"
proof -
have "arr (prX I A i)"
using assms by auto
thus ?thesis
using assms Fun_mkarr [of "prodX I A" "A i" "PrX I A i"] prX_def by metis
qed
definition TupleX :: "'a set ⇒ 'U ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) ⇒ 'U ⇒ 'U"
where "TupleX I c A F ≡ (λx. if x ∈ Set c then IN (ProdX I A) (λi. Fun (F i) x) else null)"
lemma TupleX_in_Hom:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null"
shows "TupleX I c A F ∈ Hom c (prodX I A)"
proof
show "TupleX I c A F ∈ {F. ∀x. x ∉ Set c ⟶ F x = null}"
unfolding TupleX_def
using assms by auto
show "TupleX I c A F ∈ Set c → Set (prodX I A)"
proof (cases "I = {}")
case False
show ?thesis
proof
fix x
assume x: "x ∈ Set c"
have "∀i. i ∈ I ⟶ x ∈ Set (dom (F i))"
using False assms x by blast
moreover have "(λi. Fun (F i) x) ∈ ProdX I A"
using False assms x Fun_def by auto
ultimately show "TupleX I c A F x ∈ Set (prodX I A)"
unfolding TupleX_def
using False assms x ide_prodX(3) [of I A] bij_betw_apply
by (metis (mono_tags, lifting))
qed
next
case True
show ?thesis
unfolding TupleX_def
using True assms ide_prodX(3) bij_betw_apply Fun_def
by auto[1] fastforce
qed
qed
definition tupleX :: "'a set ⇒ 'U ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) ⇒ 'U"
where "tupleX I c A F ≡ mkarr c (prodX I A) (TupleX I c A F)"
lemma tupleX_in_hom [intro, simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "«tupleX I c A F : c → prodX I A»"
unfolding tupleX_def
using assms ide_prodX TupleX_in_Hom
by (intro mkarr_in_hom) auto
lemma tupleX_simps [simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "arr (tupleX I c A F)"
and "dom (tupleX I c A F) = c"
and "cod (tupleX I c A F) = prodX I A"
using assms in_homE tupleX_in_hom by metis+
lemma comp_prX_tupleX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null"
shows "i ∈ I ⟹ C (prX I A i) (tupleX I c A F) = F i"
proof -
assume i: "i ∈ I"
have I: "I ≠ {}"
using i by blast
hence c: "ide c"
using assms(4) ide_dom by blast
show "C (prX I A i) (tupleX I c A F) = F i"
proof -
have "C (prX I A i) (tupleX I c A F) =
mkarr (prodX I A) (A i) (PrX I A i) ⋅ mkarr c (prodX I A) (TupleX I c A F)"
unfolding prX_def tupleX_def TupleX_def
using assms i I comp_mkarr by simp
also have "... = mkarr c (A i) (PrX I A i ∘ TupleX I c A F)"
proof -
have "«mkarr c (prodX I A) (TupleX I c A F) : c → prodX I A»"
by (metis assms c tupleX_def tupleX_in_hom)
moreover have "«mkarr (prodX I A) (A i) (PrX I A i) : prodX I A → A i»"
proof -
have "«prX I A i : prodX I A → A i»"
using assms(1-3) i by blast
thus ?thesis
by (simp add: prX_def)
qed
ultimately show ?thesis
using assms i comp_mkarr [of c "prodX I A" "TupleX I c A F" "A i" "PrX I A i"]
by auto
qed
also have "... = mkarr c (A i)
(λx. if TupleX I c A F x ∈ Set (prodX I A)
then OUT (ProdX I A) (TupleX I c A F x) i
else null)"
using I by (simp add: comp_def)
also have "... = mkarr c (A i)
(λx. if x ∈ Set c then OUT (ProdX I A) (TupleX I c A F x) i else null)"
proof -
have "(λx. if TupleX I c A F x ∈ Set (prodX I A)
then OUT (ProdX I A) (TupleX I c A F x) i
else null) =
(λx. if x ∈ Set c then OUT (ProdX I A) (TupleX I c A F x) i else null)"
proof
fix x
show "(if TupleX I c A F x ∈ Set (prodX I A)
then OUT (ProdX I A) (TupleX I c A F x) i
else null) =
(if x ∈ Set c then OUT (ProdX I A) (TupleX I c A F x) i else null)"
using assms TupleX_in_Hom
by auto blast
qed
thus ?thesis by simp
qed
also have "... = mkarr c (A i)
(λx. if x ∈ Set c
then OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i
else null)"
proof -
have "(λx. if x ∈ Set c then OUT (ProdX I A) (TupleX I c A F x) i else null) =
(λx. if x ∈ Set c
then OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i
else null)"
proof
fix x
show "(if x ∈ Set c then OUT (ProdX I A) (TupleX I c A F x) i else null) =
(if x ∈ Set c
then OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i
else null)"
unfolding TupleX_def by argo
qed
thus ?thesis by simp
qed
also have "... = mkarr c (A i) (λx. if x ∈ Set c then Fun (F i) x else null)"
proof -
have "(λx. if x ∈ Set c
then OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i
else null) =
(λx. if x ∈ Set c then Fun (F i) x else null)"
proof
fix x
show "(if x ∈ Set c
then OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i
else null) =
(if x ∈ Set c then Fun (F i) x else null)"
proof (cases "x ∈ Set c")
case False
show ?thesis
using False by simp
next
case True
show ?thesis
proof -
have "(λi. Fun (F i) x) ∈ ProdX I A"
using assms(4-5) True Fun_def by auto
hence "OUT (ProdX I A) (IN (ProdX I A) (λi. Fun (F i) x)) i = Fun (F i) x"
using assms OUT_IN [of "ProdX I A" "λi. Fun (F i) x"]
small_ProdX embeds_ProdX
by presburger
thus ?thesis by simp
qed
qed
qed
thus ?thesis by simp
qed
also have "... = F i"
proof -
have "Fun (F i) = (λx. if x ∈ Set c then Fun (F i) x else null)"
using assms(4) i Fun_def by fastforce
thus ?thesis
using assms(4) i mkarr_Fun by force
qed
finally show ?thesis by blast
qed
qed
lemma Fun_tupleX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "Fun (tupleX I c A F) =
(λx. if x ∈ Set c then IN (ProdX I A) (λi. Fun (F i) x) else null)"
proof -
have "Fun (tupleX I c A F) =
(λx. if x ∈ Set c then mkarr c (prodX I A) (TupleX I c A F) ⋅ x else null)"
unfolding tupleX_def Fun_def
apply simp
by (metis ext mem_Collect_eq dom_mkarr seqE)
also have "... = (λx. if x ∈ Set c then TupleX I c A F x else null)"
using assms app_mkarr
by (metis (no_types, lifting) CollectD tupleX_def tupleX_in_hom)
also have "... = (λx. if x ∈ Set c then IN (ProdX I A) (λi. Fun (F i) x) else null)"
unfolding TupleX_def by auto
finally show ?thesis by blast
qed
lemma product_cone_prodX:
assumes "discrete_diagram J C D" and "Collect (partial_composition.arr J) = I"
and "small I" and "I ⊆ Collect arr"
shows "has_as_product J D (prodX I D)"
and "product_cone J C D (prodX I D) (prX I D)"
proof -
interpret J: category J
using assms(1) discrete_diagram_def by blast
interpret D: discrete_diagram J C D
using assms(1) by blast
let ?π = "prX I D"
let ?a = "prodX I D"
interpret A: constant_functor J C ?a
using assms ide_prodX
apply unfold_locales
using D.is_discrete by auto
interpret π: natural_transformation J C A.map D ?π
proof
fix j
show "¬ J.arr j ⟹ prX I D j = null"
by (metis (no_types, lifting) D.as_nat_trans.extensionality ideD(1) mkarr_def
not_arr_null prX_def)
assume j: "J.arr j"
show 1: "arr (prX I D j)"
using D.is_discrete assms j by force
show "D j ⋅ prX I D (J.dom j) = prX I D j"
by (metis (lifting) 1 D.is_discrete J.ideD(2) comp_cod_arr cod_mkarr j prX_def)
show "prX I D (J.cod j) ⋅ A.map j = prX I D j"
by (metis (lifting) 1 A.map_simp D.is_discrete J.ide_char comp_arr_dom j
dom_mkarr prX_def)
qed
show "product_cone J C D ?a ?π"
proof
fix a' χ'
assume χ': "D.cone a' χ'"
interpret χ': cone J C D a' χ'
using χ' by blast
show "∃!f. «f : a' → prodX I D» ∧ D.cones_map f (prX I D) = χ'"
proof -
let ?f = "tupleX I a' D χ'"
have f: "«?f : a' → prodX I D»"
using assms tupleX_in_hom
by (metis D.is_discrete D.preserves_ide J.ide_char Pi_I'
χ'.component_in_hom χ'.extensionality χ'.ide_apex mem_Collect_eq)
moreover have "D.cones_map ?f (prX I D) = χ'"
proof
fix i
show "D.cones_map ?f (prX I D) i = χ' i"
proof -
have "J.arr i ⟹ prX I D i ⋅ ?f = χ' i"
using assms comp_prX_tupleX [of I D χ' a' i]
by (metis D.is_discrete D.preserves_ide J.ide_char Pi_I'
χ'.component_in_hom χ'.extensionality mem_Collect_eq)
moreover have "¬ J.arr i ⟹ null = χ' i"
using χ'.extensionality by auto
moreover have "D.cone (cod ?f) (prX I D)"
proof -
have "D.cone (prodX I D) (prX I D)" ..
moreover have "cod ?f = prodX I D"
using f by blast
ultimately show ?thesis by auto
qed
ultimately show ?thesis
using assms χ'.cone_axioms by auto
qed
qed
moreover have "⋀f'. ⟦«f' : a' → prodX I D»; D.cones_map f' (prX I D) = χ'⟧
⟹ f' = ?f"
proof -
fix f'
assume f': "«f' : a' → prodX I D»"
assume 1: "D.cones_map f' (prX I D) = χ'"
show "f' = ?f"
proof (intro arr_eqI [of f'])
show par: "par f' ?f"
using f f' by fastforce
show "Fun f' = Fun (tupleX I a' D χ')"
proof
fix x
show "Fun f' x = Fun (tupleX I a' D χ') x"
proof (cases "x ∈ Set a'")
case False
show ?thesis
using False par f' Fun_def by auto
next
case True
have 2: "D.cone (cod f') (prX I D)"
by (metis A.constant_functor_axioms Limit.cone_def
π.natural_transformation_axioms χ' f' in_homE)
have "Fun (tupleX I a' D χ') x = IN (ProdX I D) (λi. Fun (χ' i) x)"
proof -
have "dom (tupleX I a' D χ') = a'"
using f by auto
have *: "(λx. if «x : 𝟭⇧? → a'» then tupleX I a' D χ' ⋅ x else null) =
(λx. if «x : 𝟭⇧? → a'» then IN (ProdX I D) (λi. Fun (χ' i) x) else null)"
proof -
have "D ∈ I → Collect ide"
using assms(2) D.is_discrete by force
moreover have "⋀i. i ∈ I ⟹ «χ' i : a' → D i»"
using assms(2) D.is_discrete χ'.component_in_hom by fastforce
moreover have "⋀i. i ∉ I ⟹ χ' i = null"
using assms(2) χ'.extensionality by blast
moreover have "ide a'"
using χ'.ide_apex by auto
ultimately show ?thesis
using assms f Fun_tupleX [of I D χ' a'] Fun_arr by force
qed
have "Fun (tupleX I a' D χ') x = tupleX I a' D χ' ⋅ x"
using True ‹dom (tupleX I a' D χ') = a'› Fun_def by presburger
also have "... = (λx. if «x : 𝟭⇧? → a'» then tupleX I a' D χ' ⋅ x else null) x"
using True by simp
also have "... = (λx. if «x : 𝟭⇧? → a'»
then IN (ProdX I D) (λi. Fun (χ' i) x)
else null) x"
using * by meson
also have "... = IN (ProdX I D) (λi. Fun (χ' i) x)"
using True by simp
finally show ?thesis by blast
qed
also have "... = IN (ProdX I D) (λi. χ' i ⋅ x)"
unfolding Fun_def
by (metis J.dom_cod True χ'.A.map_simp χ'.cod_determines_component
χ'.preserves_dom χ'.preserves_reflects_arr local.ext seqE)
also have "... = IN (ProdX I D) (λi. D.cones_map f' (prX I D) i ⋅ x)"
using 1 by simp
also have "... = IN (ProdX I D) (λi. (if J.arr i then prX I D i ⋅ f' else null) ⋅ x)"
using 2 by simp
also have "... = IN (ProdX I D) (λi. if J.arr i then prX I D i ⋅ (f' ⋅ x) else null)"
proof -
have "(λi. (if J.arr i then prX I D i ⋅ f' else null) ⋅ x) =
(λi. if J.arr i then prX I D i ⋅ (f' ⋅ x) else null)"
proof
fix i
show "(if J.arr i then prX I D i ⋅ f' else null) ⋅ x =
(if J.arr i then prX I D i ⋅ (f' ⋅ x) else null)"
using comp_assoc by auto
qed
thus ?thesis by simp
qed
also have "... = IN (ProdX I D)
(λi. if J.arr i then prX I D i ⋅ (Fun f' x) else null)"
unfolding Fun_def
using True f' by auto
also have "... = IN (ProdX I D)
(λi. if J.arr i then Fun (prX I D i) (Fun f' x) else null)"
proof -
have "(λi. if J.arr i then prX I D i ⋅ (Fun f' x) else null) =
(λi. if J.arr i then Fun (prX I D i) (Fun f' x) else null)"
proof
fix i
show "(if J.arr i then prX I D i ⋅ (Fun f' x) else null) =
(if J.arr i then Fun (prX I D i) (Fun f' x) else null)"
using f' Fun_def by fastforce
qed
thus ?thesis by simp
qed
also have "... = IN (ProdX I D)
(λi. if J.arr i
then (if Fun f' x ∈ Set (prodX I D)
then OUT (ProdX I D) (Fun f' x) i else null)
else null)"
proof -
have "⋀i. J.arr i ⟹ Fun (prX I D i) =
(λx. if x ∈ Set (prodX I D)
then OUT (ProdX I D) x i else null)"
using assms Fun_prX D.is_discrete by force
hence "(λi. if J.arr i then Fun (prX I D i) (Fun f' x) else null) =
(λi. if J.arr i
then (λx. if x ∈ Set (prodX I D)
then OUT (ProdX I D) x i else null)
(Fun f' x)
else null)"
by auto
thus ?thesis by simp
qed
also have "... = IN (ProdX I D)
(λi. if J.arr i then OUT (ProdX I D) (Fun f' x) i else null)"
proof -
have "(λi. if J.arr i
then (λx. if x ∈ Set (prodX I D)
then OUT (ProdX I D) x i else null)
(Fun f' x)
else null) =
(λi. if J.arr i then OUT (ProdX I D) (Fun f' x) i else null)"
using True f' Fun_def Fun_arr comp_in_homI by auto
thus ?thesis by simp
qed
also have "... = IN (ProdX I D) (OUT (ProdX I D) (Fun f' x))"
proof -
have "(λi. if J.arr i then OUT (ProdX I D) (Fun f' x) i else null) =
OUT (ProdX I D) (Fun f' x)"
proof
fix i
show "(if J.arr i then OUT (ProdX I D) (Fun f' x) i else null) =
OUT (ProdX I D) (Fun f' x) i"
proof (cases "J.arr i")
case True
show ?thesis
using True by simp
next
case False
have 1: "Fun f' x ∈ Set (prodX I D)"
using True f' Fun_def by auto
moreover have "small (ProdX I D)" and "embeds (ProdX I D)"
using assms small_ProdX [of I D] embeds_ProdX [of I D]
D.is_discrete D.preserves_ide
by auto
moreover have "«Fun f' x : 𝟭⇧? → mkide (ProdX I D)»"
using True f'
by (metis 1 prodX_def mem_Collect_eq)
ultimately have "OUT (ProdX I D) (Fun f' x) ∈ ProdX I D"
using OUT_elem_of [of "ProdX I D" "Fun f' x"] Fun_in_Hom
by fastforce
thus ?thesis
using False assms(2) by fastforce
qed
qed
thus ?thesis by simp
qed
also have "... = Fun f' x"
proof -
have "small (ProdX I D)"
using assms small_ProdX D.is_discrete by fastforce
moreover have "∃ι. is_embedding_of ι (ProdX I D)"
using assms embeds_ProdX [of I D] D.is_discrete by auto
moreover have "Fun f' x ∈ Set (mkide (ProdX I D))"
proof -
have "Fun f' x ∈ Set (prodX I D)"
using Fun_in_Hom True f' by blast
thus ?thesis
by (simp add: prodX_def)
qed
ultimately show ?thesis
using assms IN_OUT [of "ProdX I D" "Fun f' x"] by blast
qed
finally show ?thesis by simp
qed
qed
qed
qed
ultimately show ?thesis by blast
qed
qed
thus "has_as_product J D (prodX I D)"
using has_as_product_def by blast
qed
lemma has_small_products:
assumes "small I" and "I ⊆ Collect arr"
shows "has_products I"
proof (unfold has_products_def, intro conjI)
show "I ≠ UNIV"
using assms not_arr_null by blast
show "∀J D. discrete_diagram J (⋅) D ∧ Collect (partial_composition.arr J) = I
⟶ (∃a. has_as_product J D a)"
using assms product_cone_prodX by blast
qed
end
subsection "Exported Notions"
context sets_cat_with_tupling
begin
interpretation Products: small_products_in_sets_cat ..
abbreviation ProdX :: "'a set ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) set"
where "ProdX ≡ Products.ProdX"
abbreviation prodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'U"
where "prodX ≡ Products.prodX"
abbreviation prX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'a ⇒ 'U"
where "prX ≡ Products.prX"
abbreviation tupleX :: "'a set ⇒ 'U ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) ⇒ 'U"
where "tupleX ≡ Products.tupleX"
lemma small_prod_comparison_map_props:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "OUT (ProdX I A) ∈ Set (prodX I A) → ProdX I A"
and "IN (ProdX I A) ∈ ProdX I A → Set (prodX I A)"
and "⋀x. x ∈ Set (prodX I A) ⟹ IN (ProdX I A) (OUT (ProdX I A) x) = x"
and "⋀y. y ∈ ProdX I A ⟹ OUT (ProdX I A) (IN (ProdX I A) y) = y"
and "bij_betw (OUT (ProdX I A)) (Set (prodX I A)) (ProdX I A)"
and "bij_betw (IN (ProdX I A)) (ProdX I A) (Set (prodX I A))"
proof -
show "OUT (ProdX I A) ∈ Set (prodX I A) → ProdX I A"
proof -
have "bij_betw
(OUT ({f. ∀a. a ∈ I ⟶ f a ∈ Set (A a)} ∩ {f. ∀a. a ∉ I ⟶ f a = null}))
(Set (prodX I A))
({f. ∀a. a ∈ I ⟶ f a ∈ Set (A a)} ∩ {f. ∀a. a ∉ I ⟶ f a = null})"
using Products.ide_prodX(2) assms(1-3) by blast
then show ?thesis
by (simp add: bij_betw_imp_funcset)
qed
show "IN (ProdX I A) ∈ ProdX I A → Set (prodX I A)"
proof -
have "bij_betw
(OUT ({f. ∀a. a ∈ I ⟶ f a ∈ Set (A a)} ∩ {f. ∀a. a ∉ I ⟶ f a = null}))
(Set (prodX I A))
({f. ∀a. a ∈ I ⟶ f a ∈ Set (A a)} ∩ {f. ∀a. a ∉ I ⟶ f a = null})"
using Products.ide_prodX(2) assms(1-3) by blast
then show ?thesis
by (simp add: Products.prodX_def bij_betw_imp_funcset bij_betw_inv_into)
qed
show "⋀x. x ∈ Set (prodX I A) ⟹ IN (ProdX I A) (OUT (ProdX I A) x) = x"
using assms IN_OUT [of "ProdX I A"] Products.small_ProdX Products.embeds_ProdX
by (simp add: Products.prodX_def)
show "⋀y. y ∈ ProdX I A ⟹ OUT (ProdX I A) (IN (ProdX I A) y) = y"
using assms OUT_IN [of "ProdX I A"] Products.small_ProdX Products.embeds_ProdX
by (simp add: Products.prodX_def)
show "bij_betw (OUT (ProdX I A)) (Set (prodX I A)) (ProdX I A)"
using assms Products.ide_prodX by fastforce
show "bij_betw (IN (ProdX I A)) (ProdX I A) (Set (prodX I A))"
using assms Products.ide_prodX by fastforce
qed
lemma Fun_prX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "Fun (prX I A i) = Products.PrX I A i"
using assms Products.Fun_prX by auto
lemma Fun_tupleX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : c → A i»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "Fun (tupleX I c A F) =
(λx. if x ∈ Set c then IN (Products.ProdX I A) (λi. Fun (F i) x) else null)"
using assms Products.Fun_tupleX by auto
lemma product_cone:
assumes "discrete_diagram J C D" and "Collect (partial_composition.arr J) = I"
and "small I" and "I ⊆ Collect arr"
shows "has_as_product J D (prodX I D)"
and "product_cone J C D (prodX I D) (prX I D)"
using assms Products.product_cone_prodX by auto
lemma has_small_products:
assumes "small I" and "I ⊆ Collect arr"
shows "has_products I"
using assms Products.has_small_products by blast
text‹
Clearly it is not required that the index set ‹I› be actually a subset of
@{term ‹Collect arr›} but rather only that it be embedded in it. So we are free to form
products indexed by small sets at arbitrary types, as long as @{term ‹Collect arr›}
is large enough to embed them. We do have to satisfy the technical requirement that the
index set ‹I› not exhaust the elements at its type, which we introduced in the
definition of @{term has_products} as a convenience to avoid the use of coercion maps.
›
lemma has_small_products':
assumes "small I" and "embeds I" and "I ≠ UNIV"
shows "has_products I"
proof -
obtain I' where I': "I' ⊆ Collect arr ∧ I ≈ I'"
using assms inj_on_image_eqpoll_1 by auto
have "has_products I'"
using assms I'
by (meson eqpoll_sym eqpoll_trans has_small_products small_def)
thus ?thesis
using assms(3) I' has_products_preserved_by_bijection
by (metis eqpoll_def eqpoll_sym)
qed
end
section "Small Coproducts"
text‹
In this section we show that the category of small sets and functions has small coproducts.
For this we need to assume the existence of a pairing function and also that the notion
of smallness is respected by small sums.
›
locale small_coproducts_in_sets_cat =
sets_cat_with_cotupling sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
text‹
The global elements of a coproduct ‹CoprodX I A› are in bijection with
‹⋃i∈I. {i} × Set (A i)›.
›
abbreviation CoprodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ ('a × 'U) set"
where "CoprodX I A ≡ ⋃i∈I. {i} × Set (A i)"
definition coprodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'U"
where "coprodX I A ≡ mkide (CoprodX I A)"
lemma small_CoprodX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "small (CoprodX I A)"
using assms small_Set small_Union
by (simp add: Pi_iff smaller_than_small)
lemma embeds_CoprodX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "embeds (CoprodX I A)"
proof
let ?ι = "(λx. pair (fst x) (snd x))"
show "is_embedding_of ?ι (CoprodX I A)"
proof
show "?ι ` CoprodX I A ⊆ Collect arr"
using arrI assms(3) some_pairing_in_univ by auto
show "inj_on ?ι (CoprodX I A)"
proof -
have "inj_on ?ι (Collect arr × Collect arr)"
using some_pairing_is_embedding by auto
moreover have "CoprodX I A ⊆ Collect arr × Collect arr"
using arrI assms(3) by auto
ultimately show ?thesis
by (meson inj_on_subset)
qed
qed
qed
lemma ide_coprodX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "ide (coprodX I A)"
and "bij_betw (OUT (CoprodX I A)) (Set (coprodX I A)) (CoprodX I A)"
and "bij_betw (IN (CoprodX I A)) (CoprodX I A) (Set (coprodX I A))"
and "⋀x. x ∈ Set (coprodX I A) ⟹ OUT (CoprodX I A) x ∈ CoprodX I A"
and "⋀y. y ∈ CoprodX I A ⟹ IN (CoprodX I A) y ∈ Set (coprodX I A)"
and "⋀x. x ∈ Set (coprodX I A) ⟹ IN (CoprodX I A) (OUT (CoprodX I A) x) = x"
and "⋀y. y ∈ CoprodX I A ⟹ OUT (CoprodX I A) (IN (CoprodX I A) y) = y"
proof -
show "ide (coprodX I A)"
unfolding coprodX_def
by (simp add: assms(1,2,3) small_CoprodX embeds_CoprodX ide_mkide(1))
show 1: "bij_betw (OUT (CoprodX I A)) (Set (coprodX I A)) (CoprodX I A)"
unfolding coprodX_def
using assms small_CoprodX embeds_CoprodX bij_OUT [of "CoprodX I A"] by fastforce
show 2: "bij_betw (IN (CoprodX I A)) (CoprodX I A) (Set (coprodX I A))"
unfolding coprodX_def
using assms small_CoprodX embeds_CoprodX bij_IN [of "CoprodX I A"] by fastforce
show "⋀x. x ∈ Set (coprodX I A) ⟹ OUT (CoprodX I A) x ∈ CoprodX I A"
using 1 bij_betwE by blast
show "⋀y. y ∈ CoprodX I A ⟹ IN (CoprodX I A) y ∈ Set (coprodX I A)"
using 2 bij_betwE by blast
show "⋀x. x ∈ Set (coprodX I A) ⟹ IN (CoprodX I A) (OUT (CoprodX I A) x) = x"
using 1 bij_betw_inv_into_left
[of "OUT (CoprodX I A)" "Set (coprodX I A)" "CoprodX I A"]
by (auto simp add: coprodX_def)
show "⋀y. y ∈ CoprodX I A ⟹ OUT (CoprodX I A) (IN (CoprodX I A) y) = y"
by (simp add: OUT_IN assms(1,2,3) small_CoprodX embeds_CoprodX)
qed
abbreviation InX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'a ⇒ 'U ⇒ 'U"
where "InX I A i ≡ λx. if x ∈ Set (A i) then IN (CoprodX I A) (i, x) else null"
definition inX
where "inX I A i ≡ mkarr (A i) (coprodX I A) (InX I A i)"
lemma InX_in_Hom:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "InX I A i ∈ Hom (A i) (coprodX I A)"
using assms ide_coprodX(2-3,5) by auto
lemma inX_in_hom [intro, simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "in_hom (inX I A i) (A i) (coprodX I A)"
using assms ide_coprodX InX_in_Hom
by (unfold inX_def, intro mkarr_in_hom) auto
lemma inX_simps [simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "arr (inX I A i)" and "dom (inX I A i) = A i" and "cod (inX I A i) = coprodX I A"
using assms inX_in_hom by blast+
lemma Fun_inX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "Fun (inX I A i) = InX I A i"
proof -
have "arr (inX I A i)"
by (simp add: assms)
thus ?thesis
by (simp add: inX_def)
qed
definition CotupleX :: "'a set ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) ⇒ 'U ⇒ 'U"
where "CotupleX I A F ≡
(λx. if x ∈ Set (coprodX I A)
then Fun (F (fst (OUT (CoprodX I A) x))) (snd (OUT (CoprodX I A) x))
else null)"
lemma CotupleX_in_Hom:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null"
shows "CotupleX I A F ∈ Hom (coprodX I A) c"
proof
show "CotupleX I A F ∈ {F. ∀x. x ∉ Set (coprodX I A) ⟶ F x = null}"
by (cases "I = {}") (auto simp add: CotupleX_def)
show "CotupleX I A F ∈ Set (coprodX I A) → Set c"
proof (cases "I = {}")
case False
show ?thesis
proof
fix x
assume x: "x ∈ Set (coprodX I A)"
have "OUT (CoprodX I A) x ∈ CoprodX I A"
using assms x ide_coprodX
by (meson bij_betwE)
hence "⋀i. i = fst (OUT (CoprodX I A) x) ⟹
«F i : A i → c» ∧ snd (OUT (CoprodX I A) x) ∈ Set (A i)"
using assms(4) by force
thus "CotupleX I A F x ∈ Set c"
using x CotupleX_def [of I A F] Fun_def by auto
qed
next
case True
show ?thesis
by (metis (no_types, lifting) Pi_I' True True True True UN_E all_not_in_conv
assms(1,3) bij_betwE ide_coprodX(2))
qed
qed
definition cotupleX
where "cotupleX I c A F ≡ mkarr (coprodX I A) c (CotupleX I A F)"
lemma cotupleX_in_hom [intro, simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "«cotupleX I c A F : coprodX I A → c»"
using assms ide_coprodX CotupleX_in_Hom
unfolding cotupleX_def CotupleX_def
by (intro mkarr_in_hom) auto
lemma cotupleX_simps [simp]:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "arr (cotupleX I c A F)"
and "dom (cotupleX I c A F) = coprodX I A"
and "cod (cotupleX I c A F) = c"
using assms cotupleX_in_hom in_homE by blast+
lemma comp_cotupleX_inX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "i ∈ I ⟹ cotupleX I c A F ⋅ inX I A i = F i"
proof -
assume i: "i ∈ I"
have I: "I ≠ {}"
using i by blast
show "cotupleX I c A F ⋅ inX I A i = F i"
proof -
have 1: "cotupleX I c A F ⋅ inX I A i =
mkarr (coprodX I A) c (CotupleX I A F) ⋅ mkarr (A i) (coprodX I A) (InX I A i)"
unfolding inX_def cotupleX_def CotupleX_def
using assms i I comp_mkarr by simp
also have "... = mkarr (A i) c (CotupleX I A F ∘ InX I A i)"
using assms i comp_mkarr
by (metis (no_types, lifting) 1 seqI cotupleX_def cotupleX_simps(1)
dom_mkarr inX_simps(1,3) seqE)
also have "... = mkarr (A i) c
(λx. if x ∈ Set (A i)
then CotupleX I A F (IN (CoprodX I A) (i, x))
else null)"
proof -
have "CotupleX I A F ∘ InX I A i =
(λx. if x ∈ Set (A i) then CotupleX I A F (IN (CoprodX I A) (i, x)) else null)"
proof
fix x
show "(CotupleX I A F ∘ InX I A i) x =
(if x ∈ Set (A i) then CotupleX I A F (IN (CoprodX I A) (i, x)) else null)"
unfolding CotupleX_def by auto
qed
thus ?thesis by simp
qed
also have "... = mkarr (A i) c
(λx. if x ∈ Set (A i)
then Fun (F (fst (OUT (CoprodX I A) (IN (CoprodX I A) (i, x)))))
(snd (OUT (CoprodX I A) (IN (CoprodX I A) (i, x))))
else null)"
proof -
have "⋀x. x ∈ Set (A i) ⟹ IN (CoprodX I A) (i, x) ∈ Set (coprodX I A)"
using assms(1,2,3) i bij_betwE ide_coprodX(3) by blast
hence "(λx. if x ∈ Set (A i)
then CotupleX I A F (IN (CoprodX I A) (i, x))
else null) =
(λx. if x ∈ Set (A i)
then Fun (F (fst (OUT (CoprodX I A) (IN (CoprodX I A) (i, x)))))
(snd (OUT (CoprodX I A) (IN (CoprodX I A) (i, x))))
else null)"
unfolding CotupleX_def by force
thus ?thesis by simp
qed
also have "... = mkarr (A i) c (λx. if x ∈ Set (A i) then Fun (F i) x else null)"
proof -
have "⋀x. x ∈ Set (A i) ⟹ OUT (CoprodX I A) (IN (CoprodX I A) (i, x)) = (i, x)"
using assms i ide_coprodX by auto
hence "(λx. if «x : 𝟭⇧? → A i»
then Fun (F (fst (OUT (CoprodX I A) (IN (CoprodX I A) (i, x)))))
(snd (OUT (CoprodX I A) (IN (CoprodX I A) (i, x))))
else null) =
(λx. if «x : 𝟭⇧? → A i» then Fun (F i) x else null)"
by force
thus ?thesis by simp
qed
also have "... = mkarr (A i) c (Fun (F i))"
by (metis (lifting) Fun_def assms(4) category.in_homE category_axioms
i mem_Collect_eq)
also have "... = F i"
using assms(4) i mkarr_Fun by blast
finally show ?thesis by blast
qed
qed
lemma Fun_cotupleX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "Fun (cotupleX I c A F) =
(λx. if x ∈ Set (coprodX I A)
then Fun (F (fst (OUT (CoprodX I A) x))) (snd (OUT (CoprodX I A) x))
else null)"
using assms Fun_mkarr CotupleX_in_Hom CotupleX_def [of I A F] cotupleX_def cotupleX_simps(1)
by (metis (lifting))
lemma coproduct_cocone_coprodX:
assumes "discrete_diagram J C D" and "Collect (partial_composition.arr J) = I"
and "small I" and "I ⊆ Collect arr"
shows "has_as_coproduct J D (coprodX I D)"
and "coproduct_cocone J C D (coprodX I D) (inX I D)"
proof -
interpret J: category J
using assms(1) discrete_diagram_def by blast
interpret D: discrete_diagram J C D
using assms(1) by blast
let ?π = "inX I D"
let ?a = "coprodX I D"
interpret A: constant_functor J C ?a
using assms ide_coprodX
using D.is_discrete by unfold_locales auto
interpret π: natural_transformation J C D A.map ?π
proof
fix j
show "¬ J.arr j ⟹ inX I D j = null"
by (metis (no_types, lifting) D.as_nat_trans.extensionality ideD(1)
mkarr_def not_arr_null inX_def)
assume j: "J.arr j"
show 1: "arr (inX I D j)"
using D.is_discrete assms j by force
show "inX I D (J.cod j) ⋅ D j = inX I D j"
by (metis (lifting) 1 D.is_discrete D.preserves_ide D.preserves_reflects_arr
J.ideD(3) comp_arr_ide dom_mkarr ideD(3) j inX_def seqI)
show "A.map j ⋅ inX I D (J.dom j) = inX I D j"
by (metis (lifting) 1 A.map_simp D.is_discrete J.ide_char comp_cod_arr j
cod_mkarr inX_def)
qed
show "coproduct_cocone J C D ?a ?π"
proof
fix a' χ'
assume χ': "D.cocone a' χ'"
interpret χ': cocone J C D a' χ'
using χ' by blast
show "∃!f. «f : coprodX I D → a'» ∧ D.cocones_map f (inX I D) = χ'"
proof -
let ?f = "cotupleX I a' D χ'"
have f: "«?f : coprodX I D → a'»"
using assms cotupleX_in_hom
by (metis D.is_discrete D.preserves_ide J.ide_char Pi_I'
χ'.component_in_hom χ'.extensionality χ'.ide_apex mem_Collect_eq)
moreover have "D.cocones_map ?f (inX I D) = χ'"
proof
fix i
show "D.cocones_map ?f (inX I D) i = χ' i"
proof -
have "J.arr i ⟹ ?f ⋅ inX I D i = χ' i"
using assms comp_cotupleX_inX
by (metis D.is_discrete D.preserves_ide J.ide_char Pi_I'
χ'.component_in_hom χ'.extensionality χ'.ide_apex mem_Collect_eq)
moreover have "¬ J.arr i ⟹ null = χ' i"
using χ'.extensionality by auto
moreover have "D.cocone (dom ?f) (inX I D)"
by (metis A.constant_functor_axioms D.diagram_axioms
π.natural_transformation_axioms cocone_def diagram_def f in_homE)
ultimately show ?thesis
using assms χ'.cocone_axioms by auto
qed
qed
moreover have "⋀f'. ⟦«f' : coprodX I D → a'»; D.cocones_map f' (inX I D) = χ'⟧
⟹ f' = ?f"
proof -
fix f'
assume f': "«f' : coprodX I D → a'»"
assume 1: "D.cocones_map f' (inX I D) = χ'"
show "f' = ?f"
proof (intro arr_eqI [of f'])
show par: "par f' ?f"
using f f' by fastforce
show "Fun f' = Fun (cotupleX I a' D χ')"
proof
fix x
show "Fun f' x = Fun (cotupleX I a' D χ') x"
proof (cases "x ∈ Set (coprodX I D)")
case False
show ?thesis
using False par f' Fun_def by auto
next
case True
have 2: "D.cocone (dom f') (inX I D)"
by (metis A.constant_functor_axioms cocone_def
π.natural_transformation_axioms χ' f' in_homE)
have "Fun (cotupleX I a' D χ') x =
Fun (χ' (fst (OUT (CoprodX I D) x))) (snd (OUT (CoprodX I D) x))"
proof -
have "Fun (cotupleX I a' D χ') x = cotupleX I a' D χ' ⋅ x"
using True f Fun_def by auto
also have "... = (λx. if «x : 𝟭⇧? → coprodX I D»
then cotupleX I a' D χ' ⋅ x else null) x"
using True by simp
also have "... =
Fun (χ' (fst (OUT (CoprodX I D) x))) (snd (OUT (CoprodX I D) x))"
using assms f True cotupleX_def [of I a' D χ'] CotupleX_def [of I D χ']
app_mkarr cotupleX_in_hom
by auto
finally show ?thesis by blast
qed
also have "... = Fun f' x"
proof (cases "OUT (CoprodX I D) x")
case (Pair i x')
have ix': "(i, x') ∈ CoprodX I D"
using assms True Pair ide_coprodX(2) [of I D]
by (metis (no_types, lifting) D.is_discrete D.preserves_ide Pi_I'
bij_betwE mem_Collect_eq)
have "Fun (χ' (fst (OUT (CoprodX I D) x))) (snd (OUT (CoprodX I D) x)) =
Fun (χ' i) x'"
by (simp add: Pair)
also have "... = Fun (D.cocones_map f' (inX I D) i) x'"
using 1 by simp
also have "... = (f' ⋅ inX I D i) ⋅ x'"
using assms 2 f' ix' inX_in_hom Fun_def D.extensionality D.is_discrete
π.extensionality
by auto
also have "... = f' ⋅ (inX I D i ⋅ x')"
using comp_assoc by simp
also have "... = f' ⋅ IN (CoprodX I D) (i, x')"
proof -
have "«inX I D i : D i → coprodX I D»"
using assms inX_in_hom D.is_discrete ix' by fastforce
hence "«mkarr (D i) (coprodX I D) (InX I D i) : D i → coprodX I D»"
unfolding inX_def by simp
thus ?thesis
unfolding inX_def
using assms ix' app_mkarr by auto
qed
also have "... = f' ⋅ x"
proof -
have "IN (CoprodX I D) (i, x') = IN (CoprodX I D) (OUT (CoprodX I D) x)"
using Pair by simp
also have "... = x"
proof -
have "small (CoprodX I D)"
using assms small_CoprodX D.is_discrete by fastforce
thus ?thesis
using assms True ide_coprodX(6) D.is_discrete D.preserves_ide
Pi_I' coprodX_def
by force
qed
finally show ?thesis by simp
qed
finally show ?thesis
using True f' Fun_def by force
qed
finally show ?thesis by simp
qed
qed
qed
qed
ultimately show ?thesis by blast
qed
qed
thus "has_as_coproduct J D (coprodX I D)"
using has_as_coproduct_def by blast
qed
lemma has_small_coproducts:
assumes "small I" and "I ⊆ Collect arr"
shows "has_coproducts I"
proof (unfold has_coproducts_def, intro conjI)
show "I ≠ UNIV"
using assms not_arr_null by blast
show "∀J D. discrete_diagram J (⋅) D ∧ Collect (partial_composition.arr J) = I
⟶ (∃a. has_as_coproduct J D a)"
using assms coproduct_cocone_coprodX by blast
qed
end
subsection "Exported Notions"
context sets_cat_with_cotupling
begin
interpretation Coproducts: small_coproducts_in_sets_cat ..
abbreviation CoprodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ ('a × 'U) set"
where "CoprodX ≡ Coproducts.CoprodX"
abbreviation coprodX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'U"
where "coprodX ≡ Coproducts.coprodX"
abbreviation inX :: "'a set ⇒ ('a ⇒ 'U) ⇒ 'a ⇒ 'U"
where "inX ≡ Coproducts.inX"
abbreviation cotupleX :: "'a set ⇒ 'U ⇒ ('a ⇒ 'U) ⇒ ('a ⇒ 'U) ⇒ 'U"
where "cotupleX ≡ Coproducts.cotupleX"
lemma coprod_comparison_map_props:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
shows "OUT (CoprodX I A) ∈ Set (coprodX I A) → CoprodX I A"
and "IN (CoprodX I A) ∈ CoprodX I A → Set (coprodX I A)"
and "⋀x. x ∈ Set (coprodX I A) ⟹ IN (CoprodX I A) (OUT (CoprodX I A) x) = x"
and "⋀y. y ∈ CoprodX I A ⟹ OUT (CoprodX I A) (IN (CoprodX I A) y) = y"
and "bij_betw (OUT (CoprodX I A)) (Set (coprodX I A)) (CoprodX I A)"
and "bij_betw (IN (CoprodX I A)) (CoprodX I A) (Set (coprodX I A))"
using assms Coproducts.ide_coprodX by auto
lemma Fun_inX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "i ∈ I"
shows "Fun (inX I A i) = Coproducts.InX I A i"
using assms Coproducts.Fun_inX by auto
lemma Fun_cotupleX:
assumes "small I" and "A ∈ I → Collect ide" and "I ⊆ Collect arr"
and "⋀i. i ∈ I ⟹ «F i : A i → c»" and "⋀i. i ∉ I ⟹ F i = null" and "ide c"
shows "Fun (cotupleX I c A F) =
(λx. if x ∈ Set (coprodX I A)
then Fun (F (fst (OUT (⋃i∈I. {i} × Set (A i)) x)))
(snd (OUT (⋃i∈I. {i} × Set (A i)) x))
else null)"
using assms Coproducts.Fun_cotupleX app_mkarr Coproducts.cotupleX_def by auto
lemma coproduct_cocone_coprodX:
assumes "discrete_diagram J C D" and "Collect (partial_composition.arr J) = I"
and "small I" and "I ⊆ Collect arr"
shows "has_as_coproduct J D (coprodX I D)"
and "coproduct_cocone J C D (coprodX I D) (inX I D)"
using assms Coproducts.coproduct_cocone_coprodX by auto
lemma has_small_coproducts:
assumes "small I" and "I ⊆ Collect arr"
shows "has_coproducts I"
using assms Coproducts.has_small_coproducts by blast
end
section "Coequalizers"
text‹
In this section we show that a sets category has coequalizers of parallel pairs
of arrows. For this, we need to assume that the set of arrows of the category
embeds the set of all its small subsets. The reason we need this assumption is to
make it possible to obtain an object corresponding to the set of equivalence classes
that results from the quotient construction.
›
locale sets_cat_with_powering =
sets_cat sml C +
powering sml ‹Collect arr›
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
sublocale sets_cat_with_tupling ⊆ sets_cat_with_powering ..
locale coequalizers_in_sets_cat =
sets_cat_with_powering sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
text‹
The following defines the ``equivalence closure'' of a binary relation ‹r›
on a set ‹A›, and proves the characterization of it as the least equivalence relation
on ‹A› that contains ‹r›. For some reason I could not find such a thing in the
Isabelle distribution, though I did find a predicate version @{term equivclp}.
›
definition equivcl
where "equivcl A r ≡ SOME r'. r ⊆ r' ∧ equiv A r' ∧ (∀s'. r ⊆ s' ∧ equiv A s' ⟶ r' ⊆ s')"
lemma equivcl_props:
assumes "r ⊆ A × A"
shows "∃r'. r ⊆ r' ∧ equiv A r' ∧ (∀s'. r ⊆ s' ∧ equiv A s' ⟶ r' ⊆ s')"
and "r ⊆ equivcl A r" and "equiv A (equivcl A r)"
and "⋀s'. r ⊆ s' ∧ equiv A s' ⟹ equivcl A r ⊆ s'"
proof -
have 1: "equiv A (A × A)"
using refl_on_def trans_on_def
by (intro equivI symI) auto
show 2: "∃r'. r ⊆ r' ∧ equiv A r' ∧ (∀s'. r ⊆ s' ∧ equiv A s' ⟶ r' ⊆ s')"
proof -
let ?r' = "⋂ {s. equiv A s ∧ r ⊆ s}"
have "r ⊆ ?r'"
by blast
moreover have "∀s'. r ⊆ s' ∧ equiv A s' ⟶ ?r' ⊆ s'"
by blast
moreover have "equiv A ?r'"
using assms 1
apply (intro equivI symI transI refl_onI)
apply auto[4]
apply (simp add: equiv_def refl_on_def)
apply (meson equiv_def symD)
by (meson equivE transE)
ultimately show ?thesis by blast
qed
have "r ⊆ equivcl A r ∧ equiv A (equivcl A r) ∧
(∀s'. r ⊆ s' ∧ equiv A s' ⟶ equivcl A r ⊆ s')"
unfolding equivcl_def
using 2 someI_ex [of "λr'. r ⊆ r' ∧ equiv A r' ∧ (∀s'. r ⊆ s' ∧ equiv A s' ⟶ r' ⊆ s')"]
by fastforce
thus "r ⊆ equivcl A r" and "equiv A (equivcl A r)"
and "⋀s'. r ⊆ s' ∧ equiv A s' ⟹ equivcl A r ⊆ s'"
by auto
qed
text‹
The elements of the codomain of the coequalizer of ‹f› and ‹g› are the equivalence
classes of the least equivalence relation on ‹Set (cod f)› that relates ‹f ⋅ x›
and ‹g ⋅ x› whenever ‹x ∈ Set (dom f)›.
›
abbreviation Cod_coeq :: "'U ⇒ 'U ⇒ 'U set set"
where "Cod_coeq f g ≡ (λy. (equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {y})) ` Set (cod f)"
lemma small_Cod_coeq:
assumes "par f g"
shows "small (Cod_coeq f g)"
using assms ide_cod small_Set by blast
lemma embeds_Cod_coeq:
assumes "par f g"
shows "embeds (Cod_coeq f g)"
and "Cod_coeq f g ⊆ Pow (Set (cod f))"
proof -
show 1: "Cod_coeq f g ⊆ Pow (Set (cod f))"
proof -
let ?r = "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)"
have "?r ⊆ Set (cod f) × Set (cod f)"
using assms by auto
hence "equivcl (Set (cod f)) ?r ⊆ Set (cod f) × Set (cod f)"
using equivcl_props(3)
by (metis (no_types, lifting) Sigma_cong equiv_type)
thus ?thesis by blast
qed
show "embeds (Cod_coeq f g)"
proof -
have "Cod_coeq f g ⊆ {X. X ⊆ Collect arr ∧ small X}"
proof -
have "Cod_coeq f g ⊆ {X. X ⊆ Collect arr}"
using 1 by blast
moreover have "Cod_coeq f g ⊆ {X. small X}"
using assms 1 small_Set smaller_than_small
by (metis (no_types, lifting) HOL.ext Collect_mono Pow_def
ide_cod subset_trans)
ultimately show ?thesis by blast
qed
thus ?thesis
using embeds_small_sets
by (meson image_mono inj_on_subset subset_trans)
qed
qed
definition cod_coeq
where "cod_coeq f g ≡ mkide (Cod_coeq f g)"
lemma ide_cod_coeq:
assumes "par f g"
shows "ide (cod_coeq f g)"
and "bij_betw (OUT (Cod_coeq f g)) (Set (cod_coeq f g)) (Cod_coeq f g)"
and "bij_betw (IN (Cod_coeq f g)) (Cod_coeq f g) (Set (cod_coeq f g))"
and "⋀x. x ∈ Set (cod_coeq f g) ⟹ OUT (Cod_coeq f g) x ∈ Cod_coeq f g"
and "⋀y. y ∈ Cod_coeq f g ⟹ IN (Cod_coeq f g) y ∈ Set (cod_coeq f g)"
and "⋀x. x ∈ Set (cod_coeq f g) ⟹ IN (Cod_coeq f g) (OUT (Cod_coeq f g) x) = x"
and "⋀y. y ∈ Cod_coeq f g ⟹ OUT (Cod_coeq f g) (IN (Cod_coeq f g) y) = y"
proof -
have "(λx. {f ⋅ x, g ⋅ x}) ` Set (dom f) ⊆ Pow (Set (cod f))"
using assms by auto
show "ide (cod_coeq f g)"
using small_Cod_coeq embeds_Cod_coeq assms cod_coeq_def by auto
show 1: "bij_betw (OUT (Cod_coeq f g)) (Set (cod_coeq f g)) (Cod_coeq f g)"
unfolding cod_coeq_def
using assms ide_mkide bij_OUT small_Cod_coeq [of f g] embeds_Cod_coeq [of f g]
by auto
show 2: "bij_betw (IN (Cod_coeq f g)) (Cod_coeq f g) (Set (cod_coeq f g))"
unfolding cod_coeq_def
using assms ide_mkide bij_OUT bij_IN small_Cod_coeq [of f g] embeds_Cod_coeq
by fastforce
show "⋀x. x ∈ Set (cod_coeq f g) ⟹ OUT (Cod_coeq f g) x ∈ Cod_coeq f g"
using 1 bij_betwE by blast
show "⋀y. y ∈ Cod_coeq f g ⟹ IN (Cod_coeq f g) y ∈ Set (cod_coeq f g)"
using 2 bij_betwE by blast
show "⋀x. x ∈ Set (cod_coeq f g) ⟹ IN (Cod_coeq f g) (OUT (Cod_coeq f g) x) = x"
by (metis (no_types, lifting) HOL.ext "1" bij_betw_inv_into_left cod_coeq_def)
show "⋀y. y ∈ Cod_coeq f g ⟹ OUT (Cod_coeq f g) (IN (Cod_coeq f g) y) = y"
by (metis (no_types, lifting) HOL.ext "1" bij_betw_inv_into_right cod_coeq_def)
qed
definition Coeq
where "Coeq f g ≡ λy. if y ∈ Set (cod f)
then IN (Cod_coeq f g)
(equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {y})
else null"
lemma Coeq_in_Hom [intro]:
assumes "par f g"
shows "Coeq f g ∈ Hom (cod f) (cod_coeq f g)"
proof
show "Coeq f g ∈ Set (cod f) → Set (cod_coeq f g)"
proof
fix y
assume y: "y ∈ Set (cod f)"
have "Coeq f g y = IN (Cod_coeq f g)
(equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {y})"
unfolding Coeq_def
using y by simp
moreover have "... ∈ Set (cod_coeq f g)"
using assms ide_cod_coeq(5) y by blast
ultimately show "Coeq f g y ∈ Set (cod_coeq f g)" by simp
qed
show "Coeq f g ∈ {F. ∀x. x ∉ Set (cod f) ⟶ F x = null}"
unfolding Coeq_def by simp
qed
definition coeq
where "coeq f g ≡ mkarr (cod f) (cod_coeq f g) (Coeq f g)"
lemma coeq_in_hom [intro, simp]:
assumes "par f g"
shows "«coeq f g : cod f → cod_coeq f g»"
using assms ide_cod_coeq(1) Coeq_in_Hom
by (unfold coeq_def, intro mkarr_in_hom) auto
lemma coeq_simps [simp]:
assumes "par f g"
shows "arr (coeq f g)" and "dom (coeq f g) = cod f" and "cod (coeq f g) = cod_coeq f g"
using assms coeq_in_hom by blast+
lemma Fun_coeq:
assumes "par f g"
shows "Fun (coeq f g) = Coeq f g"
using assms Fun_mkarr coeq_def coeq_simps(1) by presburger
lemma coeq_coequalizes:
assumes "par f g"
shows "coeq f g ⋅ f = coeq f g ⋅ g"
proof (intro arr_eqI)
show par: "par (coeq f g ⋅ f) (coeq f g ⋅ g)"
using assms by auto
show "Fun (coeq f g ⋅ f) = Fun (coeq f g ⋅ g)"
proof
fix x
show "Fun (coeq f g ⋅ f) x = Fun (coeq f g ⋅ g) x"
proof (cases "x ∈ Set (dom f)")
case False
show ?thesis
using assms False Fun_coeq Fun_def by simp
next
case True
show ?thesis
proof -
have "Fun (coeq f g ⋅ f) x = Fun (coeq f g) (Fun f x)"
using assms Fun_comp comp_in_homI coeq_in_hom comp_assoc by auto
also have "... = Coeq f g (Fun f x)"
using assms True Fun_coeq
by (metis (full_types, lifting))
also have "... = IN (Cod_coeq f g)
(equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {f ⋅ x})"
unfolding Coeq_def
using True assms Fun_def by auto
also have "... = IN (Cod_coeq f g)
(equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {g ⋅ x})"
proof -
have "equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {f ⋅ x} =
equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {g ⋅ x}"
using assms True
equivcl_props(2-3) [of "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)" "Set (cod f)"]
equiv_class_eq_iff
[of "Set (cod f)"
"equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f))"
"f ⋅ x" "g ⋅ x"]
by auto
thus ?thesis by simp
qed
also have "... = Coeq f g (Fun g x)"
unfolding Coeq_def
using True assms Fun_def by auto
also have "... = Fun (coeq f g) (Fun g x)"
using assms True Fun_coeq
by (metis (full_types, lifting))
also have "... = Fun (coeq f g ⋅ g) x"
using assms Fun_comp comp_in_homI coeq_in_hom comp_assoc by auto
finally show ?thesis by blast
qed
qed
qed
qed
lemma Coeq_surj:
assumes "par f g" and "Set (cod f) ≠ {}" and "y ∈ Set (cod_coeq f g)"
shows "∃x. x ∈ Set (cod f) ∧ Coeq f g x = y"
proof -
have 1: "(⋃x∈Set (dom f). {f ⋅ x, g ⋅ x}) ⊆ Set (cod f)"
using assms by auto
have y: "OUT (Cod_coeq f g) y ∈ Cod_coeq f g"
using assms ide_cod_coeq(2) [of f g] bij_betwE by blast
obtain x where x: "x ∈ Set (cod f) ∧
OUT (Cod_coeq f g) y =
equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) ``{x}"
using assms y by blast
hence 2: "x ∈ OUT (Cod_coeq f g) y"
proof -
have "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f) ⊆ Set (cod f) × Set (cod f)"
using assms by auto
hence "x ∈ equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) ``{x}"
using assms x equivcl_props(3) [of "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)" "Set (cod f)"]
equiv_class_self
by (metis (lifting))
thus ?thesis
using x by argo
qed
have "Coeq f g x = y"
proof -
have "OUT (Cod_coeq f g) (Coeq f g x) =
OUT (Cod_coeq f g)
(IN (Cod_coeq f g)
(equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) ``{x}))"
unfolding Coeq_def
using x by presburger
also have "... = equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) ``{x}"
using assms x y ide_cod_coeq(7) by (metis (lifting))
also have "... = OUT (Cod_coeq f g) y"
proof -
have "OUT (Cod_coeq f g) y ∈ Cod_coeq f g"
using assms x by force
thus ?thesis
using assms x 1 2 by blast
qed
finally have "IN (Cod_coeq f g) (OUT (Cod_coeq f g) (Coeq f g x)) =
IN (Cod_coeq f g) (OUT (Cod_coeq f g) y)"
by simp
thus ?thesis
using assms x y ide_cod_coeq(6) cod_coeq_def Coeq_def
by (metis (lifting))
qed
thus "∃x. x ∈ Set (cod f) ∧ Coeq f g x = y"
using x by blast
qed
lemma coeq_is_coequalizer:
assumes "par f g" and "Set (cod f) ≠ {}"
shows "has_as_coequalizer f g (coeq f g)"
proof
show "par f g" by fact
show "seq (coeq f g) f"
using assms by auto
show "coeq f g ⋅ f = coeq f g ⋅ g"
using assms coeq_coequalizes by blast
show "⋀q'. ⟦seq q' f; q' ⋅ f = q' ⋅ g⟧ ⟹ ∃!h. h ⋅ coeq f g = q'"
proof -
fix q'
assume seq: "seq q' f" and eq: "q' ⋅ f = q' ⋅ g"
let ?H = "λy. if y ∈ Set (cod_coeq f g)
then q' ⋅ (SOME x. x ∈ Set (cod f) ∧ Coeq f g x = y)
else null"
have H: "?H ∈ Hom (cod_coeq f g) (cod q')"
proof
show "?H ∈ Set (cod_coeq f g) → Set (cod q')"
proof
fix y
assume y: "y ∈ Set (cod_coeq f g)"
have "?H y = q' ⋅ (SOME x. x ∈ Set (cod f) ∧ Coeq f g x = y)"
using y by simp
moreover have "... ∈ Set (cod q')"
using assms y someI_ex [of "λx. x ∈ Set (cod f) ∧ Coeq f g x = y"]
Coeq_surj seq in_homI
by blast
ultimately show "?H y ∈ Set (cod q')" by simp
qed
show "?H ∈ {F. ∀x. x ∉ Set (cod_coeq f g) ⟶ F x = null}"
by simp
qed
let ?h = "mkarr (cod_coeq f g) (cod q') ?H"
have h: "«?h : cod_coeq f g → cod q'»"
using assms H ide_cod_coeq seq
by (intro mkarr_in_hom) auto
have *: "?h ⋅ coeq f g = q'"
proof (intro arr_eqI)
show par: "par (?h ⋅ coeq f g) q'"
using assms h seq by fastforce
show "Fun (?h ⋅ coeq f g) = Fun q'"
proof -
have "Fun (?h ⋅ coeq f g) = Fun ?h ∘ Fun (coeq f g)"
using Fun_comp par by blast
also have "... = ?H ∘ Coeq f g"
using assms h Fun_coeq Fun_mkarr arrI by auto
also have "... = Fun q'"
proof
fix y
show "(?H ∘ Coeq f g) y = Fun q' y"
proof (cases "y ∈ Set (cod f)")
case False
show ?thesis
unfolding Coeq_def
using False seq Fun_def by auto
next
case True
have "(?H ∘ Coeq f g) y =
q' ⋅ (SOME x'. x' ∈ Set (cod f) ∧ Coeq f g x' = Coeq f g y)"
using Coeq_in_Hom True assms(1) by auto
also have "... = q' ⋅ y"
proof -
let ?e = "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)"
have e: "?e ⊆ Set (cod f) × Set (cod f)"
using assms by auto
let ?ℰ = "equivcl (Set (cod f)) ?e"
let ?ℰ' = "{p ∈ Set (cod f) × Set (cod f). q' ⋅ fst p = q' ⋅ snd p}"
have "?ℰ ⊆ ?ℰ'"
proof -
have "equiv (Set (cod f)) ?ℰ'"
by (intro equivI symI) (auto simp add: refl_on_def trans_on_def)
moreover have "(λx. (f ⋅ x, g ⋅ x)) ` Set (dom f) ⊆ ?ℰ'"
proof -
have "⋀x. x ∈ Set (dom f) ⟹ (f ⋅ x, g ⋅ x) ∈ ?ℰ'"
proof -
fix x
assume x: "x ∈ Set (dom f)"
have "(f ⋅ x, g ⋅ x) ∈ Set (cod f) × Set (cod f)"
using assms x by auto
moreover have "q' ⋅ f ⋅ x = q' ⋅ g ⋅ x"
using eq comp_assoc by metis
ultimately show "(f ⋅ x, g ⋅ x) ∈ ?ℰ'" by fastforce
qed
thus ?thesis
by (meson image_subsetI)
qed
ultimately show ?thesis
by (meson equiv_type equivcl_props(4) subset_trans)
qed
moreover have "⋀y'. y' ∈ Set (cod f) ∧ Coeq f g y' = Coeq f g y
⟹ (y', y) ∈ ?ℰ"
proof -
fix y'
assume y': "y' ∈ Set (cod f) ∧ Coeq f g y' = Coeq f g y"
have eq: "equivcl (Set (cod f)) ?e `` {y'} =
equivcl (Set (cod f)) ?e `` {y}"
using assms(1) True y' ide_cod_coeq(7) [of f g]
unfolding Coeq_def
by (metis (mono_tags, lifting) image_eqI)
moreover have "y' ∈ equivcl (Set (cod f)) ?e `` {y'} ∧
y ∈ equivcl (Set (cod f)) ?e `` {y}"
proof
have 1: "equiv (Set (cod f)) (equivcl (Set (cod f)) ?e)"
by (simp add: e equivcl_props(3))
show "y' ∈ equivcl (Set (cod f)) ?e `` {y'}"
by (metis (lifting) 1 equiv_class_self y')
show "y ∈ equivcl (Set (cod f)) ((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {y}"
by (metis (no_types, lifting) 1 True equiv_class_self)
qed
ultimately show "(y', y) ∈ ?ℰ" by blast
qed
ultimately have "⋀y'. y' ∈ Set (cod f) ∧ Coeq f g y' = Coeq f g y
⟹ (y', y) ∈ ?ℰ'"
by (meson subsetD)
thus ?thesis
using True someI_ex [of "λy'. y' ∈ Set (cod f) ∧ Coeq f g y' = Coeq f g y"]
by (metis (mono_tags, lifting) fst_conv mem_Collect_eq snd_conv)
qed
also have "... = Fun q' y"
using True seq Fun_def by auto
finally show ?thesis by blast
qed
qed
finally show ?thesis by blast
qed
qed
moreover have "⋀h'. h' ⋅ coeq f g = q' ⟹ h' = ?h"
proof -
fix h'
assume h': "h' ⋅ coeq f g = q'"
show "h' = ?h"
proof (intro arr_eqI [of h'])
show par: "par h' ?h"
using h h' seq
by (metis (lifting) calculation cod_comp seqE)
show "Fun h' = Fun ?h"
proof -
have 1: "Fun h' ∘ Coeq f g = Fun ?h ∘ Coeq f g"
using assms h' * Fun_coeq Fun_comp seq seqE
by (metis (lifting))
show ?thesis
proof
fix z
show "Fun h' z = Fun ?h z"
proof (cases "z ∈ Set (cod_coeq f g)")
case False
show ?thesis
using assms False h' par Fun_def by auto
next
case True
obtain x where x: "x ∈ Set (cod f) ∧ Coeq f g x = z"
using assms True Coeq_surj by blast
show ?thesis
using True x h' 1 * Fun_comp comp_apply
by (metis (lifting))
qed
qed
qed
qed
qed
ultimately show "∃!h. h ⋅ coeq f g = q'" by auto
qed
qed
lemma has_coequalizers:
assumes "par f g"
shows "∃e. has_as_coequalizer f g e"
proof (cases "Set (cod f) = {}")
case False
show ?thesis
using assms False coeq_is_coequalizer by blast
next
case True
have "f = g"
using assms True
by (metis arr_eqI' comp_in_homI empty_Collect_eq in_homI)
hence "has_as_coequalizer f g (cod f)"
using assms comp_arr_dom comp_cod_arr seqE
by (intro has_as_coequalizerI) metis+
thus ?thesis by blast
qed
end
subsection "Exported Notions"
context sets_cat_with_powering
begin
interpretation Coeq: coequalizers_in_sets_cat sml C ..
abbreviation Cod_coeq
where "Cod_coeq ≡ Coeq.Cod_coeq"
abbreviation coeq
where "coeq ≡ Coeq.coeq"
lemma coequalizer_comparison_map_props:
assumes "par f g"
shows "bij_betw (OUT (Cod_coeq f g)) (Set (cod (coeq f g))) (Cod_coeq f g)"
and "bij_betw (IN (Cod_coeq f g)) (Cod_coeq f g) (Set (cod (coeq f g)))"
and "⋀x. x ∈ Set (cod (coeq f g)) ⟹ OUT (Cod_coeq f g) x ∈ Cod_coeq f g"
and "⋀y. y ∈ Cod_coeq f g ⟹ IN (Cod_coeq f g) y ∈ Set (cod (coeq f g))"
and "⋀x. x ∈ Set (cod (coeq f g)) ⟹ IN (Cod_coeq f g) (OUT (Cod_coeq f g) x) = x"
and "⋀y. y ∈ Cod_coeq f g ⟹ OUT (Cod_coeq f g) (IN (Cod_coeq f g) y) = y"
using assms Coeq.ide_cod_coeq by auto
lemma coeq_is_coequalizer:
assumes "par f g" and "Set (cod f) ≠ {}"
shows "has_as_coequalizer f g (coeq f g)"
using assms Coeq.coeq_is_coequalizer by blast
text‹
Since the fact ‹Fun_coeq› below is not very useful without the notions used in
stating it, the function ‹equivcl› and characteristic fact ‹equivcl_props› are
also exported here. It would be better if ‹Fun_coeq› could be expressed completely
in terms of existing notions from the library.
›
definition equivcl
where "equivcl ≡ Coeq.equivcl"
lemma equivcl_props:
assumes "r ⊆ A × A"
shows "∃r'. r ⊆ r' ∧ equiv A r' ∧ (∀s'. r ⊆ s' ∧ equiv A s' ⟶ r' ⊆ s')"
and "r ⊆ equivcl A r" and "equiv A (equivcl A r)"
and "⋀s'. r ⊆ s' ∧ equiv A s' ⟹ equivcl A r ⊆ s'"
using assms Coeq.equivcl_props [of r A]
unfolding equivcl_def by auto
lemma Fun_coeq:
assumes "par f g"
shows "Fun (coeq f g) = (λy. if y ∈ Set (cod f)
then IN (Cod_coeq f g)
(equivcl (Set (cod f))
((λx. (f ⋅ x, g ⋅ x)) ` Set (dom f)) `` {y})
else null)"
using assms Coeq.Fun_coeq Coeq.Coeq_def
unfolding equivcl_def by auto
lemma has_coequalizers:
assumes "par f g"
shows "∃e. has_as_coequalizer f g e"
using assms Coeq.has_coequalizers by blast
end
section "Exponentials"
text‹
In this section we show that the category is cartesian closed.
›
locale exponentials_in_sets_cat =
sets_cat_with_tupling sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
abbreviation app :: "'U ⇒ 'U ⇒ 'U"
where "app f ≡ inv_into SEF some_embedding_of_small_functions f"
abbreviation Exp :: "'U ⇒ 'U ⇒ ('U ⇒ 'U) set"
where "Exp a b ≡ {F. F ∈ Set a → Set b ∧ (∀x. x ∉ Set a ⟶ F x = null)}"
definition exp :: "'U ⇒ 'U ⇒ 'U"
where "exp a b ≡ mkide (Exp a b)"
lemma memb_Exp_popular_value:
assumes "ide a" and "ide b" and "F ∈ Exp a b"
and "popular_value F y"
shows "y = null"
proof -
have "y ∈ Set b ∨ y = null"
using assms popular_value_in_range [of F y] by blast
hence "y ≠ null ⟹ {x. F x = y} ⊆ Set a"
using assms by blast
thus "y = null"
using assms smaller_than_small small_Set by auto
qed
lemma memb_Exp_imp_small_function:
assumes "ide a" and "ide b" and "F ∈ Exp a b"
shows "small_function F"
proof
show "small (range F)"
proof -
have "range F ⊆ Set b ∪ {null}"
using assms by blast
moreover have "small ..."
using assms small_Set by auto
ultimately show ?thesis
using smaller_than_small by blast
qed
show "at_most_one_popular_value F"
using assms memb_Exp_popular_value Uniq_def
by (metis (no_types, lifting))
qed
lemma small_Exp:
assumes "ide a" and "ide b"
shows "small (Exp a b)"
proof -
show ?thesis
proof (cases "small (UNIV :: 'U set)")
case False
have "Exp a b ⊆ {F. small_function F ∧ SF_Dom F ⊆ Set a ∧ range F ⊆ Set b ∪ {null}}"
proof
fix F
assume F: "F ∈ Exp a b"
have "small_function F"
using assms F memb_Exp_imp_small_function [of a b F] by blast
moreover have "SF_Dom F ⊆ Set a"
proof -
have "popular_value F null"
proof -
have "⋀F y. F ∈ Exp a b ⟹ popular_value F y ⟹ y = null"
using assms memb_Exp_popular_value by meson
moreover have "∃y. popular_value F y"
by (metis (no_types, lifting) HOL.ext False assms(1,2) ex_popular_value_iff
F memb_Exp_imp_small_function)
ultimately show ?thesis
using F by blast
qed
thus ?thesis
using F by auto
qed
moreover have "range F ⊆ Set b ∪ {null}"
using F by blast
ultimately
show "F ∈ {F. small_function F ∧ SF_Dom F ⊆ Set a ∧ range F ⊆ Set b ∪ {null}}"
by blast
qed
thus ?thesis
using False small_funcset [of "Set a" "Set b ∪ {null}"]
small_Set assms(1,2) smaller_than_small
by fastforce
next
case True
have "Exp a b ⊆ {F. small_function F ∧ SF_Dom F ⊆ UNIV ∧ range F ⊆ Set b ∪ {null}}"
using assms memb_Exp_imp_small_function by auto
thus ?thesis
using True small_funcset [of UNIV "Set b ∪ {null}"]
small_Set assms(1,2) smaller_than_small
by (metis (mono_tags, lifting) subset_UNIV)
qed
qed
lemma embeds_Exp:
assumes "ide a" and "ide b"
shows "embeds (Exp a b)"
proof -
have "is_embedding_of some_embedding_of_small_functions (Exp a b)"
proof -
have "Exp a b ⊆ SEF"
unfolding EF_def
using assms memb_Exp_imp_small_function by blast
thus ?thesis
using assms some_embedding_of_small_functions_is_embedding memb_Exp_popular_value
by (meson image_mono inj_on_subset subset_trans)
qed
thus ?thesis by blast
qed
lemma ide_exp:
assumes "ide a" and "ide b"
shows "ide (exp a b)"
and "bij_betw (OUT (Exp a b)) (Set (exp a b)) (Exp a b)"
and "bij_betw (IN (Exp a b)) (Exp a b) (Set (exp a b))"
proof -
have "small (Exp a b)"
using assms small_Exp by blast
moreover have "embeds (Exp a b)"
using assms embeds_Exp by blast
ultimately show "ide (exp a b)" and "bij_betw (OUT (Exp a b)) (Set (exp a b)) (Exp a b)"
unfolding exp_def
using assms ide_mkide bij_OUT by blast+
thus "bij_betw (IN (Exp a b)) (Exp a b) (Set (exp a b))"
using bij_betw_inv_into exp_def by fastforce
qed
abbreviation Eval
where "Eval b c ≡ (λfx. if fx ∈ Set (prod (exp b c) b)
then OUT (Exp b c)
(Fun (pr⇩1 (exp b c) b) fx)
(Fun (pr⇩0 (exp b c) b) fx)
else null)"
definition eval
where "eval b c ≡ mkarr (prod (exp b c) b) c (Eval b c)"
lemma eval_in_hom [intro, simp]:
assumes "ide b" and "ide c"
shows "«eval b c : prod (exp b c) b → c»"
proof (unfold eval_def, intro mkarr_in_hom)
show "ide c" by fact
show "ide (prod (exp b c) b)"
using assms ide_exp ide_prod by auto
show "Eval b c ∈ Hom (prod (exp b c) b) c"
proof
show "Eval b c ∈ Set (prod (exp b c) b) → Set c"
proof
fix fx
assume fx: "fx ∈ Set (prod (exp b c) b)"
have "Eval b c fx = OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) fx)
(Fun (pr⇩0 (exp b c) b) fx)"
using fx by simp
moreover have "... ∈ Set c"
proof -
have "OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) fx) ∈ Exp b c"
proof -
have "Fun (pr⇩1 (exp b c) b) fx ∈ Set (exp b c)"
using assms fx Fun_def
by (simp add: comp_in_homI ide_exp(1))
thus ?thesis
using assms(1,2) bij_betwE ide_exp(2) by blast
qed
moreover have "Fun (pr⇩0 (exp b c) b) fx ∈ Set b"
using assms(1,2) fx ide_exp(1) Fun_def by auto
ultimately show ?thesis by blast
qed
ultimately show "Eval b c fx ∈ Set c" by auto
qed
show "Eval b c ∈ {F. ∀x. x ∉ Set (prod (exp b c) b) ⟶ F x = null}"
by simp
qed
qed
lemma eval_simps [simp]:
assumes "ide b" and "ide c"
shows "arr (eval b c)" and "dom (eval b c) = prod (exp b c) b" and "cod (eval b c) = c"
using assms eval_in_hom by blast+
lemma Fun_eval:
assumes "ide b" and "ide c"
shows "Fun (eval b c) = Eval b c"
using assms eval_def Fun_mkarr [of "prod (exp b c) b" c "Eval b c"]
by (metis arrI eval_in_hom)
definition Curry
where "Curry a b c ≡ λf. if «f : prod a b → c»
then mkarr a (exp b c)
(λx. if x ∈ Set a
then IN (Exp b c)
(λy. if y ∈ Set b
then C f (tuple x y)
else null)
else null)
else null"
lemma Curry_in_hom [intro]:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "«Curry a b c f : a → exp b c»"
and "Fun (Curry a b c f) =
(λx. if x ∈ Set a
then IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
else null)"
proof -
have "⋀x. x ∈ Set a ⟹
IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
∈ Set (exp b c)"
proof -
fix x
assume x: "x ∈ Set a"
have "(λy. if y ∈ Set b then C f (tuple x y) else null) ∈ Exp b c"
proof -
have "⋀y. y ∈ Set b ⟹ C f (tuple x y) ∈ Set c"
using assms x by auto
thus ?thesis by simp
qed
thus "IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
∈ Set (exp b c)"
using assms bij_betwE ide_exp
by (metis (no_types, lifting))
qed
thus "«Curry a b c f : a → exp b c»"
unfolding Curry_def
using assms ide_exp
by (simp, intro mkarr_in_hom, auto)
show "Fun (Curry a b c f) =
(λx. if x ∈ Set a
then IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
else null)"
using ‹«Curry a b c f : a → exp b c»› arrI assms(4) Curry_def app_mkarr
by auto
qed
lemma Curry_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "arr (Curry a b c f)" and "dom (Curry a b c f) = a" and "cod (Curry a b c f) = exp b c"
using assms Curry_in_hom by blast+
lemma Fun_Curry:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "Fun (Curry a b c f) =
(λx. if x ∈ Set a
then IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
else null)"
using assms Curry_in_hom(2) by blast
interpretation elementary_category_with_terminal_object C ‹𝟭⇧?› some_terminator
using extends_to_elementary_category_with_terminal_object by blast
lemma is_category_with_terminal_object:
shows "elementary_category_with_terminal_object C 𝟭⇧? some_terminator"
and "category_with_terminal_object C"
..
interpretation elementary_cartesian_closed_category
C pr⇩0 pr⇩1 ‹𝟭⇧?› some_terminator exp eval Curry
proof
show "⋀b c. ⟦ide b; ide c⟧ ⟹ «eval b c : prod (exp b c) b → c»"
using eval_in_hom by blast
show "⋀b c. ⟦ide b; ide c⟧ ⟹ ide (exp b c)"
using ide_exp by blast
show "⋀a b c g. ⟦ide a; ide b; ide c; «g : prod a b → c»⟧
⟹ «Curry a b c g : a → exp b c»"
using Curry_in_hom by simp
show "⋀a b c g. ⟦ide a; ide b; ide c; «g : prod a b → c»⟧
⟹ C (eval b c) (prod (Curry a b c g) b) = g"
proof -
fix a b c g
assume a: "ide a" and b: "ide b" and c: "ide c" and g: "«g : prod a b → c»"
show "eval b c ⋅ prod (Curry a b c g) b = g"
proof (intro arr_eqI [of _ g])
show par: "par (C (eval b c) (prod (Curry a b c g) b)) g"
using a b c g by auto
show "Fun (eval b c ⋅ prod (Curry a b c g) b) = Fun g"
proof
fix x
show "Fun (eval b c ⋅ prod (Curry a b c g) b) x = Fun g x"
proof (cases "x ∈ Set (prod a b)")
case False
show ?thesis
using False Fun_def
by (metis g in_homE par)
next
case True
have "Fun (C (eval b c) (prod (Curry a b c g) b)) x =
Fun (eval b c) (Fun (prod (Curry a b c g) b) x)"
using True a b c g Fun_comp par comp_assoc by auto
also have "... = (λfx. if fx ∈ Set (prod (exp b c) b)
then OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) fx)
(Fun (pr⇩0 (exp b c) b) fx)
else null)
((if x ∈ Set (prod a b)
then tuple
(Fun (Curry a b c g) (pr⇩1 a b ⋅ x))
(Fun b (pr⇩0 a b ⋅ x))
else null))"
proof -
have "Fun (eval b c) = (λfx. if fx ∈ Set (prod (exp b c) b)
then OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) fx)
(Fun (pr⇩0 (exp b c) b) fx)
else null)"
using b c Fun_eval by simp
moreover have "Fun (prod (Curry a b c g) b) =
(λx. if x ∈ Set (prod a b)
then tuple
(Fun (Curry a b c g) (pr⇩1 a b ⋅ x))
(Fun b (pr⇩0 a b ⋅ x))
else null)"
using a b c g Fun_prod [of "Curry a b c g" a "exp b c" b b b] Curry_in_hom
by (meson ide_in_hom)
ultimately show ?thesis by simp
qed
also have "... = OUT (Exp b c)
(Fun (pr⇩1 (exp b c) b)
(tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x))))
(Fun (pr⇩0 (exp b c) b)
(tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x))))"
proof -
have "tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x))
∈ Set (prod (exp b c) b)"
using a b c g True Fun_def by auto
thus ?thesis
using True by presburger
qed
also have "... = OUT (Exp b c)
(pr⇩1 (exp b c) b ⋅
tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x)))
(pr⇩0 (exp b c) b ⋅
tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x)))"
proof -
have "tuple
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x))
∈ Set (prod (exp b c) b)"
using a b c g True Fun_def by auto
moreover have "Set (prod (exp b c) b) = Set (dom (pr⇩1 (exp b c) b))"
using b c
by (simp add: ide_exp(1))
moreover have "Set (prod (exp b c) b) = Set (dom (pr⇩0 (exp b c) b))"
using b c
by (simp add: ide_exp(1))
ultimately show ?thesis
unfolding Fun_def
using a b c g True by auto
qed
also have "... = OUT (Exp b c)
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(Fun b (C (pr⇩0 a b) x))"
unfolding Fun_def
using True a b c g by auto
also have "... = OUT (Exp b c)
(Fun (Curry a b c g) (C (pr⇩1 a b) x))
(C (pr⇩0 a b) x)"
proof -
have "C (pr⇩0 a b) x ∈ Set b"
using True a b by blast
thus ?thesis
using b Fun_ide [of b]
by presburger
qed
also have "... = OUT (Exp b c)
((λx. if x ∈ Set a
then IN (Exp b c)
(λy. if y ∈ Set b then g ⋅ tuple x y else null)
else null)
(C (pr⇩1 a b) x))
(C (pr⇩0 a b) x)"
using a b c g Fun_Curry [of a b c g] by simp
also have "... = OUT (Exp b c)
(IN (Exp b c)
(λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null))
(pr⇩0 a b ⋅ x)"
using True a b c g by auto
also have "... = (λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null)
(pr⇩0 a b ⋅ x)"
proof -
have "(λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null) ∈ Hom b c"
proof
show "(λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null) ∈ Set b → Set c"
proof
fix y
assume y: "y ∈ Set b"
show "(if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null) ∈ Set c"
using True a b c g y by auto
qed
show "(λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null)
∈ {F. ∀x. x ∉ Set b ⟶ F x = null}"
by auto
qed
thus ?thesis
using a b c g small_Exp [of b c] embeds_Exp [of b c] ide_exp(1) [of b c]
OUT_IN
[of "Exp b c"
"λy. if y ∈ Set b then g ⋅ tuple (pr⇩1 a b ⋅ x) y else null"]
by auto
qed
also have "... = g ⋅ tuple (pr⇩1 a b ⋅ x) (pr⇩0 a b ⋅ x)"
using True a b c g by auto
also have "... = g ⋅ tuple (pr⇩1 a b) (pr⇩0 a b) ⋅ x"
using True a b c g comp_tuple_arr
by (metis CollectD in_homE pr_simps(2) span_pr)
also have "... = g ⋅ x"
using True a b tuple_pr comp_cod_arr by fastforce
also have "... = Fun g x"
using True g Fun_def by auto
finally show ?thesis by blast
qed
qed
qed
qed
show "⋀a b c h. ⟦ide a; ide b; ide c; «h : a → exp b c»⟧
⟹ Curry a b c (C (eval b c) (prod h b)) = h"
proof -
fix a b c h
assume a: "ide a" and b: "ide b" and c: "ide c" and h: "«h : a → exp b c»"
show "Curry a b c (C (eval b c) (prod h b)) = h"
proof (intro arr_eqI [of _ h])
show par: "par (Curry a b c (C (eval b c) (prod h b))) h"
using a b c h Curry_def Curry_simps(1) by auto
show "Fun (Curry a b c (C (eval b c) (prod h b))) = Fun h"
proof
fix x
show "Fun (Curry a b c (C (eval b c) (prod h b))) x = Fun h x"
proof (cases "x ∈ Set a")
case False
show ?thesis
using False a b c h
by (metis Fun_def in_homE par)
next
case True
have "OUT (Exp b c) (Fun (Curry a b c (C (eval b c) (prod h b))) x) =
OUT (Exp b c)
(IN (Exp b c)
(λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null))"
using True a b c h Fun_Curry [of a b c "C (eval b c) (prod h b)"]
eval_in_hom [of b c]
by auto
also have "... = (λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null)"
proof -
have "(λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null) ∈ Hom b c"
proof
show "(λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null)
∈ Set b → Set c"
proof
fix y
assume y: "y ∈ Set b"
show "(if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null) ∈ Set c"
using True a b c h y ide_in_hom by auto
qed
show "(λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null)
∈ {F. ∀x. x ∉ Set b ⟶ F x = null}"
by simp
qed
thus ?thesis
using True a b c h small_Exp [of b c] embeds_Exp ide_exp [of b c]
OUT_IN
[of "Exp b c"
"λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null"]
by auto
qed
also have "... = OUT (Exp b c) (Fun h x)"
proof
fix y
show "... y = OUT (Exp b c) (Fun h x) y"
proof (cases "y ∈ Set b")
assume y: "y ∉ Set b"
have "«Fun h x : 𝟭⇧? → mkide (Exp b c)»"
using True b c h
by (metis Fun_arr[of h a "cod h"] arr_iff_in_hom[of "h ⋅ x"]
dom_comp[of h x] cod_comp[of h x] exp_def[of b c]
in_homE[of h a "exp b c"] in_homE[of x "𝟭⇧?" a]
mem_Collect_eq[of x "λuub. «uub : 𝟭⇧? → a»"] seqI[of x h])
thus ?thesis
using True b c h y OUT_elem_of [of "Exp b c" "Fun h x"] small_Exp [of b c]
embeds_Exp [of b c] ide_exp [of b c]
by auto
next
assume y: "y ∈ Set b"
have "(λy. if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null) y =
(eval b c ⋅ prod h b) ⋅ tuple x y"
using y by simp
also have "... = eval b c ⋅ (prod h b ⋅ tuple x y)"
using comp_assoc by simp
also have "... = eval b c ⋅ tuple (h ⋅ x) (b ⋅ y)"
using True b c h y prod_tuple
by (metis comp_cod_arr in_homE mem_Collect_eq seqI)
also have "... = eval b c ⋅ tuple (h ⋅ x) y"
using b y
by (metis comp_cod_arr in_homE mem_Collect_eq)
also have "... = Fun (eval b c) (tuple (h ⋅ x) y)"
using True b c h y Fun_def [of "eval b c" "tuple (h ⋅ x) y"] by auto
also have "... = (λfx. if fx ∈ Set (prod (exp b c) b)
then OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) fx)
(Fun (pr⇩0 (exp b c) b) fx)
else null)
(tuple (h ⋅ x) y)"
using b c Fun_eval [of b c] by presburger
also have "... = OUT (Exp b c) (Fun (pr⇩1 (exp b c) b) (tuple (h ⋅ x) y))
(Fun (pr⇩0 (exp b c) b) (tuple (h ⋅ x) y))"
using True b c h y
by (simp add: comp_in_homI tuple_in_hom)
also have "... = OUT (Exp b c) (pr⇩1 (exp b c) b ⋅ tuple (h ⋅ x) y)
(pr⇩0 (exp b c) b ⋅ tuple (h ⋅ x) y)"
using True b c h y Fun_def ide_exp(1) span_pr by auto
also have "... = OUT (Exp b c) (h ⋅ x) y"
using True b c h y
apply auto
by fastforce
also have "... = OUT (Exp b c) (Fun h x) y"
using True h Fun_def by auto
finally show "(if y ∈ Set b then (eval b c ⋅ prod h b) ⋅ tuple x y else null) =
OUT (Exp b c) (Fun h x) y"
by blast
qed
qed
finally have *: "OUT (Exp b c) (Fun (Curry a b c (C (eval b c) (prod h b))) x) =
OUT (Exp b c) (Fun h x)"
by simp
show "Fun (Curry a b c (C (eval b c) (prod h b))) x = Fun h x"
proof -
have "Fun (Curry a b c (C (eval b c) (prod h b))) x =
IN (Exp b c) (OUT (Exp b c) (Fun (Curry a b c (C (eval b c) (prod h b))) x))"
proof -
have "Fun (Curry a b c (eval b c ⋅ prod h b)) x ∈ Set (mkide (Exp b c))"
proof -
have "«Curry a b c (eval b c ⋅ prod h b) : a → exp b c»"
using a b c h par
Curry_in_hom [of a b c "C (eval b c) (prod h b)"]
by (metis arr_iff_in_hom in_homE)
hence "Fun (Curry a b c (eval b c ⋅ prod h b)) ∈ Set a → Set (exp b c)"
using Fun_in_Hom [of "Curry a b c (eval b c ⋅ prod h b)" a "exp b c"]
by blast
thus ?thesis
using True exp_def by auto
qed
thus ?thesis
using True a b c h small_Exp embeds_Exp
IN_OUT [of "Exp b c" "Fun (Curry a b c (C (eval b c) (prod h b))) x"]
by presburger
qed
also have "... = IN (Exp b c) (OUT (Exp b c) (Fun h x))"
using * by simp
also have "... = Fun h x"
proof -
have "Fun h x ∈ Set (mkide (Exp b c))"
using True b c h Fun_def exp_def by auto
thus ?thesis
using True b c h small_Exp embeds_Exp
IN_OUT [of "Exp b c" "Fun h x"]
by presburger
qed
finally show ?thesis by blast
qed
qed
qed
qed
qed
qed
lemma is_elementary_cartesian_closed_category:
shows "elementary_cartesian_closed_category C pr⇩0 pr⇩1 𝟭⇧? some_terminator exp eval Curry"
..
lemma is_cartesian_closed_category:
shows "cartesian_closed_category C"
..
end
subsection "Exported Notions"
context sets_cat_with_tupling
begin
sublocale sets_cat_with_pairing ..
interpretation Expos: exponentials_in_sets_cat sml C ..
abbreviation Exp
where "Exp ≡ Expos.Exp"
abbreviation exp
where "exp ≡ Expos.exp"
lemma ide_exp:
assumes "ide a" and "ide b"
shows "ide (exp a b)"
using assms Expos.ide_exp by blast
lemma exp_comparison_map_props:
assumes "ide a" and "ide b"
shows "OUT (Exp a b) ∈ Set (exp a b) → Exp a b"
and "IN (Exp a b) ∈ Exp a b → Set (exp a b)"
and "⋀x. x ∈ Set (exp a b) ⟹ IN (Exp a b) (OUT (Exp a b) x) = x"
and "⋀y. y ∈ Exp a b ⟹ OUT (Exp a b) (IN (Exp a b) y) = y"
and "bij_betw (OUT (Exp a b)) (Set (exp a b)) (Exp a b)"
and "bij_betw (IN (Exp a b)) (Exp a b) (Set (exp a b))"
proof -
show "OUT (Exp a b) ∈ Set (exp a b) → Exp a b"
using assms Expos.ide_exp(2) [of a b] bij_betw_def bij_betw_imp_funcset
by simp
thus "IN (Exp a b) ∈ Exp a b → Set (exp a b)"
using assms Expos.exp_def
by (metis (no_types, lifting) HOL.ext Expos.ide_exp(2) bij_betw_imp_funcset bij_betw_inv_into)
show "⋀x. x ∈ Set (exp a b) ⟹ IN (Exp a b) (OUT (Exp a b) x) = x"
using assms
by (metis (no_types, lifting) HOL.ext Expos.exp_def Expos.ide_exp(2) bij_betw_inv_into_left)
show "⋀y. y ∈ Exp a b ⟹ OUT (Exp a b) (IN (Exp a b) y) = y"
using assms
by (metis (no_types, lifting) HOL.ext Expos.exp_def Expos.ide_exp(2) bij_betw_inv_into_right)
show "bij_betw (OUT (Exp a b)) (Set (exp a b)) (Exp a b)"
using assms Expos.exponentials_in_sets_cat_axioms exponentials_in_sets_cat.ide_exp(2)
by fastforce
show "bij_betw (IN (Exp a b)) (Exp a b) (Set (exp a b))"
using assms Expos.exponentials_in_sets_cat_axioms exponentials_in_sets_cat.ide_exp(3)
by fastforce
qed
abbreviation Eval
where "Eval ≡ Expos.Eval"
abbreviation eval
where "eval ≡ Expos.eval"
lemma eval_in_hom [intro, simp]:
assumes "ide b" and "ide c"
shows "«eval b c : prod (exp b c) b → c»"
using assms Expos.eval_in_hom by blast
lemma eval_simps [simp]:
assumes "ide b" and "ide c"
shows "arr (eval b c)" and "dom (eval b c) = prod (exp b c) b" and "cod (eval b c) = c"
using assms Expos.eval_simps by auto
lemma Fun_eval:
assumes "ide b" and "ide c"
shows "Fun (eval b c) = Eval b c"
unfolding eval_def
using assms Expos.Fun_eval [of b c] by simp
abbreviation Curry
where "Curry ≡ Expos.Curry"
lemma Curry_in_hom [intro, simp]:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "«Curry a b c f : a → exp b c»"
using assms Expos.Curry_in_hom by auto
lemma Curry_simps [simp]:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "arr (Curry a b c f)"
and "dom (Curry a b c f) = a" and "cod (Curry a b c f) = exp b c"
using assms Expos.Curry_simps by auto
lemma Fun_Curry:
assumes "ide a" and "ide b" and "ide c"
and "«f : prod a b → c»"
shows "Fun (Curry a b c f) =
(λx. if x ∈ Set a
then IN (Exp b c) (λy. if y ∈ Set b then C f (tuple x y) else null)
else null)"
using assms Expos.Fun_Curry by blast
theorem is_cartesian_closed:
shows "elementary_cartesian_closed_category C pr⇩0 pr⇩1 𝟭⇧? some_terminator exp eval Curry"
and "cartesian_closed_category C"
using Expos.is_elementary_cartesian_closed_category Expos.is_cartesian_closed_category
by auto
end
section "Subobject Classifier"
text‹
In this section we show that a sets category has a subobject classifier,
which is a categorical formulation of set comprehension. We give here a formal
definition of subobject classifier, because we have not done that elsewhere
to date, but ultimately this definition would perhaps be better placed with
a development of the theory of elementary topoi, which are cartesian closed
categories with subobject classifier.
›
context category
begin
text‹
A subobject classifier is a monomorphism ‹tt› from a terminal object into
an object ‹Ω›, which we may regard as an ``object of truth values'',
such that for every monomorphism ‹m› there exists a unique arrow ‹χ : cod m → Ω›,
such that ‹m› is given by the pullback of ‹tt› along ‹χ›.
›
definition subobject_classifier
where "subobject_classifier tt ≡
mono tt ∧ terminal (dom tt) ∧
(∀m. mono m ⟶
(∃!χ. «χ : cod m → cod tt» ∧
has_as_pullback tt χ (THE f. «f : dom m → dom tt») m))"
lemma subobject_classifierI [intro]:
assumes "«tt : one → Ω»" and "terminal one" and "mono tt"
and "⋀m. mono m ⟹ ∃!χ. «χ : cod m → Ω» ∧
has_as_pullback tt χ (THE f. «f : dom m → one») m"
shows "subobject_classifier tt"
using assms subobject_classifier_def by blast
lemma subobject_classifierE [elim]:
assumes "subobject_classifier tt"
and "⟦mono tt; terminal (dom tt);
⋀m. mono m ⟹ ∃!χ. «χ : cod m → cod tt» ∧
has_as_pullback tt χ (THE f. «f : dom m → dom tt») m⟧
⟹ T"
shows T
using assms subobject_classifier_def by force
end
locale category_with_subobject_classifier =
category +
assumes has_subobject_classifier_ax: "∃tt. subobject_classifier tt"
begin
sublocale category_with_terminal_object
using category_axioms category_with_terminal_object.intro
category_with_terminal_object_axioms_def has_subobject_classifier_ax
by force
end
context sets_cat_with_bool
begin
text‹
For a sets category, the two-point object ‹❙𝟮› (which exists in the current context
@{locale sets_cat_with_bool}) serves as the object of truth values.
The subobject classifier will be the arrow ‹tt : 𝟭⇧? → ❙𝟮›.
Here we define a mapping ‹χ› that takes a monomorphism ‹m› to a corresponding
``predicate'' ‹χ m : cod m → ❙𝟮›.
›
abbreviation Chi
where "Chi m ≡ λy. if y ∈ Set (cod m)
then
if y ∈ Fun m ` Set (dom m) then tt else ff
else null"
definition χ :: "'U ⇒ 'U"
where "χ m ≡ mkarr (cod m) ❙𝟮 (Chi m)"
lemma χ_in_hom [intro, simp]:
assumes "«m : b → a»" and "mono m"
shows "«χ m : a → ❙𝟮»"
using assms ide_two ff_in_hom tt_in_hom χ_def mkarr_in_hom by auto
lemma χ_simps [simp]:
assumes "«m : b → a»" and "mono m"
shows "arr (χ m)" and "dom (χ m) = a" and "cod (χ m) = ❙𝟮"
using assms χ_in_hom by blast+
lemma Fun_χ:
assumes "«m : b → a»" and "mono m"
shows "Fun (χ m) = Chi m"
unfolding χ_def
using assms Fun_mkarr
by (metis (no_types, lifting) χ_def χ_in_hom arrI)
lemma bij_Fun_mono:
assumes "«m : b → a»" and "mono m"
shows "bij_betw (Fun m) (Set b) {y. y ∈ Set a ∧ χ m ⋅ y = tt}"
proof -
have "{y. y ∈ Set a ∧ χ m ⋅ y = tt} = {y. y ∈ Set a ∧ Chi m y = tt}"
proof -
have "⋀y. y ∈ Set a ⟹ χ m ⋅ y = tt ⟷ Chi m y = tt"
by (metis Fun_χ Fun_arr χ_in_hom assms(1,2))
thus ?thesis by blast
qed
moreover have "bij_betw (Fun m) (Set b) {y. y ∈ Set a ∧ Chi m y = tt}"
unfolding bij_betw_def
using assms mono_char tt_def ff_def tt_ne_ff Fun_def by auto
ultimately show ?thesis by simp
qed
lemma has_subobject_classifier:
shows "subobject_classifier tt"
proof
show "«tt : 𝟭⇧? → ❙𝟮»"
using tt_in_hom by blast
show "terminal 𝟭⇧?"
using terminal_some_terminal by blast
show "mono tt"
using mono_tt by blast
fix m
assume m: "mono m"
define b where b_def: "b = dom m"
define a where a_def: "a = cod m"
have m: "«m : b → a» ∧ mono m"
using m a_def b_def mono_implies_arr by blast
have bij_Fun_m: "bij_betw (Fun m) (Set b) {y ∈ Set a. χ m ⋅ y = tt}"
using m bij_Fun_mono by presburger
have "∃!χ. «χ : a → ❙𝟮» ∧ has_as_pullback tt χ 𝗍⇧?[b] m"
proof -
have 1: "«χ m : a → ❙𝟮»"
using m χ_in_hom by blast
moreover have 2: "has_as_pullback tt (χ m) 𝗍⇧?[b] m"
proof
show cs: "commutative_square tt (χ m) 𝗍⇧?[b] m"
proof
show "cospan tt (χ m)"
by (metis (lifting) χ_in_hom arr_iff_in_hom m in_homE mono_char tt_simps(1,3))
show span: "span 𝗍⇧?[b] m"
using m by auto
show "dom tt = cod 𝗍⇧?[b]"
using m by auto
show "tt ⋅ 𝗍⇧?[b] = χ m ⋅ m"
proof (intro arr_eqI)
show par: "par (tt ⋅ 𝗍⇧?[b]) (χ m ⋅ m)"
using m ‹span 𝗍⇧?[b] m› a_def b_def by auto
show "Fun (tt ⋅ 𝗍⇧?[b]) = Fun (χ m ⋅ m)"
proof
fix x
show "Fun (tt ⋅ 𝗍⇧?[b]) x = Fun (χ m ⋅ m) x"
proof (cases "x ∈ Set b")
case False
show ?thesis
using False par m Fun_def by auto
next
case True
have "Fun (tt ⋅ 𝗍⇧?[b]) x = Fun tt (Fun 𝗍⇧?[b] x)"
using Fun_comp par by auto
also have "... = (λx. if x ∈ Set 𝟭⇧? then tt else null)
(if x ∈ Set b then 𝟭⇧? else null)"
using Fun_some_terminator Fun_tt span b_def ide_dom by auto
also have "... = tt"
using True ide_in_hom ide_some_terminal by auto
also have "... = (λx. if x ∈ Set a then tt else null) (Fun m x)"
using m True Fun_def
by (metis CollectD CollectI in_homE comp_in_homI)
also have "... = Chi m (Fun m x)"
using app_mkarr m Fun_def by auto
also have "... = Fun (χ m) (Fun m x)"
using m Fun_χ [of m b a] by simp
also have "... = Fun (χ m ⋅ m) x"
by (metis comp_eq_dest_lhs par Fun_comp)
finally show ?thesis by blast
qed
qed
qed
qed
show "⋀h k. commutative_square tt (χ m) h k ⟹ ∃!l. 𝗍⇧?[b] ⋅ l = h ∧ m ⋅ l = k"
proof -
fix h k
assume hk: "commutative_square tt (χ m) h k"
have inj_m: "inj_on (Fun m) (Set b)"
using m mono_char by blast
have kx: "⋀x. x ∈ Set (dom h) ⟹ k ⋅ x ∈ {y ∈ Set a. χ m ⋅ y = tt}"
proof -
fix x
assume x: "x ∈ Set (dom h)"
have "χ m ⋅ k ⋅ x = tt ⋅ h ⋅ x"
using hk comp_assoc
by (metis (no_types, lifting) commutative_squareE)
hence "χ m ⋅ k ⋅ x = tt"
by (metis (lifting) IntI Int_Collect comp_arr_dom comp_in_homI' in_homE
commutative_squareE hk ide_some_terminal ide_in_hom some_trm_eqI
tt_simps(2) x)
thus "k ⋅ x ∈ {y ∈ Set a. χ m ⋅ y = tt}"
using hk comp_assoc
by (metis (mono_tags, lifting) "1" dom_comp in_homE in_homI mem_Collect_eq
seqE tt_simps(1,2))
qed
let ?l = "mkarr (dom h) b
(λx. if x ∈ Set (dom h) then inv_into (Set b) (Fun m) (k ⋅ x) else null)"
have l: "«?l : dom h → b»"
proof (intro mkarr_in_hom)
show "ide (dom h)"
using hk ide_dom by blast
show "ide b"
using m by auto
show "(λx. if x ∈ Set (dom h) then inv_into (Set b) (Fun m) (k ⋅ x) else null)
∈ Hom (dom h) b"
proof
show "(λx. if x ∈ Set (dom h) then inv_into (Set b) (Fun m) (k ⋅ x) else null)
∈ Set (dom h) → Set b"
proof
fix x
assume x: "x ∈ Set (dom h)"
have "inv_into (Set b) (Fun m) (k ⋅ x) ∈ Set b ∧
Fun m (inv_into (Set b) (Fun m) (k ⋅ x)) = k ⋅ x"
using x bij_Fun_m kx
by (meson bij_betw_apply bij_betw_inv_into bij_betw_inv_into_right)
thus "(if x ∈ Set (dom h) then inv_into (Set b) (Fun m) (k ⋅ x) else null)
∈ Set b"
using x by presburger
qed
show "(λx. if x ∈ Set (dom h) then inv_into (Set b) (Fun m) (k ⋅ x) else null)
∈ {F. ∀x. x ∉ Set (dom h) ⟶ F x = null}"
by auto
qed
qed
have "𝗍⇧?[b] ⋅ ?l = h"
by (metis (lifting) commutative_square_def comp_cod_arr
elementary_category_with_terminal_object.trm_naturality
elementary_category_with_terminal_object.trm_one
extends_to_elementary_category_with_terminal_object hk in_homE l
tt_simps(2))
moreover have "m ⋅ ?l = k"
proof (intro arr_eqI)
show par: "par (m ⋅ ?l) k"
by (metis (no_types, lifting) HOL.ext χ_simps(2) m cod_comp dom_comp seqI'
commutative_squareE hk in_homE l)
show "Fun (m ⋅ ?l) = Fun k"
proof
fix x
show "Fun (m ⋅ ?l) x = Fun k x"
proof (cases "x ∈ Set (dom h)")
case False
show ?thesis
using False par commutative_square_def Fun_def by auto
next
case True
have "Fun (m ⋅ ?l) x = Fun m (Fun ?l x)"
using True Fun_comp CollectI m comp_in_homI in_homE l comp_assoc par
by fastforce
also have "... = Fun m (inv_into (Set b) (Fun m) (k ⋅ x))"
using True m app_mkarr l by auto
also have "... = k ⋅ x"
using True bij_Fun_m bij_betw_inv_into_right kx by force
also have "... = Fun k x"
using True hk Fun_def by fastforce
finally show ?thesis by blast
qed
qed
qed
ultimately have 1: "𝗍⇧?[b] ⋅ ?l = h ∧ m ⋅ ?l = k" by blast
moreover have "⋀l'. 𝗍⇧?[b] ⋅ l' = h ∧ m ⋅ l' = k ⟹ l' = ?l"
using m l
by (metis (lifting) ‹m ⋅ ?l = k› seqI' mono_cancel)
ultimately show "∃!l. 𝗍⇧?[b] ⋅ l = h ∧ m ⋅ l = k" by auto
qed
qed
moreover have "⋀χ'. «χ' : a → ❙𝟮» ∧ has_as_pullback tt χ' 𝗍⇧?[b] m ⟹ χ' = χ m"
proof -
fix χ'
assume χ': "«χ' : a → ❙𝟮» ∧ has_as_pullback tt χ' 𝗍⇧?[b] m"
show "χ' = χ m"
proof (intro arr_eqI' [of χ'])
show "«χ' : a → ❙𝟮»"
using χ' by simp
show "«χ m : a → ❙𝟮»"
using "1" by force
show "⋀y. «y : 𝟭⇧? → a» ⟹ χ' ⋅ y = χ m ⋅ y"
proof -
fix y
assume y: "«y : 𝟭⇧? → a»"
show "χ' ⋅ y = χ m ⋅ y"
proof (cases "y ∈ Set a")
case False
show ?thesis
using False y by blast
next
case True
show ?thesis
proof (cases "y ∈ Fun m ` Set b")
case True
obtain x where x: "x ∈ Set b ∧ y = Fun m x"
using True by blast
have "χ' ⋅ y = χ' ⋅ m ⋅ x"
using x y Fun_def by auto
also have "... = tt ⋅ 𝟭⇧?"
using χ' x Fun_def
by (metis (no_types, lifting) HOL.ext Fun_some_terminator m
commutative_square_def has_as_pullbackE ide_dom in_homE comp_assoc)
also have "... = χ m ⋅ m ⋅ x"
using 1 2 x χ_def app_mkarr m comp_arr_dom y Fun_def by auto
also have "... = χ m ⋅ y"
using x y Fun_def by auto
finally show ?thesis by blast
next
case False
have "χ' ⋅ y = ff"
proof -
have "χ' ⋅ y = tt ⟹ False"
proof -
assume 3: "χ' ⋅ y = tt"
hence "commutative_square tt χ' 𝟭⇧? y"
by (metis ‹«χ' : a → ❙𝟮»› commutative_squareI comp_arr_dom ideD(1,2,3)
ide_some_terminal in_homE tt_simps(1,2,3) y)
hence "∃x. x ∈ Set b ∧ m ⋅ x = y ∧ 𝗍⇧?[b] ⋅ x = 𝟭⇧?"
using χ' has_as_pullbackE [of tt χ' "𝗍⇧?[b]" m]
by (metis arr_iff_in_hom m dom_comp in_homE mem_Collect_eq seqE y)
thus False
using False χ' m Fun_def by auto
qed
thus ?thesis
using Set_two χ' y by blast
qed
also have "... = χ m ⋅ y"
using "1" False app_mkarr m y χ_def by auto
finally show ?thesis by blast
qed
qed
qed
qed
qed
ultimately show "∃!χ. «χ : a → ❙𝟮» ∧ has_as_pullback tt χ 𝗍⇧?[b] m"
by blast
qed
moreover have "𝗍⇧?[b] = (THE t. «t : dom m → 𝟭⇧?»)"
using terminal_some_terminal the1_equality [of "λt. «t : dom m → 𝟭⇧?»"]
by (simp add: b_def m mono_implies_arr some_terminator_def)
ultimately show "∃!χ. «χ : cod m → ❙𝟮» ∧
has_as_pullback tt χ (THE t. «t : dom m → 𝟭⇧?») m"
using m by auto
qed
sublocale category_with_subobject_classifier
using has_subobject_classifier
by unfold_locales auto
lemma is_category_with_subobject_classifier:
shows "category_with_subobject_classifier C"
..
end
section "Natural Numbers Object"
text‹
In this section we show that a sets category has a natural numbers object,
assuming that the smallness notion is such that the set of natural numbers is small,
and assuming that that the collection of arrows admits lifting, so that the category
has infinitely many arrows.
›
locale sets_cat_with_infinity =
sets_cat sml C +
small_nat sml +
lifting ‹Collect arr›
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
abbreviation nat ("❙N")
where "nat ≡ mkide (UNIV :: nat set)"
lemma ide_nat:
shows "ide ❙N"
and "bij_betw (OUT (UNIV :: nat set)) (Set ❙N) (UNIV :: nat set)"
and "bij_betw (IN (UNIV :: nat set)) (UNIV :: nat set) (Set ❙N)"
using small_nat embeds_nat bij_OUT bij_IN by auto
abbreviation Zero
where "Zero ≡ λx. if x ∈ Set 𝟭⇧? then IN (UNIV :: nat set) 0 else null"
lemma Zero_in_Hom:
shows "Zero ∈ Hom 𝟭⇧? ❙N"
using Pi_I' bij_betwE ide_nat(3) by fastforce
definition zero
where "zero ≡ mkarr 𝟭⇧? ❙N Zero"
lemma zero_in_hom [intro, simp]:
shows "«zero : 𝟭⇧? → ❙N»"
using mkarr_in_hom [of "𝟭⇧?" "❙N"] Zero_in_Hom ide_nat(1) ide_some_terminal zero_def
by presburger
lemma zero_simps [simp]:
shows "arr zero" and "dom zero = 𝟭⇧?" and "cod zero = ❙N"
using zero_in_hom by blast+
lemma Fun_zero:
shows "Fun zero = Zero"
using zero_def app_mkarr zero_in_hom zero_simps(2) by auto
abbreviation Succ
where "Succ ≡ λx. if x ∈ Set ❙N then IN (UNIV :: nat set) (Suc (OUT UNIV x)) else null"
lemma Succ_in_Hom:
shows "Succ ∈ Hom ❙N ❙N"
using Pi_I' bij_betwE ide_nat(3) by fastforce
definition succ
where "succ ≡ mkarr ❙N ❙N Succ"
lemma succ_in_hom [intro]:
shows "«succ : ❙N → ❙N»"
using Succ_in_Hom ide_nat(1) succ_def by auto
lemma succ_simps [simp]:
shows "arr succ" and "dom succ = ❙N" and "cod succ = ❙N"
using succ_in_hom by blast+
lemma Fun_succ:
shows "Fun succ = Succ"
using succ_def app_mkarr succ_in_hom succ_simps(2) by auto
lemma nat_universality:
assumes "«Z : 𝟭⇧? → a»" and "«S : a → a»"
shows "∃!f. «f : ❙N → a» ∧ f ⋅ zero = Z ∧ f ⋅ succ = S ⋅ f"
proof -
let ?F = "λn. if n ∈ Set ❙N then ((⋅) S ^^ OUT (UNIV :: nat set) n) Z else null"
have F: "?F ∈ Hom ❙N a"
proof
show "?F ∈ {F. ∀x. x ∉ Set (mkide (UNIV :: nat set)) ⟶ F x = null}" by simp
show "?F ∈ Set ❙N → Set a"
proof
have 1: "⋀k. ((⋅) S ^^ k) Z ∈ Set a"
proof -
fix k
show "((⋅) S ^^ k) Z ∈ Set a"
using assms by (induct k) auto
qed
fix n
assume n: "n ∈ Set ❙N"
show "?F n ∈ Set a"
using n 1 by auto
qed
qed
let ?f = "mkarr ❙N a ?F"
have f: "«?f : ❙N → a»"
using mkarr_in_hom F assms(2) ide_nat(1) by auto
have "«?f : ❙N → a» ∧ ?f ⋅ zero = Z ∧ ?f ⋅ succ = S ⋅ ?f"
proof (intro conjI)
show "«?f : ❙N → a»" by fact
show "?f ⋅ zero = Z"
proof (intro arr_eqI)
show par: "par (?f ⋅ zero) Z"
using assms(1) f by fastforce
show "Fun (?f ⋅ zero) = Fun Z"
proof -
have "Fun (?f ⋅ zero) = Fun ?f ∘ Fun zero"
using Fun_comp par by blast
also have "... = ?F ∘ Zero"
using Fun_mkarr Fun_zero par by fastforce
also have "... = Fun Z"
proof
fix x
show "(?F ∘ Zero) x = Fun Z x"
proof (cases "x ∈ Set 𝟭⇧?")
case False
show ?thesis
using False par Fun_def by auto
next
case True
have "(?F ∘ Zero) x =
((⋅) S ^^ OUT (UNIV :: nat set) (IN (UNIV :: nat set) 0)) Z"
using True bij_betw_imp_surj_on ide_nat(3) by fastforce
also have "... = ((⋅) S ^^ 0) Z"
using OUT_IN [of "UNIV :: nat set" "0 :: nat"] small_nat embeds_nat
by simp
also have "... = Fun Z x"
using True Fun_def
by (metis assms(1) comp_arr_dom funpow_0 ide_in_hom ide_some_terminal
in_homE mem_Collect_eq some_trm_eqI)
finally show ?thesis by blast
qed
qed
finally show ?thesis by blast
qed
qed
show "?f ⋅ succ = S ⋅ ?f"
proof (intro arr_eqI)
show par: "par (?f ⋅ succ) (S ⋅ ?f)"
using assms(2) f by fastforce
show "Fun (?f ⋅ succ) = Fun (S ⋅ ?f)"
proof -
have "Fun (?f ⋅ succ) = Fun ?f ∘ Fun succ"
using Fun_comp par by blast
also have "... = Fun S ∘ Fun ?f"
proof
fix x
show "(Fun ?f ∘ Fun succ) x = (Fun S ∘ Fun ?f) x"
proof (cases "x ∈ Set ❙N")
case False
show ?thesis
using False f Fun_def by auto
next
case True
have "(Fun ?f ∘ Fun succ) x = ?F (succ ⋅ x)"
using True f app_mkarr [of "❙N" a _ "succ ⋅ x"] Fun_def by auto
also have "... = ((⋅) S ^^ OUT UNIV (succ ⋅ x)) Z"
using True f by auto
also have "... = ((⋅) S ^^ Suc (OUT UNIV x)) Z"
by (metis (no_types, lifting) Fun_def Fun_succ True UNIV_I bij_betw_def
bij_betw_inv_into_left ide_nat(2,3) mem_Collect_eq rangeI succ_simps(2))
also have "... = S ⋅ ((⋅) S ^^ OUT UNIV x) Z"
by auto
also have "... = S ⋅ ?F x"
using True by auto
also have "... = S ⋅ Fun ?f x"
using f by auto
also have "... = Fun S (Fun ?f x)"
by (metis (no_types, lifting) CollectD CollectI Fun_def dom_comp in_homE
in_homI ext null_is_zero(2) seqE)
also have "... = (Fun S ∘ Fun ?f) x"
by simp
finally show ?thesis by blast
qed
qed
also have "... = Fun (S ⋅ ?f)"
using Fun_comp par by presburger
finally show ?thesis by blast
qed
qed
qed
moreover have "⋀f'. «f' : ❙N → a» ∧ f' ⋅ zero = Z ∧ f' ⋅ succ = S ⋅ f' ⟶ f' = ?f"
proof (intro impI arr_eqI)
fix f'
assume f': "«f' : ❙N → a» ∧ f' ⋅ zero = Z ∧ f' ⋅ succ = S ⋅ f'"
show par: "par f' ?f"
using f f' by fastforce
have *: "⋀k. ((⋅) S ^^ k) Z = Fun f' (IN UNIV k)"
proof -
fix k
show "((⋅) S ^^ k) Z = Fun f' (IN UNIV k)"
proof (induct k)
show "((⋅) S ^^ 0) Z = Fun f' (IN (UNIV :: nat set) 0)"
using f' app_mkarr
unfolding zero_def
by (metis (no_types, lifting) CollectI Fun_zero comp_arr_dom f' funpow_0
ide_in_hom ide_some_terminal in_homE zero_in_hom Fun_def)
fix k
assume ind: "((⋅) S ^^ k) Z = Fun f' (IN UNIV k)"
have "Fun f' (IN UNIV (Suc k)) = Fun f' (succ ⋅ IN UNIV k)"
proof -
have "⋀n. OUT UNIV (IN UNIV (n::nat)) = n"
by (metis (no_types) bij_betw_inv_into_right ide_nat(2) iso_tuple_UNIV_I)
thus ?thesis
by (metis (no_types) Fun_def Fun_succ bij_betwE ide_nat(3) iso_tuple_UNIV_I
succ_simps(2))
qed
also have "... = f' ⋅ succ ⋅ IN UNIV k"
using bij_betwE f' ide_nat(3) Fun_def by fastforce
also have "... = (f' ⋅ succ) ⋅ IN UNIV k"
using comp_assoc by simp
also have "... = S ⋅ Fun f' (IN UNIV k)"
using f' bij_betw_apply ide_nat(3) comp_assoc Fun_def by fastforce
also have "... = S ⋅ ((⋅) S ^^ k) Z"
using ind by simp
also have "... = ((⋅) S ^^ Suc k) Z"
by auto
finally show "((⋅) S ^^ Suc k) Z = Fun f' (IN UNIV (Suc k))"
by simp
qed
qed
show "Fun f' = Fun ?f"
proof
fix x
show "Fun f' x = Fun ?f x"
proof (cases "x ∈ Set ❙N")
case False
show ?thesis
using False par Fun_def by auto
next
case True
have "Fun ?f x = ((⋅) S ^^ OUT UNIV x) Z"
using True app_mkarr f par by force
also have "... = Fun f' (IN (UNIV :: nat set) (OUT UNIV x))"
using * by simp
also have "... = Fun f' x"
using True IN_OUT small_nat embeds_nat by metis
finally show ?thesis by simp
qed
qed
qed
ultimately show ?thesis by auto
qed
lemma has_natural_numbers_object:
shows "∃a z s. «z : 𝟭⇧? → a» ∧ «s : a → a» ∧
(∀a' z' s'. «z' : 𝟭⇧? → a'» ∧ «s' : a' → a'» ⟶
(∃!f. «f : a → a'» ∧ f ⋅ z = z' ∧ f ⋅ s = s' ⋅ f))"
proof -
have "«zero : 𝟭⇧? → nat» ∧ «succ : nat → nat» ∧
(∀a' z' s'. «z' : 𝟭⇧? → a'» ∧ «s' : a' → a'» ⟶
(∃!f. «f : nat → a'» ∧ f ⋅ zero = z' ∧ f ⋅ succ = s' ⋅ f))"
using nat_universality by auto
thus ?thesis by auto
qed
end
section "Sets Category with Tupling and Infinity"
text‹
Finally, if the collection of arrows of a sets category admits embeddings of all the
usual set-theoretic constructions, then the category supports all of the constructions
considered; in particular it is small-complete and small-cocomplete, is cartesian closed,
has a subobject classifier (so that it is an elementary topos), and validates an
axiom of infinity in the form of the existence of a natural numbers object.
›
context sets_cat_with_tupling
begin
lemmas is_well_pointed epis_split has_binary_products has_binary_coproducts
has_small_products has_small_coproducts has_equalizers has_coequalizers
is_cartesian_closed has_subobject_classifier
end
locale sets_cat_with_tupling_and_infinity =
sets_cat_with_tupling sml C +
sets_cat_with_infinity sml C
for sml :: "'V set ⇒ bool"
and C :: "'U comp" (infixr ‹⋅› 55)
begin
sublocale universe sml ‹Collect arr› null ..
lemmas has_natural_numbers_object
end
end