Theory SetCategory
chapter SetCategory
theory SetCategory
imports Category Functor Subcategory
begin
text‹
This theory defines a locale ‹set_category› that axiomatizes the notion
``category of @{typ 'a}-sets and functions between them'' in the context of HOL.
A primary reason for doing this is to make it possible to prove results
(such as the Yoneda Lemma) that use such categories without having to commit to a
particular element type @{typ 'a} and without having the results depend on the
concrete details of a particular construction.
The axiomatization given here is categorical, in the sense that if categories
@{term S} and @{term S'} each interpret the ‹set_category› locale,
then a bijection between the sets of terminal objects of @{term S} and @{term S'}
extends to an isomorphism of @{term S} and @{term S'} as categories.
The axiomatization is based on the following idea: if, for some type @{typ 'a},
category @{term S} is the category of all @{typ 'a}-sets and functions between
them, then the elements of type @{typ 'a} are in bijective correspondence with
the terminal objects of category @{term S}. In addition, if @{term unity}
is an arbitrarily chosen terminal object of @{term S}, then for each object @{term a},
the hom-set @{term "hom unity a"} (\emph{i.e.} the set of ``points'' or
``global elements'' of @{term a}) is in bijective correspondence with a subset
of the terminal objects of @{term S}. By making a specific, but arbitrary,
choice of such a correspondence, we can then associate with each object @{term a}
of @{term S} a set @{term "set a"} that consists of all terminal objects @{term t}
that correspond to some point @{term x} of @{term a}. Each arrow @{term f}
then induces a function ‹Fun f ∈ set (dom f) → set (cod f)›,
defined on terminal objects of @{term S} by passing to points of @{term "dom f"},
composing with @{term f}, then passing back from points of @{term "cod f"}
to terminal objects. Once we can associate a set with each object of @{term S}
and a function with each arrow, we can force @{term S} to be isomorphic to the
category of @{typ 'a}-sets by imposing suitable extensionality and completeness axioms.
›
section "Some Lemmas about Restriction"
text‹
\sloppypar
The development of the ‹set_category› locale makes heavy use of the
theory @{theory "HOL-Library.FuncSet"}. However, in some cases, I found that
that theory did not provide results about restriction in the form that was
most useful to me. I used the following additional results in various places.
›
lemma restr_eqI:
assumes "A = A'" and "⋀x. x ∈ A ⟹ F x = F' x"
shows "restrict F A = restrict F' A'"
using assms by force
lemma restr_eqE [elim]:
assumes "restrict F A = restrict F' A" and "x ∈ A"
shows "F x = F' x"
using assms restrict_def by metis
lemma compose_eq' [simp]:
shows "compose A G F = restrict (G o F) A"
unfolding compose_def restrict_def by auto
section "Set Categories"
text‹
We first define the locale ‹set_category_data›, which sets out the basic
data and definitions for the ‹set_category› locale, without imposing any conditions
other than that @{term S} is a category and that @{term img} is a function defined
on the arrow type of @{term S}. The function @{term img} should be thought of
as a mapping that takes a point @{term "x ∈ hom unity a"} to a corresponding
terminal object @{term "img x"}. Eventually, assumptions will be introduced so
that this is in fact the case. The set of terminal objects of the category will
serve as abstract ``elements'' of sets; we will refer to the set of \emph{all}
terminal objects as the \emph{universe}.
›
locale set_category_data = category S
for S :: "'s comp" (infixr ‹⋅› 55)
and img :: "'s ⇒ 's"
begin
notation in_hom (‹«_ : _ → _»›)
text‹
Call the set of all terminal objects of S the ``universe''.
›
abbreviation Univ :: "'s set"
where "Univ ≡ Collect terminal"
text‹
Choose an arbitrary element of the universe and call it @{term unity}.
›
definition unity :: 's
where "unity = (SOME t. terminal t)"
text‹
Each object @{term a} determines a subset @{term "set a"} of the universe,
consisting of all those terminal objects @{term t} such that @{term "t = img x"}
for some @{term "x ∈ hom unity a"}.
›
definition set :: "'s ⇒ 's set"
where "set a = img ` hom unity a"
end
text‹
Next, we define a locale ‹set_category_given_img› that augments the
‹set_category_data› locale with assumptions that serve to define
the notion of a set category with a chosen correspondence between points
and terminal objects. The assumptions require that the universe be nonempty
(so that the definition of @{term unity} makes sense), that the map
@{term img} is a locally injective map taking points to terminal objects,
that each terminal object @{term t} belongs to @{term "set t"},
that two objects of @{term S} are equal if they determine the same set,
that two parallel arrows of @{term S} are equal if they determine the same
function, and that for any objects @{term a} and @{term b} and function
@{term "F ∈ hom unity a → hom unity b"} there is an arrow @{term "f ∈ hom a b"}
whose action under the composition of @{term S} coincides with the function @{term F}.
The parameter @{term setp} is a predicate that determines which subsets of the
universe are to be regarded as defining objects of the category. This parameter
has been introduced because most of the characteristic properties of a category
of sets and functions do not depend on there being an object corresponding to
\emph{every} subset of the universe, and we intend to consider in particular the
cases in which only finite subsets or only ``small'' subsets of the universe
determine objects. Accordingly, we assume that there is an object corresponding
to each subset of the universe that satisfies @{term setp}.
It is also necessary to assume some basic regularity properties of the predicate
@{term setp}; namely, that it holds for all subsets of the universe corresponding
to objects of @{term S}, and that it respects subset and union.
›
locale set_category_given_img = set_category_data S img
for S :: "'s comp" (infixr ‹⋅› 55)
and img :: "'s ⇒ 's"
and setp :: "'s set ⇒ bool" +
assumes setp_imp_subset_Univ: "setp A ⟹ A ⊆ Univ"
and setp_set_ide: "ide a ⟹ setp (set a)"
and setp_respects_subset: "A' ⊆ A ⟹ setp A ⟹ setp A'"
and setp_respects_union: "⟦ setp A; setp B ⟧ ⟹ setp (A ∪ B)"
and nonempty_Univ: "Univ ≠ {}"
and inj_img: "ide a ⟹ inj_on img (hom unity a)"
and stable_img: "terminal t ⟹ t ∈ img ` hom unity t"
and extensional_set: "⟦ ide a; ide b; set a = set b ⟧ ⟹ a = b"
and extensional_arr: "⟦ par f f'; ⋀x. «x : unity → dom f» ⟹ f ⋅ x = f' ⋅ x ⟧ ⟹ f = f'"
and set_complete: "setp A ⟹ ∃a. ide a ∧ set a = A"
and fun_complete_ax: "⟦ ide a; ide b; F ∈ hom unity a → hom unity b ⟧
⟹ ∃f. «f : a → b» ∧ (∀x. «x : unity → dom f» ⟶ f ⋅ x = F x)"
begin
lemma setp_singleton:
assumes "terminal a"
shows "setp {a}"
using assms
by (metis setp_set_ide Set.set_insert Un_upper1 insert_is_Un set_def
setp_respects_subset stable_img terminal_def)
lemma setp_empty:
shows "setp {}"
using setp_singleton setp_respects_subset nonempty_Univ by blast
lemma finite_imp_setp:
assumes "A ⊆ Univ" and "finite A"
shows "setp A"
using setp_empty setp_singleton setp_respects_union
by (metis assms(1-2) finite_subset_induct insert_is_Un mem_Collect_eq)
text‹
Each arrow @{term "f ∈ hom a b"} determines a function @{term "Fun f ∈ Univ → Univ"},
by passing from @{term Univ} to @{term "hom a unity"}, composing with @{term f},
then passing back to @{term Univ}.
›
definition Fun :: "'s ⇒ 's ⇒ 's"
where "Fun f = restrict (img o S f o inv_into (hom unity (dom f)) img) (set (dom f))"
lemma comp_arr_point⇩S⇩C:
assumes "arr f" and "«x : unity → dom f»"
shows "f ⋅ x = inv_into (hom unity (cod f)) img (Fun f (img x))"
proof -
have "«f ⋅ x : unity → cod f»"
using assms by blast
thus ?thesis
using assms Fun_def inj_img set_def by simp
qed
text‹
Parallel arrows that determine the same function are equal.
›
lemma arr_eqI⇩S⇩C:
assumes "par f f'" and "Fun f = Fun f'"
shows "f = f'"
using assms comp_arr_point⇩S⇩C extensional_arr by metis
lemma terminal_unity⇩S⇩C:
shows "terminal unity"
using unity_def nonempty_Univ by (simp add: someI_ex)
lemma ide_unity [simp]:
shows "ide unity"
using terminal_unity⇩S⇩C terminal_def by blast
lemma setp_set' [simp]:
assumes "ide a"
shows "setp (set a)"
using assms setp_set_ide by auto
lemma inj_on_set:
shows "inj_on set (Collect ide)"
using extensional_set by (intro inj_onI, auto)
text‹
The inverse of the map @{term set} is a map @{term mkIde} that takes each subset
of the universe to an identity of @{term[source=true] S}.
›
definition mkIde :: "'s set ⇒ 's"
where "mkIde A = (if setp A then inv_into (Collect ide) set A else null)"
lemma mkIde_set [simp]:
assumes "ide a"
shows "mkIde (set a) = a"
by (simp add: assms inj_on_set mkIde_def)
lemma set_mkIde [simp]:
assumes "setp A"
shows "set (mkIde A) = A"
using assms mkIde_def set_complete someI_ex [of "λa. a ∈ Collect ide ∧ set a = A"]
mkIde_set
by metis
lemma ide_mkIde [simp]:
assumes "setp A"
shows "ide (mkIde A)"
using assms mkIde_def mkIde_set set_complete by metis
lemma arr_mkIde [iff]:
shows "arr (mkIde A) ⟷ setp A"
using not_arr_null mkIde_def ide_mkIde by auto
lemma dom_mkIde [simp]:
assumes "setp A"
shows "dom (mkIde A) = mkIde A"
using assms ide_mkIde by simp
lemma cod_mkIde [simp]:
assumes "setp A"
shows "cod (mkIde A) = mkIde A"
using assms ide_mkIde by simp
text‹
Each arrow @{term f} determines an extensional function from
@{term "set (dom f)"} to @{term "set (cod f)"}.
›
lemma Fun_mapsto:
assumes "arr f"
shows "Fun f ∈ extensional (set (dom f)) ∩ (set (dom f) → set (cod f))"
proof
show "Fun f ∈ extensional (set (dom f))" using Fun_def by fastforce
show "Fun f ∈ set (dom f) → set (cod f)"
proof
fix t
assume t: "t ∈ set (dom f)"
have "Fun f t = img (f ⋅ inv_into (hom unity (dom f)) img t)"
using assms t Fun_def comp_def by simp
moreover have "... ∈ set (cod f)"
using assms t set_def inv_into_into [of t img "hom unity (dom f)"] by blast
ultimately show "Fun f t ∈ set (cod f)" by auto
qed
qed
text‹
Identities of @{term[source=true] S} correspond to restrictions of the identity function.
›
lemma Fun_ide:
assumes "ide a"
shows "Fun a = restrict (λx. x) (set a)"
using assms Fun_def inj_img set_def comp_cod_arr by fastforce
lemma Fun_mkIde [simp]:
assumes "setp A"
shows "Fun (mkIde A) = restrict (λx. x) A"
using assms ide_mkIde set_mkIde Fun_ide by simp
text‹
Composition in @{term S} corresponds to extensional function composition.
›
lemma Fun_comp [simp]:
assumes "seq g f"
shows "Fun (g ⋅ f) = restrict (Fun g o Fun f) (set (dom f))"
proof -
have "restrict (img o S (g ⋅ f) o (inv_into (hom unity (dom (g ⋅ f))) img))
(set (dom (g ⋅ f)))
= restrict (Fun g o Fun f) (set (dom f))"
proof -
let ?img' = "λa. λt. inv_into (hom unity a) img t"
have 1: "set (dom (g ⋅ f)) = set (dom f)"
using assms by auto
moreover have "⋀t. t ∈ set (dom (g ⋅ f)) ⟹
(img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = (Fun g o Fun f) t"
proof -
fix t
assume "t ∈ set (dom (g ⋅ f))"
hence t: "t ∈ set (dom f)" by (simp add: 1)
have "(img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = img (g ⋅ f ⋅ ?img' (dom f) t)"
using assms dom_comp comp_assoc by simp
also have "... = img (g ⋅ ?img' (dom g) (Fun f t))"
proof -
have "⋀a x. x ∈ hom unity a ⟹ ?img' a (img x) = x"
using assms inj_img ide_cod inv_into_f_eq
by (metis arrI in_homE mem_Collect_eq)
thus ?thesis
using assms t Fun_def set_def comp_arr_point⇩S⇩C by auto
qed
also have "... = Fun g (Fun f t)"
proof -
have "Fun f t ∈ img ` hom unity (cod f)"
using assms t Fun_mapsto set_def by fast
thus ?thesis
using assms by (auto simp add: set_def Fun_def)
qed
finally show "(img o S (g ⋅ f) o ?img' (dom (g ⋅ f))) t = (Fun g o Fun f) t"
by auto
qed
ultimately show ?thesis by auto
qed
thus ?thesis using Fun_def by auto
qed
text‹
The constructor @{term mkArr} is used to obtain an arrow given subsets
@{term A} and @{term B} of the universe and a function @{term "F ∈ A → B"}.
›
definition mkArr :: "'s set ⇒ 's set ⇒ ('s ⇒ 's) ⇒ 's"
where "mkArr A B F = (if setp A ∧ setp B ∧ F ∈ A → B
then (THE f. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F A)
else null)"
text‹
Each function @{term "F ∈ set a → set b"} determines a unique arrow @{term "f ∈ hom a b"},
such that @{term "Fun f"} is the restriction of @{term F} to @{term "set a"}.
›
lemma fun_complete:
assumes "ide a" and "ide b" and "F ∈ set a → set b"
shows "∃!f. «f : a → b» ∧ Fun f = restrict F (set a)"
proof -
let ?P = "λf. «f : a → b» ∧ Fun f = restrict F (set a)"
show "∃!f. ?P f"
proof
have "∃f. ?P f"
proof -
let ?F' = "λx. inv_into (hom unity b) img (F (img x))"
have "?F' ∈ hom unity a → hom unity b"
proof
fix x
assume x: "x ∈ hom unity a"
have "F (img x) ∈ set b" using assms(3) x set_def by auto
thus "inv_into (hom unity b) img (F (img x)) ∈ hom unity b"
using assms setp_set_ide inj_img set_def by auto
qed
hence "∃f. «f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = ?F' x)"
using assms fun_complete_ax [of a b] by force
from this obtain f where f: "«f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = ?F' x)"
by blast
let ?img' = "λa. λt. inv_into (hom unity a) img t"
have "Fun f = restrict F (set a)"
proof (unfold Fun_def, intro restr_eqI)
show "set (dom f) = set a" using f by auto
show "⋀t. t ∈ set (dom f) ⟹ (img ∘ S f ∘ ?img' (dom f)) t = F t"
proof -
fix t
assume t: "t ∈ set (dom f)"
have "(img ∘ S f ∘ ?img' (dom f)) t = img (f ⋅ ?img' (dom f) t)"
by simp
also have "... = img (?F' (?img' (dom f) t))"
by (metis f in_homE inv_into_into set_def mem_Collect_eq t)
also have "... = img (?img' (cod f) (F t))"
using f t set_def inj_img by auto
also have "... = F t"
proof -
have "F t ∈ set (cod f)"
using assms f t by auto
thus ?thesis
using f t set_def inj_img by auto
qed
finally show "(img ∘ S f ∘ ?img' (dom f)) t = F t" by auto
qed
qed
thus ?thesis using f by blast
qed
thus F: "?P (SOME f. ?P f)" using someI_ex [of ?P] by fast
show "⋀f'. ?P f' ⟹ f' = (SOME f. ?P f)"
using F arr_eqI⇩S⇩C
by (metis (no_types, lifting) in_homE)
qed
qed
lemma mkArr_in_hom:
assumes "setp A" and "setp B" and "F ∈ A → B"
shows "«mkArr A B F : mkIde A → mkIde B»"
using assms mkArr_def fun_complete [of "mkIde A" "mkIde B" F] ide_mkIde set_mkIde
theI' [of "λf. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F A"]
setp_imp_subset_Univ
by simp
text‹
The ``only if'' direction of the next lemma can be achieved only if there exists a
non-arrow element of type @{typ 's}, which can be used as the value of @{term "mkArr A B F"}
in cases where @{term "F ∉ A → B"}. Nevertheless, it is essential to have this,
because without the ``only if'' direction, we can't derive any useful
consequences from an assumption of the form @{term "arr (mkArr A B F)"};
instead we have to obtain @{term "F ∈ A → B"} some other way.
This is is usually highly inconvenient and it makes the theory very weak and almost
unusable in practice. The observation that having a non-arrow value of type @{typ 's}
solves this problem is ultimately what led me to incorporate @{term null} first into the
definition of the ‹set_category› locale and then, ultimately, into the definition
of the ‹category› locale. I believe this idea is critical to the usability of the
entire development.
›
lemma arr_mkArr [iff]:
shows "arr (mkArr A B F) ⟷ setp A ∧ setp B ∧ F ∈ A → B"
proof
show "arr (mkArr A B F) ⟹ setp A ∧ setp B ∧ F ∈ A → B"
using mkArr_def not_arr_null ex_un_null someI_ex [of "λf. ¬arr f"] setp_imp_subset_Univ
by metis
show "setp A ∧ setp B ∧ F ∈ A → B ⟹ arr (mkArr A B F)"
using mkArr_in_hom by auto
qed
lemma arr_mkArrI [intro]:
assumes "setp A" and "setp B" and "F ∈ A → B"
shows "arr (mkArr A B F)"
using assms arr_mkArr by blast
lemma Fun_mkArr':
assumes "arr (mkArr A B F)"
shows "«mkArr A B F : mkIde A → mkIde B»"
and "Fun (mkArr A B F) = restrict F A"
proof -
have 1: "setp A ∧ setp B ∧ F ∈ A → B" using assms by fast
have 2: "mkArr A B F ∈ hom (mkIde A) (mkIde B) ∧
Fun (mkArr A B F) = restrict F (set (mkIde A))"
proof -
have "∃!f. f ∈ hom (mkIde A) (mkIde B) ∧ Fun f = restrict F (set (mkIde A))"
using 1 fun_complete [of "mkIde A" "mkIde B" F] ide_mkIde set_mkIde by simp
thus ?thesis using 1 mkArr_def theI' set_mkIde by simp
qed
show "«mkArr A B F : mkIde A → mkIde B»" using 1 2 by auto
show "Fun (mkArr A B F) = restrict F A" using 1 2 set_mkIde by auto
qed
lemma mkArr_Fun:
assumes "arr f"
shows "mkArr (set (dom f)) (set (cod f)) (Fun f) = f"
proof -
have 1: "setp (set (dom f)) ∧ setp (set (cod f)) ∧ ide (dom f) ∧ ide (cod f) ∧
Fun f ∈ extensional (set (dom f)) ∩ (set (dom f) → set (cod f))"
using Fun_mapsto assms ide_cod ide_dom setp_set' by presburger
hence "∃!f'. f' ∈ hom (dom f) (cod f) ∧ Fun f' = restrict (Fun f) (set (dom f))"
using fun_complete by force
moreover have "f ∈ hom (dom f) (cod f) ∧ Fun f = restrict (Fun f) (set (dom f))"
using assms 1 extensional_restrict by force
ultimately have "f = (THE f'. f' ∈ hom (dom f) (cod f) ∧
Fun f' = restrict (Fun f) (set (dom f)))"
using theI' [of "λf'. f' ∈ hom (dom f) (cod f) ∧ Fun f' = restrict (Fun f) (set (dom f))"]
by blast
also have "... = mkArr (set (dom f)) (set (cod f)) (Fun f)"
using assms 1 mkArr_def mkIde_set by simp
finally show ?thesis by auto
qed
lemma dom_mkArr [simp]:
assumes "arr (mkArr A B F)"
shows "dom (mkArr A B F) = mkIde A"
using assms Fun_mkArr' by auto
lemma cod_mkArr [simp]:
assumes "arr (mkArr A B F)"
shows "cod (mkArr A B F) = mkIde B"
using assms Fun_mkArr' by auto
lemma Fun_mkArr [simp]:
assumes "arr (mkArr A B F)"
shows "Fun (mkArr A B F) = restrict F A"
using assms Fun_mkArr' by auto
text‹
The following provides the basic technique for showing that arrows
constructed using @{term mkArr} are equal.
›
lemma mkArr_eqI [intro]:
assumes "arr (mkArr A B F)"
and "A = A'" and "B = B'" and "⋀x. x ∈ A ⟹ F x = F' x"
shows "mkArr A B F = mkArr A' B' F'"
using assms Fun_mkArr
by (intro arr_eqI⇩S⇩C, auto simp add: Pi_iff)
text‹
This version avoids trivial proof obligations when the domain and codomain
sets are identical from the context.
›
lemma mkArr_eqI' [intro]:
assumes "arr (mkArr A B F)" and "⋀x. x ∈ A ⟹ F x = F' x"
shows "mkArr A B F = mkArr A B F'"
using assms mkArr_eqI by simp
lemma mkArr_restrict_eq:
assumes "arr (mkArr A B F)"
shows "mkArr A B (restrict F A) = mkArr A B F"
using assms by (intro mkArr_eqI', auto)
lemma mkArr_restrict_eq':
assumes "arr (mkArr A B (restrict F A))"
shows "mkArr A B (restrict F A) = mkArr A B F"
using assms by (intro mkArr_eqI', auto)
lemma mkIde_as_mkArr [simp]:
assumes "setp A"
shows "mkArr A A (λx. x) = mkIde A"
using assms arr_mkIde dom_mkIde cod_mkIde Fun_mkIde
by (intro arr_eqI⇩S⇩C, auto)
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)"
proof (intro arr_eqI⇩S⇩C)
have 1: "seq (mkArr B C G) (mkArr A B F)" using assms by force
have 2: "G o F ∈ A → C" using assms by auto
show "par (mkArr B C G ⋅ mkArr A B F) (mkArr A C (G ∘ F))"
using assms 1 2
by (intro conjI) simp_all
show "Fun (mkArr B C G ⋅ mkArr A B F) = Fun (mkArr A C (G ∘ F))"
using 1 2 by fastforce
qed
text‹
The locale assumption @{prop stable_img} forces @{term "t ∈ set t"} in case
@{term t} is a terminal object. This is very convenient, as it results in the
characterization of terminal objects as identities @{term t} for which
@{term "set t = {t}"}. However, it is not absolutely necessary to have this.
The following weaker characterization of terminal objects can be proved without
the @{prop stable_img} assumption.
›
lemma terminal_char1:
shows "terminal t ⟷ ide t ∧ (∃!x. x ∈ set t)"
proof -
have "terminal t ⟹ ide t ∧ (∃!x. x ∈ set t)"
proof -
assume t: "terminal t"
have "ide t" using t terminal_def by auto
moreover have "∃!x. x ∈ set t"
proof -
have "∃!x. x ∈ hom unity t"
using t terminal_unity⇩S⇩C terminal_def by auto
thus ?thesis using set_def by auto
qed
ultimately show "ide t ∧ (∃!x. x ∈ set t)" by auto
qed
moreover have "ide t ∧ (∃!x. x ∈ set t) ⟹ terminal t"
proof -
assume t: "ide t ∧ (∃!x. x ∈ set t)"
from this obtain t' where "set t = {t'}" by blast
hence t': "set t = {t'} ∧ setp {t'} ∧ t = mkIde {t'}"
using t setp_set_ide mkIde_set by metis
show "terminal t"
proof
show "ide t" using t by simp
show "⋀a. ide a ⟹ ∃!f. «f : a → t»"
proof -
fix a
assume a: "ide a"
show "∃!f. «f : a → t»"
proof
show 1: "«mkArr (set a) {t'} (λx. t') : a → t»"
using a t t' mkArr_in_hom
by (metis Pi_I' mkIde_set setp_set_ide singletonD)
show "⋀f. «f : a → t» ⟹ f = mkArr (set a) {t'} (λx. t')"
proof -
fix f
assume f: "«f : a → t»"
show "f = mkArr (set a) {t'} (λx. t')"
proof (intro arr_eqI⇩S⇩C)
show 1: "par f (mkArr (set a) {t'} (λx. t'))" using 1 f in_homE by metis
show "Fun f = Fun (mkArr (set a) {t'} (λx. t'))"
proof -
have "Fun (mkArr (set a) {t'} (λx. t')) = (λx∈set a. t')"
using 1 Fun_mkArr by simp
also have "... = Fun f"
proof -
have "⋀x. x ∈ set a ⟹ Fun f x = t'"
using f t' Fun_def mkArr_Fun arr_mkArr
by (metis PiE in_homE singletonD)
moreover have "⋀x. x ∉ set a ⟹ Fun f x = undefined"
using f Fun_def by auto
ultimately show ?thesis by auto
qed
finally show ?thesis by force
qed
qed
qed
qed
qed
qed
qed
ultimately show ?thesis by blast
qed
text‹
As stated above, in the presence of the @{prop stable_img} assumption we have
the following stronger characterization of terminal objects.
›
lemma terminal_char2:
shows "terminal t ⟷ ide t ∧ set t = {t}"
proof
assume t: "terminal t"
show "ide t ∧ set t = {t}"
proof
show "ide t" using t terminal_char1 by auto
show "set t = {t}"
proof -
have "∃!x. x ∈ hom unity t" using t terminal_def terminal_unity⇩S⇩C by force
moreover have "t ∈ img ` hom unity t" using t stable_img set_def by simp
ultimately show ?thesis using set_def by auto
qed
qed
next
assume "ide t ∧ set t = {t}"
thus "terminal t" using terminal_char1 by force
qed
end
text‹
At last, we define the ‹set_category› locale by existentially quantifying
out the choice of a particular @{term img} map. We need to know that such a map
exists, but it does not matter which one we choose.
›
locale set_category = category S
for S :: "'s comp" (infixr ‹⋅› 55)
and setp :: "'s set ⇒ bool" +
assumes ex_img: "∃img. set_category_given_img S img setp"
begin
notation in_hom (‹«_ : _ → _»›)
definition some_img
where "some_img = (SOME img. set_category_given_img S img setp)"
sublocale set_category_given_img S some_img setp
proof -
have "∃img. set_category_given_img S img setp" using ex_img by auto
thus "set_category_given_img S some_img setp"
using someI_ex [of "λimg. set_category_given_img S img setp"] some_img_def
by metis
qed
end
text‹We call a set category \emph{replete} if there is an object corresponding to
every subset of the universe.
›
locale replete_set_category =
category S +
set_category S ‹λA. A ⊆ Collect terminal›
for S :: "'s comp" (infixr ‹⋅› 55)
begin
abbreviation setp
where "setp ≡ λA. A ⊆ Univ"
lemma is_set_category:
shows "set_category S (λA. A ⊆ Collect terminal)"
..
end
context set_category
begin
text‹
The arbitrary choice of @{term img} induces a system of arrows corresponding
to inclusions of subsets.
›
definition incl :: "'s ⇒ bool"
where "incl f = (arr f ∧ set (dom f) ⊆ set (cod f) ∧
f = mkArr (set (dom f)) (set (cod f)) (λx. x))"
lemma Fun_incl:
assumes "incl f"
shows "Fun f = (λx ∈ set (dom f). x)"
using assms incl_def by (metis Fun_mkArr)
lemma ex_incl_iff_subset:
assumes "ide a" and "ide b"
shows "(∃f. «f : a → b» ∧ incl f) ⟷ set a ⊆ set b"
proof
show "∃f. «f : a → b» ∧ incl f ⟹ set a ⊆ set b"
using incl_def by auto
show "set a ⊆ set b ⟹ ∃f. «f : a → b» ∧ incl f"
proof
assume 1: "set a ⊆ set b"
show "«mkArr (set a) (set b) (λx. x) : a → b» ∧ incl (mkArr (set a) (set b) (λx. x))"
proof
show "«mkArr (set a) (set b) (λx. x) : a → b»"
by (metis 1 assms image_ident image_subset_iff_funcset mkIde_set
mkArr_in_hom setp_set_ide)
thus "incl (mkArr (set a) (set b) (λx. x))"
using 1 incl_def by force
qed
qed
qed
end
section "Categoricity"
text‹
In this section we show that the ‹set_category› locale completely characterizes
the structure of its interpretations as categories, in the sense that for any two
interpretations @{term S} and @{term S'}, a @{term setp}-respecting bijection
between the universe of @{term S} and the universe of @{term S'} extends
to an isomorphism of @{term S} and @{term S'}.
›
locale two_set_categories_bij_betw_Univ =
S: set_category S setp +
S': set_category S' setp'
for S :: "'s comp" (infixr ‹⋅› 55)
and setp :: "'s set ⇒ bool"
and S' :: "'t comp" (infixr ‹⋅´› 55)
and setp' :: "'t set ⇒ bool"
and φ :: "'s ⇒ 't" +
assumes bij_φ: "bij_betw φ S.Univ S'.Univ"
and φ_respects_setp: "A ⊆ S.Univ ⟹ setp' (φ ` A) ⟷ setp A"
begin
notation S.in_hom (‹«_ : _ → _»›)
notation S'.in_hom (‹«_ : _ →'' _»›)
abbreviation ψ
where "ψ ≡ inv_into S.Univ φ"
lemma ψ_φ:
assumes "t ∈ S.Univ"
shows "ψ (φ t) = t"
using assms bij_φ bij_betw_inv_into_left by metis
lemma φ_ψ:
assumes "t' ∈ S'.Univ"
shows "φ (ψ t') = t'"
using assms bij_φ bij_betw_inv_into_right by metis
lemma ψ_img_φ_img:
assumes "A ⊆ S.Univ"
shows "ψ ` φ ` A = A"
using assms bij_φ by (simp add: bij_betw_def)
lemma φ_img_ψ_img:
assumes "A' ⊆ S'.Univ"
shows "φ ` ψ ` A' = A'"
using assms bij_φ by (simp add: bij_betw_def image_inv_into_cancel)
text‹
We define the object map @{term Φo} of a functor from @{term[source=true] S}
to @{term[source=true] S'}.
›
definition Φo
where "Φo = (λa ∈ Collect S.ide. S'.mkIde (φ ` S.set a))"
lemma set_Φo:
assumes "S.ide a"
shows "S'.set (Φo a) = φ ` S.set a"
by (simp add: S.setp_imp_subset_Univ Φo_def φ_respects_setp assms)
lemma Φo_preserves_ide:
assumes "S.ide a"
shows "S'.ide (Φo a)"
using assms S'.ide_mkIde bij_φ bij_betw_def image_mono restrict_apply' S.setp_set'
φ_respects_setp S.setp_imp_subset_Univ
unfolding Φo_def
by simp
text‹
The map @{term Φa} assigns to each arrow @{term f} of @{term[source=true] S} the function on
the universe of @{term[source=true] S'} that is the same as the function induced by @{term f}
on the universe of @{term[source=true] S}, up to the bijection @{term φ} between the two
universes.
›
definition Φa
where "Φa = (λf. λx' ∈ φ ` S.set (S.dom f). φ (S.Fun f (ψ x')))"
lemma Φa_mapsto:
assumes "S.arr f"
shows "Φa f ∈ S'.set (Φo (S.dom f)) → S'.set (Φo (S.cod f))"
proof -
have "Φa f ∈ φ ` S.set (S.dom f) → φ ` S.set (S.cod f)"
proof
fix x
assume x: "x ∈ φ ` S.set (S.dom f)"
have "ψ x ∈ S.set (S.dom f)"
using assms x ψ_img_φ_img [of "S.set (S.dom f)"] S.setp_imp_subset_Univ by auto
hence "S.Fun f (ψ x) ∈ S.set (S.cod f)" using assms S.Fun_mapsto by auto
hence "φ (S.Fun f (ψ x)) ∈ φ ` S.set (S.cod f)" by simp
thus "Φa f x ∈ φ ` S.set (S.cod f)" using x Φa_def by auto
qed
thus ?thesis using assms set_Φo Φo_preserves_ide by auto
qed
text‹
The map @{term Φa} takes composition of arrows to extensional
composition of functions.
›
lemma Φa_comp:
assumes gf: "S.seq g f"
shows "Φa (g ⋅ f) = restrict (Φa g o Φa f) (S'.set (Φo (S.dom f)))"
proof -
have "Φa (g ⋅ f) = (λx' ∈ φ ` S.set (S.dom f). φ (S.Fun (S g f) (ψ x')))"
using gf Φa_def by auto
also have "... = (λx' ∈ φ ` S.set (S.dom f).
φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')))"
using gf set_Φo S.Fun_comp by simp
also have "... = restrict (Φa g o Φa f) (S'.set (Φo (S.dom f)))"
proof -
have "⋀x'. x' ∈ φ ` S.set (S.dom f)
⟹ φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')) = Φa g (Φa f x')"
proof -
fix x'
assume X': "x' ∈ φ ` S.set (S.dom f)"
hence 1: "ψ x' ∈ S.set (S.dom f)"
using gf ψ_img_φ_img S.setp_imp_subset_Univ S.ide_dom S.setp_set_ide
by blast
hence "φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x'))
= φ (S.Fun g (S.Fun f (ψ x')))"
using restrict_apply by auto
also have "... = φ (S.Fun g (ψ (φ (S.Fun f (ψ x')))))"
proof -
have "S.Fun f (ψ x') ∈ S.set (S.cod f)"
using gf 1 S.Fun_mapsto by fast
hence "ψ (φ (S.Fun f (ψ x'))) = S.Fun f (ψ x')"
using assms bij_φ S.setp_imp_subset_Univ bij_betw_def inv_into_f_f subsetCE
S.ide_cod S.setp_set_ide
by (metis S.seqE)
thus ?thesis by auto
qed
also have "... = Φa g (Φa f x')"
proof -
have "Φa f x' ∈ φ ` S.set (S.cod f)"
using gf S.ide_dom S.ide_cod X' Φa_mapsto [of f] set_Φo [of "S.dom f"]
set_Φo [of "S.cod f"]
by blast
thus ?thesis using gf X' Φa_def by auto
qed
finally show "φ (restrict (S.Fun g o S.Fun f) (S.set (S.dom f)) (ψ x')) =
Φa g (Φa f x')"
by auto
qed
thus ?thesis using assms set_Φo by fastforce
qed
finally show ?thesis by auto
qed
text‹
Finally, we use @{term Φo} and @{term Φa} to define a functor @{term Φ}.
›
definition Φ
where "Φ f = (if S.arr f then
S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f)
else S'.null)"
lemma Φ_in_hom:
assumes "S.arr f"
shows "Φ f ∈ S'.hom (Φo (S.dom f)) (Φo (S.cod f))"
proof -
have "«Φ f : S'.dom (Φ f) →' S'.cod (Φ f)»"
using assms Φ_def Φa_mapsto Φo_preserves_ide
by (intro S'.in_homI) auto
thus ?thesis
using assms Φ_def Φa_mapsto Φo_preserves_ide by auto
qed
lemma Φ_ide [simp]:
assumes "S.ide a"
shows "Φ a = Φo a"
proof -
have "Φ a = S'.mkArr (S'.set (Φo a)) (S'.set (Φo a)) (λx'. x')"
proof -
have "«Φ a : Φo a →' Φo a»"
using assms Φ_in_hom S.ide_in_hom by fastforce
moreover have "Φa a = restrict (λx'. x') (S'.set (Φo a))"
proof -
have "Φa a = (λx' ∈ φ ` S.set a. φ (S.Fun a (ψ x')))"
using assms Φa_def restrict_apply by auto
also have "... = (λx' ∈ S'.set (Φo a). φ (ψ x'))"
proof -
have "S.Fun a = (λx ∈ S.set a. x)"
using assms S.Fun_ide by auto
moreover have "⋀x'. x' ∈ φ ` S.set a ⟹ ψ x' ∈ S.set a"
using assms bij_φ S.setp_imp_subset_Univ image_iff S.setp_set_ide
by (metis ψ_img_φ_img)
ultimately show ?thesis
using assms set_Φo by auto
qed
also have "... = restrict (λx'. x') (S'.set (Φo a))"
using assms S'.setp_imp_subset_Univ S'.setp_set_ide Φo_preserves_ide φ_ψ
by (meson restr_eqI subsetCE)
ultimately show ?thesis by auto
qed
ultimately show ?thesis
using assms Φ_def Φo_preserves_ide S'.mkArr_restrict_eq'
by (metis S'.arrI S.ide_char)
qed
thus ?thesis
using assms S'.mkIde_as_mkArr Φo_preserves_ide Φ_in_hom S'.mkIde_set
by simp
qed
lemma set_dom_Φ:
assumes "S.arr f"
shows "S'.set (S'.dom (Φ f)) = φ ` (S.set (S.dom f))"
using assms S.ide_dom Φ_in_hom Φ_ide set_Φo by fastforce
lemma Φ_comp:
assumes "S.seq g f"
shows "Φ (g ⋅ f) = Φ g ⋅´ Φ f"
proof -
have "Φ (g ⋅ f) = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g))) (Φa (S g f))"
using Φ_def assms by auto
also have "... = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g)))
(restrict (Φa g o Φa f) (S'.set (Φo (S.dom f))))"
using assms Φa_comp set_Φo by force
also have "... = S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod g))) (Φa g o Φa f)"
by (metis S'.mkArr_restrict_eq' Φ_in_hom assms calculation S'.in_homE mem_Collect_eq)
also have "... = S' (S'.mkArr (S'.set (Φo (S.dom g))) (S'.set (Φo (S.cod g))) (Φa g))
(S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f))"
proof -
have "S'.arr (S'.mkArr (S'.set (Φo (S.dom f))) (S'.set (Φo (S.cod f))) (Φa f))"
using assms Φa_mapsto set_Φo S.ide_dom S.ide_cod Φo_preserves_ide
S'.arr_mkArr S'.setp_imp_subset_Univ S'.setp_set_ide S.seqE
by metis
moreover have "S'.arr (S'.mkArr (S'.set (Φo (S.dom g))) (S'.set (Φo (S.cod g)))
(Φa g))"
using assms Φa_mapsto set_Φo S.ide_dom S.ide_cod Φo_preserves_ide S'.arr_mkArr
S'.setp_imp_subset_Univ S'.setp_set_ide S.seqE
by metis
ultimately show ?thesis using assms S'.comp_mkArr by auto
qed
also have "... = Φ g ⋅´ Φ f" using assms Φ_def by force
finally show ?thesis by fast
qed
interpretation Φ: "functor" S S' Φ
apply unfold_locales
using Φ_def
apply simp
using Φ_in_hom Φ_comp
by auto
lemma Φ_is_functor:
shows "functor S S' Φ" ..
lemma Fun_Φ:
assumes "S.arr f" and "x ∈ S.set (S.dom f)"
shows "S'.Fun (Φ f) (φ x) = Φa f (φ x)"
using assms Φ_def Φ.preserves_arr set_Φo by auto
lemma Φ_acts_elementwise:
assumes "S.ide a"
shows "S'.set (Φ a) = Φ ` S.set a"
proof
have 0: "S'.set (Φ a) = φ ` S.set a"
using assms Φ_ide set_Φo by simp
have 1: "⋀x. x ∈ S.set a ⟹ Φ x = φ x"
proof -
fix x
assume x: "x ∈ S.set a"
have 1: "S.terminal x" using assms x S.setp_imp_subset_Univ S.setp_set_ide by blast
hence 2: "S'.terminal (φ x)"
by (metis CollectD CollectI bij_φ bij_betw_def image_iff)
have "Φ x = Φo x"
using assms x 1 Φ_ide S.terminal_def by auto
also have "... = φ x"
proof -
have "Φo x = S'.mkIde (φ ` S.set x)"
using assms 1 x Φo_def S.terminal_def by auto
moreover have "S'.mkIde (φ ` S.set x) = φ x"
using assms x 1 2 S.terminal_char2 S'.terminal_char2 S'.mkIde_set bij_φ
by (metis (no_types, lifting) empty_is_image image_insert)
ultimately show ?thesis by auto
qed
finally show "Φ x = φ x" by auto
qed
show "S'.set (Φ a) ⊆ Φ ` S.set a" using 0 1 by force
show "Φ ` S.set a ⊆ S'.set (Φ a)" using 0 1 by force
qed
lemma Φ_preserves_incl:
assumes "S.incl m"
shows "S'.incl (Φ m)"
proof -
have 1: "S.arr m ∧ S.set (S.dom m) ⊆ S.set (S.cod m) ∧
m = S.mkArr (S.set (S.dom m)) (S.set (S.cod m)) (λx. x)"
using assms S.incl_def by blast
have "S'.arr (Φ m)" using 1 by auto
moreover have 2: "S'.set (S'.dom (Φ m)) ⊆ S'.set (S'.cod (Φ m))"
using 1 Φ.preserves_dom Φ.preserves_cod Φ_acts_elementwise by auto
moreover have "Φ m =
S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (λx'. x')"
proof -
have "Φ m = S'.mkArr (S'.set (Φo (S.dom m))) (S'.set (Φo (S.cod m))) (Φa m)"
using 1 Φ_def by simp
also have "... = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (Φa m)"
using 1 Φ_ide by auto
finally have 3: "Φ m =
S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (Φa m)"
by auto
also have "... = S'.mkArr (S'.set (S'.dom (Φ m))) (S'.set (S'.cod (Φ m))) (λx'. x')"
proof -
have 4: "S.Fun m = restrict (λx. x) (S.set (S.dom m))"
using assms S.incl_def by (metis (full_types) S.Fun_mkArr)
hence "Φa m = restrict (λx'. x') (φ ` (S.set (S.dom m)))"
proof -
have 5: "⋀x'. x' ∈ φ ` S.set (S.dom m) ⟹ φ (ψ x') = x'"
by (meson 1 S.ide_dom S.setp_imp_subset_Univ S.setp_set' f_inv_into_f
image_mono subset_eq)
have "Φa m = restrict (λx'. φ (S.Fun m (ψ x'))) (φ ` S.set (S.dom m))"
using Φa_def by simp
also have "... = restrict (λx'. x') (φ ` S.set (S.dom m))"
proof -
have "⋀x. x ∈ φ ` (S.set (S.dom m)) ⟹ φ (S.Fun m (ψ x)) = x"
proof -
fix x
assume x: "x ∈ φ ` (S.set (S.dom m))"
hence "ψ x ∈ S.set (S.dom m)"
using 1 S.ide_dom S.setp_imp_subset_Univ S.setp_set_ide ψ_img_φ_img image_eqI
by metis
thus "φ (S.Fun m (ψ x)) = x" using 1 4 5 x by simp
qed
thus ?thesis by auto
qed
finally show ?thesis by auto
qed
hence "Φa m = restrict (λx'. x') (S'.set (S'.dom (Φ m)))"
using 1 set_dom_Φ by auto
thus ?thesis
using 2 3 ‹S'.arr (Φ m)› S'.mkArr_restrict_eq S'.ide_cod S'.ide_dom S'.incl_def
by (metis S'.arr_mkArr image_restrict_eq image_subset_iff_funcset)
qed
finally show ?thesis by auto
qed
ultimately show ?thesis using S'.incl_def by blast
qed
lemma ψ_respects_sets:
assumes "A' ⊆ S'.Univ"
shows "setp (ψ ` A') ⟷ setp' A'"
using assms φ_respects_setp φ_img_ψ_img bij_φ
by (metis ψ_img_φ_img bij_betw_def image_mono order_refl)
text‹
Interchange the role of @{term φ} and @{term ψ} to obtain a functor ‹Ψ›
from @{term[source=true] S'} to @{term[source=true] S}.
›
interpretation INV: two_set_categories_bij_betw_Univ S' setp' S setp ψ
using ψ_respects_sets bij_φ bij_betw_inv_into
by unfold_locales auto
abbreviation Ψo
where "Ψo ≡ INV.Φo"
abbreviation Ψa
where "Ψa ≡ INV.Φa"
abbreviation Ψ
where "Ψ ≡ INV.Φ"
interpretation Ψ: "functor" S' S Ψ
using INV.Φ_is_functor by auto
text‹
The functors @{term Φ} and @{term Ψ} are inverses.
›
lemma Fun_Ψ:
assumes "S'.arr f'" and "x' ∈ S'.set (S'.dom f')"
shows "S.Fun (Ψ f') (ψ x') = Ψa f' (ψ x')"
using assms INV.Fun_Φ by blast
lemma Ψo_Φo:
assumes "S.ide a"
shows "Ψo (Φo a) = a"
using assms Φo_def INV.Φo_def ψ_img_φ_img Φo_preserves_ide set_Φo S.mkIde_set
by (simp add: S.setp_imp_subset_Univ)
lemma ΦΨ:
assumes "S.arr f"
shows "Ψ (Φ f) = f"
proof (intro S.arr_eqI⇩S⇩C)
show par: "S.par (Ψ (Φ f)) f"
using assms Φo_preserves_ide Ψo_Φo by auto
show "S.Fun (Ψ (Φ f)) = S.Fun f"
proof -
have "S.arr (Ψ (Φ f))" using assms by auto
moreover have "Ψ (Φ f) = S.mkArr (S.set (S.dom f)) (S.set (S.cod f)) (Ψa (Φ f))"
using assms INV.Φ_def Φ_in_hom Ψo_Φo by auto
moreover have "Ψa (Φ f) = (λx ∈ S.set (S.dom f). ψ (S'.Fun (Φ f) (φ x)))"
proof -
have "Ψa (Φ f) = (λx ∈ ψ ` S'.set (S'.dom (Φ f)). ψ (S'.Fun (Φ f) (φ x)))"
proof -
have "⋀x. x ∈ ψ ` S'.set (S'.dom (Φ f)) ⟹ INV.ψ x = φ x"
using assms S.ide_dom S.setp_imp_subset_Univ Ψ.preserves_reflects_arr par bij_φ
inv_into_inv_into_eq subsetCE INV.set_dom_Φ
by (metis (no_types) S.setp_set')
thus ?thesis
using INV.Φa_def by auto
qed
moreover have "ψ ` S'.set (S'.dom (Φ f)) = S.set (S.dom f)"
using assms by (metis par Ψ.preserves_reflects_arr INV.set_dom_Φ)
ultimately show ?thesis by auto
qed
ultimately have 1: "S.Fun (Ψ (Φ f)) = (λx ∈ S.set (S.dom f). ψ (S'.Fun (Φ f) (φ x)))"
using S'.Fun_mkArr by simp
show ?thesis
proof
fix x
have "x ∉ S.set (S.dom f) ⟹ S.Fun (Ψ (Φ f)) x = S.Fun f x"
using 1 assms extensional_def S.Fun_mapsto S.Fun_def by auto
moreover have "x ∈ S.set (S.dom f) ⟹ S.Fun (Ψ (Φ f)) x = S.Fun f x"
proof -
assume x: "x ∈ S.set (S.dom f)"
have "S.Fun (Ψ (Φ f)) x = ψ (φ (S.Fun f (ψ (φ x))))"
using assms x 1 Fun_Φ bij_φ Φa_def by auto
also have "... = S.Fun f x"
proof -
have 2: "⋀x. x ∈ S.Univ ⟹ ψ (φ x) = x"
using bij_φ bij_betw_inv_into_left by fast
have "S.Fun f (ψ (φ x)) = S.Fun f x"
using assms x 2 S.ide_dom S.setp_imp_subset_Univ
by (metis S.setp_set' subsetD)
moreover have "S.Fun f x ∈ S.Univ"
using x assms S.Fun_mapsto S.setp_imp_subset_Univ S.setp_set' S.ide_cod
by blast
ultimately show ?thesis using 2 by auto
qed
finally show ?thesis by auto
qed
ultimately show "S.Fun (Ψ (Φ f)) x = S.Fun f x" by auto
qed
qed
qed
lemma Φo_Ψo:
assumes "S'.ide a'"
shows "Φo (Ψo a') = a'"
using assms Φo_def INV.Φo_def φ_img_ψ_img INV.Φo_preserves_ide ψ_φ INV.set_Φo
S'.mkIde_set S'.setp_imp_subset_Univ
by force
lemma ΨΦ:
assumes "S'.arr f'"
shows "Φ (Ψ f') = f'"
proof (intro S'.arr_eqI⇩S⇩C)
show par: "S'.par (Φ (Ψ f')) f'"
using assms Φ.preserves_ide Ψ.preserves_ide Φ_ide INV.Φ_ide Φo_Ψo by auto
show "S'.Fun (Φ (Ψ f')) = S'.Fun f'"
proof -
have "S'.arr (Φ (Ψ f'))" using assms by blast
moreover have "Φ (Ψ f') =
S'.mkArr (S'.set (S'.dom f')) (S'.set (S'.cod f')) (Φa (Ψ f'))"
using assms Φ_def INV.Φ_in_hom Φo_Ψo by simp
moreover have "Φa (Ψ f') = (λx' ∈ S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))"
unfolding Φa_def
using assms par Ψ.preserves_arr set_dom_Φ by metis
ultimately have 1: "S'.Fun (Φ (Ψ f')) =
(λx' ∈ S'.set (S'.dom f'). φ (S.Fun (Ψ f') (ψ x')))"
using S'.Fun_mkArr by simp
show ?thesis
proof
fix x'
have "x' ∉ S'.set (S'.dom f') ⟹ S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'"
using 1 assms S'.Fun_mapsto extensional_def by (simp add: S'.Fun_def)
moreover have "x' ∈ S'.set (S'.dom f') ⟹ S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'"
proof -
assume x': "x' ∈ S'.set (S'.dom f')"
have "S'.Fun (Φ (Ψ f')) x' = φ (S.Fun (Ψ f') (ψ x'))"
using x' 1 by auto
also have "... = φ (Ψa f' (ψ x'))"
using Fun_Ψ x' assms S'.setp_imp_subset_Univ bij_φ by metis
also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))"
proof -
have "φ (Ψa f' (ψ x')) = φ (ψ (S'.Fun f' x'))"
proof -
have "x' ∈ S'.Univ"
by (meson S'.ide_dom S'.setp_imp_subset_Univ S'.setp_set_ide assms subsetCE x')
thus ?thesis
by (simp add: INV.Φa_def INV.ψ_φ x')
qed
also have "... = φ (ψ (S'.Fun f' (φ (ψ x'))))"
using assms x' φ_ψ S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom
by (metis subsetCE)
finally show ?thesis by auto
qed
also have "... = S'.Fun f' x'"
proof -
have 2: "⋀x'. x' ∈ S'.Univ ⟹ φ (ψ x') = x'"
using bij_φ bij_betw_inv_into_right by fast
have "S'.Fun f' (φ (ψ x')) = S'.Fun f' x'"
using assms x' 2 S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_dom
by (metis subsetCE)
moreover have "S'.Fun f' x' ∈ S'.Univ"
using x' assms S'.Fun_mapsto S'.setp_imp_subset_Univ S'.setp_set_ide S'.ide_cod
by blast
ultimately show ?thesis using 2 by auto
qed
finally show ?thesis by auto
qed
ultimately show "S'.Fun (Φ (Ψ f')) x' = S'.Fun f' x'" by auto
qed
qed
qed
lemma inverse_functors_Φ_Ψ:
shows "inverse_functors S S' Ψ Φ"
proof -
interpret ΦΨ: composite_functor S S' S Φ Ψ ..
have inv: "Ψ o Φ = S.map"
using ΦΨ S.map_def ΦΨ.is_extensional by auto
interpret ΨΦ: composite_functor S' S S' Ψ Φ ..
have inv': "Φ o Ψ = S'.map"
using ΨΦ S'.map_def ΨΦ.is_extensional by auto
show ?thesis
using inv inv' by (unfold_locales, auto)
qed
lemma are_isomorphic:
shows "∃Φ. invertible_functor S S' Φ ∧ (∀m. S.incl m ⟶ S'.incl (Φ m))"
proof -
interpret inverse_functors S S' Ψ Φ
using inverse_functors_Φ_Ψ by auto
have 1: "inverse_functors S S' Ψ Φ" ..
interpret invertible_functor S S' Φ
apply unfold_locales using 1 by auto
have "invertible_functor S S' Φ" ..
thus ?thesis using Φ_preserves_incl by auto
qed
end
text‹
The main result: @{locale set_category} is categorical, in the following (logical) sense:
If ‹S› and ‹S'› are two "set categories", and if the sets of terminal objects of ‹S› and ‹S'›
are in correspondence via a @{term setp}-preserving bijection, then ‹S› and ‹S'› are
isomorphic as categories, via a functor that preserves inclusion maps, hence also the
inclusion relation between sets.
›
theorem set_category_is_categorical:
assumes "set_category S setp" and "set_category S' setp'"
and "bij_betw φ (set_category_data.Univ S) (set_category_data.Univ S')"
and "⋀A. A ⊆ set_category_data.Univ S ⟹ setp' (φ ` A) ⟷ setp A"
shows "∃Φ. invertible_functor S S' Φ ∧
(∀m. set_category.incl S setp m ⟶ set_category.incl S' setp' (Φ m))"
proof -
interpret S: set_category S setp using assms(1) by auto
interpret S': set_category S' setp' using assms(2) by auto
interpret two_set_categories_bij_betw_Univ S setp S' setp' φ
apply (unfold_locales) using assms(3-4) by auto
show ?thesis using are_isomorphic by auto
qed
section "Further Properties of Set Categories"
text‹
In this section we further develop the consequences of the ‹set_category›
axioms, and establish characterizations of a number of standard category-theoretic
notions for a ‹set_category›.
›
context set_category
begin
abbreviation Dom
where "Dom f ≡ set (dom f)"
abbreviation Cod
where "Cod f ≡ set (cod f)"
subsection "Initial Object"
text‹
The object corresponding to the empty set is an initial object.
›
definition empty
where "empty = mkIde {}"
lemma initial_empty:
shows "initial empty"
proof
show 0: "ide empty"
using empty_def by (simp add: setp_empty)
show "⋀b. ide b ⟹ ∃!f. «f : empty → b»"
proof -
fix b
assume b: "ide b"
show "∃!f. «f : empty → b»"
proof
show 1: "«mkArr {} (set b) (λx. x) : empty → b»"
using 0 b empty_def mkArr_in_hom mkIde_set setp_imp_subset_Univ arr_mkIde
by (metis Pi_I empty_iff ide_def mkIde_def)
show "⋀f. «f : empty → b» ⟹ f = mkArr {} (set b) (λx. x)"
by (metis "1" arr_mkArr empty_iff in_homE empty_def mkArr_Fun mkArr_eqI set_mkIde)
qed
qed
qed
subsection "Identity Arrows"
text‹
Identity arrows correspond to restrictions of the identity function.
›
lemma ide_char⇩S⇩C:
assumes "arr f"
shows "ide f ⟷ Dom f = Cod f ∧ Fun f = (λx ∈ Dom f. x)"
using assms mkIde_as_mkArr mkArr_Fun Fun_ide in_homE ide_cod mkArr_Fun mkIde_set
by (metis ide_char)
lemma ideI:
assumes "arr f" and "Dom f = Cod f" and "⋀x. x ∈ Dom f ⟹ Fun f x = x"
shows "ide f"
proof -
have "Fun f = (λx ∈ Dom f. x)"
using assms Fun_def by auto
thus ?thesis using assms ide_char⇩S⇩C by blast
qed
subsection "Inclusions"
lemma ide_implies_incl:
assumes "ide a"
shows "incl a"
by (simp add: assms incl_def)
definition incl_in :: "'s ⇒ 's ⇒ bool"
where "incl_in a b = (ide a ∧ ide b ∧ set a ⊆ set b)"
abbreviation incl_of
where "incl_of a b ≡ mkArr (set a) (set b) (λx. x)"
lemma elem_set_implies_set_eq_singleton:
assumes "a ∈ set b"
shows "set a = {a}"
proof -
have "ide b" using assms set_def by auto
thus ?thesis using assms setp_imp_subset_Univ terminal_char2
by (metis setp_set' insert_subset mem_Collect_eq mk_disjoint_insert)
qed
lemma elem_set_implies_incl_in:
assumes "a ∈ set b"
shows "incl_in a b"
proof -
have b: "ide b" using assms set_def by auto
hence "setp (set b)" by simp
hence "a ∈ Univ ∧ set a ⊆ set b"
using setp_imp_subset_Univ assms elem_set_implies_set_eq_singleton by auto
hence "ide a ∧ set a ⊆ set b"
using b terminal_char1 by simp
thus ?thesis using b incl_in_def by simp
qed
lemma incl_incl_of [simp]:
assumes "incl_in a b"
shows "incl (incl_of a b)"
and "«incl_of a b : a → b»"
proof -
show "«incl_of a b : a → b»"
using assms incl_in_def mkArr_in_hom
by (metis image_ident image_subset_iff_funcset mkIde_set setp_set_ide)
thus "incl (incl_of a b)"
using assms incl_def incl_in_def by fastforce
qed
text‹
There is at most one inclusion between any pair of objects.
›
lemma incls_coherent:
assumes "par f f'" and "incl f" and "incl f'"
shows "f = f'"
using assms incl_def fun_complete by auto
text‹
The set of inclusions is closed under composition.
›
lemma incl_comp [simp]:
assumes "incl f" and "incl g" and "cod f = dom g"
shows "incl (g ⋅ f)"
proof -
have 1: "seq g f" using assms incl_def by auto
moreover have 2: "Dom (g ⋅ f) ⊆ Cod (g ⋅ f)"
using assms 1 incl_def by auto
moreover have "g ⋅ f = mkArr (Dom f) (Cod g) (restrict (λx. x) (Dom f))"
proof (intro arr_eqI⇩S⇩C)
have 3: "arr (mkArr (Dom f) (Cod g) (λx∈Dom f. x))"
by (metis 1 2 cod_comp dom_comp ide_cod ide_dom incl_def incl_in_def
incl_incl_of(1) mkArr_restrict_eq)
show 4: "par (g ⋅ f) (mkArr (Dom f) (Cod g) (λx∈Dom f. x))"
using assms 1 3 mkIde_set by auto
show "Fun (g ⋅ f) = Fun (mkArr (Dom f) (Cod g) (λx∈Dom f. x))"
using assms 3 4 Fun_comp Fun_mkArr
by (metis comp_cod_arr dom_cod ide_cod ide_implies_incl incl_def mkArr_restrict_eq')
qed
ultimately show ?thesis using incl_def by force
qed
subsection "Image Factorization"
text‹
The image of an arrow is the object that corresponds to the set-theoretic
image of the domain set under the function induced by the arrow.
›
abbreviation Img
where "Img f ≡ Fun f ` Dom f"
definition img
where "img f = mkIde (Img f)"
lemma ide_img [simp]:
assumes "arr f"
shows "ide (img f)"
proof -
have "Fun f ` Dom f ⊆ Cod f" using assms Fun_mapsto by blast
moreover have "setp (Cod f)" using assms by simp
ultimately show ?thesis using img_def setp_respects_subset by auto
qed
lemma set_img [simp]:
assumes "arr f"
shows "set (img f) = Img f"
proof -
have 1: "Img f ⊆ Cod f ∧ setp (set (cod f))"
using assms Fun_mapsto by auto
hence "Fun f ` set (dom f) ⊆ Univ"
using setp_imp_subset_Univ by blast
thus ?thesis
using assms 1 img_def set_mkIde setp_respects_subset by auto
qed
lemma img_point_in_Univ:
assumes "«x : unity → a»"
shows "img x ∈ Univ"
proof -
have "set (img x) = {Fun x unity}"
using assms terminal_char2 terminal_unity⇩S⇩C by auto
thus "img x ∈ Univ" using assms terminal_char1 by auto
qed
lemma incl_in_img_cod:
assumes "arr f"
shows "incl_in (img f) (cod f)"
proof (unfold img_def)
have 1: "Img f ⊆ Cod f ∧ setp (Cod f)"
using assms Fun_mapsto by auto
hence 2: "ide (mkIde (Img f))"
using setp_respects_subset by auto
moreover have "ide (cod f)" using assms by auto
moreover have "set (mkIde (Img f)) ⊆ Cod f"
using 1 2 using setp_respects_subset by force
ultimately show "incl_in (mkIde (Img f)) (cod f)"
using assms incl_in_def ide_cod by blast
qed
lemma img_point_elem_set:
assumes "«x : unity → a»"
shows "img x ∈ set a"
by (metis assms img_point_in_Univ in_homE incl_in_img_cod insert_subset
mem_Collect_eq incl_in_def terminal_char2)
text‹
The corestriction of an arrow @{term f} is the arrow
@{term "corestr f ∈ hom (dom f) (img f)"} that induces the same function
on the universe as @{term f}.
›
definition corestr
where "corestr f = mkArr (Dom f) (Img f) (Fun f)"
lemma corestr_in_hom:
assumes "arr f"
shows "«corestr f : dom f → img f»"
by (metis assms corestr_def equalityD2 ide_dom ide_img image_subset_iff_funcset
mkIde_set set_img mkArr_in_hom setp_set_ide)
text‹
Every arrow factors as a corestriction followed by an inclusion.
›
lemma img_fact:
assumes "arr f"
shows "S (incl_of (img f) (cod f)) (corestr f) = f"
proof (intro arr_eqI⇩S⇩C)
have 1: "«corestr f : dom f → img f»"
using assms corestr_in_hom by blast
moreover have 2: "«incl_of (img f) (cod f) : img f → cod f»"
using assms incl_in_img_cod incl_incl_of by fast
ultimately show P: "par (incl_of (img f) (cod f) ⋅ corestr f) f"
using assms in_homE by blast
show "Fun (incl_of (img f) (cod f) ⋅ corestr f) = Fun f"
by (metis (no_types, lifting) 1 2 Fun_comp Fun_ide Fun_mkArr P comp_cod_arr
corestr_def ide_img in_homE mkArr_Fun)
qed
lemma Fun_corestr:
assumes "arr f"
shows "Fun (corestr f) = Fun f"
by (metis Fun_mkArr arrI assms corestr_def corestr_in_hom mkArr_Fun)
subsection "Points and Terminal Objects"
text‹
To each element @{term t} of @{term "set a"} is associated a point
@{term "mkPoint a t ∈ hom unity a"}. The function induced by such
a point is the constant-@{term t} function on the set @{term "{unity}"}.
›
definition mkPoint
where "mkPoint a t ≡ mkArr {unity} (set a) (λ_. t)"
lemma mkPoint_in_hom:
assumes "ide a" and "t ∈ set a"
shows "«mkPoint a t : unity → a»"
using assms mkArr_in_hom
by (metis Pi_I mkIde_set setp_set_ide terminal_char2 terminal_unity⇩S⇩C mkPoint_def)
lemma Fun_mkPoint:
assumes "ide a" and "t ∈ set a"
shows "Fun (mkPoint a t) = (λ_ ∈ {unity}. t)"
using assms mkPoint_def terminal_unity⇩S⇩C mkPoint_in_hom by fastforce
text‹
For each object @{term a} the function @{term "mkPoint a"} has as its inverse
the restriction of the function @{term img} to @{term "hom unity a"}
›
lemma mkPoint_img:
shows "img ∈ hom unity a → set a"
and "⋀x. «x : unity → a» ⟹ mkPoint a (img x) = x"
proof -
show "img ∈ hom unity a → set a"
using img_point_elem_set by simp
show "⋀x. «x : unity → a» ⟹ mkPoint a (img x) = x"
proof -
fix x
assume x: "«x : unity → a»"
show "mkPoint a (img x) = x"
proof (intro arr_eqI⇩S⇩C)
have 0: "img x ∈ set a"
using x img_point_elem_set by metis
hence 1: "mkPoint a (img x) ∈ hom unity a"
using x mkPoint_in_hom by force
thus 2: "par (mkPoint a (img x)) x"
using x by fastforce
have "Fun (mkPoint a (img x)) = (λ_ ∈ {unity}. img x)"
using 1 mkPoint_def by auto
also have "... = Fun x"
by (metis 0 Fun_corestr calculation elem_set_implies_set_eq_singleton
ide_cod ide_unity in_homE mem_Collect_eq Fun_mkPoint corestr_in_hom
img_point_in_Univ mkPoint_in_hom singletonI terminalE x)
finally show "Fun (mkPoint a (img x)) = Fun x" by auto
qed
qed
qed
lemma img_mkPoint:
assumes "ide a"
shows "mkPoint a ∈ set a → hom unity a"
and "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t"
proof -
show "mkPoint a ∈ set a → hom unity a"
using assms(1) mkPoint_in_hom by simp
show "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t"
proof -
fix t
assume t: "t ∈ set a"
show "img (mkPoint a t) = t"
proof -
have 1: "arr (mkPoint a t)"
using assms t mkPoint_in_hom by auto
have "Fun (mkPoint a t) ` {unity} = {t}"
using 1 mkPoint_def by simp
thus ?thesis
by (metis in_homE img_def mkIde_set mkPoint_in_hom elem_set_implies_incl_in
elem_set_implies_set_eq_singleton incl_in_def t terminal_char2 terminal_unity⇩S⇩C)
qed
qed
qed
text‹
For each object @{term a} the elements of @{term "hom unity a"} are therefore in
bijective correspondence with @{term "set a"}.
›
lemma bij_betw_points_and_set:
assumes "ide a"
shows "bij_betw img (hom unity a) (set a)"
proof (intro bij_betwI)
show "img ∈ hom unity a → set a"
using assms mkPoint_img by auto
show "mkPoint a ∈ set a → hom unity a"
using assms img_mkPoint by auto
show "⋀x. x ∈ hom unity a ⟹ mkPoint a (img x) = x"
using assms mkPoint_img by auto
show "⋀t. t ∈ set a ⟹ img (mkPoint a t) = t"
using assms img_mkPoint by auto
qed
lemma setp_img_points:
assumes "ide a"
shows "setp (img ` hom unity a)"
using assms
by (metis image_subset_iff_funcset mkPoint_img(1) setp_respects_subset setp_set_ide)
text‹
The function on the universe induced by an arrow @{term f} agrees, under the bijection
between @{term "hom unity (dom f)"} and @{term "Dom f"}, with the action of @{term f}
by composition on @{term "hom unity (dom f)"}.
›
lemma Fun_point:
assumes "«x : unity → a»"
shows "Fun x = (λ_ ∈ {unity}. img x)"
using assms mkPoint_img img_mkPoint Fun_mkPoint [of a "img x"] img_point_elem_set
by auto
lemma comp_arr_mkPoint:
assumes "arr f" and "t ∈ Dom f"
shows "f ⋅ mkPoint (dom f) t = mkPoint (cod f) (Fun f t)"
proof (intro arr_eqI⇩S⇩C)
have 0: "seq f (mkPoint (dom f) t)"
using assms mkPoint_in_hom [of "dom f" t] by auto
have 1: "«f ⋅ mkPoint (dom f) t : unity → cod f»"
using assms mkPoint_in_hom [of "dom f" t] by auto
show "par (f ⋅ mkPoint (dom f) t) (mkPoint (cod f) (Fun f t))"
proof -
have "«mkPoint (cod f) (Fun f t) : unity → cod f»"
using assms Fun_mapsto mkPoint_in_hom [of "cod f" "Fun f t"] by auto
thus ?thesis using 1 by fastforce
qed
show "Fun (f ⋅ mkPoint (dom f) t) = Fun (mkPoint (cod f) (Fun f t))"
proof -
have "Fun (f ⋅ mkPoint (dom f) t) = restrict (Fun f o Fun (mkPoint (dom f) t)) {unity}"
using assms 0 1 Fun_comp terminal_char2 terminal_unity⇩S⇩C by auto
also have "... = (λ_ ∈ {unity}. Fun f t)"
using assms Fun_mkPoint by auto
also have "... = Fun (mkPoint (cod f) (Fun f t))"
using assms Fun_mkPoint [of "cod f" "Fun f t"] Fun_mapsto by fastforce
finally show ?thesis by auto
qed
qed
lemma comp_arr_point⇩S⇩S⇩C:
assumes "arr f" and "«x : unity → dom f»"
shows "f ⋅ x = mkPoint (cod f) (Fun f (img x))"
by (metis assms comp_arr_mkPoint img_point_elem_set mkPoint_img(2))
text‹
This agreement allows us to express @{term "Fun f"} in terms of composition.
›
lemma Fun_in_terms_of_comp:
assumes "arr f"
shows "Fun f = restrict (img o S f o mkPoint (dom f)) (Dom f)"
proof
fix t
have "t ∉ Dom f ⟹ Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t"
using assms by (simp add: Fun_def)
moreover have "t ∈ Dom f ⟹
Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t"
proof -
assume t: "t ∈ Dom f"
have 1: "f ⋅ mkPoint (dom f) t = mkPoint (cod f) (Fun f t)"
using assms t comp_arr_mkPoint by simp
hence "img (f ⋅ mkPoint (dom f) t) = img (mkPoint (cod f) (Fun f t))" by simp
thus ?thesis
proof -
have "Fun f t ∈ Cod f" using assms t Fun_mapsto by auto
thus ?thesis using assms t 1 img_mkPoint by auto
qed
qed
ultimately show "Fun f t = restrict (img o S f o mkPoint (dom f)) (Dom f) t" by auto
qed
text‹
We therefore obtain a rule for proving parallel arrows equal by showing
that they have the same action by composition on points.
›
lemma arr_eqI'⇩S⇩C:
assumes "par f f'" and "⋀x. «x : unity → dom f» ⟹ f ⋅ x = f' ⋅ x"
shows "f = f'"
using assms Fun_in_terms_of_comp mkPoint_in_hom by (intro arr_eqI⇩S⇩C, auto)
text‹
An arrow can therefore be specified by giving its action by composition on points.
In many situations, this is more natural than specifying it as a function on the universe.
›
definition mkArr'
where "mkArr' a b F = mkArr (set a) (set b) (img o F o mkPoint a)"
lemma mkArr'_in_hom:
assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b"
shows "«mkArr' a b F : a → b»"
proof -
have "img o F o mkPoint a ∈ set a → set b"
using assms(1,3) img_mkPoint(1) mkPoint_img(1) by fastforce
thus ?thesis
using assms mkArr'_def mkArr_in_hom [of "set a" "set b"] mkIde_set by simp
qed
lemma comp_point_mkArr':
assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b"
shows "⋀x. «x : unity → a» ⟹ mkArr' a b F ⋅ x = F x"
proof -
fix x
assume x: "«x : unity → a»"
have "Fun (mkArr' a b F) (img x) = img (F x)"
unfolding mkArr'_def
using assms x Fun_mkArr img_point_elem_set mkPoint_img mkPoint_in_hom
by (simp add: Pi_iff)
hence "mkArr' a b F ⋅ x = mkPoint b (img (F x))"
using assms x mkArr'_in_hom [of a b F] comp_arr_point⇩S⇩S⇩C by auto
thus "mkArr' a b F ⋅ x = F x"
using assms x mkPoint_img(2) by auto
qed
text‹
A third characterization of terminal objects is as those objects whose set of
points is a singleton.
›
lemma terminal_char3:
assumes "∃!x. «x : unity → a»"
shows "terminal a"
proof -
have a: "ide a"
using assms ide_cod mem_Collect_eq by blast
hence "bij_betw img (hom unity a) (set a)"
using assms bij_betw_points_and_set by auto
hence "img ` (hom unity a) = set a"
by (simp add: bij_betw_def)
moreover have "hom unity a = {THE x. x ∈ hom unity a}"
using assms theI' [of "λx. x ∈ hom unity a"] by auto
ultimately have "set a = {img (THE x. x ∈ hom unity a)}"
by (metis image_empty image_insert)
thus ?thesis using a terminal_char1 by simp
qed
text‹
The following is an alternative formulation of functional completeness, which says that
any function on points uniquely determines an arrow.
›
lemma fun_complete':
assumes "ide a" and "ide b" and "F ∈ hom unity a → hom unity b"
shows "∃!f. «f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = F x)"
proof
have 1: "«mkArr' a b F : a → b»" using assms mkArr'_in_hom by auto
moreover have 2: "⋀x. «x : unity → a» ⟹ mkArr' a b F ⋅ x = F x"
using assms comp_point_mkArr' by auto
ultimately show "«mkArr' a b F : a → b» ∧
(∀x. «x : unity → a» ⟶ mkArr' a b F ⋅ x = F x)" by blast
fix f
assume f: "«f : a → b» ∧ (∀x. «x : unity → a» ⟶ f ⋅ x = F x)"
show "f = mkArr' a b F"
using f 1 2 by (intro arr_eqI'⇩S⇩C [of f "mkArr' a b F"], fastforce, auto)
qed
subsection "The `Determines Same Function' Relation on Arrows"
text‹
An important part of understanding the structure of a category of sets and functions
is to characterize when it is that two arrows ``determine the same function''.
The following result provides one answer to this: two arrows with a common domain
determine the same function if and only if they can be rendered equal by composing with
a cospan of inclusions.
›
lemma eq_Fun_iff_incl_joinable:
assumes "span f f'"
shows "Fun f = Fun f' ⟷
(∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f')"
proof
assume ff': "Fun f = Fun f'"
let ?b = "mkIde (Cod f ∪ Cod f')"
let ?m = "incl_of (cod f) ?b"
let ?m' = "incl_of (cod f') ?b"
have incl_m: "incl ?m"
using assms incl_incl_of [of "cod f" ?b] incl_in_def setp_respects_union by simp
have incl_m': "incl ?m'"
using assms incl_incl_of [of "cod f'" ?b] incl_in_def setp_respects_union by simp
have m: "?m = mkArr (Cod f) (Cod f ∪ Cod f') (λx. x)"
using setp_respects_union by (simp add: assms)
have m': "?m' = mkArr (Cod f') (Cod f ∪ Cod f') (λx. x)"
using setp_respects_union by (simp add: assms)
have seq: "seq ?m f ∧ seq ?m' f'"
using assms m m' using setp_respects_union by simp
have "?m ⋅ f = ?m' ⋅ f'"
by (metis assms comp_mkArr ff' incl_def incl_m incl_m' mkArr_Fun)
hence "incl ?m ∧ incl ?m' ∧ seq ?m f ∧ seq ?m' f' ∧ ?m ⋅ f = ?m' ⋅ f'"
using seq ‹incl ?m› ‹incl ?m'› by simp
thus "∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f'" by auto
next
assume ff': "∃m m'. incl m ∧ incl m' ∧ seq m f ∧ seq m' f' ∧ m ⋅ f = m' ⋅ f'"
show "Fun f = Fun f'"
using ff'
by (metis Fun_comp Fun_ide comp_cod_arr ide_cod seqE Fun_incl)
qed
text‹
Another answer to the same question: two arrows with a common domain determine the
same function if and only if their corestrictions are equal.
›
lemma eq_Fun_iff_eq_corestr:
assumes "span f f'"
shows "Fun f = Fun f' ⟷ corestr f = corestr f'"
using assms corestr_def Fun_corestr by metis
subsection "Retractions, Sections, and Isomorphisms"
text‹
An arrow is a retraction if and only if its image coincides with its codomain.
›
lemma retraction_if_Img_eq_Cod:
assumes "arr g" and "Img g = Cod g"
shows "retraction g"
and "ide (g ⋅ mkArr (Cod g) (Dom g) (inv_into (Dom g) (Fun g)))"
proof -
let ?F = "inv_into (Dom g) (Fun g)"
let ?f = "mkArr (Cod g) (Dom g) ?F"
have f: "arr ?f"
by (simp add: assms inv_into_into)
show "ide (g ⋅ ?f)"
proof -
have "g = mkArr (Dom g) (Cod g) (Fun g)" using assms mkArr_Fun by auto
hence "g ⋅ ?f = mkArr (Cod g) (Cod g) (Fun g o ?F)"
using assms(1) f comp_mkArr by metis
moreover have "mkArr (Cod g) (Cod g) (λy. y) = ..."
proof (intro mkArr_eqI')
show "arr (mkArr (Cod g) (Cod g) (λy. y))"
using assms arr_cod_iff_arr by auto
show "⋀y. y ∈ Cod g ⟹ y = (Fun g o ?F) y"
using assms by (simp add: f_inv_into_f)
qed
ultimately show ?thesis
using assms f mkIde_as_mkArr by auto
qed
thus "retraction g" by auto
qed
lemma retraction_char:
shows "retraction g ⟷ arr g ∧ Img g = Cod g"
proof
assume G: "retraction g"
show "arr g ∧ Img g = Cod g"
proof
show "arr g" using G by blast
show "Img g = Cod g"
proof -
from G obtain f where f: "ide (g ⋅ f)" by blast
have "Fun g ` Fun f ` Cod g = Cod g"
proof -
have "restrict (Fun g o Fun f) (Cod g) = restrict (λx. x) (Cod g)"
using f Fun_comp Fun_ide ide_compE by metis
thus ?thesis
by (metis image_comp image_ident image_restrict_eq)
qed
moreover have "Fun f ` Cod g ⊆ Dom g"
using f Fun_mapsto arr_mkArr mkArr_Fun funcset_image
by (metis seqE ide_compE ide_compE)
moreover have "Img g ⊆ Cod g"
using f Fun_mapsto by blast
ultimately show ?thesis by blast
qed
qed
next
assume "arr g ∧ Img g = Cod g"
thus "retraction g" using retraction_if_Img_eq_Cod by blast
qed
text‹
Every corestriction is a retraction.
›
lemma retraction_corestr:
assumes "arr f"
shows "retraction (corestr f)"
using assms retraction_char Fun_corestr corestr_in_hom in_homE set_img
by metis
text‹
An arrow is a section if and only if it induces an injective function on its
domain, except in the special case that it has an empty domain set and a
nonempty codomain set.
›
lemma section_if_inj:
assumes "arr f" and "inj_on (Fun f) (Dom f)" and "Dom f = {} ⟶ Cod f = {}"
shows "section f"
and "ide (mkArr (Cod f) (Dom f)
(λy. if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
else SOME x. x ∈ Dom f)
⋅ f)"
proof -
let ?P= "λy. λx. x ∈ Dom f ∧ Fun f x = y"
let ?G = "λy. if y ∈ Img f then SOME x. ?P y x else SOME x. x ∈ Dom f"
let ?g = "mkArr (Cod f) (Dom f) ?G"
have g: "arr ?g"
proof -
have 1: "setp (Cod f)" using assms by simp
have 2: "setp (Dom f)" using assms by simp
have 3: "?G ∈ Cod f → Dom f"
proof
fix y
assume Y: "y ∈ Cod f"
show "?G y ∈ Dom f"
proof (cases "y ∈ Img f")
assume "y ∈ Img f"
hence "(∃x. ?P y x) ∧ ?G y = (SOME x. ?P y x)" using Y by auto
hence "?P y (?G y)" using someI_ex [of "?P y"] by argo
thus "?G y ∈ Dom f" by auto
next
assume "y ∉ Img f"
hence "(∃x. x ∈ Dom f) ∧ ?G y = (SOME x. x ∈ Dom f)" using assms Y by auto
thus "?G y ∈ Dom f" using someI_ex [of "λx. x ∈ Dom f"] by argo
qed
qed
show ?thesis using 1 2 3 by simp
qed
show "ide (?g ⋅ f)"
proof -
have "f = mkArr (Dom f) (Cod f) (Fun f)" using assms mkArr_Fun by auto
hence "?g ⋅ f = mkArr (Dom f) (Dom f) (?G o Fun f)"
using assms(1) g comp_mkArr [of "Dom f" "Cod f" "Fun f" "Dom f" ?G] by argo
moreover have "mkArr (Dom f) (Dom f) (λx. x) = ..."
proof (intro mkArr_eqI')
show "arr (mkArr (Dom f) (Dom f) (λx. x))"
using assms by auto
show "⋀x. x ∈ Dom f ⟹ x = (?G o Fun f) x"
proof -
fix x
assume x: "x ∈ Dom f"
have "Fun f x ∈ Img f" using x by blast
hence *: "(∃x'. ?P (Fun f x) x') ∧ ?G (Fun f x) = (SOME x'. ?P (Fun f x) x')"
by auto
then have "?P (Fun f x) (?G (Fun f x))"
using someI_ex [of "?P (Fun f x)"] by argo
with * have "x = ?G (Fun f x)"
using assms x inj_on_def [of "Fun f" "Dom f"] by simp
thus "x = (?G o Fun f) x" by simp
qed
qed
ultimately show ?thesis
using assms mkIde_as_mkArr mkIde_set by auto
qed
thus "section f" by auto
qed
lemma section_char:
shows "section f ⟷ arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
proof
assume f: "section f"
from f obtain g where g: "ide (g ⋅ f)" using section_def by blast
show "arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
proof -
have "arr f" using f by blast
moreover have "Dom f = {} ⟶ Cod f = {}"
proof -
have "Cod f ≠ {} ⟶ Dom f ≠ {}"
proof
assume "Cod f ≠ {}"
from this obtain y where "y ∈ Cod f" by blast
hence "Fun g y ∈ Dom f"
using g Fun_mapsto
by (metis seqE ide_compE image_eqI retractionI retraction_char)
thus "Dom f ≠ {}" by blast
qed
thus ?thesis by auto
qed
moreover have "inj_on (Fun f) (Dom f)"
by (metis Fun_comp Fun_ide g ide_compE inj_on_id2 inj_on_imageI2 inj_on_restrict_eq)
ultimately show ?thesis by auto
qed
next
assume F: "arr f ∧ (Dom f = {} ⟶ Cod f = {}) ∧ inj_on (Fun f) (Dom f)"
thus "section f" using section_if_inj by auto
qed
text‹
Section-retraction pairs can also be characterized by an inverse relationship
between the functions they induce.
›
lemma section_retraction_char:
shows "ide (g ⋅ f) ⟷ antipar f g ∧ compose (Dom f) (Fun g) (Fun f) = (λx ∈ Dom f. x)"
by (metis Fun_comp cod_comp compose_eq' dom_comp ide_char⇩S⇩C ide_compE seqE)
text‹
Antiparallel arrows @{term f} and @{term g} are inverses if the functions
they induce are inverses.
›
lemma inverse_arrows_char:
shows "inverse_arrows f g ⟷
antipar f g ∧ compose (Dom f) (Fun g) (Fun f) = (λx ∈ Dom f. x)
∧ compose (Dom g) (Fun f) (Fun g) = (λy ∈ Dom g. y)"
using section_retraction_char by blast
text‹
An arrow is an isomorphism if and only if the function it induces is a bijection.
›
lemma iso_char:
shows "iso f ⟷ arr f ∧ bij_betw (Fun f) (Dom f) (Cod f)"
by (metis bij_betw_def image_empty iso_iff_section_and_retraction retraction_char
section_char)
text‹
The inverse of an isomorphism is constructed by inverting the induced function.
›
lemma inv_char:
assumes "iso f"
shows "inv f = mkArr (Cod f) (Dom f) (inv_into (Dom f) (Fun f))"
proof -
let ?g = "mkArr (Cod f) (Dom f) (inv_into (Dom f) (Fun f))"
have "ide (f ⋅ ?g)"
using assms iso_is_retraction retraction_char retraction_if_Img_eq_Cod by simp
moreover have "ide (?g ⋅ f)"
proof -
let ?g' = "mkArr (Cod f) (Dom f)
(λy. if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
else SOME x. x ∈ Dom f)"
have 1: "ide (?g' ⋅ f)"
using assms iso_is_section section_char section_if_inj by simp
moreover have "?g' = ?g"
proof
show "arr ?g'" using 1 ide_compE by blast
show "⋀y. y ∈ Cod f ⟹ (if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
else SOME x. x ∈ Dom f)
= inv_into (Dom f) (Fun f) y"
proof -
fix y
assume "y ∈ Cod f"
hence "y ∈ Img f" using assms iso_is_retraction retraction_char by metis
thus "(if y ∈ Img f then SOME x. x ∈ Dom f ∧ Fun f x = y
else SOME x. x ∈ Dom f)
= inv_into (Dom f) (Fun f) y"
using inv_into_def by metis
qed
qed
ultimately show ?thesis by auto
qed
ultimately have "inverse_arrows f ?g" by auto
thus ?thesis using inverse_unique by blast
qed
lemma Fun_inv:
assumes "iso f"
shows "Fun (inv f) = restrict (inv_into (Dom f) (Fun f)) (Cod f)"
using assms inv_in_hom inv_char iso_inv_iso iso_is_arr Fun_mkArr by metis
subsection "Monomorphisms and Epimorphisms"
text‹
An arrow is a monomorphism if and only if the function it induces is injective.
›
lemma mono_char:
shows "mono f ⟷ arr f ∧ inj_on (Fun f) (Dom f)"
proof
assume f: "mono f"
hence "arr f" using mono_def by auto
moreover have "inj_on (Fun f) (Dom f)"
proof (intro inj_onI)
have 0: "inj_on (S f) (hom unity (dom f))"
proof -
have "hom unity (dom f) ⊆ {g. seq f g}"
using f mono_def arrI by auto
hence "∃A. hom unity (dom f) ⊆ A ∧ inj_on (S f) A"
using f mono_def by auto
thus ?thesis
by (meson subset_inj_on)
qed
fix x x'
assume x: "x ∈ Dom f" and x': "x' ∈ Dom f" and xx': "Fun f x = Fun f x'"
have "mkPoint (dom f) x ∈ hom unity (dom f) ∧
mkPoint (dom f) x' ∈ hom unity (dom f)"
using x x' ‹arr f› mkPoint_in_hom by simp
moreover have "f ⋅ mkPoint (dom f) x = f ⋅ mkPoint (dom f) x'"
using ‹arr f› x x' xx' comp_arr_mkPoint by simp
ultimately have "mkPoint (dom f) x = mkPoint (dom f) x'"
using 0 inj_onD [of "S f" "hom unity (dom f)" "mkPoint (dom f) x"] by simp
thus "x = x'"
using ‹arr f› x x' img_mkPoint(2) img_mkPoint(2) ide_dom by metis
qed
ultimately show "arr f ∧ inj_on (Fun f) (Dom f)" by auto
next
assume f: "arr f ∧ inj_on (Fun f) (Dom f)"
show "mono f"
proof
show "arr f" using f by auto
show "⋀g g'. ⟦seq f g; seq f g'; f ⋅ g = f ⋅ g'⟧ ⟹ g = g'"
proof -
fix g g'
assume fg: "seq f g" and fg': "seq f g'" and eq: "f ⋅ g = f ⋅ g'"
show "g = g'"
proof (intro arr_eqI⇩S⇩C)
show par: "par g g'"
using fg' eq dom_comp by (metis seqE)
show "Fun g = Fun g'"
by (metis empty_is_image eq f fg' ide_dom incl_in_def incl_in_img_cod
initial_arr_unique initial_empty empty_def monoE mkIde_set
section_if_inj(1) section_is_mono seqE set_img subset_empty)
qed
qed
qed
qed
text‹
Inclusions are monomorphisms.
›
lemma mono_imp_incl:
assumes "incl f"
shows "mono f"
using assms incl_def Fun_incl mono_char by auto
text‹
A monomorphism is a section, except in case it has an empty domain set and
a nonempty codomain set.
›
lemma mono_imp_section:
assumes "mono f" and "Dom f = {} ⟶ Cod f = {}"
shows "section f"
using assms mono_char section_char by auto
text‹
An arrow is an epimorphism if and only if either its image coincides with its
codomain, or else the universe has only a single element (in which case all arrows
are epimorphisms).
›
lemma epi_char:
shows "epi f ⟷ arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
proof
assume epi: "epi f"
show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
proof -
have f: "arr f" using epi epi_implies_arr by auto
moreover have "¬(∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t') ⟹ Img f = Cod f"
proof -
assume "¬(∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')"
from this obtain tt and ff
where B: "tt ∈ Univ ∧ ff ∈ Univ ∧ tt ≠ ff" by blast
show "Img f = Cod f"
proof
show "Img f ⊆ Cod f" using f Fun_mapsto by auto
show "Cod f ⊆ Img f"
proof
let ?g = "mkArr (Cod f) {ff, tt} (λy. tt)"
let ?g' = "mkArr (Cod f) {ff, tt} (λy. if ∃x. x ∈ Dom f ∧ Fun f x = y
then tt else ff)"
let ?b = "mkIde {ff, tt}"
have b: "ide ?b"
by (metis B finite.emptyI finite_imp_setp finite_insert ide_mkIde
insert_subset setp_imp_subset_Univ setp_singleton mem_Collect_eq)
have g: "«?g : cod f → ?b» ∧ Fun ?g = (λy ∈ Cod f. tt)"
using f B in_homI [of ?g "cod f" "mkIde {ff, tt}"] finite_imp_setp by simp
have g': "?g' ∈ hom (cod f) ?b ∧
Fun ?g' = (λy ∈ Cod f. if ∃x. x ∈ Dom f ∧ Fun f x = y then tt else ff)"
using f B in_homI [of ?g'] finite_imp_setp by simp
have "?g ⋅ f = ?g' ⋅ f"
proof (intro arr_eqI⇩S⇩C)
show "par (?g ⋅ f) (?g' ⋅ f)"
using f g g' by auto
show "Fun (?g ⋅ f) = Fun (?g' ⋅ f)"
using f g g' Fun_comp comp_mkArr by fastforce
qed
hence gg': "?g = ?g'"
by (metis (no_types, lifting) epiE epi f g in_homE seqI)
fix y
assume y: "y ∈ Cod f"
have "Fun ?g' y = tt" using gg' g y by simp
hence "(if ∃x. x ∈ Dom f ∧ Fun f x = y then tt else ff) = tt"
using g' y by simp
hence "∃x. x ∈ Dom f ∧ Fun f x = y"
using B by argo
thus "y ∈ Img f" by blast
qed
qed
qed
ultimately show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))"
by fast
qed
next
show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')) ⟹ epi f"
proof -
have "arr f ∧ Img f = Cod f ⟹ epi f"
using retraction_char retraction_is_epi by presburger
moreover have "arr f ∧ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t') ⟹ epi f"
proof -
assume f: "arr f ∧ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t')"
have "⋀f f'. par f f' ⟹ f = f'"
proof -
fix f f'
assume ff': "par f f'"
show "f = f'"
proof (intro arr_eqI⇩S⇩C)
show "par f f'" using ff' by simp
have "⋀t t'. t ∈ Cod f ∧ t' ∈ Cod f ⟹ t = t'"
using f ff' setp_imp_subset_Univ setp_set_ide ide_cod subsetD by blast
thus "Fun f = Fun f'"
using ff' Fun_mapsto [of f] Fun_mapsto [of f']
extensional_arb [of "Fun f" "Dom f"] extensional_arb [of "Fun f'" "Dom f"]
by fastforce
qed
qed
moreover have "⋀g g'. par (g ⋅ f) (g' ⋅ f) ⟹ par g g'"
by force
ultimately show "epi f"
using f by (intro epiI; metis)
qed
ultimately show "arr f ∧ (Img f = Cod f ∨ (∀t t'. t ∈ Univ ∧ t' ∈ Univ ⟶ t = t'))
⟹ epi f"
by auto
qed
qed
text‹
An epimorphism is a retraction, except in the case of a degenerate universe with only
a single element.
›
lemma epi_imp_retraction:
assumes "epi f" and "∃t t'. t ∈ Univ ∧ t' ∈ Univ ∧ t ≠ t'"
shows "retraction f"
using assms epi_char retraction_char by auto
text‹
Retraction/inclusion factorization is unique (not just up to isomorphism -- remember
that the notion of inclusion is not categorical but depends on the arbitrarily chosen
@{term img}).
›
lemma unique_retr_incl_fact:
assumes "seq m e" and "seq m' e'" and "m ⋅ e = m' ⋅ e'"
and "incl m" and "incl m'" and "retraction e" and "retraction e'"
shows "m = m'" and "e = e'"
proof -
have 1: "cod m = cod m' ∧ dom e = dom e'"
using assms(1-3) by (metis dom_comp cod_comp)
hence 2: "span e e'" using assms(1-2) by blast
hence 3: "Fun e = Fun e'"
using assms eq_Fun_iff_incl_joinable by meson
hence "img e = img e'" using assms 1 img_def by auto
moreover have "img e = cod e ∧ img e' = cod e'"
using assms(6-7) retraction_char img_def mkIde_set by simp
ultimately have "par e e'" using 2 by simp
thus "e = e'" using 3 arr_eqI⇩S⇩C by blast
hence "par m m'" using assms(1) assms(2) 1 by fastforce
thus "m = m'" using assms(4) assms(5) incls_coherent by blast
qed
end
section "Concrete Set Categories"
text‹
The ‹set_category› locale is useful for stating results that depend on a
category of @{typ 'a}-sets and functions, without having to commit to a particular
element type @{typ 'a}. However, in applications we often need to work with a
category of sets and functions that is guaranteed to contain sets corresponding
to the subsets of some extrinsically given type @{typ 'a}.
A \emph{concrete set category} is a set category ‹S› that is equipped
with an injective function @{term ι} from type @{typ 'a} to ‹S.Univ›.
The following locale serves to facilitate some of the technical aspects of passing
back and forth between elements of type @{typ 'a} and the elements of ‹S.Univ›.
›
locale concrete_set_category = set_category S setp
for S :: "'s comp" (infixr ‹⋅⇩S› 55)
and setp :: "'s set ⇒ bool"
and U :: "'a set"
and ι :: "'a ⇒ 's" +
assumes UP_mapsto: "ι ∈ U → Univ"
and inj_UP: "inj_on ι U"
begin
abbreviation UP
where "UP ≡ ι"
abbreviation DN
where "DN ≡ inv_into U UP"
lemma DN_mapsto:
shows "DN ∈ UP ` U → U"
by (simp add: inv_into_into)
lemma DN_UP [simp]:
assumes "x ∈ U"
shows "DN (UP x) = x"
using assms inj_UP inv_into_f_f by simp
lemma UP_DN [simp]:
assumes "t ∈ UP ` U"
shows "UP (DN t) = t"
using assms o_def inj_UP by auto
lemma bij_UP:
shows "bij_betw UP U (UP ` U)"
using inj_UP inj_on_imp_bij_betw by blast
lemma bij_DN:
shows "bij_betw DN (UP ` U) U"
using bij_UP bij_betw_inv_into by blast
end
locale replete_concrete_set_category =
replete_set_category S +
concrete_set_category S ‹λA. A ⊆ Univ› U UP
for S :: "'s comp" (infixr ‹⋅⇩S› 55)
and U :: "'a set"
and UP :: "'a ⇒ 's"
section "Sub-Set Categories"
text‹
In this section, we show that a full subcategory of a set category, obtained
by imposing suitable further restrictions on the subsets of the universe
that correspond to objects, is again a set category.
›
locale sub_set_category =
S: set_category +
fixes ssetp :: "'a set ⇒ bool"
assumes ssetp_singleton: "⋀t. t ∈ S.Univ ⟹ ssetp {t}"
and subset_closed: "⋀B A. ⟦B ⊆ A; ssetp A⟧ ⟹ ssetp B"
and union_closed: "⋀A B. ⟦ssetp A; ssetp B⟧ ⟹ ssetp (A ∪ B)"
and containment: "⋀A. ssetp A ⟹ setp A"
begin
sublocale full_subcategory S ‹λa. S.ide a ∧ ssetp (S.set a)›
by unfold_locales auto
lemma is_full_subcategory:
shows "full_subcategory S (λa. S.ide a ∧ ssetp (S.set a))"
..
lemma ide_char⇩S⇩S⇩C:
shows "ide a ⟷ S.ide a ∧ ssetp (S.set a)"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C by fastforce
lemma terminal_unity⇩S⇩S⇩C:
shows "terminal S.unity"
proof
show "ide S.unity"
using S.terminal_unity⇩S⇩C S.terminal_def [of S.unity] S.terminal_char2 ide_char⇩S⇩S⇩C
ssetp_singleton
by force
thus "⋀a. ide a ⟹ ∃!f. in_hom f a S.unity"
using S.terminal_unity⇩S⇩C S.terminal_def ide_char⇩S⇩b⇩C ide_char' in_hom_char⇩F⇩S⇩b⇩C
by (metis (no_types, lifting))
qed
lemma terminal_char:
shows "terminal t ⟷ S.terminal t"
proof
fix t
assume t: "S.terminal t"
have "ide t"
using t ssetp_singleton ide_char⇩S⇩S⇩C S.terminal_char2 by force
thus "terminal t"
using t in_hom_char⇩F⇩S⇩b⇩C ide_char⇩S⇩S⇩C arr_char⇩S⇩b⇩C S.terminal_def terminalI by auto
next
assume t: "terminal t"
have 1: "S.ide t"
using t ide_char⇩S⇩b⇩C terminal_def by simp
moreover have "card (S.set t) = 1"
proof -
have "card (S.set t) = card (S.hom S.unity t)"
using S.set_def S.inj_img
by (metis 1 S.bij_betw_points_and_set bij_betw_same_card)
also have "... = card (hom S.unity t)"
using t in_hom_char⇩F⇩S⇩b⇩C terminal_def terminal_unity⇩S⇩S⇩C by auto
also have "... = 1"
proof -
have "∃!f. f ∈ hom S.unity t"
using t terminal_def terminal_unity⇩S⇩S⇩C by force
moreover have "⋀A. card A = 1 ⟷ (∃!a. a ∈ A)"
apply (intro iffI)
apply (metis card_1_singletonE empty_iff insert_iff)
using card_1_singleton_iff by auto
ultimately show ?thesis by auto
qed
finally show ?thesis by blast
qed
ultimately show "S.terminal t"
using 1 S.terminal_char1 card_1_singleton_iff
by (metis One_nat_def singleton_iff)
qed
sublocale set_category comp ssetp
proof
text‹
Here things are simpler if we define ‹img› appropriately so that we have
‹set = T.set› after accounting for the definition ‹unity ≡ SOME t. terminal t›,
which is different from that of S.unity.
›
have 1: "terminal (SOME t. terminal t)"
using terminal_unity⇩S⇩S⇩C someI_ex [of terminal] by blast
obtain i where i: "«i : S.unity → SOME t. terminal t»"
using terminal_unity⇩S⇩S⇩C someI_ex [of terminal] in_hom_char⇩F⇩S⇩b⇩C terminal_def
by auto
obtain i' where i': "«i' : (SOME t. terminal t) → S.unity»"
using terminal_unity⇩S⇩S⇩C someI_ex [of S.terminal] S.terminal_def
by (metis (no_types, lifting) 1 terminal_def)
have ii': "inverse_arrows i i'"
proof
have "i' ⋅ i = S.unity"
using i i' terminal_unity⇩S⇩S⇩C
by (metis (no_types, lifting) S.comp_in_homI' S.ide_in_hom S.ide_unity S.in_homE
S.terminalE S.terminal_unity⇩S⇩C in_hom_char⇩F⇩S⇩b⇩C)
thus 2: "ide (comp i' i)"
by (metis (no_types, lifting) cod_comp comp_simp i i' ide_char' in_homE seqI')
have "i ⋅ i' = (SOME t. terminal t)"
using 1
by (metis (no_types, lifting) 2 comp_simp i' ide_compE in_homE inverse_arrowsE
iso_iff_mono_and_retraction point_is_mono retractionI section_retraction_of_iso(2))
thus "ide (comp i i')"
using comp_char
by (metis (no_types, lifting) 2 ide_char' dom_comp i' ide_compE in_homE seq_char⇩S⇩b⇩C)
qed
interpret set_category_data comp ‹λx. S.some_img (x ⋅ i)› ..
have i_in_hom: "«i : S.unity → unity»"
using i unity_def by simp
have i'_in_hom: "«i' : unity → S.unity»"
using i' unity_def by simp
have "⋀a. ide a ⟹ set a = S.set a"
proof -
fix a
assume a: "ide a"
have "set a = (λx. S.some_img (x ⋅ i)) ` hom unity a"
using set_def by simp
also have "... = S.some_img ` S.hom S.unity a"
proof
show "(λx. S.some_img (x ⋅ i)) ` hom unity a ⊆ S.some_img ` S.hom S.unity a"
using i in_hom_char⇩F⇩S⇩b⇩C i_in_hom by auto
show "S.some_img ` S.hom S.unity a ⊆ (λx. S.some_img (x ⋅ i)) ` hom unity a"
proof
fix b
assume b: "b ∈ S.some_img ` S.hom S.unity a"
obtain x where x: "x ∈ S.hom S.unity a ∧ S.some_img x = b"
using b by blast
have "x ⋅ i' ∈ hom unity a"
using x in_hom_char⇩F⇩S⇩b⇩C S.comp_in_homI a i' ideD(1) unity_def by force
moreover have "S.some_img ((x ⋅ i') ⋅ i) = b"
by (metis (no_types, lifting) i ii' x S.comp_assoc calculation comp_simp
ide_compE in_homE inverse_arrowsE mem_Collect_eq S.comp_arr_ide seqI'
seq_char⇩S⇩b⇩C S.ide_unity unity_def)
ultimately show "b ∈ (λx. S.some_img (x ⋅ i)) ` hom unity a" by blast
qed
qed
also have "... = S.set a"
using S.set_def by auto
finally show "set a = S.set a" by blast
qed
interpret T: set_category_given_img comp ‹λx. S.some_img (x ⋅ i)› ssetp
proof
show "Collect terminal ≠ {}"
using terminal_unity⇩S⇩S⇩C by blast
show "⋀A' A. ⟦A' ⊆ A; ssetp A⟧ ⟹ ssetp A'"
using subset_closed by blast
show "⋀A B. ⟦ssetp A; ssetp B⟧ ⟹ ssetp (A ∪ B)"
using union_closed by simp
show "⋀A. ssetp A ⟹ A ⊆ Univ"
using S.setp_imp_subset_Univ containment terminal_char by presburger
show "⋀a b. ⟦ide a; ide b; set a = set b⟧ ⟹ a = b"
using ide_char⇩S⇩b⇩C ‹⋀a. ide a ⟹ set a = S.set a› S.extensional_set by auto
show "⋀a. ide a ⟹ ssetp (set a)"
using ‹⋀a. ide a ⟹ set a = S.set a› ide_char⇩S⇩S⇩C by force
show "⋀A. ssetp A ⟹ ∃a. ide a ∧ set a = A"
using S.set_complete ‹⋀a. ide a ⟹ set a = S.set a› containment ide_char⇩S⇩S⇩C by blast
show "⋀t. terminal t ⟹ t ∈ (λx. S.some_img (x ⋅ i)) ` hom unity t"
using S.set_def S.stable_img ‹⋀a. ide a ⟹ set a = S.set a› set_def
terminal_char terminal_def
by force
show "⋀a. ide a ⟹ inj_on (λx. S.some_img (x ⋅ i)) (hom unity a)"
proof -
fix a
assume a: "ide a"
show "inj_on (λx. S.some_img (x ⋅ i)) (hom unity a)"
proof
fix x y
assume x: "x ∈ hom unity a" and y: "y ∈ hom unity a"
and eq: "S.some_img (x ⋅ i) = S.some_img (y ⋅ i)"
have "x ⋅ i = y ⋅ i"
proof -
have "x ⋅ i ∈ S.hom S.unity a ∧ y ⋅ i ∈ S.hom S.unity a"
using in_hom_char⇩F⇩S⇩b⇩C ‹«i : S.unity → unity»› x y by blast
thus ?thesis
using a eq ide_char⇩S⇩b⇩C S.inj_img [of a] inj_on_def [of S.some_img] by simp
qed
have "x = (x ⋅ i) ⋅ i'"
by (metis (no_types, lifting) S.comp_arr_ide S.comp_assoc S.inverse_arrowsE
S.match_4 i i' ii' inclusion_preserves_inverse mem_Collect_eq seqI'
seq_char⇩S⇩b⇩C unity_def x)
also have "... = (y ⋅ i) ⋅ i'"
using ‹x ⋅ i = y ⋅ i› by simp
also have "... = y"
by (metis (no_types, lifting) S.comp_arr_ide S.comp_assoc S.inverse_arrowsE
S.match_4 i i' ii' inclusion_preserves_inverse mem_Collect_eq seqI'
seq_char⇩S⇩b⇩C unity_def y)
finally show "x = y" by simp
qed
qed
show "⋀f f'. ⟦par f f'; ⋀x. in_hom x unity (dom f) ⟹ comp f x = comp f' x⟧
⟹ f = f'"
proof -
fix f f'
assume par: "par f f'"
assume eq: "⋀x. in_hom x unity (dom f) ⟹ comp f x = comp f' x"
have "S.par f f'"
using par arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C by auto
moreover have "⋀x. S.in_hom x S.unity (S.dom f) ⟹ f ⋅ x = f' ⋅ x"
proof -
fix x
assume x: "S.in_hom x S.unity (S.dom f)"
have "S.in_hom (x ⋅ i') unity (S.dom f)"
using i'_in_hom in_hom_char⇩F⇩S⇩b⇩C x by blast
hence 1: "in_hom (x ⋅ i') unity (dom f)"
using arr_dom dom_simp i in_hom_char⇩F⇩S⇩b⇩C par unity_def by force
hence "comp f (x ⋅ i') = comp f' (x ⋅ i')"
using eq by blast
hence "(f ⋅ (x ⋅ i')) ⋅ i = (f' ⋅ (x ⋅ i')) ⋅ i"
using comp_char
by (metis (no_types, lifting) 1 comp_simp in_homE seqI par)
thus "f ⋅ x = f' ⋅ x"
by (metis (no_types, lifting) S.comp_arr_dom S.comp_assoc S.comp_inv_arr
S.in_homE i_in_hom ii' in_hom_char⇩F⇩S⇩b⇩C inclusion_preserves_inverse x)
qed
ultimately show "f = f'"
using S.extensional_arr by blast
qed
show "⋀a b F. ⟦ide a; ide b; F ∈ hom unity a → hom unity b⟧
⟹ ∃f. in_hom f a b ∧
(∀x. in_hom x unity (dom f) ⟶ comp f x = F x)"
proof -
fix a b F
assume a: "ide a" and b: "ide b" and F: "F ∈ hom unity a → hom unity b"
have "S.ide a"
using a ide_char⇩S⇩b⇩C by blast
have "S.ide b"
using b ide_char⇩S⇩b⇩C by blast
have 1: "(λx. F (x ⋅ i') ⋅ i) ∈ S.hom S.unity a → S.hom S.unity b"
proof
fix x
assume x: "x ∈ S.hom S.unity a"
have "x ⋅ i' ∈ S.hom unity a"
using i'_in_hom in_hom_char⇩F⇩S⇩b⇩C x by blast
hence "x ⋅ i' ∈ hom unity a"
using a in_hom_char⇩F⇩S⇩b⇩C
by (metis (no_types, lifting) ideD(1) i'_in_hom in_hom_char⇩F⇩S⇩b⇩C mem_Collect_eq)
hence "F (x ⋅ i') ∈ hom unity b"
using a b F by blast
hence "F (x ⋅ i') ∈ S.hom unity b"
using b in_hom_char⇩F⇩S⇩b⇩C by blast
thus "F (x ⋅ i') ⋅ i ∈ S.hom S.unity b"
using i in_hom_char⇩F⇩S⇩b⇩C unity_def by auto
qed
obtain f where f: "S.in_hom f a b ∧ (∀x. S.in_hom x S.unity (S.dom f)
⟶ f ⋅ x = (λx. F (x ⋅ i') ⋅ i) x)"
using 1 S.fun_complete_ax ‹S.ide a› ‹S.ide b› by presburger
show "∃f. in_hom f a b ∧ (∀x. in_hom x unity (dom f) ⟶ comp f x = F x)"
proof -
have "in_hom f a b"
using f in_hom_char⇩F⇩S⇩b⇩C ideD(1) a b by presburger
moreover have "∀x. in_hom x unity (dom f) ⟶ comp f x = F x"
proof (intro allI impI)
fix x
assume x: "in_hom x unity (dom f)"
have xi: "S.in_hom (x ⋅ i) S.unity (S.dom f)"
using f x i in_hom_char⇩F⇩S⇩b⇩C dom_char⇩S⇩b⇩C
by (metis (no_types, lifting) in_homE unity_def calculation S.comp_in_homI)
hence 1: "f ⋅ (x ⋅ i) = F ((x ⋅ i) ⋅ i') ⋅ i"
using f by blast
hence "((f ⋅ x) ⋅ i) ⋅ i' = (F x ⋅ i) ⋅ i'"
by (metis (no_types, lifting) xi S.comp_assoc S.inverse_arrowsE
S.seqI' i' ii' in_hom_char⇩F⇩S⇩b⇩C inclusion_preserves_inverse S.comp_arr_ide)
hence "f ⋅ x = F x"
by (metis (no_types, lifting) xi 1 S.invert_side_of_triangle(2) S.match_2 S.match_3
S.seqI arr_char⇩S⇩b⇩C calculation S.in_homE S.inverse_unique S.isoI
ii' in_homE inclusion_preserves_inverse)
thus "comp f x = F x"
using comp_char
by (metis (no_types, lifting) comp_simp in_homE seqI calculation x)
qed
ultimately show ?thesis by blast
qed
qed
qed
show "∃img. set_category_given_img comp img ssetp"
using T.set_category_given_img_axioms by blast
qed
lemma is_set_category:
shows "set_category comp ssetp"
..
end
end