(* Copyright 2021 (C) Mihails Milehins *) section‹Digraph\label{sec:digraph}› theory CZH_DG_Digraph imports CZH_DG_Introduction begin subsection‹Background› named_theorems dg_field_simps definition Obj :: V where [dg_field_simps]: "Obj = 0" definition Arr :: V where [dg_field_simps]: "Arr = 1⇩_{ℕ}" definition Dom :: V where [dg_field_simps]: "Dom = 2⇩_{ℕ}" definition Cod :: V where [dg_field_simps]: "Cod = 3⇩_{ℕ}" subsection‹Arrow with a domain and a codomain› text‹ The definition of and notation for an arrow with a domain and codomain is adapted from Chapter I-1 in \<^cite>‹"mac_lane_categories_2010"›. The definition is applicable to digraphs and all other relevant derived entities, such as semicategories and categories, that are presented in the subsequent chapters. In this work, by convention, the definition of an arrow with a domain and a codomain is nearly always preferred to the explicit use of the domain and codomain functions for the specification of the fundamental properties of arrows. Thus, to say that ‹f› is an arrow with the domain ‹a›, it is preferable to write ‹f : a ↦⇘_{ℭ}⇙ b› (‹b› can be assumed to be arbitrary) instead of \<^term>‹f ∈⇩_{∘}ℭ⦇Arr⦈› and \<^term>‹ℭ⦇Dom⦈⦇f⦈ = a›. › definition is_arr :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" where "is_arr ℭ a b f ⟷ f ∈⇩_{∘}ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇f⦈ = a ∧ ℭ⦇Cod⦈⦇f⦈ = b" syntax "_is_arr" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" (‹_ : _ ↦ı _› [51, 51, 51] 51) translations "f : a ↦⇘ℭ⇙ b" ⇌ "CONST is_arr ℭ a b f" text‹Rules.› mk_ide is_arr_def |intro is_arrI| |dest is_arrD[dest]| |elim is_arrE[elim]| lemmas [dg_shared_cs_intros, dg_cs_intros] = is_arrD(1) lemmas [dg_shared_cs_simps, dg_cs_simps] = is_arrD(2,3) subsection‹‹Hom›-set› text‹See Chapter I-8 in \<^cite>‹"mac_lane_categories_2010"›.› abbreviation Hom :: "V ⇒ V ⇒ V ⇒ V" where "Hom ℭ a b ≡ set {f. f : a ↦⇘ℭ⇙ b}" lemma small_Hom[simp]: "small {f. f : a ↦⇘ℭ⇙ b}" unfolding is_arr_def by simp text‹Rules.› lemma HomI[dg_shared_cs_intros, dg_cs_intros]: assumes "f : a ↦⇘ℭ⇙ b" shows "f ∈⇩_{∘}Hom ℭ a b" using assms by auto lemma in_Hom_iff[dg_shared_cs_simps, dg_cs_simps]: "f ∈⇩_{∘}Hom ℭ a b ⟷ f : a ↦⇘ℭ⇙ b" by simp text‹ The ‹Hom›-sets in a given digraph are pairwise disjoint. This property was exposed as Axiom (v) in an alternative definition of a category presented in Chapter I-8 in \<^cite>‹"mac_lane_categories_2010"›. Within the scope of the definitional framework employed in this study, this property holds unconditionally. › lemma Hom_vdisjnt: assumes "a ≠ a' ∨ b ≠ b'" and "a ∈⇩_{∘}ℭ⦇Obj⦈" and "a' ∈⇩_{∘}ℭ⦇Obj⦈" and "b ∈⇩_{∘}ℭ⦇Obj⦈" and "b' ∈⇩_{∘}ℭ⦇Obj⦈" shows "vdisjnt (Hom ℭ a b) (Hom ℭ a' b')" proof(intro vdisjntI, unfold in_Hom_iff) fix g f assume "g : a ↦⇘ℭ⇙ b" and "f : a' ↦⇘ℭ⇙ b'" then have "g ∈⇩_{∘}ℭ⦇Arr⦈" and "f ∈⇩_{∘}ℭ⦇Arr⦈" and "ℭ⦇Dom⦈⦇g⦈ = a" and "ℭ⦇Cod⦈⦇g⦈ = b" and "ℭ⦇Dom⦈⦇f⦈ = a'" and "ℭ⦇Cod⦈⦇f⦈ = b'" by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+ with assms(1) have "ℭ⦇Dom⦈⦇g⦈ ≠ ℭ⦇Dom⦈⦇f⦈ ∨ ℭ⦇Cod⦈⦇g⦈ ≠ ℭ⦇Cod⦈⦇f⦈" by auto then show "g ≠ f" by clarsimp qed subsection‹Digraph: background information› text‹ The definition of a digraph that is employed in this work is similar to the definition of a ‹directed graph› presented in Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›. However, there are notable differences. More specifically, the definition is parameterized by a limit ordinal ‹α›, such that ‹ω < α›; the set of objects is assumed to be a subset of the set ‹V⇩_{α}› in the von Neumann hierarchy of sets (e.g., see \<^cite>‹"takeuti_introduction_1971"›). Such digraphs are called ‹α›-‹digraphs› to make the dependence on the parameter ‹α› explicit.\footnote{ The prefix ``‹α›-'' may be omitted whenever it is possible to infer the value of ‹α› from the context. This applies not only to the digraphs, but all other entities that are parameterized by a limit ordinal ‹α› such that ‹ω < α›.} This definition was inspired by the ideas expressed in \<^cite>‹"feferman_set-theoretical_1969"›, \<^cite>‹"sica_doing_2006"› and \<^cite>‹"shulman_set_2008"›. In ZFC in HOL, the predicate \<^term>‹small› is used for distinguishing the terms of any type of the form \<^typ>‹'a set› that are isomorphic to elements of a term of the type \<^typ>‹V› (the elements can be exposed via the predicate \<^const>‹elts›). Thus, the collection of the elements associated with any term of the type \<^typ>‹V› (e.g., \<^term>‹elts (a::V)›) is always small (see the theorem @{thm [source] small_elts} in \<^cite>‹"paulson_zermelo_2019"›). Therefore, in this study, in an attempt to avoid confusion, the term ``small'' is never used to refer to digraphs. Instead, a new terminology is introduced in this body of work. Thus, in this work, an ‹α›-digraph is a tiny ‹α›-digraph if and only if the set of its objects and the set of its arrows both belong to the set ‹V⇩_{α}›. This notion is similar to the notion of a small category in the sense of the definition employed in Chapter I-6 in \<^cite>‹"mac_lane_categories_2010"›, if it is assumed that the ``smallness'' is determined with respect to the set ‹V⇩_{α}› instead of the universe ‹U›. Also, in what follows, any member of the set ‹V⇩_{α}› will be referred to as an ‹α›-tiny set. All of the large (i.e. non-tiny) digraphs that are considered within the scope of this work have a slightly unconventional condition associated with the size of their ‹Hom›-sets. This condition implies that all ‹Hom›-sets of a digraph are tiny, but it is not equivalent to all ‹Hom›-sets being tiny. The condition was introduced in an attempt to resolve some of the issues related to the lack of an analogue of the Axiom Schema of Replacement closed with respect to ‹V⇩_{α}›. › subsection‹Digraph: definition and elementary properties› locale digraph = 𝒵 α + vfsequence ℭ + Dom: vsv ‹ℭ⦇Dom⦈› + Cod: vsv ‹ℭ⦇Cod⦈› for α ℭ + assumes dg_length[dg_cs_simps]: "vcard ℭ = 4⇩_{ℕ}" and dg_Dom_vdomain[dg_cs_simps]: "𝒟⇩_{∘}(ℭ⦇Dom⦈) = ℭ⦇Arr⦈" and dg_Dom_vrange: "ℛ⇩_{∘}(ℭ⦇Dom⦈) ⊆⇩_{∘}ℭ⦇Obj⦈" and dg_Cod_vdomain[dg_cs_simps]: "𝒟⇩_{∘}(ℭ⦇Cod⦈) = ℭ⦇Arr⦈" and dg_Cod_vrange: "ℛ⇩_{∘}(ℭ⦇Cod⦈) ⊆⇩_{∘}ℭ⦇Obj⦈" and dg_Obj_vsubset_Vset: "ℭ⦇Obj⦈ ⊆⇩_{∘}Vset α" and dg_Hom_vifunion_in_Vset[dg_cs_intros]: "⟦ A ⊆⇩_{∘}ℭ⦇Obj⦈; B ⊆⇩_{∘}ℭ⦇Obj⦈; A ∈⇩_{∘}Vset α; B ∈⇩_{∘}Vset α ⟧ ⟹ (⋃⇩_{∘}a∈⇩_{∘}A. ⋃⇩_{∘}b∈⇩_{∘}B. Hom ℭ a b) ∈⇩_{∘}Vset α" lemmas [dg_cs_simps] = digraph.dg_length digraph.dg_Dom_vdomain digraph.dg_Cod_vdomain lemmas [dg_cs_intros] = digraph.dg_Hom_vifunion_in_Vset text‹Rules.› lemma (in digraph) digraph_axioms'[dg_cs_intros]: assumes "α' = α" shows "digraph α' ℭ" unfolding assms by (rule digraph_axioms) mk_ide rf digraph_def[unfolded digraph_axioms_def] |intro digraphI| |dest digraphD[dest]| |elim digraphE[elim]| text‹Elementary properties.› lemma dg_eqI: assumes "digraph α 𝔄" and "digraph α 𝔅" and "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" and "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" and "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" and "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈" shows "𝔄 = 𝔅" proof- interpret 𝔄: digraph α 𝔄 by (rule assms(1)) interpret 𝔅: digraph α 𝔅 by (rule assms(2)) show ?thesis proof(rule vsv_eqI) have dom_lhs: "𝒟⇩_{∘}𝔄 = 4⇩_{ℕ}" by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps) show "a ∈⇩_{∘}𝒟⇩_{∘}𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a by (unfold dom_lhs, elim_in_numeral, insert assms) (auto simp: dg_field_simps) qed ( cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps cs_intro: V_cs_intros )+ qed lemma (in digraph) dg_def: "ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]⇩_{∘}" proof(rule vsv_eqI) have dom_lhs: "𝒟⇩_{∘}ℭ = 4⇩_{ℕ}" by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps) have dom_rhs: "𝒟⇩_{∘}[ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]⇩_{∘}= 4⇩_{ℕ}" by (simp add: nat_omega_simps) then show "𝒟⇩_{∘}ℭ = 𝒟⇩_{∘}[ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]⇩_{∘}" unfolding dom_lhs dom_rhs by simp show "a ∈⇩_{∘}𝒟⇩_{∘}ℭ ⟹ ℭ⦇a⦈ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]⇩_{∘}⦇a⦈" for a by (unfold dom_lhs, elim_in_numeral, unfold dg_field_simps) (simp_all add: nat_omega_simps) qed (auto simp: vsv_axioms) lemma (in digraph) dg_Obj_if_Dom_vrange: assumes "a ∈⇩_{∘}ℛ⇩_{∘}(ℭ⦇Dom⦈)" shows "a ∈⇩_{∘}ℭ⦇Obj⦈" using assms dg_Dom_vrange by auto lemma (in digraph) dg_Obj_if_Cod_vrange: assumes "a ∈⇩_{∘}ℛ⇩_{∘}(ℭ⦇Cod⦈)" shows "a ∈⇩_{∘}ℭ⦇Obj⦈" using assms dg_Cod_vrange by auto lemma (in digraph) dg_is_arrD: assumes "f : a ↦⇘ℭ⇙ b" shows "f ∈⇩_{∘}ℭ⦇Arr⦈" and "a ∈⇩_{∘}ℭ⦇Obj⦈" and "b ∈⇩_{∘}ℭ⦇Obj⦈" and "ℭ⦇Dom⦈⦇f⦈ = a" and "ℭ⦇Cod⦈⦇f⦈ = b" proof- from assms show prems: "f ∈⇩_{∘}ℭ⦇Arr⦈" and fa[symmetric]: "ℭ⦇Dom⦈⦇f⦈ = a" and fb[symmetric]: "ℭ⦇Cod⦈⦇f⦈ = b" by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+ from digraph_axioms prems have "f ∈⇩_{∘}𝒟⇩_{∘}(ℭ⦇Dom⦈)" "f ∈⇩_{∘}𝒟⇩_{∘}(ℭ⦇Cod⦈)" by (cs_concl cs_shallow cs_simp: dg_cs_simps)+ with assms show "a ∈⇩_{∘}ℭ⦇Obj⦈" "b ∈⇩_{∘}ℭ⦇Obj⦈" by ( cs_concl cs_intro: dg_Obj_if_Dom_vrange dg_Obj_if_Cod_vrange V_cs_intros cs_simp: fa fb )+ qed lemmas [dg_cs_intros] = digraph.dg_is_arrD(1-3) lemma (in digraph) dg_is_arrE[elim]: assumes "f : a ↦⇘ℭ⇙ b" obtains "f ∈⇩_{∘}ℭ⦇Arr⦈" and "a ∈⇩_{∘}ℭ⦇Obj⦈" and "b ∈⇩_{∘}ℭ⦇Obj⦈" and "ℭ⦇Dom⦈⦇f⦈ = a" and "ℭ⦇Cod⦈⦇f⦈ = b" using assms by (blast dest: dg_is_arrD) lemma (in digraph) dg_in_ArrE[elim]: assumes "f ∈⇩_{∘}ℭ⦇Arr⦈" obtains a b where "f : a ↦⇘ℭ⇙ b" and "a ∈⇩_{∘}ℭ⦇Obj⦈" and "b ∈⇩_{∘}ℭ⦇Obj⦈" using assms by (auto dest: dg_is_arrD(2,3) is_arrI) lemma (in digraph) dg_Hom_in_Vset[dg_cs_intros]: assumes "a ∈⇩_{∘}ℭ⦇Obj⦈" and "b ∈⇩_{∘}ℭ⦇Obj⦈" shows "Hom ℭ a b ∈⇩_{∘}Vset α" proof- let ?A = ‹set {a}› and ?B = ‹set {b}› from assms have A: "?A ⊆⇩_{∘}ℭ⦇Obj⦈" and B: "?B ⊆⇩_{∘}ℭ⦇Obj⦈" by auto from assms dg_Obj_vsubset_Vset have "a ∈⇩_{∘}Vset α" and "b ∈⇩_{∘}Vset α" by auto then have a: "set {a} ∈⇩_{∘}Vset α" and b: "set {b} ∈⇩_{∘}Vset α" by (metis Axiom_of_Pairing insert_absorb2)+ from dg_Hom_vifunion_in_Vset[OF A B a b] show "Hom ℭ a b ∈⇩_{∘}Vset α" by simp qed lemmas [dg_cs_intros] = digraph.dg_Hom_in_Vset text‹Size.› lemma (in digraph) dg_Arr_vsubset_Vset: "ℭ⦇Arr⦈ ⊆⇩_{∘}Vset α" proof(intro vsubsetI) fix f assume "f ∈⇩_{∘}ℭ⦇Arr⦈" then obtain a b where f: "f : a ↦⇘ℭ⇙ b" and a: "a ∈⇩_{∘}ℭ⦇Obj⦈" and b: "b ∈⇩_{∘}ℭ⦇Obj⦈" by blast show "f ∈⇩_{∘}Vset α" by (rule Vset_trans, rule HomI[OF f], rule dg_Hom_in_Vset[OF a b]) qed lemma (in digraph) dg_Dom_vsubset_Vset: "ℭ⦇Dom⦈ ⊆⇩_{∘}Vset α" by ( rule Dom.vbrelation_Limit_vsubset_VsetI, unfold dg_cs_simps, insert dg_Dom_vrange dg_Obj_vsubset_Vset ) (auto intro!: dg_Arr_vsubset_Vset) lemma (in digraph) dg_Cod_vsubset_Vset: "ℭ⦇Cod⦈ ⊆⇩_{∘}Vset α" by ( rule Cod.vbrelation_Limit_vsubset_VsetI, unfold dg_cs_simps, insert dg_Cod_vrange dg_Obj_vsubset_Vset ) (auto intro!: dg_Arr_vsubset_Vset) lemma (in digraph) dg_digraph_in_Vset_4: "ℭ ∈⇩_{∘}Vset (α + 4⇩_{ℕ})" proof- note [folded VPow_iff, folded Vset_succ[OF Ord_α], dg_cs_intros] = dg_Obj_vsubset_Vset dg_Arr_vsubset_Vset dg_Dom_vsubset_Vset dg_Cod_vsubset_Vset show ?thesis by (subst dg_def, succ_of_numeral) ( cs_concl cs_simp: plus_V_succ_right V_cs_simps cs_intro: dg_cs_intros V_cs_intros ) qed lemma (in digraph) dg_Obj_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "ℭ⦇Obj⦈ ∈⇩_{∘}Vset β" using assms dg_Obj_vsubset_Vset Vset_in_mono by auto lemma (in digraph) dg_in_Obj_in_Vset[dg_cs_intros]: assumes "a ∈⇩_{∘}ℭ⦇Obj⦈" shows "a ∈⇩_{∘}Vset α" using assms dg_Obj_vsubset_Vset by auto lemma (in digraph) dg_Arr_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "ℭ⦇Arr⦈ ∈⇩_{∘}Vset β" using assms dg_Arr_vsubset_Vset Vset_in_mono by auto lemma (in digraph) dg_in_Arr_in_Vset[dg_cs_intros]: assumes "a ∈⇩_{∘}ℭ⦇Arr⦈" shows "a ∈⇩_{∘}Vset α" using assms dg_Arr_vsubset_Vset by auto lemma (in digraph) dg_Dom_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "ℭ⦇Dom⦈ ∈⇩_{∘}Vset β" by (meson assms dg_Dom_vsubset_Vset Vset_in_mono vsubset_in_VsetI) lemma (in digraph) dg_Cod_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "ℭ⦇Cod⦈ ∈⇩_{∘}Vset β" by (meson assms dg_Cod_vsubset_Vset Vset_in_mono vsubset_in_VsetI) lemma (in digraph) dg_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "ℭ ∈⇩_{∘}Vset β" proof- interpret β: 𝒵 β by (rule assms(1)) note [dg_cs_intros] = dg_Obj_in_Vset dg_Arr_in_Vset dg_Dom_in_Vset dg_Cod_in_Vset from assms(2) show ?thesis by (subst dg_def) (cs_concl cs_shallow cs_intro: dg_cs_intros V_cs_intros) qed lemma (in digraph) dg_digraph_if_ge_Limit: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "digraph β ℭ" proof(rule digraphI) show "vfsequence ℭ" by (simp add: vfsequence_axioms) show "ℭ⦇Obj⦈ ⊆⇩_{∘}Vset β" by (rule vsubsetI) (meson Vset_in_mono Vset_trans assms(2) dg_Obj_vsubset_Vset vsubsetE) fix A B assume "A ⊆⇩_{∘}ℭ⦇Obj⦈" "B ⊆⇩_{∘}ℭ⦇Obj⦈" "A ∈⇩_{∘}Vset β" "B ∈⇩_{∘}Vset β" then have "(⋃⇩_{∘}a∈⇩_{∘}A. ⋃⇩_{∘}b∈⇩_{∘}B. Hom ℭ a b) ⊆⇩_{∘}ℭ⦇Arr⦈" by auto moreover note dg_Arr_vsubset_Vset moreover have "Vset α ∈⇩_{∘}Vset β" by (simp add: Vset_in_mono assms(2)) ultimately show "(⋃⇩_{∘}a∈⇩_{∘}A. ⋃⇩_{∘}b∈⇩_{∘}B. Hom ℭ a b) ∈⇩_{∘}Vset β" by auto qed (auto simp: assms(1) dg_Dom_vrange dg_Cod_vrange dg_cs_simps) lemma small_digraph[simp]: "small {ℭ. digraph α ℭ}" proof(cases ‹𝒵 α›) case True with digraph.dg_in_Vset show ?thesis by (intro down[of _ ‹Vset (α + ω)›] subsetI) (auto simp: 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω) next case False then have "{ℭ. digraph α ℭ} = {}" by auto then show ?thesis by simp qed lemma (in 𝒵) digraphs_in_Vset: assumes "𝒵 β" and "α ∈⇩_{∘}β" shows "set {ℭ. digraph α ℭ} ∈⇩_{∘}Vset β" proof(rule vsubset_in_VsetI) interpret β: 𝒵 β by (rule assms(1)) show "set {ℭ. digraph α ℭ} ⊆⇩_{∘}Vset (α + 4⇩_{ℕ})" proof(intro vsubsetI) fix ℭ assume "ℭ ∈⇩_{∘}set {ℭ. digraph α ℭ}" then interpret digraph α ℭ by simp show "ℭ ∈⇩_{∘}Vset (α + 4⇩_{ℕ})" unfolding VPow_iff by (rule dg_digraph_in_Vset_4) qed from assms(2) show "Vset (α + 4⇩_{ℕ}) ∈⇩_{∘}Vset β" by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros) qed lemma digraph_if_digraph: assumes "digraph β ℭ" and "𝒵 α" and "ℭ⦇Obj⦈ ⊆⇩_{∘}Vset α" and "⋀A B. ⟦ A ⊆⇩_{∘}ℭ⦇Obj⦈; B ⊆⇩_{∘}ℭ⦇Obj⦈; A ∈⇩_{∘}Vset α; B ∈⇩_{∘}Vset α ⟧ ⟹ (⋃⇩_{∘}a∈⇩_{∘}A. ⋃⇩_{∘}b∈⇩_{∘}B. Hom ℭ a b) ∈⇩_{∘}Vset α" shows "digraph α ℭ" proof- interpret digraph β ℭ by (rule assms(1)) interpret α: 𝒵 α by (rule assms(2)) show ?thesis proof(intro digraphI) show "vfsequence ℭ" by (simp add: vfsequence_axioms) show "(⋃⇩_{∘}a∈⇩_{∘}A. ⋃⇩_{∘}b∈⇩_{∘}B. Hom ℭ a b) ∈⇩_{∘}Vset α" if "A ⊆⇩_{∘}ℭ⦇Obj⦈" "B ⊆⇩_{∘}ℭ⦇Obj⦈" "A ∈⇩_{∘}Vset α" "B ∈⇩_{∘}Vset α" for A B by (rule assms(4)[OF that]) qed (auto simp: assms(3) dg_Cod_vrange dg_cs_simps intro!: dg_Dom_vrange) qed text‹Further properties.› lemma (in digraph) dg_Dom_app_in_Obj: assumes "f ∈⇩_{∘}ℭ⦇Arr⦈" shows "ℭ⦇Dom⦈⦇f⦈ ∈⇩_{∘}ℭ⦇Obj⦈" using assms dg_Dom_vrange by (auto simp: Dom.vsv_vimageI2) lemma (in digraph) dg_Cod_app_in_Obj: assumes "f ∈⇩_{∘}ℭ⦇Arr⦈" shows "ℭ⦇Cod⦈⦇f⦈ ∈⇩_{∘}ℭ⦇Obj⦈" using assms dg_Cod_vrange by (auto simp: Cod.vsv_vimageI2) lemma (in digraph) dg_Arr_vempty_if_Obj_vempty: assumes "ℭ⦇Obj⦈ = 0" shows "ℭ⦇Arr⦈ = 0" by (metis assms eq0_iff dg_Cod_app_in_Obj) lemma (in digraph) dg_Dom_vempty_if_Arr_vempty: assumes "ℭ⦇Arr⦈ = 0" shows "ℭ⦇Dom⦈ = 0" using assms Dom.vdomain_vrange_is_vempty by (auto intro: Dom.vsv_vrange_vempty simp: dg_cs_simps) lemma (in digraph) dg_Cod_vempty_if_Arr_vempty: assumes "ℭ⦇Arr⦈ = 0" shows "ℭ⦇Cod⦈ = 0" using assms Cod.vdomain_vrange_is_vempty by (auto intro: Cod.vsv_vrange_vempty simp: dg_cs_simps) subsection‹Opposite digraph› subsubsection‹Definition and elementary properties› text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.› definition op_dg :: "V ⇒ V" where "op_dg ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Cod⦈, ℭ⦇Dom⦈]⇩_{∘}" text‹Components.› lemma op_dg_components[dg_op_simps]: shows "op_dg ℭ⦇Obj⦈ = ℭ⦇Obj⦈" and "op_dg ℭ⦇Arr⦈ = ℭ⦇Arr⦈" and "op_dg ℭ⦇Dom⦈ = ℭ⦇Cod⦈" and "op_dg ℭ⦇Cod⦈ = ℭ⦇Dom⦈" unfolding op_dg_def dg_field_simps by (auto simp: nat_omega_simps) lemma op_dg_component_intros[dg_op_intros]: shows "a ∈⇩_{∘}ℭ⦇Obj⦈ ⟹ a ∈⇩_{∘}op_dg ℭ⦇Obj⦈" and "f ∈⇩_{∘}ℭ⦇Arr⦈ ⟹ f ∈⇩_{∘}op_dg ℭ⦇Arr⦈" unfolding dg_op_simps by simp_all text‹Elementary properties.› lemma op_dg_is_arr[dg_op_simps]: "f : b ↦⇘op_dg ℭ⇙ a ⟷ f : a ↦⇘ℭ⇙ b" unfolding dg_op_simps is_arr_def by auto lemmas [dg_op_intros] = op_dg_is_arr[THEN iffD2] lemma op_dg_Hom[dg_op_simps]: "Hom (op_dg ℭ) a b = Hom ℭ b a" unfolding dg_op_simps by simp subsubsection‹Further properties› lemma (in digraph) digraph_op[dg_op_intros]: "digraph α (op_dg ℭ)" proof(intro digraphI, unfold op_dg_components dg_op_simps) show "vfsequence (op_dg ℭ)" unfolding op_dg_def by simp show "vcard (op_dg ℭ) = 4⇩_{ℕ}" unfolding op_dg_def by (simp add: nat_omega_simps) fix A B assume "A ⊆⇩_{∘}ℭ⦇Obj⦈" "B ⊆⇩_{∘}ℭ⦇Obj⦈" "A ∈⇩_{∘}Vset α" "B ∈⇩_{∘}Vset α" then show "⋃⇩_{∘}((λa∈⇩_{∘}A. ⋃⇩_{∘}((λaa∈⇩_{∘}B. Hom ℭ aa a) `⇩_{∘}B)) `⇩_{∘}A) ∈⇩_{∘}Vset α" by (subst vifunion_vifunion_flip) (intro dg_Hom_vifunion_in_Vset) qed (auto simp: dg_Dom_vrange dg_Cod_vrange dg_Obj_vsubset_Vset dg_cs_simps) lemmas digraph_op[dg_op_intros] = digraph.digraph_op lemma (in digraph) dg_op_dg_op_dg[dg_op_simps]: "op_dg (op_dg ℭ) = ℭ" by (rule dg_eqI[of α], unfold dg_op_simps) (simp_all add: digraph_axioms digraph.digraph_op digraph_op) lemmas dg_op_dg_op_dg[dg_op_simps] = digraph.dg_op_dg_op_dg lemma eq_op_dg_iff[dg_op_simps]: assumes "digraph α 𝔄" and "digraph α 𝔅" shows "op_dg 𝔄 = op_dg 𝔅 ⟷ 𝔄 = 𝔅" proof interpret 𝔄: digraph α 𝔄 by (rule assms(1)) interpret 𝔅: digraph α 𝔅 by (rule assms(2)) assume prems: "op_dg 𝔄 = op_dg 𝔅" show "𝔄 = 𝔅" proof(rule dg_eqI[of α]) from prems show "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈" by (metis prems 𝔄.dg_op_dg_op_dg 𝔅.dg_op_dg_op_dg)+ qed (simp_all add: assms) qed auto text‹\newpage› end