Theory Category3.FreeCategory
chapter FreeCategory
theory FreeCategory
imports Category ConcreteCategory
begin
text‹
This theory defines locales for constructing the free category generated by
a graph, as well as some special cases, including the discrete category generated
by a set of objects, the ``quiver'' generated by a set of arrows, and a ``parallel pair''
of arrows, which is the diagram shape required for equalizers.
Other diagram shapes can be constructed in a similar fashion.
›
section Graphs
text‹
The following locale gives a definition of graphs in a traditional style.
›
locale graph =
fixes Obj :: "'obj set"
and Arr :: "'arr set"
and Dom :: "'arr ⇒ 'obj"
and Cod :: "'arr ⇒ 'obj"
assumes dom_is_obj: "x ∈ Arr ⟹ Dom x ∈ Obj"
and cod_is_obj: "x ∈ Arr ⟹ Cod x ∈ Obj"
begin
text‹
The list of arrows @{term p} forms a path from object @{term x} to object @{term y}
if the domains and codomains of the arrows match up in the expected way.
›
definition path
where "path x y p ≡ (p = [] ∧ x = y ∧ x ∈ Obj) ∨
(p ≠ [] ∧ x = Dom (hd p) ∧ y = Cod (last p) ∧
(∀n. n ≥ 0 ∧ n < length p ⟶ nth p n ∈ Arr) ∧
(∀n. n ≥ 0 ∧ n < (length p)-1 ⟶ Cod (nth p n) = Dom (nth p (n+1))))"
lemma path_Obj:
assumes "x ∈ Obj"
shows "path x x []"
using assms path_def by simp
lemma path_single_Arr:
assumes "x ∈ Arr"
shows "path (Dom x) (Cod x) [x]"
using assms path_def by simp
lemma path_concat:
assumes "path x y p" and "path y z q"
shows "path x z (p @ q)"
proof -
have "p = [] ∨ q = [] ⟹ ?thesis"
using assms path_def by auto
moreover have "p ≠ [] ∧ q ≠ [] ⟹ ?thesis"
proof -
assume pq: "p ≠ [] ∧ q ≠ []"
have Cod_last: "Cod (last p) = Cod (nth (p @ q) ((length p)-1))"
using assms pq by (simp add: last_conv_nth nth_append)
moreover have Dom_hd: "Dom (hd q) = Dom (nth (p @ q) (length p))"
using assms pq by (simp add: hd_conv_nth less_not_refl2 nth_append)
show ?thesis
proof -
have 1: "⋀n. n ≥ 0 ∧ n < length (p @ q) ⟹ nth (p @ q) n ∈ Arr"
proof -
fix n
assume n: "n ≥ 0 ∧ n < length (p @ q)"
have "(n ≥ 0 ∧ n < length p) ∨ (n ≥ length p ∧ n < length (p @ q))"
using n by auto
thus "nth (p @ q) n ∈ Arr"
using assms pq nth_append path_def le_add_diff_inverse length_append
less_eq_nat.simps(1) nat_add_left_cancel_less
by metis
qed
have 2: "⋀n. n ≥ 0 ∧ n < length (p @ q) - 1 ⟹
Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
proof -
fix n
assume n: "n ≥ 0 ∧ n < length (p @ q) - 1"
have 1: "(n ≥ 0 ∧ n < (length p) - 1) ∨ (n ≥ length p ∧ n < length (p @ q) - 1)
∨ n = (length p) - 1"
using n by auto
thus "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n+1))"
proof -
have "n ≥ 0 ∧ n < (length p) - 1 ⟹ ?thesis"
using assms pq nth_append path_def by (metis add_lessD1 less_diff_conv)
moreover have "n = (length p) - 1 ⟹ ?thesis"
using assms pq nth_append path_def Dom_hd Cod_last by simp
moreover have "n ≥ length p ∧ n < length (p @ q) - 1 ⟹ ?thesis"
proof -
assume 1: "n ≥ length p ∧ n < length (p @ q) - 1"
have "Cod (nth (p @ q) n) = Cod (nth q (n - length p))"
using 1 nth_append leD by metis
also have "... = Dom (nth q (n - length p + 1))"
using 1 assms(2) path_def by auto
also have "... = Dom (nth (p @ q) (n + 1))"
using 1 nth_append
by (metis Nat.add_diff_assoc2 ex_least_nat_le le_0_eq le_add1 le_neq_implies_less
le_refl le_trans length_0_conv pq)
finally show "Cod (nth (p @ q) n) = Dom (nth (p @ q) (n + 1))" by auto
qed
ultimately show ?thesis using 1 by auto
qed
qed
show ?thesis
unfolding path_def using assms pq path_def hd_append2 Cod_last Dom_hd 1 2
by simp
qed
qed
ultimately show ?thesis by auto
qed
end
section "Free Categories"
text‹
The free category generated by a graph has as its arrows all triples @{term "MkArr x y p"},
where @{term x} and @{term y} are objects and @{term p} is a path from @{term x} to @{term y}.
We construct it here an instance of the general construction given by the
@{locale concrete_category} locale.
›
locale free_category =
G: graph Obj Arr D C
for Obj :: "'obj set"
and Arr :: "'arr set"
and D :: "'arr ⇒ 'obj"
and C :: "'arr ⇒ 'obj"
begin
type_synonym ('o, 'a) arr = "('o, 'a list) concrete_category.arr"
sublocale concrete_category ‹Obj :: 'obj set› ‹λx y. Collect (G.path x y)›
‹λ_. []› ‹λ_ _ _ g f. f @ g›
using G.path_Obj G.path_concat
by (unfold_locales, simp_all)
abbreviation comp (infixr ‹⋅› 55)
where "comp ≡ COMP"
notation in_hom (‹«_ : _ → _»›)
abbreviation Path
where "Path ≡ Map"
lemma arr_single [simp]:
assumes "x ∈ Arr"
shows "arr (MkArr (D x) (C x) [x])"
using assms
by (simp add: G.cod_is_obj G.dom_is_obj G.path_single_Arr)
end
section "Discrete Categories"
text‹
A discrete category is a category in which every arrow is an identity.
We could construct it as the free category generated by a graph with no
arrows, but it is simpler just to apply the @{locale concrete_category}
construction directly.
›
locale discrete_category =
fixes Obj :: "'obj set"
begin
type_synonym 'o arr = "('o, unit) concrete_category.arr"
sublocale concrete_category ‹Obj :: 'obj set› ‹λx y. if x = y then {x} else {}›
‹λx. x› ‹λ_ _ x _ _. x›
apply unfold_locales
apply simp_all
apply (metis empty_iff)
by (metis empty_iff singletonD)
abbreviation comp (infixr ‹⋅› 55)
where "comp ≡ COMP"
notation in_hom (‹«_ : _ → _»›)
lemma is_discrete:
shows "arr f ⟷ ide f"
using ide_char⇩C⇩C arr_char by simp
lemma arr_char:
shows "arr f ⟷ Dom f ∈ Obj ∧ f = MkIde (Dom f)"
using is_discrete
by (metis (no_types, lifting) cod_char dom_char ide_MkIde ide_char⇩C⇩C ide_char')
lemma arr_char':
shows "arr f ⟷ f ∈ MkIde ` Obj"
using arr_char image_iff by auto
lemma dom_char:
shows "dom f = (if arr f then f else null)"
using dom_char is_discrete by simp
lemma cod_char:
shows "cod f = (if arr f then f else null)"
using cod_char is_discrete by simp
lemma in_hom_char:
shows "«f : a → b» ⟷ arr f ∧ f = a ∧ f = b"
using is_discrete by auto
lemma seq_char:
shows "seq g f ⟷ arr f ∧ f = g"
using is_discrete
by (metis (no_types, lifting) comp_arr_dom seqE dom_char)
lemma comp_char:
shows "g ⋅ f = (if seq g f then f else null)"
proof -
have "¬ seq g f ⟹ ?thesis"
using comp_char by presburger
moreover have "seq g f ⟹ ?thesis"
using seq_char comp_char comp_arr_ide is_discrete
by (metis (no_types, lifting))
ultimately show ?thesis by blast
qed
end
text‹
The empty category is the discrete category generated by an empty set of objects.
›
locale empty_category =
discrete_category "{} :: unit set"
begin
lemma is_empty:
shows "¬arr f"
using arr_char by simp
end
section "Quivers"
text‹
A quiver is a two-object category whose non-identity arrows all point in the
same direction. A quiver is specified by giving the set of these non-identity arrows.
›
locale quiver =
fixes Arr :: "'arr set"
begin
type_synonym 'a arr = "(unit, 'a) concrete_category.arr"
sublocale free_category "{False, True}" Arr "λ_. False" "λ_. True"
by (unfold_locales, simp_all)
notation comp (infixr ‹⋅› 55)
notation in_hom (‹«_ : _ → _»›)
definition Zero
where "Zero ≡ MkIde False"
definition One
where "One ≡ MkIde True"
definition fromArr
where "fromArr x ≡ if x ∈ Arr then MkArr False True [x] else null"
definition toArr
where "toArr f ≡ hd (Path f)"
lemma ide_char:
shows "ide f ⟷ f = Zero ∨ f = One"
proof -
have "ide f ⟷ f = MkIde False ∨ f = MkIde True"
using ide_char⇩C⇩C concrete_category.MkIde_Dom' concrete_category_axioms by fastforce
thus ?thesis
using comp_def Zero_def One_def by simp
qed
lemma arr_char':
shows "arr f ⟷ f =
MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
proof
assume f: "f = MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
show "arr f" using f by auto
next
assume f: "arr f"
have "¬(f = MkIde False ∨ f = MkIde True) ⟹ f ∈ (λx. MkArr False True [x]) ` Arr"
proof -
assume f': "¬(f = MkIde False ∨ f = MkIde True)"
have 0: "Dom f = False ∧ Cod f = True"
using f f' arr_char G.path_def MkArr_Map by fastforce
have 1: "f = MkArr False True (Path f)"
using f 0 arr_char MkArr_Map by force
moreover have "length (Path f) = 1"
proof -
have "length (Path f) ≠ 0"
using f f' 0 arr_char G.path_def by simp
moreover have "⋀x y p. length p > 1 ⟹ ¬ G.path x y p"
using G.path_def less_diff_conv by fastforce
ultimately show ?thesis
using f arr_char
by (metis less_one linorder_neqE_nat mem_Collect_eq)
qed
moreover have "⋀p. length p = 1 ⟷ (∃x. p = [x])"
by (auto simp: length_Suc_conv)
ultimately have "∃x. x ∈ Arr ∧ Path f = [x]"
using f G.path_def arr_char
by (metis (no_types, lifting) Cod.simps(1) Dom.simps(1) le_eq_less_or_eq
less_numeral_extra(1) mem_Collect_eq nth_Cons_0)
thus "f ∈ (λx. MkArr False True [x]) ` Arr"
using 1 by auto
qed
thus "f = MkIde False ∨ f = MkIde True ∨ f ∈ (λx. MkArr False True [x]) ` Arr"
by auto
qed
lemma arr_char:
shows "arr f ⟷ f = Zero ∨ f = One ∨ f ∈ fromArr ` Arr"
using arr_char' Zero_def One_def fromArr_def by simp
lemma dom_char:
shows "dom f = (if arr f then
if f = One then One else Zero
else null)"
proof -
have "¬ arr f ⟹ ?thesis"
using dom_char by simp
moreover have "arr f ⟹ ?thesis"
proof -
assume f: "arr f"
have 1: "dom f = MkIde (Dom f)"
using f dom_char by simp
have "f = One ⟹ ?thesis"
using f 1 One_def by (metis (full_types) Dom.simps(1))
moreover have "f = Zero ⟹ ?thesis"
using f 1 Zero_def by (metis (full_types) Dom.simps(1))
moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
using f fromArr_def G.path_def Zero_def calculation(1) by auto
ultimately show ?thesis
using f arr_char by blast
qed
ultimately show ?thesis by blast
qed
lemma cod_char:
shows "cod f = (if arr f then
if f = Zero then Zero else One
else null)"
proof -
have "¬ arr f ⟹ ?thesis"
using cod_char by simp
moreover have "arr f ⟹ ?thesis"
proof -
assume f: "arr f"
have 1: "cod f = MkIde (Cod f)"
using f cod_char by simp
have "f = One ⟹ ?thesis"
using f 1 One_def by (metis (full_types) Cod.simps(1) f)
moreover have "f = Zero ⟹ ?thesis"
using f 1 Zero_def by (metis (full_types) Cod.simps(1) f)
moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
using f fromArr_def G.path_def One_def calculation(2) by auto
ultimately show ?thesis
using f arr_char by blast
qed
ultimately show ?thesis by blast
qed
lemma seq_char:
shows "seq g f ⟷ arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
proof
assume gf: "arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
show "seq g f"
using gf dom_char cod_char by auto
next
assume gf: "seq g f"
hence 1: "arr f ∧ arr g ∧ dom g = cod f" by auto
have "Cod f = False ⟹ f = Zero"
using gf 1 arr_char [of f] G.path_def Zero_def One_def cod_char Dom_cod
by (metis (no_types, lifting) Dom.simps(1))
moreover have "Cod f = True ⟹ g = One"
using gf 1 arr_char [of f] G.path_def Zero_def One_def dom_char Dom_cod
by (metis (no_types, lifting) Dom.simps(1))
moreover have "¬(f = MkIde False ∧ g = MkIde True)"
using 1 by auto
ultimately show "arr g ∧ arr f ∧ ((f = Zero ∧ g ≠ One) ∨ (f ≠ Zero ∧ g = One))"
using gf arr_char One_def Zero_def by blast
qed
lemma not_ide_fromArr:
shows "¬ ide (fromArr x)"
using fromArr_def ide_char ide_def Zero_def One_def
by (metis Cod.simps(1) Dom.simps(1))
lemma in_hom_char:
shows "«f : a → b» ⟷ (a = Zero ∧ b = Zero ∧ f = Zero) ∨
(a = One ∧ b = One ∧ f = One) ∨
(a = Zero ∧ b = One ∧ f ∈ fromArr ` Arr)"
proof -
have "f = Zero ⟹ ?thesis"
using arr_char' [of f] ide_char'
by (metis (no_types, lifting) Zero_def category.in_homE category.in_homI
cod_MkArr dom_MkArr imageE is_category not_ide_fromArr)
moreover have "f = One ⟹ ?thesis"
using arr_char' [of f] ide_char'
by (metis (no_types, lifting) One_def category.in_homE category.in_homI
cod_MkArr dom_MkArr image_iff is_category not_ide_fromArr)
moreover have "f ∈ fromArr ` Arr ⟹ ?thesis"
proof -
assume f: "f ∈ fromArr ` Arr"
have 1: "arr f" using f arr_char by simp
moreover have "dom f = Zero ∧ cod f = One"
using f 1 arr_char dom_char cod_char fromArr_def
by (metis (no_types, lifting) ide_char imageE not_ide_fromArr)
ultimately have "in_hom f Zero One" by auto
thus "in_hom f a b ⟷ (a = Zero ∧ b = Zero ∧ f = Zero ∨
a = One ∧ b = One ∧ f = One ∨
a = Zero ∧ b = One ∧ f ∈ fromArr ` Arr)"
using f ide_char by auto
qed
ultimately show ?thesis
using arr_char [of f] by fast
qed
lemma Zero_not_eq_One [simp]:
shows "Zero ≠ One"
by (simp add: One_def Zero_def)
lemma Zero_not_eq_fromArr [simp]:
shows "Zero ∉ fromArr ` Arr"
using ide_char not_ide_fromArr
by (metis (no_types, lifting) image_iff)
lemma One_not_eq_fromArr [simp]:
shows "One ∉ fromArr ` Arr"
using ide_char not_ide_fromArr
by (metis (no_types, lifting) image_iff)
lemma comp_char:
shows "g ⋅ f = (if seq g f then
if f = Zero then g else if g = One then f else null
else null)"
proof -
have "seq g f ⟹ f = Zero ⟹ g ⋅ f = g"
using seq_char comp_char [of g f] Zero_def dom_char cod_char comp_arr_dom
by auto
moreover have "seq g f ⟹ g = One ⟹ g ⋅ f = f"
using seq_char comp_char [of g f] One_def dom_char cod_char comp_cod_arr
by simp
moreover have "seq g f ⟹ f ≠ Zero ⟹ g ≠ One ⟹ g ⋅ f = null"
using seq_char Zero_def One_def by simp
moreover have "¬seq g f ⟹ g ⋅ f = null"
using comp_char ext by fastforce
ultimately show ?thesis by argo
qed
lemma comp_simp [simp]:
assumes "seq g f"
shows "f = Zero ⟹ g ⋅ f = g"
and "g = One ⟹ g ⋅ f = f"
using assms seq_char comp_char by metis+
lemma arr_fromArr:
assumes "x ∈ Arr"
shows "arr (fromArr x)"
using assms fromArr_def arr_char image_eqI by simp
lemma toArr_in_Arr:
assumes "arr f" and "¬ide f"
shows "toArr f ∈ Arr"
proof -
have "⋀a. a ∈ Arr ⟹ Path (fromArr a) = [a]"
using fromArr_def arr_char by simp
hence "hd (Path f) ∈ Arr"
using assms arr_char ide_char by auto
thus ?thesis
by (simp add: toArr_def)
qed
lemma toArr_fromArr [simp]:
assumes "x ∈ Arr"
shows "toArr (fromArr x) = x"
using assms fromArr_def toArr_def
by (simp add: toArr_def)
lemma fromArr_toArr [simp]:
assumes "arr f" and "¬ide f"
shows "fromArr (toArr f) = f"
using assms fromArr_def toArr_def arr_char ide_char toArr_fromArr by auto
end
section "Parallel Pairs"
text‹
A parallel pair is a quiver with two non-identity arrows.
It is important in the definition of equalizers.
›
locale parallel_pair =
quiver "{False, True} :: bool set"
begin
typedef arr = "UNIV :: bool quiver.arr set" ..
definition j0
where "j0 ≡ fromArr False"
definition j1
where "j1 ≡ fromArr True"
lemma arr_char:
shows "arr f ⟷ f = Zero ∨ f = One ∨ f = j0 ∨ f = j1"
using arr_char j0_def j1_def by simp
lemma dom_char:
shows "dom f = (if f = j0 ∨ f = j1 then Zero else if arr f then f else null)"
using arr_char dom_char j0_def j1_def
by (metis ide_char not_ide_fromArr)
lemma cod_char:
shows "cod f = (if f = j0 ∨ f = j1 then One else if arr f then f else null)"
using arr_char cod_char j0_def j1_def
by (metis ide_char not_ide_fromArr)
lemma j0_not_eq_j1 [simp]:
shows "j0 ≠ j1"
using j0_def j1_def
by (metis insert_iff toArr_fromArr)
lemma Zero_not_eq_j0 [simp]:
shows "Zero ≠ j0"
using Zero_def j0_def Zero_not_eq_fromArr by auto
lemma Zero_not_eq_j1 [simp]:
shows "Zero ≠ j1"
using Zero_def j1_def Zero_not_eq_fromArr by auto
lemma One_not_eq_j0 [simp]:
shows "One ≠ j0"
using One_def j0_def One_not_eq_fromArr by auto
lemma One_not_eq_j1 [simp]:
shows "One ≠ j1"
using One_def j1_def One_not_eq_fromArr by auto
lemma dom_simp [simp]:
shows "dom Zero = Zero"
and "dom One = One"
and "dom j0 = Zero"
and "dom j1 = Zero"
using dom_char arr_char by auto
lemma cod_simp [simp]:
shows "cod Zero = Zero"
and "cod One = One"
and "cod j0 = One"
and "cod j1 = One"
using cod_char arr_char by auto
end
end