# Theory CZH_DG_Digraph

(* 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⇩ℕ"
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)
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)

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 auto

text‹\newpage›

end