# Theory CZH_ECAT_Discrete

```(* Copyright 2021 (C) Mihails Milehins *)

section‹Discrete category›
theory CZH_ECAT_Discrete
imports
CZH_ECAT_Simple
CZH_ECAT_Small_Functor
begin

subsection‹Abstract discrete category›

named_theorems cat_discrete_cs_simps
named_theorems cat_discrete_cs_intros

subsubsection‹Definition and elementary properties›

text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›

locale cat_discrete = category α ℭ for α ℭ +
assumes cat_discrete_Arr: "f ∈⇩∘ ℭ⦇Arr⦈ ⟹ f ∈⇩∘ ℛ⇩∘ (ℭ⦇CId⦈)"

text‹Rules.›

lemma (in cat_discrete)
assumes "α' = α" "ℭ' = ℭ"
shows "cat_discrete α' ℭ'"
unfolding assms by (rule cat_discrete_axioms)

mk_ide rf cat_discrete_def[unfolded cat_discrete_axioms_def]
|intro cat_discreteI|
|dest cat_discreteD[dest]|
|elim cat_discreteE[elim]|

lemmas [cat_discrete_cs_intros] = cat_discreteD(1)

text‹Elementary properties.›

lemma (in cat_discrete) cat_discrete_is_arrD[dest]:
assumes "f : a ↦⇘ℭ⇙ b"
shows "b = a" and "f = ℭ⦇CId⦈⦇a⦈"
proof-
from assms cat_discrete_Arr have "f ∈⇩∘ ℛ⇩∘ (ℭ⦇CId⦈)"
by (auto simp: cat_cs_simps)
with cat_CId_vdomain obtain a' where f_def: "f = ℭ⦇CId⦈⦇a'⦈" and "a' ∈⇩∘ ℭ⦇Obj⦈"
by (blast dest: CId.vrange_atD)
then have "f : a' ↦⇘ℭ⇙ a'" by (auto intro: cat_CId_is_arr')
with assms have "a = a'" and "b = a'" by blast+
with f_def show "b = a" and "f = ℭ⦇CId⦈⦇a⦈" by auto
qed

lemma (in cat_discrete) cat_discrete_is_arrE[elim]:
assumes "f : b ↦⇘ℭ⇙ c"
obtains a where "f : a ↦⇘ℭ⇙ a" and "f = ℭ⦇CId⦈⦇a⦈"
using assms by auto

subsection‹The discrete category›

text‹
As explained in Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›, every discrete
category is identified with its set of objects.
In this work, it is assumed that the set of objects and the set of arrows
in the canonical discrete category coincide; the domain and the codomain
functions are identities.
›

subsubsection‹Definition and elementary properties›

definition the_cat_discrete :: "V ⇒ V" (‹:⇩C›)
where ":⇩C I = [I, I, vid_on I, vid_on I, (λfg∈⇩∘fid_on I. fg⦇0⦈), vid_on I]⇩∘"

text‹Components.›

lemma the_cat_discrete_components:
shows ":⇩C I⦇Obj⦈ = I"
and ":⇩C I⦇Arr⦈ = I"
and ":⇩C I⦇Dom⦈ = vid_on I"
and ":⇩C I⦇Cod⦈ = vid_on I"
and ":⇩C I⦇Comp⦈ = (λfg∈⇩∘fid_on I. fg⦇0⦈)"
and ":⇩C I⦇CId⦈ = vid_on I"
unfolding the_cat_discrete_def dg_field_simps

subsubsection‹Domain›

mk_VLambda the_cat_discrete_components(3)[folded VLambda_vid_on]
|vsv the_cat_discrete_Dom_vsv[cat_discrete_cs_intros]|
|vdomain the_cat_discrete_Dom_vdomain[cat_discrete_cs_simps]|
|app the_cat_discrete_Dom_app[cat_discrete_cs_simps]|

subsubsection‹Codomain›

mk_VLambda the_cat_discrete_components(4)[folded VLambda_vid_on]
|vsv the_cat_discrete_Cod_vsv[cat_discrete_cs_intros]|
|vdomain the_cat_discrete_Cod_vdomain[cat_discrete_cs_simps]|
|app the_cat_discrete_Cod_app[cat_discrete_cs_simps]|

subsubsection‹Composition›

lemma the_cat_discrete_Comp_vsv[cat_discrete_cs_intros]: "vsv (:⇩C I⦇Comp⦈)"
unfolding the_cat_discrete_components by simp

lemma the_cat_discrete_Comp_vdomain: "𝒟⇩∘ (:⇩C I⦇Comp⦈) = fid_on I"
unfolding the_cat_discrete_components by simp

lemma the_cat_discrete_Comp_vrange:
"ℛ⇩∘ (:⇩C I⦇Comp⦈) = I"
proof(intro vsubset_antisym vsubsetI)
fix f assume "f ∈⇩∘ ℛ⇩∘ (:⇩C I⦇Comp⦈)"
then obtain gg where f_def: "f = :⇩C I⦇Comp⦈⦇gg⦈" and gg: "gg ∈⇩∘ fid_on I"
unfolding the_cat_discrete_components by auto
from gg show "f ∈⇩∘ I"
unfolding f_def the_cat_discrete_components by clarsimp
next
fix f assume "f ∈⇩∘ I"
then have "[f, f]⇩∘ ∈⇩∘ fid_on I" by clarsimp
moreover then have "f = :⇩C I⦇Comp⦈⦇f, f⦈⇩∙"
unfolding the_cat_discrete_components by simp
ultimately show "f ∈⇩∘ ℛ⇩∘ (:⇩C I⦇Comp⦈)"
unfolding the_cat_discrete_components
by (metis rel_VLambda.vsv_vimageI2 vdomain_VLambda)
qed

lemma the_cat_discrete_Comp_app[cat_discrete_cs_simps]:
assumes "i ∈⇩∘ I"
shows "i ∘⇩A⇘:⇩C I⇙ i = i"
proof-
from assms have "[i, i]⇩∘ ∈⇩∘ fid_on I" by clarsimp
then show ?thesis unfolding the_cat_discrete_components by simp
qed

subsubsection‹Identity›

mk_VLambda the_cat_discrete_components(6)[folded VLambda_vid_on]
|vsv the_cat_discrete_CId_vsv[cat_discrete_cs_intros]|
|vdomain the_cat_discrete_CId_vdomain[cat_discrete_cs_simps]|
|app the_cat_discrete_CId_app[cat_discrete_cs_simps]|

subsubsection‹Arrow with a domain and a codomain›

lemma the_cat_discrete_is_arrI:
assumes "i ∈⇩∘ I"
shows "i : i ↦⇘:⇩C I⇙ i"
using assms unfolding is_arr_def the_cat_discrete_components by simp

lemma the_cat_discrete_is_arrI'[cat_discrete_cs_intros]:
assumes "i ∈⇩∘ I"
and "a = i"
and "b = i"
shows "i : a ↦⇘:⇩C I⇙ b"
using assms(1) unfolding assms(2,3) by (rule the_cat_discrete_is_arrI)

lemma the_cat_discrete_is_arrD:
assumes "f : a ↦⇘:⇩C I⇙ b"
shows "f : f ↦⇘:⇩C I⇙ f"
and "a : a ↦⇘:⇩C I⇙ a"
and "b : b ↦⇘:⇩C I⇙ b"
and "f ∈⇩∘ I"
and "a ∈⇩∘ I"
and "b ∈⇩∘ I"
and "f = a"
and "f = b"
and "b = a"
using assms unfolding is_arr_def the_cat_discrete_components by force+

subsubsection‹The discrete category is a discrete category›

lemma (in 𝒵) cat_discrete_the_cat_discrete:
assumes "I ⊆⇩∘ Vset α"
shows "cat_discrete α (:⇩C I)"
proof(intro cat_discreteI categoryI')
show "vfsequence (:⇩C I)" unfolding the_cat_discrete_def by simp
show "vcard (:⇩C I) = 6⇩ℕ"
unfolding the_cat_discrete_def by (simp add: nat_omega_simps)
show "gf ∈⇩∘ 𝒟⇩∘ (:⇩C I⦇Comp⦈) ⟷
(∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘:⇩C I⇙ c ∧ f : a ↦⇘:⇩C I⇙ b)"
for gf
unfolding the_cat_discrete_Comp_vdomain
proof
assume "gf ∈⇩∘ fid_on I"
then obtain a where "gf = [a, a]⇩∘" and "a ∈⇩∘ I" by clarsimp
moreover then have "a : a ↦⇘:⇩C I⇙ a"
by (auto intro: the_cat_discrete_is_arrI)
ultimately show
"∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘:⇩C I⇙ c ∧ f : a ↦⇘:⇩C I⇙ b"
by auto
next
assume "∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘:⇩C I⇙ c ∧ f : a ↦⇘:⇩C I⇙ b"
then obtain g f b c a where gf_def: "gf = [g, f]⇩∘"
and g: "g : b ↦⇘:⇩C I⇙ c"
and f: "f : a ↦⇘:⇩C I⇙ b"
by clarsimp
then have "g = f" by (metis is_arrE the_cat_discrete_is_arrD(1))
with the_cat_discrete_is_arrD(4)[OF f] show "gf ∈⇩∘ fid_on I"
unfolding gf_def by clarsimp
qed
show "g ∘⇩A⇘:⇩C I⇙ f : a ↦⇘:⇩C I⇙ c" if "g : b ↦⇘:⇩C I⇙ c" and "f : a ↦⇘:⇩C I⇙ b"
for g b c f a
proof-
from that have fba: "f = a" "b = a" and a: "a ∈⇩∘ I"
unfolding the_cat_discrete_is_arrD[OF that(2)] by (simp_all add: ‹a ∈⇩∘ I›)
from that have gcb: "g = b" "c = b"
unfolding the_cat_discrete_is_arrD[OF that(1)] by simp_all
from a show ?thesis
unfolding fba gcb
by
(
cs_concl cs_shallow
cs_simp: cat_discrete_cs_simps cs_intro: cat_discrete_cs_intros
)
qed
show "h ∘⇩A⇘:⇩C I⇙ g ∘⇩A⇘:⇩C I⇙ f = h ∘⇩A⇘:⇩C I⇙ (g ∘⇩A⇘:⇩C I⇙ f)"
if "h : c ↦⇘:⇩C I⇙ d" and "g : b ↦⇘:⇩C I⇙ c" and "f : a ↦⇘:⇩C I⇙ b"
for h c d g b f a
proof-
from that have fba: "f = a" "b = a" and a: "a ∈⇩∘ I"
unfolding the_cat_discrete_is_arrD[OF that(3)] by (simp_all add: ‹a ∈⇩∘ I›)
from that have gcb: "g = b" "c = b"
unfolding the_cat_discrete_is_arrD[OF that(2)] by simp_all
from that have hcd: "h = c" "d = c"
unfolding the_cat_discrete_is_arrD[OF that(1)] by simp_all
from a show ?thesis
unfolding fba gcb hcd
by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps)
qed
show ":⇩C I⦇CId⦈⦇b⦈ ∘⇩A⇘:⇩C I⇙ f = f" if "f : a ↦⇘:⇩C I⇙ b" for f a b
proof-
from that have fba: "f = a" "b = a" and a: "a ∈⇩∘ I"
unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹a ∈⇩∘ I›)
from a show ?thesis
by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps fba)
qed
show "f ∘⇩A⇘:⇩C I⇙ :⇩C I⦇CId⦈⦇b⦈ = f" if "f : b ↦⇘:⇩C I⇙ c" for f b c
proof-
from that have fba: "f = b" "c = b" and b: "b ∈⇩∘ I"
unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹b ∈⇩∘ I›)
from b show ?thesis
by (cs_concl cs_shallow cs_simp: cat_discrete_cs_simps fba)
qed
show ":⇩C I⦇CId⦈⦇a⦈ : a ↦⇘:⇩C I⇙ a"
if "a ∈⇩∘ :⇩C I⦇Obj⦈" for a
using that
by (auto simp: the_cat_discrete_components intro: cat_discrete_cs_intros)
show "⋃⇩∘((λa∈⇩∘A. ⋃⇩∘(VLambda B (Hom (:⇩C I) a) `⇩∘ B)) `⇩∘ A) ∈⇩∘ Vset α"
if "A ⊆⇩∘ :⇩C I⦇Obj⦈"
and "B ⊆⇩∘ :⇩C I⦇Obj⦈"
and "A ∈⇩∘ Vset α"
and "B ∈⇩∘ Vset α"
for A B
proof-
have "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (:⇩C I) a b) ⊆⇩∘ A ∪⇩∘ B"
proof(intro vsubsetI, elim vifunionE, unfold in_Hom_iff)
fix i j f assume prems: "i ∈⇩∘ A" "j ∈⇩∘ B" "f : i ↦⇘:⇩C I⇙ j"
then show "f ∈⇩∘ A ∪⇩∘ B"
unfolding the_cat_discrete_is_arrD[OF prems(3)] by simp
qed
moreover have "A ∪⇩∘ B ∈⇩∘ Vset α" by (simp add: that(3,4) vunion_in_VsetI)
ultimately show "(⋃⇩∘a∈⇩∘A. ⋃⇩∘b∈⇩∘B. Hom (:⇩C I) a b) ∈⇩∘ Vset α"
by (auto simp: vsubset_in_VsetI)
qed
qed (auto simp: assms the_cat_discrete_components intro: cat_cs_intros)

lemmas [cat_discrete_cs_intros] = 𝒵.cat_discrete_the_cat_discrete

subsubsection‹Opposite discrete category›

lemma (in 𝒵) the_cat_discrete_op[cat_op_simps]:
assumes "I ⊆⇩∘ Vset α"
shows "op_cat (:⇩C I) = :⇩C I"
proof(rule cat_eqI[of α])
from assms show dI: "category α (:⇩C I)"
by (cs_concl cs_intro: cat_discrete_the_cat_discrete cat_discrete_cs_intros)
then show op_dI: "category α (op_cat (:⇩C I))"
by (cs_concl cs_shallow cs_intro: cat_op_intros)
interpret category α ‹op_cat (:⇩C I)› by (rule op_dI)
show "op_cat (:⇩C I)⦇Comp⦈ = :⇩C I⦇Comp⦈"
proof(rule vsv_eqI)
show "𝒟⇩∘ (op_cat (:⇩C I)⦇Comp⦈) = 𝒟⇩∘ (:⇩C I⦇Comp⦈)"
fix gf assume "gf ∈⇩∘ 𝒟⇩∘ (op_cat (:⇩C I)⦇Comp⦈)"
then have "gf ∈⇩∘ fid_on I"
then obtain h where gf_def: "gf = [h, h]⇩∘" and h: "h ∈⇩∘ I" by clarsimp
from dI h show "op_cat (:⇩C I)⦇Comp⦈⦇gf⦈ = :⇩C I⦇Comp⦈⦇gf⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps gf_def cs_intro: cat_discrete_cs_intros
)
qed (auto intro: cat_discrete_cs_intros)
qed (unfold the_cat_discrete_components op_cat_components, simp_all)

subsection‹Discrete functor›

subsubsection‹Local assumptions for the discrete functor›

text‹See Chapter III in \<^cite>‹"mac_lane_categories_2010"›).›

locale cf_discrete = category α ℭ for α I F ℭ +
assumes cf_discrete_selector_vrange[cat_discrete_cs_intros]:
"i ∈⇩∘ I ⟹ F i ∈⇩∘ ℭ⦇Obj⦈"
and cf_discrete_vdomain_vsubset_Vset: "I ⊆⇩∘ Vset α"

lemmas (in cf_discrete) cf_discrete_category = category_axioms

lemmas [cat_discrete_cs_intros] = cf_discrete.cf_discrete_category

text‹Rules.›

lemma (in cf_discrete) cf_discrete_axioms'[cat_discrete_cs_intros]:
assumes "α' = α" and "I' = I" and "F' = F"
shows "cf_discrete α' I' F' ℭ"
unfolding assms by (rule cf_discrete_axioms)

mk_ide rf cf_discrete_def[unfolded cf_discrete_axioms_def]
|intro cf_discreteI|
|dest cf_discreteD[dest]|
|elim cf_discreteE[elim]|

text‹Elementary properties.›

lemma (in cf_discrete) cf_discrete_is_functor_cf_CId_selector_is_arr:
assumes "i ∈⇩∘ I"
shows "ℭ⦇CId⦈⦇F i⦈ : F i ↦⇘ℭ⇙ F i"
using assms by (meson cat_CId_is_arr' cf_discreteD(2) cf_discrete_axioms)

lemma (in cf_discrete)
cf_discrete_is_functor_cf_CId_selector_is_arr'[cat_discrete_cs_intros]:
assumes "i ∈⇩∘ I" and "a = F i" and "b = F i"
shows "ℭ⦇CId⦈⦇F i⦈ : a ↦⇘ℭ⇙ b"
using assms(1)
unfolding assms(2,3)
by (rule cf_discrete_is_functor_cf_CId_selector_is_arr)

subsubsection‹Definition and elementary properties›

definition the_cf_discrete :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V" (‹:→:›)
where ":→: I F ℭ = [VLambda I F, (λi∈⇩∘I. ℭ⦇CId⦈⦇F i⦈), :⇩C I, ℭ]⇩∘"

text‹Components.›

lemma the_cf_discrete_components:
shows ":→: I F ℭ⦇ObjMap⦈ = (λi∈⇩∘I. F i)"
and ":→: I F ℭ⦇ArrMap⦈ = (λi∈⇩∘I. ℭ⦇CId⦈⦇F i⦈)"
and [cat_discrete_cs_simps]: ":→: I F ℭ⦇HomDom⦈ = :⇩C I"
and [cat_discrete_cs_simps]: ":→: I F ℭ⦇HomCod⦈ = ℭ"
unfolding the_cf_discrete_def dghm_field_simps

subsubsection‹Object map›

mk_VLambda the_cf_discrete_components(1)
|vsv the_cf_discrete_ObjMap_vsv[cat_discrete_cs_intros]|
|vdomain the_cf_discrete_ObjMap_vdomain[cat_discrete_cs_simps]|
|app the_cf_discrete_ObjMap_app[cat_discrete_cs_simps]|

lemma (in cf_discrete) cf_discrete_the_cf_discrete_ObjMap_vrange:
"ℛ⇩∘ (:→: I F ℭ⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
using cf_discrete_is_functor_cf_CId_selector_is_arr
unfolding the_cf_discrete_components
by (intro vrange_VLambda_vsubset) auto

subsubsection‹Arrow map›

mk_VLambda the_cf_discrete_components(2)
|vsv the_cf_discrete_ArrMap_vsv[cat_discrete_cs_intros]|
|vdomain the_cf_discrete_ArrMap_vdomain[cat_discrete_cs_simps]|
|app the_cf_discrete_ArrMap_app[cat_discrete_cs_simps]|

lemma (in cf_discrete) cf_discrete_the_cf_discrete_ArrMap_vrange:
"ℛ⇩∘ (:→: I F ℭ⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
using cf_discrete_is_functor_cf_CId_selector_is_arr
unfolding the_cf_discrete_components
by (intro vrange_VLambda_vsubset) (auto simp: cf_discrete_selector_vrange)

subsubsection‹Discrete functor is a functor›

lemma (in cf_discrete) cf_discrete_the_cf_discrete_is_functor:
":→: I F ℭ : :⇩C I ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_functorI')
show "vfsequence (:→: I F ℭ)" unfolding the_cf_discrete_def by simp
show "category α (:⇩C I)"
by
(
cat_discrete_the_cat_discrete
cf_discrete_vdomain_vsubset_Vset
cat_discrete.axioms(1)
)
show "vcard (:→: I F ℭ) = 4⇩ℕ"
unfolding the_cf_discrete_def by (simp add: nat_omega_simps)
show
":→: I F ℭ⦇ArrMap⦈⦇f⦈ : :→: I F ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ :→: I F ℭ⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘:⇩C I⇙ b" for f a b
proof-
from that have fba: "f = a" "b = a" and a: "a ∈⇩∘ I"
unfolding the_cat_discrete_is_arrD[OF that] by (simp_all add: ‹a ∈⇩∘ I›)
from that ‹a ∈⇩∘ I› show ?thesis
by
(
cs_concl cs_shallow
cs_simp: cat_discrete_cs_simps fba cs_intro: cat_discrete_cs_intros
)
qed
show ":→: I F ℭ⦇ArrMap⦈⦇g ∘⇩A⇘:⇩C I⇙ f⦈ =
:→: I F ℭ⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ :→: I F ℭ⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘:⇩C I⇙ c" and "f : a ↦⇘:⇩C I⇙ b" for g b c f a
proof-
from that have gfacb: "f = a" "a = b" "g = b" "c = b" and b: "b ∈⇩∘ I"
by
(
the_cat_discrete_is_arrD(8-9)[OF that(1)]
the_cat_discrete_is_arrD(5-9)[OF that(2)]
)
have "F b ∈⇩∘ ℭ⦇Obj⦈" by (simp add: b cf_discrete_selector_vrange)
from b category_axioms this show ?thesis
using that
unfolding gfacb
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_discrete_cs_simps cs_intro: cat_cs_intros
)
qed
show ":→: I F ℭ⦇ArrMap⦈⦇:⇩C I⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇:→: I F ℭ⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ :⇩C I⦇Obj⦈" for c
using that
unfolding the_cat_discrete_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_discrete_cs_simps cs_intro: cat_cs_intros
)
qed
(
auto simp:
the_cf_discrete_components
the_cat_discrete_components
cat_cs_intros
cat_discrete_cs_intros
)

lemma (in cf_discrete) cf_discrete_the_cf_discrete_is_functor':
assumes "𝔄' = :⇩C I" and "ℭ' = ℭ"
shows ":→: I F ℭ : 𝔄' ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule cf_discrete_the_cf_discrete_is_functor)

lemmas [cat_discrete_cs_intros] =
cf_discrete.cf_discrete_the_cf_discrete_is_functor'

subsubsection‹Uniqueness of the discrete category›

lemma (in cat_discrete) cat_discrete_iso_the_cat_discrete:
assumes "I ⊆⇩∘ Vset α" and "I ≈⇩∘ ℭ⦇Obj⦈"
obtains F where ":→: I F ℭ : :⇩C I ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
proof-

from assms obtain F where v11_f: "v11 F"
and dr[simp]: "𝒟⇩∘ F = I" "ℛ⇩∘ F = ℭ⦇Obj⦈"
by auto
let ?F = "λi. F⦇i⦈"
interpret F: v11 F by (rule v11_f)
from assms(1) interpret ℭ: cf_discrete α I ?F ℭ
apply(intro cf_discreteI)
unfolding dr[symmetric]
by (cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros)+
have ":→: I ?F ℭ : :⇩C I ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
proof(intro is_iso_functorI')
from ℭ.cf_discrete_selector_vrange show
":→: I ?F ℭ : :⇩C I ↦↦⇩C⇘α⇙ ℭ"
by (intro cf_discrete.cf_discrete_the_cf_discrete_is_functor cf_discreteI)
(auto simp: category_axioms assms(1))
show "v11 (:→: I ?F ℭ⦇ArrMap⦈)"
proof(rule vsv.vsv_valeq_v11I, unfold the_cf_discrete_ArrMap_vdomain)
fix i j assume prems:
"i ∈⇩∘ I" "j ∈⇩∘ I" ":→: I ?F ℭ⦇ArrMap⦈⦇i⦈ = :→: I ?F ℭ⦇ArrMap⦈⦇j⦈"
from prems(3) have "ℭ⦇CId⦈⦇?F i⦈ = ℭ⦇CId⦈⦇?F j⦈"
unfolding
the_cf_discrete_ArrMap_app[OF prems(1)]
the_cf_discrete_ArrMap_app[OF prems(2)].
then have "?F i = ?F j"
by
(
metis
ℭ.cf_discrete_is_functor_cf_CId_selector_is_arr
prems(1,2)
cat_is_arrD(4)
)
with F.v11_eq_iff prems show "i = j" by simp
show "ℛ⇩∘ (:→: I ?F ℭ⦇ArrMap⦈) = ℭ⦇Arr⦈"
proof(intro vsubset_antisym vsubsetI)
fix f assume "f ∈⇩∘ ℛ⇩∘ (:→: I ?F ℭ⦇ArrMap⦈)"
with ℭ.cf_discrete_the_cf_discrete_ArrMap_vrange show "f ∈⇩∘ ℭ⦇Arr⦈"
by auto
next
fix f assume "f ∈⇩∘ ℭ⦇Arr⦈"
then obtain a b where "f : a ↦⇘ℭ⇙ b" by auto
then obtain a where f_def: "f = ℭ⦇CId⦈⦇a⦈" and a: "a ∈⇩∘ ℭ⦇Obj⦈" by auto
from a F.vrange_atD dr obtain i where a_def: "a = ?F i" and i: "i ∈⇩∘ I"
by blast
from a i show "f ∈⇩∘ ℛ⇩∘ (:→: I ?F ℭ⦇ArrMap⦈)"
unfolding a_def f_def the_cf_discrete_components by auto
qed
qed (auto simp: v11_f the_cf_discrete_components)
with that show ?thesis by simp

qed

subsubsection‹Opposite discrete functor›

lemma (in cf_discrete) cf_discrete_the_cf_discrete_op[cat_op_simps]:
"op_cf (:→: I F ℭ) = :→: I F (op_cat ℭ)"
proof(rule cf_eqI)
from cf_discrete_vdomain_vsubset_Vset show
"op_cf (:→: I F ℭ) : :⇩C I ↦↦⇩C⇘α⇙ op_cat ℭ"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_op_intros cat_discrete_cs_intros
)
show ":→: I F (op_cat ℭ) : :⇩C I ↦↦⇩C⇘α⇙ op_cat ℭ"
proof(intro cf_discrete.cf_discrete_the_cf_discrete_is_functor cf_discreteI)
fix i assume "i ∈⇩∘ I"
then show "F i ∈⇩∘ op_cat ℭ⦇Obj⦈"
qed (intro cf_discrete_vdomain_vsubset_Vset cat_cs_intros)+
qed (unfold cat_op_simps the_cf_discrete_components, simp_all)

lemmas [cat_op_simps] = cf_discrete.cf_discrete_the_cf_discrete_op

lemma (in cf_discrete) cf_discrete_op[cat_op_intros]:
"cf_discrete α I F (op_cat ℭ)"
proof(intro cf_discreteI)
show "category α (op_cat ℭ)"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
fix i assume "i ∈⇩∘ I"
then show "F i ∈⇩∘ op_cat ℭ⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_discrete_cs_intros
)
qed (intro cf_discrete_vdomain_vsubset_Vset)

lemmas [cat_op_intros] = cf_discrete.cf_discrete_op

subsection‹Tiny discrete category›

subsubsection‹Background›

named_theorems cat_small_discrete_cs_simps
named_theorems cat_small_discrete_cs_intros

lemmas [cat_small_discrete_cs_simps] = cat_discrete_cs_simps
lemmas [cat_small_discrete_cs_intros] = cat_discrete_cs_intros

subsubsection‹Definition and elementary properties›

locale tiny_cat_discrete = cat_discrete α ℭ + tiny_category α ℭ for α ℭ

text‹Rules.›

lemma (in tiny_cat_discrete) tiny_cat_discrete_axioms'[cat_discrete_cs_intros]:
assumes "α' = α" and "ℭ' = ℭ"
shows "tiny_cat_discrete α' ℭ'"
unfolding assms by (rule tiny_cat_discrete_axioms)

mk_ide rf tiny_cat_discrete_def
|intro tiny_cat_discreteI|
|dest tiny_cat_discreteD[dest]|
|elim tiny_cat_discreteE[elim]|

lemmas [cat_small_discrete_cs_intros] = tiny_cat_discreteD

lemma tiny_cat_discreteI':
assumes "tiny_category α ℭ" and "⋀f. f ∈⇩∘ ℭ⦇Arr⦈ ⟹ f ∈⇩∘ ℛ⇩∘ (ℭ⦇CId⦈)"
shows "tiny_cat_discrete α ℭ"
proof(intro tiny_cat_discreteI cat_discreteI)
interpret tiny_category α ℭ by (rule assms(1))
show "category α ℭ" by (auto intro: tiny_cat_category)
show "f ∈⇩∘ ℛ⇩∘ (ℭ⦇CId⦈)" if "f ∈⇩∘ ℭ⦇Arr⦈" for f using that by (rule assms(2))
qed (auto intro: assms(1))

subsubsection‹The discrete category is a tiny category›

lemma (in 𝒵) tiny_cat_discrete_the_cat_discrete[cat_small_discrete_cs_intros]:
assumes "I ∈⇩∘ Vset α"
shows "tiny_cat_discrete α (:⇩C I)"
proof(intro tiny_cat_discreteI cat_discrete_the_cat_discrete)
from assms show "I ⊆⇩∘ Vset α" by auto
then interpret cat_discrete α ‹:⇩C I› by (intro cat_discrete_the_cat_discrete)
show "tiny_category α (:⇩C I)"
by (intro tiny_categoryI', unfold the_cat_discrete_components)
(auto intro: cat_cs_intros assms)
qed

lemmas [cat_small_discrete_cs_intros] = 𝒵.cat_discrete_the_cat_discrete

subsection‹Discrete functor with tiny maps›

subsubsection‹Definition and elementary properties›

locale tm_cf_discrete = category α ℭ for α I F ℭ +
assumes tm_cf_discrete_selector_vrange[cat_small_discrete_cs_intros]:
"i ∈⇩∘ I ⟹ F i ∈⇩∘ ℭ⦇Obj⦈"
and tm_cf_discrete_ObjMap_in_Vset: "VLambda I F ∈⇩∘ Vset α"
and tm_cf_discrete_ArrMap_in_Vset: "(λi∈⇩∘I. ℭ⦇CId⦈⦇F i⦈) ∈⇩∘ Vset α"

text‹Rules.›

lemma (in tm_cf_discrete) tm_cf_discrete_axioms'[cat_small_discrete_cs_intros]:
assumes "α' = α" and "I' = I" and "F' = F"
shows "tm_cf_discrete α' I' F' ℭ"
unfolding assms by (rule tm_cf_discrete_axioms)

mk_ide rf tm_cf_discrete_def[unfolded tm_cf_discrete_axioms_def]
|intro tm_cf_discreteI|
|dest tm_cf_discreteD[dest]|
|elim tm_cf_discreteE[elim]|

lemma tm_cf_discreteI':
assumes "cf_discrete α I F ℭ"
and "(λi∈⇩∘I. F i) ∈⇩∘ Vset α"
and "(λi∈⇩∘I. ℭ⦇CId⦈⦇F i⦈) ∈⇩∘ Vset α"
shows "tm_cf_discrete α I F ℭ"
proof-
interpret cf_discrete α I F ℭ by (rule assms(1))
show ?thesis
by (intro tm_cf_discreteI)
(auto intro: assms cf_discrete_selector_vrange cat_cs_intros)
qed

text‹Elementary properties.›

sublocale tm_cf_discrete ⊆ cf_discrete
proof(intro cf_discreteI)
from tm_cf_discrete_ObjMap_in_Vset have "𝒟⇩∘ (λi∈⇩∘I. F i) ∈⇩∘ Vset α"
by (cs_concl cs_shallow cs_intro: vdomain_in_VsetI)
then show "I ⊆⇩∘ Vset α" by auto
qed (auto intro: cat_cs_intros tm_cf_discrete_selector_vrange)

lemmas (in tm_cf_discrete) tm_cf_discrete_is_cf_discrete_axioms =
cf_discrete_axioms

lemmas [cat_small_discrete_cs_intros] =
tm_cf_discrete.tm_cf_discrete_is_cf_discrete_axioms

lemma (in tm_cf_discrete)
tm_cf_discrete_index_in_Vset[cat_small_discrete_cs_intros]:
"I ∈⇩∘ Vset α"
proof-
from tm_cf_discrete_ObjMap_in_Vset have "𝒟⇩∘ (λi∈⇩∘I. F i) ∈⇩∘ Vset α"
by (cs_concl cs_shallow cs_intro: vdomain_in_VsetI)
then show ?thesis by simp
qed

subsubsection‹Opposite discrete functor with tiny maps›

lemma (in tm_cf_discrete) tm_cf_discrete_op[cat_op_intros]:
"tm_cf_discrete α I F (op_cat ℭ)"
using tm_cf_discrete_ObjMap_in_Vset tm_cf_discrete_ArrMap_in_Vset
by (intro tm_cf_discreteI' cf_discrete_op) (auto simp: cat_op_simps)

lemmas [cat_op_intros] = tm_cf_discrete.tm_cf_discrete_op

subsubsection‹Discrete functor with tiny maps is a functor with tiny maps›

lemma (in tm_cf_discrete) tm_cf_discrete_the_cf_discrete_is_tm_functor:
":→: I F ℭ : :⇩C I ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
by (intro is_tm_functorI' cf_discrete_the_cf_discrete_is_functor)
(
auto simp:
the_cf_discrete_components
tm_cf_discrete_ObjMap_in_Vset
tm_cf_discrete_ArrMap_in_Vset
)

lemma (in tm_cf_discrete) tm_cf_discrete_the_cf_discrete_is_tm_functor':
assumes "𝔄' = :⇩C I" and "ℭ' = ℭ"
shows ":→: I F ℭ : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
unfolding assms by (rule tm_cf_discrete_the_cf_discrete_is_tm_functor)

lemmas [cat_discrete_cs_intros] =
tm_cf_discrete.tm_cf_discrete_the_cf_discrete_is_tm_functor'

text‹\newpage›

end```