(* Title: FreeCategory Author: Eugene W. Stark <stark@cs.stonybrook.edu>, 2016 Maintainer: Eugene W. Stark <stark@cs.stonybrook.edu> *) 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) apply (metis empty_iff singletonD) 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