Theory CZH_ECAT_Structure_Example
section‹Example: categories with additional structure›
theory CZH_ECAT_Structure_Example
imports
CZH_ECAT_Introduction
CZH_ECAT_PCategory
CZH_ECAT_Set
begin
subsection‹Background›
text‹
The examples that are presented in this section showcase
how the framework developed in this article can
be used for the formalization of the theory of
categories with additional structure. The content of
this section also indicates some of the potential
future directions for this body of work.
›
subsection‹Dagger category›
named_theorems dag_field_simps
named_theorems dagcat_cs_simps
named_theorems dagcat_cs_intros
definition DagCat :: V where [dag_field_simps]: "DagCat = 0"
definition DagDag :: V where [dag_field_simps]: "DagDag = 1⇩ℕ"
abbreviation DagDag_app :: "V ⇒ V" (‹†⇩C›)
where "†⇩C ℭ ≡ ℭ⦇DagDag⦈"
subsubsection‹Definition and elementary properties›
text‹
For further information see
\<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/dagger+category
}}.
›
locale dagger_category =
𝒵 α +
vfsequence ℭ +
DagCat: category α ‹ℭ⦇DagCat⦈› +
DagDag: is_functor α ‹op_cat (ℭ⦇DagCat⦈)› ‹ℭ⦇DagCat⦈› ‹†⇩C ℭ›
for α ℭ +
assumes dagcat_length: "vcard ℭ = 2⇩ℕ"
and dagcat_ObjMap_identity[dagcat_cs_simps]:
"a ∈⇩∘ ℭ⦇DagCat⦈⦇Obj⦈ ⟹ (†⇩C ℭ)⦇ObjMap⦈⦇a⦈ = a"
and dagcat_DagCat_idem[dagcat_cs_simps]:
"†⇩C ℭ ⇩C⇩F∘ †⇩C ℭ = cf_id (ℭ⦇DagCat⦈)"
lemmas [dagcat_cs_simps] =
dagger_category.dagcat_ObjMap_identity
dagger_category.dagcat_DagCat_idem
text‹Rules.›
lemma (in dagger_category) dagger_category_axioms'[dagcat_cs_intros]:
assumes "α' = α"
shows "dagger_category α' ℭ"
unfolding assms by (rule dagger_category_axioms)
mk_ide rf dagger_category_def[unfolded dagger_category_axioms_def]
|intro dagger_categoryI|
|dest dagger_categoryD[dest]|
|elim dagger_categoryE[elim]|
lemma category_if_dagger_category[dagcat_cs_intros]:
assumes "ℭ' = (ℭ⦇DagCat⦈)" and "dagger_category α ℭ"
shows "category α ℭ'"
unfolding assms(1) using assms(2) by (rule dagger_categoryD(3))
lemma (in dagger_category) dagcat_is_functor'[dagcat_cs_intros]:
assumes "𝔄' = op_cat (ℭ⦇DagCat⦈)" and "𝔅' = ℭ⦇DagCat⦈"
shows "†⇩C ℭ : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule DagDag.is_functor_axioms)
lemmas [dagcat_cs_intros] = dagger_category.dagcat_is_functor'
subsection‹‹Rel› as a dagger category›
subsubsection‹Definition and elementary properties›
text‹
For further information see
\<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{
https://ncatlab.org/nlab/show/Rel
}}.
›
definition dagcat_Rel :: "V ⇒ V"
where "dagcat_Rel α = [cat_Rel α, †⇩C⇩.⇩R⇩e⇩l α]⇩∘"
text‹Components.›
lemma dagcat_Rel_components:
shows "dagcat_Rel α⦇DagCat⦈ = cat_Rel α"
and "dagcat_Rel α⦇DagDag⦈ = †⇩C⇩.⇩R⇩e⇩l α"
unfolding dagcat_Rel_def dag_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹‹Rel› is a dagger category›
lemma (in 𝒵) dagger_category_dagcat_Rel: "dagger_category α (dagcat_Rel α)"
proof(intro dagger_categoryI)
show "category α (dagcat_Rel α⦇DagCat⦈)"
by
(
cs_concl cs_shallow
cs_simp: dagcat_Rel_components cs_intro: cat_Rel_cs_intros
)
show "†⇩C (dagcat_Rel α) :
op_cat (dagcat_Rel α⦇DagCat⦈) ↦↦⇩C⇘α⇙ dagcat_Rel α⦇DagCat⦈"
unfolding dagcat_Rel_components
by (cs_concl cs_intro: cf_cs_intros cat_cs_intros)
show "vcard (dagcat_Rel α) = 2⇩ℕ"
unfolding dagcat_Rel_def by (simp add: nat_omega_simps)
show "†⇩C (dagcat_Rel α)⦇ObjMap⦈⦇a⦈ = a"
if "a ∈⇩∘ dagcat_Rel α⦇DagCat⦈⦇Obj⦈" for a
using that
unfolding dagcat_Rel_components cat_Rel_components(1)
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_Rel_cs_simps)
show "†⇩C (dagcat_Rel α) ⇩C⇩F∘ †⇩C (dagcat_Rel α) = dghm_id (dagcat_Rel α⦇DagCat⦈)"
unfolding dagcat_Rel_components
by (cs_concl cs_shallow cs_simp: cf_cn_comp_cf_dag_Rel_cf_dag_Rel)
qed (auto simp: dagcat_Rel_def)
subsection‹Monoidal category›
text‹
For background information see Chapter 2 in \<^cite>‹"etingof_tensor_2015"›.
›
subsubsection‹Background›
named_theorems mcat_field_simps
named_theorems mcat_cs_simps
named_theorems mcat_cs_intros
definition Mcat :: V where [mcat_field_simps]: "Mcat = 0"
definition Mcf :: V where [mcat_field_simps]: "Mcf = 1⇩ℕ"
definition Me :: V where [mcat_field_simps]: "Me = 2⇩ℕ"
definition Mα :: V where [mcat_field_simps]: "Mα = 3⇩ℕ"
definition Ml :: V where [mcat_field_simps]: "Ml = 4⇩ℕ"
definition Mr :: V where [mcat_field_simps]: "Mr = 5⇩ℕ"
subsubsection‹Definition and elementary properties›
locale monoidal_category =
𝒵 α +
vfsequence ℭ +
Mcat: category α ‹ℭ⦇Mcat⦈› +
Mcf: is_functor α ‹(ℭ⦇Mcat⦈) ×⇩C (ℭ⦇Mcat⦈)› ‹ℭ⦇Mcat⦈› ‹ℭ⦇Mcf⦈› +
Mα: is_iso_ntcf
α ‹ℭ⦇Mcat⦈^⇩C⇩3› ‹ℭ⦇Mcat⦈› ‹cf_blcomp (ℭ⦇Mcf⦈)› ‹cf_brcomp (ℭ⦇Mcf⦈)› ‹ℭ⦇Mα⦈› +
Ml: is_iso_ntcf
α
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcf⦈⇘ℭ⦇Mcat⦈,ℭ⦇Mcat⦈⇙(ℭ⦇Me⦈,-)⇩C⇩F›
‹cf_id (ℭ⦇Mcat⦈)›
‹ℭ⦇Ml⦈› +
Mr: is_iso_ntcf
α
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcat⦈›
‹ℭ⦇Mcf⦈⇘ℭ⦇Mcat⦈,ℭ⦇Mcat⦈⇙(-,ℭ⦇Me⦈)⇩C⇩F›
‹cf_id (ℭ⦇Mcat⦈)›
‹ℭ⦇Mr⦈›
for α ℭ +
assumes mcat_length[mcat_cs_simps]: "vcard ℭ = 6⇩ℕ"
and mcat_Me_is_obj[mcat_cs_intros]: "ℭ⦇Me⦈ ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈"
and mcat_pentagon:
"⟦
a ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
b ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
c ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈;
d ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈
⟧ ⟹
(ℭ⦇Mcat⦈⦇CId⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mα⦈⦇NTMap⦈⦇b, c, d⦈⇩∙) ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a, b ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ c, d⦈⇩∙ ∘⇩A⇘ℭ⦇Mcat⦈⇙
(ℭ⦇Mα⦈⦇NTMap⦈⦇a, b, c⦈⇩∙ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mcat⦈⦇CId⦈⦇d⦈) =
ℭ⦇Mα⦈⦇NTMap⦈⦇a, b, c ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ d⦈⇩∙ ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a ⊗⇩H⇩M⇩.⇩O⇘ℭ⦇Mcf⦈⇙ b, c, d⦈⇩∙"
and mcat_triangle[mcat_cs_simps]:
"⟦ a ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈; b ∈⇩∘ ℭ⦇Mcat⦈⦇Obj⦈ ⟧ ⟹
(ℭ⦇Mcat⦈⦇CId⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Ml⦈⦇NTMap⦈⦇b⦈) ∘⇩A⇘ℭ⦇Mcat⦈⇙
ℭ⦇Mα⦈⦇NTMap⦈⦇a, ℭ⦇Me⦈, b⦈⇩∙ =
(ℭ⦇Mr⦈⦇NTMap⦈⦇a⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇Mcf⦈⇙ ℭ⦇Mcat⦈⦇CId⦈⦇b⦈)"
lemmas [mcat_cs_intros] = monoidal_category.mcat_Me_is_obj
lemmas [mcat_cs_simps] = monoidal_category.mcat_triangle
text‹Rules.›
lemma (in monoidal_category) monoidal_category_axioms'[mcat_cs_intros]:
assumes "α' = α"
shows "monoidal_category α' ℭ"
unfolding assms by (rule monoidal_category_axioms)
mk_ide rf monoidal_category_def[unfolded monoidal_category_axioms_def]
|intro monoidal_categoryI|
|dest monoidal_categoryD[dest]|
|elim monoidal_categoryE[elim]|
text‹Elementary properties.›
lemma mcat_eqI:
assumes "monoidal_category α 𝔄"
and "monoidal_category α 𝔅"
and "𝔄⦇Mcat⦈ = 𝔅⦇Mcat⦈"
and "𝔄⦇Mcf⦈ = 𝔅⦇Mcf⦈"
and "𝔄⦇Me⦈ = 𝔅⦇Me⦈"
and "𝔄⦇Mα⦈ = 𝔅⦇Mα⦈"
and "𝔄⦇Ml⦈ = 𝔅⦇Ml⦈"
and "𝔄⦇Mr⦈ = 𝔅⦇Mr⦈"
shows "𝔄 = 𝔅"
proof-
interpret 𝔄: monoidal_category α 𝔄 by (rule assms(1))
interpret 𝔅: monoidal_category α 𝔅 by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ 𝔄 = 6⇩ℕ"
by (cs_concl cs_shallow cs_simp: mcat_cs_simps V_cs_simps)
show "𝒟⇩∘ 𝔄 = 𝒟⇩∘ 𝔅"
by (cs_concl cs_shallow cs_simp: mcat_cs_simps V_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert assms)
(auto simp: mcat_field_simps)
qed auto
qed
subsection‹Components for ‹Mα› for ‹Rel››
subsubsection‹Definition and elementary properties›
definition Mα_Rel_arrow_lr :: "V ⇒ V ⇒ V ⇒ V"
where "Mα_Rel_arrow_lr A B C =
[
(λab_c∈⇩∘(A ×⇩∘ B) ×⇩∘ C. ⟨vfst (vfst ab_c), ⟨vsnd (vfst ab_c), vsnd ab_c⟩⟩),
(A ×⇩∘ B) ×⇩∘ C,
A ×⇩∘ (B ×⇩∘ C)
]⇩∘"
definition Mα_Rel_arrow_rl :: "V ⇒ V ⇒ V ⇒ V"
where "Mα_Rel_arrow_rl A B C =
[
(λa_bc∈⇩∘A ×⇩∘ (B ×⇩∘ C). ⟨⟨vfst a_bc, vfst (vsnd a_bc)⟩, vsnd (vsnd a_bc)⟩),
A ×⇩∘ (B ×⇩∘ C),
(A ×⇩∘ B) ×⇩∘ C
]⇩∘"
text‹Components.›
lemma Mα_Rel_arrow_lr_components:
shows "Mα_Rel_arrow_lr A B C⦇ArrVal⦈ =
(λab_c∈⇩∘(A ×⇩∘ B) ×⇩∘ C. ⟨vfst (vfst ab_c), ⟨vsnd (vfst ab_c), vsnd ab_c⟩⟩)"
and [cat_cs_simps]: "Mα_Rel_arrow_lr A B C⦇ArrDom⦈ = (A ×⇩∘ B) ×⇩∘ C"
and [cat_cs_simps]: "Mα_Rel_arrow_lr A B C⦇ArrCod⦈ = A ×⇩∘ (B ×⇩∘ C)"
unfolding Mα_Rel_arrow_lr_def arr_field_simps by (simp_all add: nat_omega_simps)
lemma Mα_Rel_arrow_rl_components:
shows "Mα_Rel_arrow_rl A B C⦇ArrVal⦈ =
(λa_bc∈⇩∘A ×⇩∘ (B ×⇩∘ C). ⟨⟨vfst a_bc, vfst (vsnd a_bc)⟩, vsnd (vsnd a_bc)⟩)"
and [cat_cs_simps]: "Mα_Rel_arrow_rl A B C⦇ArrDom⦈ = A ×⇩∘ (B ×⇩∘ C)"
and [cat_cs_simps]: "Mα_Rel_arrow_rl A B C⦇ArrCod⦈ = (A ×⇩∘ B) ×⇩∘ C"
unfolding Mα_Rel_arrow_rl_def arr_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Arrow value›
mk_VLambda Mα_Rel_arrow_lr_components(1)
|vsv Mα_Rel_arrow_lr_ArrVal_vsv[cat_cs_intros]|
|vdomain Mα_Rel_arrow_lr_ArrVal_vdomain[cat_cs_simps]|
|app Mα_Rel_arrow_lr_ArrVal_app'|
lemma Mα_Rel_arrow_lr_ArrVal_app[cat_cs_simps]:
assumes "ab_c = ⟨⟨a, b⟩, c⟩" and "ab_c ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C"
shows "Mα_Rel_arrow_lr A B C⦇ArrVal⦈⦇ab_c⦈ = ⟨a, ⟨b, c⟩⟩"
using assms(2)
unfolding assms(1)
by (simp_all add: Mα_Rel_arrow_lr_ArrVal_app' nat_omega_simps)
mk_VLambda Mα_Rel_arrow_rl_components(1)
|vsv Mα_Rel_arrow_rl_ArrVal_vsv[cat_cs_intros]|
|vdomain Mα_Rel_arrow_rl_ArrVal_vdomain[cat_cs_simps]|
|app Mα_Rel_arrow_rl_ArrVal_app'|
lemma Mα_Rel_arrow_rl_ArrVal_app[cat_cs_simps]:
assumes "a_bc = ⟨a, ⟨b, c⟩⟩" and "a_bc ∈⇩∘ A ×⇩∘ (B ×⇩∘ C)"
shows "Mα_Rel_arrow_rl A B C⦇ArrVal⦈⦇a_bc⦈ = ⟨⟨a, b⟩, c⟩"
using assms(2)
unfolding assms(1)
by (simp_all add: Mα_Rel_arrow_rl_ArrVal_app' nat_omega_simps)
subsubsection‹Components for ‹Mα› for ‹Rel› are arrows›
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr_Vset:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof(intro cat_Set_is_arrI arr_SetI)
show "vfsequence (Mα_Rel_arrow_lr A B C)" unfolding Mα_Rel_arrow_lr_def by auto
show "vcard (Mα_Rel_arrow_lr A B C) = 3⇩ℕ"
unfolding Mα_Rel_arrow_lr_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (Mα_Rel_arrow_lr A B C⦇ArrVal⦈) ⊆⇩∘ Mα_Rel_arrow_lr A B C⦇ArrCod⦈"
unfolding Mα_Rel_arrow_lr_components by auto
qed
(
use assms in
‹
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
›
)+
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr_Vset:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof(intro cat_Set_is_arrI arr_SetI)
show "vfsequence (Mα_Rel_arrow_rl A B C)" unfolding Mα_Rel_arrow_rl_def by auto
show "vcard (Mα_Rel_arrow_rl A B C) = 3⇩ℕ"
unfolding Mα_Rel_arrow_rl_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (Mα_Rel_arrow_rl A B C⦇ArrVal⦈) ⊆⇩∘ Mα_Rel_arrow_rl A B C⦇ArrCod⦈"
unfolding Mα_Rel_arrow_rl_components by auto
qed
(
use assms in
‹
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
›
)+
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
using assms
unfolding cat_Set_components
by (rule Mα_Rel_arrow_lr_is_cat_Set_arr_Vset)
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Set_arr)
lemmas [cat_rel_par_Set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Set_arr'
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
using assms
unfolding cat_Set_components
by (rule Mα_Rel_arrow_rl_is_cat_Set_arr_Vset)
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Set_arr)
lemmas [cat_rel_par_Set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Set_arr'
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Par_arr:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
from assms show ?thesis
unfolding cat_Par_components(1)
by (intro Set_Par.subcat_is_arrD Mα_Rel_arrow_lr_is_cat_Set_arr_Vset) auto
qed
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Par_arr)
lemmas [cat_rel_Par_set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Par_arr'
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Par_arr:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
from assms show ?thesis
unfolding cat_Par_components(1)
by (intro Set_Par.subcat_is_arrD Mα_Rel_arrow_rl_is_cat_Set_arr_Vset) auto
qed
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Par_arr)
lemmas [cat_rel_Par_set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Par_arr'
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Rel_arr:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule subcat_trans[
OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
]
)
from assms show ?thesis
unfolding cat_Rel_components(1)
by (intro Set_Rel.subcat_is_arrD Mα_Rel_arrow_lr_is_cat_Set_arr_Vset) auto
qed
lemma (in 𝒵) Mα_Rel_arrow_lr_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_lr_is_cat_Rel_arr)
lemmas [cat_Rel_par_set_cs_intros] = 𝒵.Mα_Rel_arrow_lr_is_cat_Rel_arr'
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Rel_arr:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule subcat_trans[
OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
]
)
from assms show ?thesis
unfolding cat_Rel_components(1)
by (intro Set_Rel.subcat_is_arrD Mα_Rel_arrow_rl_is_cat_Set_arr_Vset) auto
qed
lemma (in 𝒵) Mα_Rel_arrow_rl_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇘ℭ'⇙ B'"
using assms(1-3) unfolding assms(4-6) by (rule Mα_Rel_arrow_rl_is_cat_Rel_arr)
lemmas [cat_Rel_par_set_cs_intros] = 𝒵.Mα_Rel_arrow_rl_is_cat_Rel_arr'
subsubsection‹Further properties›
lemma (in 𝒵) Mα_Rel_arrow_rl_Mα_Rel_arrow_lr[cat_cs_simps]:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms have lhs:
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1)
cs_intro: cat_rel_par_Set_cs_intros cat_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈) =
(A ×⇩∘ B) ×⇩∘ C"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms Set.category_axioms have rhs:
"cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈ :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
cs_concl
cs_simp: cat_Set_components(1) cs_intro: V_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈)⦇ArrVal⦈) = (A ×⇩∘ B) ×⇩∘ C"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set α (Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈)"
by (auto dest: cat_Set_is_arrD(1))
show
"(Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈ =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix ab_c assume prems: "ab_c ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C"
then obtain a b c
where ab_c_def: "ab_c = ⟨⟨a, b⟩, c⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by clarsimp
from assms prems a b c lhs rhs show
"(Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C)⦇ArrVal⦈⦇ab_c⦈ =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈⦇ArrVal⦈⦇ab_c⦈"
unfolding ab_c_def
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps
cs_intro: cat_rel_par_Set_cs_intros V_cs_intros cat_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
lemma (in 𝒵) Mα_Rel_arrow_rl_Mα_Rel_arrow_lr'[cat_cs_simps]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
using assms
unfolding cat_Set_components(1)
by (rule Mα_Rel_arrow_rl_Mα_Rel_arrow_lr)
lemmas [cat_cs_simps] = 𝒵.Mα_Rel_arrow_rl_Mα_Rel_arrow_lr'
lemma (in 𝒵) Mα_Rel_arrow_lr_Mα_Rel_arrow_rl[cat_cs_simps]:
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms have lhs:
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C :
A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1)
cs_intro: cat_rel_par_Set_cs_intros cat_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈) =
A ×⇩∘ (B ×⇩∘ C)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms Set.category_axioms have rhs:
"cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈ :
A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
cs_concl
cs_simp: cat_Set_components(1) cs_intro: V_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈)⦇ArrVal⦈) = A ×⇩∘ (B ×⇩∘ C)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set α (Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs: "arr_Set α (cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈)"
by (auto dest: cat_Set_is_arrD(1))
show
"(Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈ =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a_bc assume prems: "a_bc ∈⇩∘ A ×⇩∘ (B ×⇩∘ C)"
then obtain a b c
where a_bc_def: "a_bc = ⟨a, ⟨b, c⟩⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by clarsimp
from assms prems a b c lhs rhs show
"(Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C)⦇ArrVal⦈⦇a_bc⦈ =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈⦇ArrVal⦈⦇a_bc⦈"
unfolding a_bc_def
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps
cs_intro: V_cs_intros cat_rel_par_Set_cs_intros cat_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
lemma (in 𝒵) Mα_Rel_arrow_lr_Mα_Rel_arrow_rl'[cat_cs_simps]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ (B ×⇩∘ C)⦈"
using assms
unfolding cat_Set_components(1)
by (rule Mα_Rel_arrow_lr_Mα_Rel_arrow_rl)
lemmas [cat_cs_simps] = 𝒵.Mα_Rel_arrow_lr_Mα_Rel_arrow_rl'
subsubsection‹Components for ‹Mα› for ‹Rel› are isomorphisms›
lemma (in 𝒵)
assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "C ∈⇩∘ Vset α"
shows Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set: category α ‹cat_Set α›
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
have lhs: "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by (intro Mα_Rel_arrow_rl_is_cat_Set_arr_Vset assms)
from assms have [cat_cs_simps]:
"Mα_Rel_arrow_rl A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_lr A B C =
cat_Set α⦇CId⦈⦇(A ×⇩∘ B) ×⇩∘ C⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1) cat_cs_simps cs_intro: cat_cs_intros
)
from assms have [cat_cs_simps]:
"Mα_Rel_arrow_lr A B C ∘⇩A⇘cat_Set α⇙ Mα_Rel_arrow_rl A B C =
cat_Set α⦇CId⦈⦇A ×⇩∘ B ×⇩∘ C⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1) cat_cs_simps cs_intro: cat_cs_intros
)
from
Set.is_iso_arrI'
[
OF lhs Mα_Rel_arrow_lr_is_cat_Set_arr_Vset[OF assms],
unfolded cat_cs_simps,
simplified
]
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
by auto
qed
lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Set_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Set α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Set_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Set α⇙ (A ×⇩∘ B) ×⇩∘ C"
using assms
unfolding cat_Set_components(1)
by
(
all
‹
intro
Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset
Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset
›
)
lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Set_iso_arr)
lemmas [cat_rel_par_Set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Set_iso_arr'
lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
assumes "A ∈⇩∘ cat_Set α⦇Obj⦈"
and "B ∈⇩∘ cat_Set α⦇Obj⦈"
and "C ∈⇩∘ cat_Set α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Set α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Set_iso_arr)
lemmas [cat_rel_par_Set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Set_iso_arr'
lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Par_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Par_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Par α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Par_components]
]
]
)
show "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Par α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Par_components]
]
]
)
qed
lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Par_iso_arr)
lemmas [cat_rel_Par_set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Par_iso_arr'
lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Par α⦇Obj⦈"
and "B ∈⇩∘ cat_Par α⦇Obj⦈"
and "C ∈⇩∘ cat_Par α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Par α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Par_iso_arr)
lemmas [cat_rel_Par_set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Par_iso_arr'
lemma (in 𝒵)
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
shows Mα_Rel_arrow_lr_is_cat_Rel_iso_arr:
"Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
and Mα_Rel_arrow_rl_is_cat_Rel_iso_arr:
"Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: wide_replete_subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule wr_subcat_trans
[
OF
Set_Par.wide_replete_subcategory_axioms
Par_Rel.wide_replete_subcategory_axioms
]
)
show "Mα_Rel_arrow_lr A B C : (A ×⇩∘ B) ×⇩∘ C ↦⇩i⇩s⇩o⇘cat_Rel α⇙ A ×⇩∘ (B ×⇩∘ C)"
by
(
rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_lr_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Rel_components]
]
]
)
show "Mα_Rel_arrow_rl A B C : A ×⇩∘ (B ×⇩∘ C) ↦⇩i⇩s⇩o⇘cat_Rel α⇙ (A ×⇩∘ B) ×⇩∘ C"
by
(
rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
[
THEN iffD1,
OF Mα_Rel_arrow_rl_is_cat_Set_iso_arr_Vset[
OF assms[unfolded cat_Rel_components]
]
]
)
qed
lemma (in 𝒵)
Mα_Rel_arrow_lr_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = (A ×⇩∘ B) ×⇩∘ C"
and "B' = A ×⇩∘ (B ×⇩∘ C)"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_lr A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_lr_is_cat_Rel_iso_arr)
lemmas [cat_Rel_par_set_cs_intros] =
𝒵.Mα_Rel_arrow_lr_is_cat_Rel_iso_arr'
lemma (in 𝒵)
Mα_Rel_arrow_rl_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and "A' = A ×⇩∘ (B ×⇩∘ C)"
and "B' = (A ×⇩∘ B) ×⇩∘ C"
and "ℭ' = cat_Rel α"
shows "Mα_Rel_arrow_rl A B C : A' ↦⇩i⇩s⇩o⇘ℭ'⇙ B'"
using assms(1-3)
unfolding assms(4-6)
by (rule Mα_Rel_arrow_rl_is_cat_Rel_iso_arr)
lemmas [cat_Rel_par_set_cs_intros] =
𝒵.Mα_Rel_arrow_rl_is_cat_Rel_iso_arr'
subsection‹‹Mα› for ‹Rel››
subsubsection‹Definition and elementary properties›
definition Mα_Rel :: "V ⇒ V"
where "Mα_Rel ℭ =
[
(λabc∈⇩∘(ℭ^⇩C⇩3)⦇Obj⦈. Mα_Rel_arrow_lr (abc⦇0⦈) (abc⦇1⇩ℕ⦈) (abc⦇2⇩ℕ⦈)),
cf_blcomp (cf_prod_2_Rel ℭ),
cf_brcomp (cf_prod_2_Rel ℭ),
ℭ^⇩C⇩3,
ℭ
]⇩∘"
text‹Components.›
lemma Mα_Rel_components:
shows "Mα_Rel ℭ⦇NTMap⦈ =
(λabc∈⇩∘(ℭ^⇩C⇩3)⦇Obj⦈. Mα_Rel_arrow_lr (abc⦇0⦈) (abc⦇1⇩ℕ⦈) (abc⦇2⇩ℕ⦈))"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDom⦈ = cf_blcomp (cf_prod_2_Rel ℭ)"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTCod⦈ = cf_brcomp (cf_prod_2_Rel ℭ)"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDGDom⦈ = ℭ^⇩C⇩3"
and [cat_cs_simps]: "Mα_Rel ℭ⦇NTDGCod⦈ = ℭ"
unfolding Mα_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Natural transformation map›
mk_VLambda Mα_Rel_components(1)
|vsv Mα_Rel_NTMap_vsv[cat_cs_intros]|
|vdomain Mα_Rel_NTMap_vdomain[cat_cs_simps]|
|app Mα_Rel_NTMap_app'|
lemma Mα_Rel_NTMap_app[cat_cs_simps]:
assumes "ABC = [A, B, C]⇩∘" and "ABC ∈⇩∘ (ℭ^⇩C⇩3)⦇Obj⦈"
shows "Mα_Rel ℭ⦇NTMap⦈⦇ABC⦈ = Mα_Rel_arrow_lr A B C"
using assms(2)
unfolding assms(1)
by (simp add: Mα_Rel_NTMap_app' nat_omega_simps)
subsubsection‹‹Mα› for ‹Rel› is a natural isomorphism›
lemma (in 𝒵) Mα_Rel_is_iso_ntcf:
"Mα_Rel (cat_Rel α) :
cf_blcomp (cf_prod_2_Rel (cat_Rel α)) ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_brcomp (cf_prod_2_Rel (cat_Rel α)) :
cat_Rel α^⇩C⇩3 ↦↦⇩C⇘α⇙ cat_Rel α"
proof-
interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)
show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence (Mα_Rel (cat_Rel α))" unfolding Mα_Rel_def by auto
show "vcard (Mα_Rel (cat_Rel α)) = 5⇩ℕ"
unfolding Mα_Rel_def by (simp add: nat_omega_simps)
show "Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈ :
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈"
if "ABC ∈⇩∘ (cat_Rel α^⇩C⇩3)⦇Obj⦈" for ABC
proof-
from that category_cat_Rel obtain A B C
where ABC_def: "ABC = [A, B, C]⇩∘"
and A: "A ∈⇩∘ cat_Rel α⦇Obj⦈"
and B: "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and C: "C ∈⇩∘ cat_Rel α⦇Obj⦈"
by (elim cat_prod_3_ObjE[rotated 3])
from that A B C show ?thesis
unfolding ABC_def
by
(
cs_concl cs_shallow
cs_intro:
cat_cs_intros cat_Rel_par_set_cs_intros cat_prod_cs_intros
cs_simp: cat_cs_simps cat_Rel_cs_simps
)
qed
then show "Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈ :
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈ ↦⇘cat_Rel α⇙
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ObjMap⦈⦇ABC⦈"
if "ABC ∈⇩∘ (cat_Rel α^⇩C⇩3)⦇Obj⦈" for ABC
using that by (simp add: cat_Rel_is_iso_arrD(1))
show
"Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC'⦈ ∘⇩A⇘cat_Rel α⇙
cf_blcomp (cf_prod_2_Rel (cat_Rel α))⦇ArrMap⦈⦇HGF⦈ =
cf_brcomp (cf_prod_2_Rel (cat_Rel α))⦇ArrMap⦈⦇HGF⦈ ∘⇩A⇘cat_Rel α⇙
Mα_Rel (cat_Rel α)⦇NTMap⦈⦇ABC⦈"
if "HGF : ABC ↦⇘cat_Rel α^⇩C⇩3⇙ ABC'" for ABC ABC' HGF
proof-
from that obtain H G F A B C A' B' C'
where HGF_def: "HGF = [H, G, F]⇩∘"
and ABC_def: "ABC = [A, B, C]⇩∘"
and ABC'_def: "ABC' = [A', B', C']⇩∘"
and H_is_arr: "H : A ↦⇘cat_Rel α⇙ A'"
and G_is_arr: "G : B ↦⇘cat_Rel α⇙ B'"
and F_is_arr: "F : C ↦⇘cat_Rel α⇙ C'"
by
(
elim cat_prod_3_is_arrE[
OF category_cat_Rel category_cat_Rel category_cat_Rel
]
)
note H = cat_Rel_is_arrD[OF H_is_arr]
note G = cat_Rel_is_arrD[OF G_is_arr]
note F = cat_Rel_is_arrD[OF F_is_arr]
interpret H: arr_Rel α H
rewrites "H⦇ArrDom⦈ = A" and "H⦇ArrCod⦈ = A'"
by (intro H)+
interpret G: arr_Rel α G
rewrites "G⦇ArrDom⦈ = B" and "G⦇ArrCod⦈ = B'"
by (intro G)+
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = C" and "F⦇ArrCod⦈ = C'"
by (intro F)+
let ?ABC' = ‹Mα_Rel_arrow_lr A' B' C'›
and ?ABC = ‹Mα_Rel_arrow_lr A B C›
and ?HG_F =
‹
prod_2_Rel_ArrVal
(prod_2_Rel_ArrVal (H⦇ArrVal⦈) (G⦇ArrVal⦈))
(F⦇ArrVal⦈)
›
and ?H_GF =
‹
prod_2_Rel_ArrVal
(H⦇ArrVal⦈)
(prod_2_Rel_ArrVal (G⦇ArrVal⦈) (F⦇ArrVal⦈))
›
have [cat_cs_simps]:
"?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F =
H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC"
proof-
from H_is_arr G_is_arr F_is_arr have lhs:
"?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A' ×⇩∘ (B' ×⇩∘ C')"
by
(
cs_concl cs_shallow
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros
)
from H_is_arr G_is_arr F_is_arr have rhs:
"H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC :
(A ×⇩∘ B) ×⇩∘ C ↦⇘cat_Rel α⇙ A' ×⇩∘ (B' ×⇩∘ C')"
by (cs_concl cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros)
show ?thesis
proof(rule arr_Rel_eqI)
from lhs show arr_Rel_lhs:
"arr_Rel α (?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F)"
by (auto dest: cat_Rel_is_arrD)
from rhs show arr_Rel_rhs:
"arr_Rel α (H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC)"
by (auto dest: cat_Rel_is_arrD)
have [cat_cs_simps]: "?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F = ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix abc_abc'' assume prems: "abc_abc'' ∈⇩∘ ?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F"
then obtain abc abc' abc''
where abc_abc''_def: "abc_abc'' = ⟨abc, abc''⟩"
and abc_abc': "⟨abc, abc'⟩ ∈⇩∘ ?HG_F"
and abc'_abc'': "⟨abc', abc''⟩ ∈⇩∘ ?ABC'⦇ArrVal⦈"
by (elim vcompE)
from abc_abc' obtain ab c ab' c'
where abc_abc'_def: "⟨abc, abc'⟩ = ⟨⟨ab, c⟩, ⟨ab', c'⟩⟩"
and ab_ab':
"⟨ab, ab'⟩ ∈⇩∘ prod_2_Rel_ArrVal (H⦇ArrVal⦈) (G⦇ArrVal⦈)"
and cc': "⟨c, c'⟩ ∈⇩∘ F⦇ArrVal⦈"
by (meson prod_2_Rel_ArrValE)
then have abc_def: "abc = ⟨ab, c⟩" and abc'_def: "abc' = ⟨ab', c'⟩"
by auto
from ab_ab' obtain a b a' b'
where ab_ab'_def: "⟨ab, ab'⟩ = ⟨⟨a, b⟩, ⟨a', b'⟩⟩"
and aa': "⟨a, a'⟩ ∈⇩∘ H⦇ArrVal⦈"
and bb': "⟨b, b'⟩ ∈⇩∘ G⦇ArrVal⦈"
by auto
then have ab_def: "ab = ⟨a, b⟩" and ab'_def: "ab' = ⟨a', b'⟩"
by auto
from cc' F.arr_Rel_ArrVal_vdomain F.arr_Rel_ArrVal_vrange
have c: "c ∈⇩∘ C" and c': "c' ∈⇩∘ C'"
by auto
from bb' G.arr_Rel_ArrVal_vdomain G.arr_Rel_ArrVal_vrange
have b: "b ∈⇩∘ B" and b': "b' ∈⇩∘ B'"
by auto
from aa' H.arr_Rel_ArrVal_vdomain H.arr_Rel_ArrVal_vrange
have a: "a ∈⇩∘ A" and a': "a' ∈⇩∘ A'"
by auto
from abc'_abc'' have "abc'' = ?ABC'⦇ArrVal⦈⦇abc'⦈"
by (simp add: vsv.vsv_appI[OF Mα_Rel_arrow_lr_ArrVal_vsv])
also from a' b' c' have "… = ⟨a', ⟨b', c'⟩⟩"
unfolding abc'_def ab'_def
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
finally have abc''_def: "abc'' = ⟨a', ⟨b', c'⟩⟩" by auto
from aa' bb' cc' a a' b b' c c' show
"abc_abc'' ∈⇩∘ ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
unfolding abc_abc''_def abc_def abc'_def abc''_def ab'_def ab_def
by (intro vcompI prod_2_Rel_ArrValI)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro:
vsv.vsv_ex1_app2[THEN iffD1]
V_cs_intros
cat_cs_intros
cat_Rel_cs_intros
)+
next
fix abc_abc'' assume prems: "abc_abc'' ∈⇩∘ ?H_GF ∘⇩∘ ?ABC⦇ArrVal⦈"
then obtain abc abc' abc''
where abc_abc''_def: "abc_abc'' = ⟨abc, abc''⟩"
and abc_abc': "⟨abc, abc'⟩ ∈⇩∘ ?ABC⦇ArrVal⦈"
and abc'_abc'': "⟨abc', abc''⟩ ∈⇩∘ ?H_GF"
by (elim vcompE)
from abc'_abc'' obtain a' bc' a'' bc''
where abc'_abc''_def: "⟨abc', abc''⟩ = ⟨⟨a', bc'⟩, ⟨a'', bc''⟩⟩"
and aa'': "⟨a', a''⟩ ∈⇩∘ H⦇ArrVal⦈"
and bc'_bc'':
"⟨bc', bc''⟩ ∈⇩∘ prod_2_Rel_ArrVal (G⦇ArrVal⦈) (F⦇ArrVal⦈)"
by (meson prod_2_Rel_ArrValE)
then have abc'_def: "abc' = ⟨a', bc'⟩"
and abc''_def: "abc'' = ⟨a'', bc''⟩"
by auto
from bc'_bc'' obtain b' c' b'' c''
where bc'_bc''_def: "⟨bc', bc''⟩ = ⟨⟨b', c'⟩, ⟨b'', c''⟩⟩"
and bb'': "⟨b', b''⟩ ∈⇩∘ G⦇ArrVal⦈"
and cc'': "⟨c', c''⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have bc'_def: "bc' = ⟨b', c'⟩"
and bc''_def: "bc'' = ⟨b'', c''⟩"
by auto
from cc'' F.arr_Rel_ArrVal_vdomain F.arr_Rel_ArrVal_vrange
have c': "c' ∈⇩∘ C" and c'': "c'' ∈⇩∘ C'"
by auto
from bb'' G.arr_Rel_ArrVal_vdomain G.arr_Rel_ArrVal_vrange
have b': "b' ∈⇩∘ B" and b'': "b'' ∈⇩∘ B'"
by auto
from aa'' H.arr_Rel_ArrVal_vdomain H.arr_Rel_ArrVal_vrange
have a': "a' ∈⇩∘ A" and a'': "a'' ∈⇩∘ A'"
by auto
from abc_abc' have "abc ∈⇩∘ 𝒟⇩∘ (?ABC⦇ArrVal⦈)" by auto
then have "abc ∈⇩∘ (A ×⇩∘ B) ×⇩∘ C" by (simp add: cat_cs_simps)
then obtain a b c
where abc_def: "abc = ⟨⟨a, b⟩, c⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
by auto
from abc_abc' have "abc' = ?ABC⦇ArrVal⦈⦇abc⦈"
by (simp add: vsv.vsv_appI[OF Mα_Rel_arrow_lr_ArrVal_vsv])
also from a b c have "… = ⟨a, ⟨b, c⟩⟩"
unfolding abc_def bc'_def
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
finally have abc'_def': "abc' = ⟨a, ⟨b, c⟩⟩" by auto
with abc'_def[unfolded bc'_def] have [cat_cs_simps]:
"a = a'" "b = b'" "c = c'"
by auto
from a'' b'' c'' have "⟨⟨a'', b''⟩, c''⟩ ∈⇩∘ (A' ×⇩∘ B') ×⇩∘ C'"
by (cs_concl cs_shallow cs_intro: V_cs_intros)
with aa'' bb'' cc'' a a' b b' c c' show
"abc_abc'' ∈⇩∘ ?ABC'⦇ArrVal⦈ ∘⇩∘ ?HG_F"
unfolding abc_abc''_def abc_def abc'_def abc''_def bc''_def
by (intro vcompI prod_2_Rel_ArrValI)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro:
vsv.vsv_ex1_app2[THEN iffD1]
V_cs_intros cat_cs_intros cat_Rel_cs_intros
)+
qed
from that H_is_arr G_is_arr F_is_arr show
"(?ABC' ∘⇩A⇘cat_Rel α⇙ (H ⇩A×⇩R⇩e⇩l G) ⇩A×⇩R⇩e⇩l F)⦇ArrVal⦈ =
(H ⇩A×⇩R⇩e⇩l (G ⇩A×⇩R⇩e⇩l F) ∘⇩A⇘cat_Rel α⇙ ?ABC)⦇ArrVal⦈"
by
(
cs_concl
cs_simp:
prod_2_Rel_components comp_Rel_components
cat_Rel_cs_simps cat_cs_simps
cs_intro:
cat_Rel_par_set_cs_intros cat_cs_intros cat_prod_cs_intros
)
qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+
qed
from that H_is_arr G_is_arr F_is_arr show ?thesis
unfolding HGF_def ABC_def ABC'_def
by
(
cs_concl
cs_intro:
cat_Rel_par_set_cs_intros cat_cs_intros cat_prod_cs_intros
cs_simp: cat_Rel_cs_simps cat_cs_simps
)
qed
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
qed
lemma (in 𝒵) Mα_Rel_is_iso_ntcf'[cat_cs_intros]:
assumes "𝔉' = cf_blcomp (cf_prod_2_Rel (cat_Rel α))"
and "𝔊' = cf_brcomp (cf_prod_2_Rel (cat_Rel α))"
and "𝔄' = cat_Rel α^⇩C⇩3"
and "𝔅' = cat_Rel α"
and "α' = α"
shows "Mα_Rel (cat_Rel α) : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
unfolding assms by (rule Mα_Rel_is_iso_ntcf)
lemmas [cat_cs_intros] = 𝒵.Mα_Rel_is_iso_ntcf'
subsection‹‹Ml› and ‹Mr› for ‹Rel››
subsubsection‹Definition and elementary properties›
definition Ml_Rel :: "V ⇒ V ⇒ V"
where "Ml_Rel ℭ a =
[
(λB∈⇩∘ℭ⦇Obj⦈. vsnd_arrow (set {a}) B),
cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(set {a},-)⇩C⇩F,
cf_id ℭ,
ℭ,
ℭ
]⇩∘"
definition Mr_Rel :: "V ⇒ V ⇒ V"
where "Mr_Rel ℭ b =
[
(λA∈⇩∘ℭ⦇Obj⦈. vfst_arrow A (set {b})),
cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(-,set {b})⇩C⇩F,
cf_id ℭ,
ℭ,
ℭ
]⇩∘"
text‹Components.›
lemma Ml_Rel_components:
shows "Ml_Rel ℭ a⦇NTMap⦈ = (λB∈⇩∘ℭ⦇Obj⦈. vsnd_arrow (set {a}) B)"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDom⦈ = cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(set {a},-)⇩C⇩F"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTCod⦈ = cf_id ℭ"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDGDom⦈ = ℭ"
and [cat_cs_simps]: "Ml_Rel ℭ a⦇NTDGCod⦈ = ℭ"
unfolding Ml_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)
lemma Mr_Rel_components:
shows "Mr_Rel ℭ b⦇NTMap⦈ = (λA∈⇩∘ℭ⦇Obj⦈. vfst_arrow A (set {b}))"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDom⦈ = cf_prod_2_Rel ℭ⇘ℭ,ℭ⇙(-,set {b})⇩C⇩F"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTCod⦈ = cf_id ℭ"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDGDom⦈ = ℭ"
and [cat_cs_simps]: "Mr_Rel ℭ b⦇NTDGCod⦈ = ℭ"
unfolding Mr_Rel_def nt_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Natural transformation map›
mk_VLambda Ml_Rel_components(1)
|vsv Ml_Rel_components_NTMap_vsv[cat_cs_intros]|
|vdomain Ml_Rel_components_NTMap_vdomain[cat_cs_simps]|
|app Ml_Rel_components_NTMap_app[cat_cs_simps]|
mk_VLambda Mr_Rel_components(1)
|vsv Mr_Rel_components_NTMap_vsv[cat_cs_intros]|
|vdomain Mr_Rel_components_NTMap_vdomain[cat_cs_simps]|
|app Mr_Rel_components_NTMap_app[cat_cs_simps]|
subsubsection‹‹Ml› and ‹Mr› for ‹Rel› are natural isomorphisms›
lemma (in 𝒵) Ml_Rel_is_iso_ntcf:
assumes "a ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Ml_Rel (cat_Rel α) a:
cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(set {a},-)⇩C⇩F ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (cat_Rel α) :
cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
proof-
let ?cf_prod = ‹cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙ (set {a},-)⇩C⇩F›
note [cat_cs_simps] = set_empty
interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)
show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence (Ml_Rel (cat_Rel α) a)" unfolding Ml_Rel_def by auto
show "vcard (Ml_Rel (cat_Rel α) a) = 5⇩ℕ"
unfolding Ml_Rel_def by (simp add: nat_omega_simps)
from assms show "?cf_prod : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
show "Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using assms that
by
(
cs_concl
cs_simp: cat_Rel_components(1) V_cs_simps cat_cs_simps
cs_intro:
cat_Rel_par_set_cs_intros
cat_cs_intros
V_cs_intros
cat_prod_cs_intros
)
with cat_Rel_is_iso_arrD[OF this] show
"Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using that by simp
show
"Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇B⦈ ∘⇩A⇘cat_Rel α⇙ ?cf_prod⦇ArrMap⦈⦇F⦈ =
cf_id (cat_Rel α)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘cat_Rel α⇙ Ml_Rel (cat_Rel α) a⦇NTMap⦈⦇A⦈"
if "F : A ↦⇘cat_Rel α⇙ B" for A B F
proof-
note F = cat_Rel_is_arrD[OF that]
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
by (intro F)+
have [cat_cs_simps]:
"vsnd_arrow (set {a}) B ∘⇩A⇘cat_Rel α⇙
(cat_Rel α⦇CId⦈⦇set {a}⦈) ⇩A×⇩R⇩e⇩l F =
F ∘⇩A⇘cat_Rel α⇙ vsnd_arrow (set {a}) A"
(is ‹?B2 ∘⇩A⇘cat_Rel α⇙ ?aF = F ∘⇩A⇘cat_Rel α⇙ ?A2›)
proof-
from assms that have lhs:
"?B2 ∘⇩A⇘cat_Rel α⇙ ?aF : set {a} ×⇩∘ A ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros V_cs_intros
)
from assms that have rhs:
"F ∘⇩A⇘cat_Rel α⇙ ?A2 : set {a} ×⇩∘ A ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros V_cs_intros
)
have [cat_cs_simps]:
"?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈) =
F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix xx'_z assume "xx'_z ∈⇩∘
?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
then obtain xx' yy' z
where xx'_z_def: "xx'_z = ⟨xx', z⟩"
and xx'_yy':
"⟨xx', yy'⟩ ∈⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
and yy'_z: "⟨yy', z⟩ ∈⇩∘ ?B2⦇ArrVal⦈"
by (meson vcompE prod_2_Rel_ArrValE)
from xx'_yy' obtain x x' y y'
where "⟨xx', yy'⟩ = ⟨⟨x, x'⟩, ⟨y, y'⟩⟩"
and "⟨x, y⟩ ∈⇩∘ vid_on (set {a})"
and xy': "⟨x', y'⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xx'_def: "xx' = ⟨a, x'⟩" and yy'_def: "yy' = ⟨a, y'⟩"
by simp_all
with yy'_z have y': "y' ∈⇩∘ B" and z_def: "z = y'"
unfolding vsnd_arrow_components by auto
from xy' vsubsetD have x': "x' ∈⇩∘ A"
by (auto intro: F.arr_Rel_ArrVal_vdomain)
show "xx'_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
unfolding xx'_z_def z_def xx'_def
by (intro vcompI, rule xy')
(auto simp: vsnd_arrow_components x' VLambda_iff2)
next
fix ay_z assume "ay_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A2⦇ArrVal⦈"
then obtain ay y z
where xx'_z_def: "ay_z = ⟨ay, z⟩"
and ay_y: "⟨ay, y⟩ ∈⇩∘ ?A2⦇ArrVal⦈"
and yz[cat_cs_intros]: "⟨y, z⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have ay_z_def: "ay_z = ⟨⟨a, y⟩, z⟩"
and y: "y ∈⇩∘ A"
and ay_def: "ay = ⟨a, y⟩"
unfolding vsnd_arrow_components by auto
from yz vsubsetD have z: "z ∈⇩∘ B"
by (auto intro: F.arr_Rel_ArrVal_vrange)
have [cat_cs_intros]: "⟨a, a⟩ ∈⇩∘ vid_on (set {a})" by auto
show "ay_z ∈⇩∘
?B2⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (vid_on (set {a})) (F⦇ArrVal⦈)"
unfolding ay_z_def
by
(
intro vcompI prod_2_Rel_ArrValI,
rule vsv.vsv_ex1_app1[THEN iffD1],
unfold cat_cs_simps,
insert z
)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
)
qed
show ?thesis
proof(rule arr_Rel_eqI)
from lhs show arr_Rel_lhs: "arr_Rel α (?B2 ∘⇩A⇘cat_Rel α⇙ ?aF)"
by (auto dest: cat_Rel_is_arrD)
from rhs show "arr_Rel α (F ∘⇩A⇘cat_Rel α⇙ ?A2)"
by (auto dest: cat_Rel_is_arrD)
note cat_Rel_CId_app[cat_Rel_cs_simps del]
note 𝒵.cat_Rel_CId_app[cat_Rel_cs_simps del]
from that assms show
"(?B2 ∘⇩A⇘cat_Rel α⇙ ?aF)⦇ArrVal⦈ = (F ∘⇩A⇘cat_Rel α⇙ ?A2)⦇ArrVal⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Rel_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
cs_simp:
id_Rel_components
cat_Rel_CId_app
comp_Rel_components(1)
prod_2_Rel_components
cat_Rel_components(1)
)
qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+
qed
from that assms show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros cat_prod_cs_intros
cs_simp: cat_Rel_components(1) V_cs_simps
)
qed
qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
qed
lemma (in 𝒵) Ml_Rel_is_iso_ntcf'[cat_cs_intros]:
assumes "a ∈⇩∘ cat_Rel α⦇Obj⦈"
and "𝔉' = cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(set {a},-)⇩C⇩F"
and "𝔊' = cf_id (cat_Rel α)"
and "𝔄' = cat_Rel α"
and "𝔅' = cat_Rel α"
and "α' = α"
shows "Ml_Rel (cat_Rel α) a : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
using assms(1) unfolding assms(2-6) by (rule Ml_Rel_is_iso_ntcf)
lemmas [cat_cs_intros] = 𝒵.Ml_Rel_is_iso_ntcf'
lemma (in 𝒵) Mr_Rel_is_iso_ntcf:
assumes "b ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "Mr_Rel (cat_Rel α) b :
cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(-,set {b})⇩C⇩F ↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (cat_Rel α) :
cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
proof-
let ?cf_prod = ‹cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙ (-,set {b})⇩C⇩F›
note [cat_cs_simps] = set_empty
interpret cf_prod: is_functor
α ‹cat_Rel α ×⇩C cat_Rel α› ‹cat_Rel α› ‹cf_prod_2_Rel (cat_Rel α)›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)
show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence (Mr_Rel (cat_Rel α) b)" unfolding Mr_Rel_def by auto
show "vcard (Mr_Rel (cat_Rel α) b) = 5⇩ℕ"
unfolding Mr_Rel_def by (simp add: nat_omega_simps)
from assms show "?cf_prod : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
show "Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇩i⇩s⇩o⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using assms that
by
(
cs_concl
cs_simp: cat_Rel_components(1) V_cs_simps cat_cs_simps
cs_intro:
cat_cs_intros
cat_Rel_par_set_cs_intros
V_cs_intros
cat_prod_cs_intros
)
with cat_Rel_is_iso_arrD[OF this] show
"Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ :
?cf_prod⦇ObjMap⦈⦇B⦈ ↦⇘cat_Rel α⇙ cf_id (cat_Rel α)⦇ObjMap⦈⦇B⦈"
if "B ∈⇩∘ cat_Rel α⦇Obj⦈" for B
using that by simp
show
"Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇B⦈ ∘⇩A⇘cat_Rel α⇙ ?cf_prod⦇ArrMap⦈⦇F⦈ =
cf_id (cat_Rel α)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘cat_Rel α⇙ Mr_Rel (cat_Rel α) b⦇NTMap⦈⦇A⦈"
if "F : A ↦⇘cat_Rel α⇙ B" for A B F
proof-
note F = cat_Rel_is_arrD[OF that]
interpret F: arr_Rel α F
rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
by (intro F)+
have [cat_cs_simps]:
"vfst_arrow B (set {b}) ∘⇩A⇘cat_Rel α⇙
F ⇩A×⇩R⇩e⇩l (cat_Rel α⦇CId⦈⦇set {b}⦈) =
F ∘⇩A⇘cat_Rel α⇙ vfst_arrow A (set {b})"
(is ‹?B1 ∘⇩A⇘cat_Rel α⇙ ?bF = F ∘⇩A⇘cat_Rel α⇙ ?A1›)
proof-
from assms that have lhs:
"?B1 ∘⇩A⇘cat_Rel α⇙ ?bF : A ×⇩∘ set {b} ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
)
from assms that have rhs:
"F ∘⇩A⇘cat_Rel α⇙ ?A1 : A ×⇩∘ set {b} ↦⇘cat_Rel α⇙ B"
by
(
cs_concl
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
)
have [cat_cs_simps]:
"?B1⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b})) =
F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
proof(intro vsubset_antisym vsubsetI)
fix xx'_z assume "xx'_z ∈⇩∘
?B1⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b}))"
then obtain xx' yy' z
where xx'_z_def: "xx'_z = ⟨xx', z⟩"
and xx'_yy':
"⟨xx', yy'⟩ ∈⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b}))"
and yy'_z: "⟨yy', z⟩ ∈⇩∘ ?B1⦇ArrVal⦈"
by (meson vcompE prod_2_Rel_ArrValE)
from xx'_yy' obtain x x' y y'
where "⟨xx', yy'⟩ = ⟨⟨x, x'⟩, ⟨y, y'⟩⟩"
and "⟨x', y'⟩ ∈⇩∘ vid_on (set {b})"
and xy: "⟨x, y⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xx'_def: "xx' = ⟨x, b⟩" and yy'_def: "yy' = ⟨y, b⟩"
by simp_all
with yy'_z have y': "y ∈⇩∘ B" and z_def: "z = y"
unfolding vfst_arrow_components by auto
from xy vsubsetD have x: "x ∈⇩∘ A"
by (auto intro: F.arr_Rel_ArrVal_vdomain)
show "xx'_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
unfolding xx'_z_def z_def xx'_def
by (intro vcompI, rule xy)
(auto simp: vfst_arrow_components x VLambda_iff2)
next
fix xy_z assume "xy_z ∈⇩∘ F⦇ArrVal⦈ ∘⇩∘ ?A1⦇ArrVal⦈"
then obtain xy y z
where xx'_z_def: "xy_z = ⟨xy, z⟩"
and xy_y: "⟨xy, y⟩ ∈⇩∘ ?A1⦇ArrVal⦈"
and yz[cat_cs_intros]: "⟨y, z⟩ ∈⇩∘ F⦇ArrVal⦈"
by auto
then have xy_z_def: "xy_z = ⟨⟨y, b⟩, z⟩"
and y: "y ∈⇩∘ A"
and xy_def: "xy = ⟨y, b⟩"
unfolding vfst_arrow_components by auto
from yz vsubsetD have z: "z ∈⇩∘ B"
by (auto intro: F.arr_Rel_ArrVal_vrange)
have [cat_cs_intros]: "⟨b, b⟩ ∈⇩∘ vid_on (set {b})" by auto
show "xy_z ∈⇩∘
?B1⦇ArrVal⦈ ∘⇩∘ prod_2_Rel_ArrVal (F⦇ArrVal⦈) (vid_on (set {b}))"
unfolding xy_z_def
by
(
intro vcompI prod_2_Rel_ArrValI,
rule vsv.vsv_ex1_app1[THEN iffD1],
unfold cat_cs_simps,
insert z
)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
)
qed
show ?thesis
proof(rule arr_Rel_eqI)
from lhs show arr_Rel_lhs: "arr_Rel α (?B1 ∘⇩A⇘cat_Rel α⇙ ?bF)"
by (auto dest: cat_Rel_is_arrD)
from rhs show "arr_Rel α (F ∘⇩A⇘cat_Rel α⇙ ?A1)"
by (auto dest: cat_Rel_is_arrD)
note cat_Rel_CId_app[cat_Rel_cs_simps del]
note 𝒵.cat_Rel_CId_app[cat_Rel_cs_simps del]
from that assms show
"(?B1 ∘⇩A⇘cat_Rel α⇙ ?bF)⦇ArrVal⦈ = (F ∘⇩A⇘cat_Rel α⇙ ?A1)⦇ArrVal⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Rel_cs_simps
cs_intro: cat_cs_intros cat_Rel_par_set_cs_intros V_cs_intros
cs_simp:
id_Rel_components
cat_Rel_CId_app
comp_Rel_components(1)
prod_2_Rel_components
cat_Rel_components(1)
)
qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+
qed
from that assms show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros cat_prod_cs_intros
cs_simp: cat_Rel_components(1) V_cs_simps
)
qed
qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
qed
lemma (in 𝒵) Mr_Rel_is_iso_ntcf'[cat_cs_intros]:
assumes "b ∈⇩∘ cat_Rel α⦇Obj⦈"
and "𝔉' = cf_prod_2_Rel (cat_Rel α)⇘cat_Rel α,cat_Rel α⇙(-,set {b})⇩C⇩F"
and "𝔊' = cf_id (cat_Rel α)"
and "𝔄' = cat_Rel α"
and "𝔅' = cat_Rel α"
and "α' = α"
shows "Mr_Rel (cat_Rel α) b : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
using assms(1) unfolding assms(2-6) by (rule Mr_Rel_is_iso_ntcf)
lemmas [cat_cs_intros] = 𝒵.Mr_Rel_is_iso_ntcf'
subsection‹‹Rel› as a monoidal category›
subsubsection‹Definition and elementary properties›
text‹
For further information see
\<^cite>‹"noauthor_wikipedia_2001"›\footnote{\url{
https://en.wikipedia.org/wiki/Category_of_relations
}}.
›
definition mcat_Rel :: "V ⇒ V ⇒ V"
where "mcat_Rel α a =
[
cat_Rel α,
cf_prod_2_Rel (cat_Rel α),
set {a},
Mα_Rel (cat_Rel α),
Ml_Rel (cat_Rel α) a,
Mr_Rel (cat_Rel α) a
]⇩∘"
text‹Components.›
lemma mcat_Rel_components:
shows "mcat_Rel α a⦇Mcat⦈ = cat_Rel α"
and "mcat_Rel α a⦇Mcf⦈ = cf_prod_2_Rel (cat_Rel α)"
and "mcat_Rel α a⦇Me⦈ = set {a}"
and "mcat_Rel α a⦇Mα⦈ = Mα_Rel (cat_Rel α)"
and "mcat_Rel α a⦇Ml⦈ = Ml_Rel (cat_Rel α) a"
and "mcat_Rel α a⦇Mr⦈ = Mr_Rel (cat_Rel α) a"
unfolding mcat_Rel_def mcat_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹‹Rel› is a monoidal category›
lemma (in 𝒵) monoidal_category_mcat_Rel:
assumes "a ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "monoidal_category α (mcat_Rel α a)"
proof-
interpret Set_Par: wide_replete_subcategory α ‹cat_Set α› ‹cat_Par α›
by (rule wide_replete_subcategory_cat_Set_cat_Par)
interpret Par_Rel: wide_replete_subcategory α ‹cat_Par α› ‹cat_Rel α›
by (rule wide_replete_subcategory_cat_Par_cat_Rel)
interpret Set_Rel: wide_replete_subcategory α ‹cat_Set α› ‹cat_Rel α›
by
(
rule wr_subcat_trans
[
OF
Set_Par.wide_replete_subcategory_axioms
Par_Rel.wide_replete_subcategory_axioms
]
)
show ?thesis
proof(rule monoidal_categoryI)
show "vfsequence (mcat_Rel α a)" unfolding mcat_Rel_def by auto
show "category α (mcat_Rel α a⦇Mcat⦈)"
unfolding mcat_Rel_components
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show "mcat_Rel α a⦇Mcf⦈ :
mcat_Rel α a⦇Mcat⦈ ×⇩C mcat_Rel α a⦇Mcat⦈ ↦↦⇩C⇘α⇙ mcat_Rel α a⦇Mcat⦈"
unfolding mcat_Rel_components
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show "mcat_Rel α a⦇Mα⦈ :
cf_blcomp (mcat_Rel α a⦇Mcf⦈) ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_brcomp (mcat_Rel α a⦇Mcf⦈) :
mcat_Rel α a⦇Mcat⦈^⇩C⇩3 ↦↦⇩C⇘α⇙ mcat_Rel α a⦇Mcat⦈"
unfolding mcat_Rel_components
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms show "mcat_Rel α a⦇Ml⦈ :
mcat_Rel α a⦇Mcf⦈⇘mcat_Rel α a⦇Mcat⦈,mcat_Rel α a⦇Mcat⦈⇙ (mcat_Rel α a⦇Me⦈,-)⇩C⇩F
↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (mcat_Rel α a⦇Mcat⦈) :
mcat_Rel α a⦇Mcat⦈ ↦↦⇩C⇘α⇙ mcat_Rel α a⦇Mcat⦈"
unfolding mcat_Rel_components
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms show "mcat_Rel α a⦇Mr⦈ :
mcat_Rel α a⦇Mcf⦈⇘mcat_Rel α a⦇Mcat⦈,mcat_Rel α a⦇Mcat⦈⇙ (-,mcat_Rel α a⦇Me⦈)⇩C⇩F
↦⇩C⇩F⇩.⇩i⇩s⇩o
cf_id (mcat_Rel α a⦇Mcat⦈) : mcat_Rel α a⦇Mcat⦈ ↦↦⇩C⇘α⇙ mcat_Rel α a⦇Mcat⦈"
unfolding mcat_Rel_components
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show "vcard (mcat_Rel α a) = 6⇩ℕ"
unfolding mcat_Rel_def by (simp add: nat_omega_simps)
from assms show "mcat_Rel α a⦇Me⦈ ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈"
unfolding mcat_Rel_components cat_Rel_components by force
show
"mcat_Rel α a⦇Mcat⦈⦇CId⦈⦇A⦈ ⊗⇩H⇩M⇩.⇩A⇘mcat_Rel α a⦇Mcf⦈⇙
mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇B, C, D⦈⇩∙ ∘⇩A⇘mcat_Rel α a⦇Mcat⦈⇙
mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇
A, B ⊗⇩H⇩M⇩.⇩O⇘mcat_Rel α a⦇Mcf⦈⇙ C, D
⦈⇩∙ ∘⇩A⇘mcat_Rel α a⦇Mcat⦈⇙
(mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇A, B, C⦈⇩∙ ⊗⇩H⇩M⇩.⇩A⇘mcat_Rel α a⦇Mcf⦈⇙
mcat_Rel α a⦇Mcat⦈⦇CId⦈⦇D⦈) =
mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇
A, B, C ⊗⇩H⇩M⇩.⇩O⇘mcat_Rel α a⦇Mcf⦈⇙ D
⦈⇩∙ ∘⇩A⇘mcat_Rel α a⦇Mcat⦈⇙
mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇A ⊗⇩H⇩M⇩.⇩O⇘mcat_Rel α a⦇Mcf⦈⇙ B, C, D⦈⇩∙"
if "A ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈"
and "B ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈"
and "C ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈"
and "D ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈"
for A B C D
proof-
have [cat_cs_simps]:
"(cat_Rel α⦇CId⦈⦇A⦈) ⇩A×⇩R⇩e⇩l (Mα_Rel_arrow_lr B C D) ∘⇩A⇘cat_Rel α⇙
(
Mα_Rel_arrow_lr A (B ×⇩∘ C) D ∘⇩A⇘cat_Rel α⇙
(Mα_Rel_arrow_lr A B C) ⇩A×⇩R⇩e⇩l (cat_Rel α⦇CId⦈⦇D⦈)
) =
Mα_Rel_arrow_lr A B (C ×⇩∘ D) ∘⇩A⇘cat_Rel α⇙
Mα_Rel_arrow_lr (A ×⇩∘ B) C D"
(
is
‹
?A_BCD ∘⇩A⇘cat_Rel α⇙ (?A_BC_D ∘⇩A⇘cat_Rel α⇙ ?ABC_D) =
?A_B_CD ∘⇩A⇘cat_Rel α⇙ ?AB_C_D
›
)
proof-
have [cat_cs_simps]:
"(cat_Set α⦇CId⦈⦇A⦈) ⇩A×⇩R⇩e⇩l (Mα_Rel_arrow_lr B C D) ∘⇩A⇘cat_Set α⇙
(
?A_BC_D ∘⇩A⇘cat_Set α⇙
(Mα_Rel_arrow_lr A B C) ⇩A×⇩R⇩e⇩l (cat_Set α⦇CId⦈⦇D⦈)
) = ?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D"
(
is
‹
?A_BCD ∘⇩A⇘cat_Set α⇙ (?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D) =
?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D
›
)
proof-
from that have lhs:
"?A_BCD ∘⇩A⇘cat_Set α⇙ (?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D) :
((A ×⇩∘ B) ×⇩∘ C) ×⇩∘ D ↦⇘cat_Set α⇙ A ×⇩∘ B ×⇩∘ C ×⇩∘ D"
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_Set_components(1)
cs_intro: cat_rel_par_Set_cs_intros cat_cs_intros V_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((?A_BCD ∘⇩A⇘cat_Set α⇙ (?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D))⦇ArrVal⦈) =
((A ×⇩∘ B) ×⇩∘ C) ×⇩∘ D"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from that have rhs: "?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D :
((A ×⇩∘ B) ×⇩∘ C) ×⇩∘ D ↦⇘cat_Set α⇙ A ×⇩∘ B ×⇩∘ C ×⇩∘ D"
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_Rel_components(1) cat_Set_components(1)
cs_intro:
cat_cs_intros V_cs_intros Mα_Rel_arrow_lr_is_cat_Set_arr'
)
then have dom_rhs:
"𝒟⇩∘ ((?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D)⦇ArrVal⦈) =
((A ×⇩∘ B) ×⇩∘ C) ×⇩∘ D"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set α (?A_BCD ∘⇩A⇘cat_Set α⇙ (?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D))"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs:
"arr_Set α (?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D)"
by (auto dest: cat_Set_is_arrD(1))
show
"(?A_BCD ∘⇩A⇘cat_Set α⇙ (?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D))⦇ArrVal⦈ =
(?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D)⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix abcd assume prems: "abcd ∈⇩∘ ((A ×⇩∘ B) ×⇩∘ C) ×⇩∘ D"
then obtain a b c d
where abcd_def: "abcd = ⟨⟨⟨a, b⟩, c⟩, d⟩"
and a: "a ∈⇩∘ A"
and b: "b ∈⇩∘ B"
and c: "c ∈⇩∘ C"
and d: "d ∈⇩∘ D"
by clarsimp
from that prems a b c d show
"(
?A_BCD ∘⇩A⇘cat_Set α⇙
(?A_BC_D ∘⇩A⇘cat_Set α⇙ ?ABC_D)
)⦇ArrVal⦈⦇abcd⦈ =
(?A_B_CD ∘⇩A⇘cat_Set α⇙ ?AB_C_D)⦇ArrVal⦈⦇abcd⦈"
unfolding abcd_def mcat_Rel_components(1) cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp:
cat_Set_components(1)
cat_cs_simps
cat_rel_par_Set_cs_simps
cs_intro:
cat_cs_intros cat_rel_par_Set_cs_intros V_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
from assms that show ?thesis
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp:
cat_cs_simps
cat_Rel_components(1)
cat_Set_components(1)
Set_Rel.subcat_CId[symmetric]
Set_Rel.subcat_Comp_simp[symmetric]
cs_intro: cat_cs_intros cat_rel_par_Set_cs_intros V_cs_intros
)+
qed
from that show ?thesis
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_Rel_components(1) cat_cs_simps
cs_intro:
cat_cs_intros
cat_Rel_par_set_cs_intros
V_cs_intros
cat_prod_cs_intros
)
qed
show
"mcat_Rel α a⦇Mcat⦈⦇CId⦈⦇A⦈ ⊗⇩H⇩M⇩.⇩A⇘mcat_Rel α a⦇Mcf⦈⇙
mcat_Rel α a⦇Ml⦈⦇NTMap⦈⦇B⦈ ∘⇩A⇘mcat_Rel α a⦇Mcat⦈⇙
mcat_Rel α a⦇Mα⦈⦇NTMap⦈⦇A, mcat_Rel α a⦇Me⦈, B⦈⇩∙ =
mcat_Rel α a⦇Mr⦈⦇NTMap⦈⦇A⦈ ⊗⇩H⇩M⇩.⇩A⇘mcat_Rel α a⦇Mcf⦈⇙
mcat_Rel α a⦇Mcat⦈⦇CId⦈⦇B⦈"
if "A ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈" and "B ∈⇩∘ mcat_Rel α a⦇Mcat⦈⦇Obj⦈" for A B
proof-
note [cat_cs_simps] = set_empty
have [cat_cs_simps]:
"(cat_Set α⦇CId⦈⦇A⦈) ⇩A×⇩R⇩e⇩l (vsnd_arrow (set {a}) B) ∘⇩A⇘cat_Set α⇙
Mα_Rel_arrow_lr A (set {a}) B =
(vfst_arrow A (set {a})) ⇩A×⇩R⇩e⇩l (cat_Set α⦇CId⦈⦇B⦈)"
(is ‹?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB = ?Aa_B›)
proof-
from assms that have lhs:
"?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB : (A ×⇩∘ set {a}) ×⇩∘ B ↦⇘cat_Set α⇙ A ×⇩∘ B"
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Rel_components(1) cat_Set_components(1)
cs_intro: cat_cs_intros cat_rel_par_Set_cs_intros V_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB)⦇ArrVal⦈) = (A ×⇩∘ set {a}) ×⇩∘ B"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms that have rhs:
"?Aa_B : (A ×⇩∘ set {a}) ×⇩∘ B ↦⇘cat_Set α⇙ A ×⇩∘ B"
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Set_components(1)
cs_intro: cat_cs_intros cat_rel_par_Set_cs_intros V_cs_intros
)
then have dom_rhs: "𝒟⇩∘ (?Aa_B⦇ArrVal⦈) = (A ×⇩∘ set {a}) ×⇩∘ B"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs: "arr_Set α (?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs: "arr_Set α ?Aa_B"
by (auto dest: cat_Set_is_arrD(1))
show "(?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB)⦇ArrVal⦈ = ?Aa_B⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix xay assume "xay ∈⇩∘ (A ×⇩∘ set {a}) ×⇩∘ B"
then obtain x y
where xay_def: "xay = ⟨⟨x, a⟩, y⟩" and x: "x ∈⇩∘ A" and y: "y ∈⇩∘ B"
by auto
from assms that x y show
"(?A_aB ∘⇩A⇘cat_Set α⇙ ?AaB)⦇ArrVal⦈⦇xay⦈ = ?Aa_B⦇ArrVal⦈⦇xay⦈"
unfolding xay_def mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp:
cat_Rel_components(1) cat_Set_components(1)
cat_cs_simps cat_rel_par_Set_cs_simps
cs_intro:
cat_cs_intros cat_rel_par_Set_cs_intros V_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_simp: cat_cs_simps›)+
qed
from assms that show ?thesis
unfolding mcat_Rel_components cat_Rel_components(1)
by
(
cs_concl cs_shallow
cs_simp:
cat_cs_simps
cat_Rel_components(1)
cat_Set_components(1)
Set_Rel.subcat_CId[symmetric]
Set_Rel.subcat_Comp_simp[symmetric]
cs_intro:
cat_cs_intros
cat_rel_par_Set_cs_intros
V_cs_intros
cat_prod_cs_intros
Set_Rel.subcat_is_arrD
)
qed
qed auto
qed
subsection‹Dagger monoidal categories›
subsubsection‹Background›
text‹See \<^cite>‹"coecke_survey_2010"› for further information.›
named_theorems dmcat_field_simps
named_theorems dmcat_cs_simps
named_theorems dmcat_cs_intros
definition DMcat :: V where [dmcat_field_simps]: "DMcat = 0"
definition DMdag :: V where [dmcat_field_simps]: "DMdag = 1⇩ℕ"
definition DMcf :: V where [dmcat_field_simps]: "DMcf = 2⇩ℕ"
definition DMe :: V where [dmcat_field_simps]: "DMe = 3⇩ℕ"
definition DMα :: V where [dmcat_field_simps]: "DMα = 4⇩ℕ"
definition DMl :: V where [dmcat_field_simps]: "DMl = 5⇩ℕ"
definition DMr :: V where [dmcat_field_simps]: "DMr = 6⇩ℕ"
abbreviation DMDag_app :: "V ⇒ V" (‹†⇩M⇩C›)
where "†⇩M⇩C ℭ ≡ ℭ⦇DMdag⦈"
subsubsection‹Slicing›
text‹Dagger category.›
definition dmcat_dagcat :: "V ⇒ V"
where "dmcat_dagcat ℭ = [ℭ⦇DMcat⦈, ℭ⦇DMdag⦈]⇩∘"
lemma dmcat_dagcat_components[slicing_simps]:
shows "dmcat_dagcat ℭ⦇DagCat⦈ = ℭ⦇DMcat⦈"
and "dmcat_dagcat ℭ⦇DagDag⦈ = ℭ⦇DMdag⦈"
unfolding dmcat_dagcat_def dmcat_field_simps dag_field_simps
by (auto simp: nat_omega_simps)
text‹Monoidal category.›
definition dmcat_mcat :: "V ⇒ V"
where "dmcat_mcat ℭ = [ℭ⦇DMcat⦈, ℭ⦇DMcf⦈, ℭ⦇DMe⦈, ℭ⦇DMα⦈, ℭ⦇DMl⦈, ℭ⦇DMr⦈]⇩∘"
lemma dmcat_mcat_components[slicing_simps]:
shows "dmcat_mcat ℭ⦇Mcat⦈ = ℭ⦇DMcat⦈"
and "dmcat_mcat ℭ⦇Mcf⦈ = ℭ⦇DMcf⦈"
and "dmcat_mcat ℭ⦇Me⦈ = ℭ⦇DMe⦈"
and "dmcat_mcat ℭ⦇Mα⦈ = ℭ⦇DMα⦈"
and "dmcat_mcat ℭ⦇Ml⦈ = ℭ⦇DMl⦈"
and "dmcat_mcat ℭ⦇Mr⦈ = ℭ⦇DMr⦈"
unfolding dmcat_mcat_def dmcat_field_simps mcat_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹Definition and elementary properties›
locale dagger_monoidal_category = 𝒵 α + vfsequence ℭ for α ℭ +
assumes dmcat_length[dmcat_cs_simps]: "vcard ℭ = 7⇩ℕ"
and dmcat_dagger_category: "dagger_category α (dmcat_dagcat ℭ)"
and dmcat_monoidal_category: "monoidal_category α (dmcat_mcat ℭ)"
and dmcat_compatibility:
"⟦ g : c ↦⇘ℭ⦇DMcat⦈⇙ d; f : a ↦⇘ℭ⦇DMcat⦈⇙ b ⟧ ⟹
†⇩M⇩C ℭ⦇ArrMap⦈⦇g ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇DMcf⦈⇙ f⦈ =
†⇩M⇩C ℭ⦇ArrMap⦈⦇g⦈ ⊗⇩H⇩M⇩.⇩A⇘ℭ⦇DMcf⦈⇙ †⇩M⇩C ℭ⦇ArrMap⦈⦇f⦈"
and dmcat_Mα_unital: "A ∈⇩∘ (ℭ⦇DMcat⦈^⇩C⇩3)⦇Obj⦈ ⟹
†⇩M⇩C ℭ⦇ArrMap⦈⦇ℭ⦇DMα⦈⦇NTMap⦈⦇A⦈⦈ = (ℭ⦇DMα⦈⦇NTMap⦈⦇A⦈)¯⇩C⇘ℭ⦇DMcat⦈⇙"
and dmcat_Ml_unital: "a ∈⇩∘ ℭ⦇DMcat⦈⦇Obj⦈ ⟹
†⇩M⇩C ℭ⦇ArrMap⦈⦇ℭ⦇DMl⦈⦇NTMap⦈⦇a⦈⦈ = (ℭ⦇DMl⦈⦇NTMap⦈⦇a⦈)¯⇩C⇘ℭ⦇DMcat⦈⇙"
and dmcat_Mr_unital: "a ∈⇩∘ ℭ⦇DMcat⦈⦇Obj⦈ ⟹
†⇩M⇩C ℭ⦇ArrMap⦈⦇ℭ⦇DMr⦈⦇NTMap⦈⦇a⦈⦈ = (ℭ⦇DMr⦈⦇NTMap⦈⦇a⦈)¯⇩C⇘ℭ⦇DMcat⦈⇙"
text‹Rules.›
lemma (in dagger_monoidal_category)
dagger_monoidal_category_axioms'[dmcat_cs_intros]:
assumes "α' = α"
shows "dagger_monoidal_category α' ℭ"
unfolding assms by (rule dagger_monoidal_category_axioms)
mk_ide rf
dagger_monoidal_category_def[unfolded dagger_monoidal_category_axioms_def]
|intro dagger_monoidal_categoryI[intro]|
|dest dagger_monoidal_categoryD[dest]|
|elim dagger_monoidal_categoryE[elim]|
text‹Elementary properties.›
lemma dmcat_eqI:
assumes "dagger_monoidal_category α 𝔄"
and "dagger_monoidal_category α 𝔅"
and "𝔄⦇DMcat⦈ = 𝔅⦇DMcat⦈"
and "𝔄⦇DMdag⦈ = 𝔅⦇DMdag⦈"
and "𝔄⦇DMcf⦈ = 𝔅⦇DMcf⦈"
and "𝔄⦇DMe⦈ = 𝔅⦇DMe⦈"
and "𝔄⦇DMα⦈ = 𝔅⦇DMα⦈"
and "𝔄⦇DMl⦈ = 𝔅⦇DMl⦈"
and "𝔄⦇DMr⦈ = 𝔅⦇DMr⦈"
shows "𝔄 = 𝔅"
proof-
interpret 𝔄: dagger_monoidal_category α 𝔄 by (rule assms(1))
interpret 𝔅: dagger_monoidal_category α 𝔅 by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ 𝔄 = 7⇩ℕ"
by (cs_concl cs_shallow cs_simp: dmcat_cs_simps V_cs_simps)
show "𝒟⇩∘ 𝔄 = 𝒟⇩∘ 𝔅"
by (cs_concl cs_shallow cs_simp: dmcat_cs_simps V_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert assms)
(auto simp: dmcat_field_simps)
qed auto
qed
text‹Slicing.›
context dagger_monoidal_category
begin
interpretation dagcat: dagger_category α ‹dmcat_dagcat ℭ›
by (rule dmcat_dagger_category)
sublocale DMCat: category α ‹ℭ⦇DMcat⦈›
by (rule dagcat.DagCat.category_axioms[unfolded slicing_simps])
sublocale DMDag: is_functor α ‹op_cat (ℭ⦇DMcat⦈)› ‹ℭ⦇DMcat⦈› ‹†⇩M⇩C ℭ›
by (rule dagcat.DagDag.is_functor_axioms[unfolded slicing_simps])
lemmas_with [unfolded slicing_simps]:
dmcat_Dom_vdomain[dmcat_cs_simps] = dagcat.dagcat_ObjMap_identity
and dmcat_DagCat_idem[dmcat_cs_simps] = dagcat.dagcat_DagCat_idem
and dmcat_is_functor'[dmcat_cs_intros] = dagcat.dagcat_is_functor'
end
lemmas [dmcat_cs_simps] =
dagger_monoidal_category.dmcat_Dom_vdomain
dagger_monoidal_category.dmcat_DagCat_idem
lemmas [dmcat_cs_intros] = dagger_monoidal_category.dmcat_is_functor'
context dagger_monoidal_category
begin
interpretation mcat: monoidal_category α ‹dmcat_mcat ℭ›
by (rule dmcat_monoidal_category)
sublocale DMcf: is_functor α ‹ℭ⦇DMcat⦈ ×⇩C ℭ⦇DMcat⦈› ‹ℭ⦇DMcat⦈› ‹ℭ⦇DMcf⦈›
by (rule mcat.Mcf.is_functor_axioms[unfolded slicing_simps])
sublocale DMα: is_iso_ntcf
α ‹ℭ⦇DMcat⦈^⇩C⇩3› ‹ℭ⦇DMcat⦈› ‹cf_blcomp (ℭ⦇DMcf⦈)› ‹cf_brcomp (ℭ⦇DMcf⦈)› ‹ℭ⦇DMα⦈›
by (rule mcat.Mα.is_iso_ntcf_axioms[unfolded slicing_simps])
sublocale DMl: is_iso_ntcf
α
‹ℭ⦇DMcat⦈›
‹ℭ⦇DMcat⦈›
‹ℭ⦇DMcf⦈⇘ℭ⦇DMcat⦈,ℭ⦇DMcat⦈⇙(ℭ⦇DMe⦈,-)⇩C⇩F›
‹cf_id (ℭ⦇DMcat⦈)›
‹ℭ⦇DMl⦈›
by (rule mcat.Ml.is_iso_ntcf_axioms[unfolded slicing_simps])
sublocale DMr: is_iso_ntcf
α
‹ℭ⦇DMcat⦈›
‹ℭ⦇DMcat⦈›
‹ℭ⦇DMcf⦈⇘ℭ⦇DMcat⦈,ℭ⦇DMcat⦈⇙(-,ℭ⦇DMe⦈)⇩C⇩F›
‹cf_id (ℭ⦇DMcat⦈)›
‹ℭ⦇DMr⦈›
by (rule mcat.Mr.is_iso_ntcf_axioms[unfolded slicing_simps])
lemmas_with [unfolded slicing_simps]:
dmcat_Me_is_obj[dmcat_cs_intros] = mcat.mcat_Me_is_obj
and dmcat_pentagon = mcat.mcat_pentagon
and dmcat_triangle[dmcat_cs_simps] = mcat.mcat_triangle
end
lemmas [dmcat_cs_intros] = dagger_monoidal_category.dmcat_Me_is_obj
lemmas [dmcat_cs_simps] = dagger_monoidal_category.dmcat_triangle
subsection‹‹Rel› as a dagger monoidal category›
subsubsection‹Definition and elementary properties›
definition dmcat_Rel :: "V ⇒ V ⇒ V"
where "dmcat_Rel α a =
[
cat_Rel α,
†⇩C⇩.⇩R⇩e⇩l α,
cf_prod_2_Rel (cat_Rel α),
set {a},
Mα_Rel (cat_Rel α),
Ml_Rel (cat_Rel α) a,
Mr_Rel (cat_Rel α) a
]⇩∘"
text‹Components.›
lemma dmcat_Rel_components:
shows "dmcat_Rel α a⦇DMcat⦈ = cat_Rel α"
and "dmcat_Rel α a⦇DMdag⦈ = †⇩C⇩.⇩R⇩e⇩l α"
and "dmcat_Rel α a⦇DMcf⦈ = cf_prod_2_Rel (cat_Rel α)"
and "dmcat_Rel α a⦇DMe⦈ = set {a}"
and "dmcat_Rel α a⦇DMα⦈ = Mα_Rel (cat_Rel α)"
and "dmcat_Rel α a⦇DMl⦈ = Ml_Rel (cat_Rel α) a"
and "dmcat_Rel α a⦇DMr⦈ = Mr_Rel (cat_Rel α) a"
unfolding dmcat_Rel_def dmcat_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma dmcat_dagcat_dmcat_Rel: "dmcat_dagcat (dmcat_Rel α a) = dagcat_Rel α"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ (dmcat_dagcat (dmcat_Rel α a)) = 2⇩ℕ"
unfolding dmcat_dagcat_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (dagcat_Rel α) = 2⇩ℕ"
unfolding dagcat_Rel_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ (dmcat_dagcat (dmcat_Rel α a)) = 𝒟⇩∘ (dagcat_Rel α)"
unfolding dom_lhs dom_rhs by simp
show "A ∈⇩∘ 𝒟⇩∘ (dmcat_dagcat (dmcat_Rel α a)) ⟹
dmcat_dagcat (dmcat_Rel α a)⦇A⦈ = dagcat_Rel α⦇A⦈"
for A
by
(
unfold dom_lhs,
elim_in_numeral,
unfold dmcat_dagcat_def dmcat_field_simps dmcat_Rel_def dagcat_Rel_def
)
(auto simp: nat_omega_simps)
qed (auto simp: dmcat_dagcat_def dagcat_Rel_def)
lemma dmcat_mcat_dmcat_Rel: "dmcat_mcat (dmcat_Rel α a) = mcat_Rel α a"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ (dmcat_mcat (dmcat_Rel α a)) = 6⇩ℕ"
unfolding dmcat_mcat_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (mcat_Rel α a) = 6⇩ℕ"
unfolding mcat_Rel_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ (dmcat_mcat (dmcat_Rel α a)) = 𝒟⇩∘ (mcat_Rel α a)"
unfolding dom_lhs dom_rhs by simp
show "A ∈⇩∘ 𝒟⇩∘ (dmcat_mcat (dmcat_Rel α a)) ⟹
dmcat_mcat (dmcat_Rel α a)⦇A⦈ = mcat_Rel α a⦇A⦈"
for A
by
(
unfold dom_lhs,
elim_in_numeral,
unfold dmcat_mcat_def dmcat_field_simps dmcat_Rel_def mcat_Rel_def
)
(auto simp: nat_omega_simps)
qed (auto simp: dmcat_mcat_def mcat_Rel_def)
subsubsection‹‹Rel› is a dagger monoidal category›
lemma (in 𝒵) dagger_monoidal_category_dmcat_Rel:
assumes "A ∈⇩∘ cat_Rel α⦇Obj⦈"
shows "dagger_monoidal_category α (dmcat_Rel α A)"
proof-
interpret Rel: category α ‹cat_Rel α› by (rule category_cat_Rel)
interpret dag_Rel: is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†⇩C⇩.⇩R⇩e⇩l α›
by (rule cf_dag_Rel_is_iso_functor)
show ?thesis
proof(rule dagger_monoidal_categoryI)
show "𝒵 α" by auto
show "vfsequence (dmcat_Rel α A)" unfolding dmcat_Rel_def by simp
show "vcard (dmcat_Rel α A) = 7⇩ℕ"
unfolding dmcat_Rel_def by (simp add: nat_omega_simps)
show "dagger_category α (dmcat_dagcat (dmcat_Rel α A))"
unfolding dmcat_dagcat_dmcat_Rel by (rule dagger_category_dagcat_Rel)
show "monoidal_category α (dmcat_mcat (dmcat_Rel α A))"
unfolding dmcat_mcat_dmcat_Rel by (intro monoidal_category_mcat_Rel assms)
show
"†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇g ⊗⇩H⇩M⇩.⇩A⇘dmcat_Rel α A⦇DMcf⦈⇙ f⦈ =
†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇g⦈ ⊗⇩H⇩M⇩.⇩A⇘dmcat_Rel α A⦇DMcf⦈⇙
†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇f⦈"
if "g : c ↦⇘dmcat_Rel α A⦇DMcat⦈⇙ d" and "f : a ↦⇘dmcat_Rel α A⦇DMcat⦈⇙ b"
for c d g a b f
using that
unfolding dmcat_Rel_components
by
(
cs_concl cs_shallow
cs_simp: cf_dag_Rel_ArrMap_app_prod_2_Rel cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_prod_cs_intros cat_op_intros
)
show
"†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇dmcat_Rel α A⦇DMα⦈⦇NTMap⦈⦇BCD⦈⦈ =
(dmcat_Rel α A⦇DMα⦈⦇NTMap⦈⦇BCD⦈)¯⇩C⇘dmcat_Rel α A⦇DMcat⦈⇙"
if "BCD ∈⇩∘ (dmcat_Rel α A⦇DMcat⦈^⇩C⇩3)⦇Obj⦈" for BCD
proof-
from that obtain B C D
where BCD_def: "BCD = [B, C, D]⇩∘"
and B: "B ∈⇩∘ cat_Rel α⦇Obj⦈"
and C: "C ∈⇩∘ cat_Rel α⦇Obj⦈"
and D: "D ∈⇩∘ cat_Rel α⦇Obj⦈"
unfolding dmcat_Rel_components
by
(
elim cat_prod_3_ObjE
[
unfolded dmcat_Rel_components,
OF Rel.category_axioms Rel.category_axioms Rel.category_axioms
]
)
from B C D show ?thesis
unfolding dmcat_Rel_components BCD_def
by
(
cs_concl cs_shallow
cs_simp: cat_Rel_cs_simps cat_cs_simps
cs_intro:
cat_Rel_is_arrD
cat_cs_intros
cat_Rel_par_set_cs_intros
cat_prod_cs_intros
)
qed
show
"†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇dmcat_Rel α A⦇DMl⦈⦇NTMap⦈⦇B⦈⦈ =
(dmcat_Rel α A⦇DMl⦈⦇NTMap⦈⦇B⦈)¯⇩C⇘dmcat_Rel α A⦇DMcat⦈⇙"
if "B ∈⇩∘ dmcat_Rel α A⦇DMcat⦈⦇Obj⦈" for B
using assms that
unfolding dmcat_Rel_components
by
(
cs_concl cs_shallow
cs_simp: cat_Rel_cs_simps
cs_intro: cat_Rel_is_arrD cat_cs_intros cat_arrow_cs_intros
)+
show
"†⇩M⇩C (dmcat_Rel α A)⦇ArrMap⦈⦇dmcat_Rel α A⦇DMr⦈⦇NTMap⦈⦇B⦈⦈ =
(dmcat_Rel α A⦇DMr⦈⦇NTMap⦈⦇B⦈)¯⇩C⇘dmcat_Rel α A⦇DMcat⦈⇙"
if "B ∈⇩∘ dmcat_Rel α A⦇DMcat⦈⦇Obj⦈" for B
using assms that
unfolding dmcat_Rel_components
by
(
cs_concl cs_shallow
cs_simp: cat_Rel_cs_simps
cs_intro: cat_Rel_is_arrD cat_cs_intros cat_arrow_cs_intros
)+
qed
qed
text‹\newpage›
end