Theory CZH_SMC_Simple
section‹Simple semicategories›
theory CZH_SMC_Simple
imports
CZH_DG_Simple
CZH_SMC_NTSMCF
begin
subsection‹Background›
text‹
The section presents a variety of simple semicategories, such as the empty
semicategory ‹0› and a semicategory with one object and one arrow ‹1›.
All of the entities presented in this section are generalizations of certain
simple categories, whose definitions can be found
in \<^cite>‹"mac_lane_categories_2010"›.
›
subsection‹Empty semicategory ‹0››
subsubsection‹Definition and elementary properties›
text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›
definition smc_0 :: "V"
where "smc_0 = [0, 0, 0, 0, 0]⇩∘"
text‹Components.›
lemma smc_0_components:
shows "smc_0⦇Obj⦈ = 0"
and "smc_0⦇Arr⦈ = 0"
and "smc_0⦇Dom⦈ = 0"
and "smc_0⦇Cod⦈ = 0"
and "smc_0⦇Comp⦈ = 0"
unfolding smc_0_def dg_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma smc_dg_smc_0: "smc_dg smc_0 = dg_0"
unfolding smc_dg_def smc_0_def dg_0_def dg_field_simps
by (simp add: nat_omega_simps)
lemmas_with (in 𝒵) [folded smc_dg_smc_0, unfolded slicing_simps]:
smc_0_is_arr_iff = dg_0_is_arr_iff
subsubsection‹‹0› is a semicategory›
lemma (in 𝒵) semicategory_smc_0[smc_cs_intros]: "semicategory α smc_0"
proof(intro semicategoryI)
show "vfsequence smc_0" unfolding smc_0_def by (simp add: nat_omega_simps)
show "vcard smc_0 = 5⇩ℕ" unfolding smc_0_def by (simp add: nat_omega_simps)
show "digraph α (smc_dg smc_0)"
by (simp add: smc_dg_smc_0 𝒵.digraph_dg_0 𝒵_axioms)
qed (auto simp: smc_0_components smc_0_is_arr_iff)
lemmas [smc_cs_intros] = 𝒵.semicategory_smc_0
subsubsection‹Opposite of the semicategory ‹0››
lemma op_smc_smc_0[smc_op_simps]: "op_smc (smc_0) = smc_0"
proof(rule smc_dg_eqI)
define β where "β = ω + ω"
interpret β: 𝒵 β unfolding β_def by (rule 𝒵_ωω)
show "semicategory β (op_smc smc_0)"
by (cs_concl cs_shallow cs_intro: smc_cs_intros smc_op_intros)
show "semicategory β smc_0" by (cs_concl cs_shallow cs_intro: smc_cs_intros)
qed
(
simp_all add:
smc_0_components op_smc_components smc_dg_smc_0
slicing_commute[symmetric] dg_op_simps
)
subsubsection‹A semicategory without objects is empty›
lemma (in semicategory) smc_smc_0_if_Obj_0:
assumes "ℭ⦇Obj⦈ = 0"
shows "ℭ = smc_0"
by (rule smc_eqI[of α])
(
auto simp:
smc_cs_intros
assms
semicategory_smc_0
smc_0_components
smc_Arr_vempty_if_Obj_vempty
smc_Cod_vempty_if_Arr_vempty
smc_Dom_vempty_if_Arr_vempty
smc_Comp_vempty_if_Arr_vempty
)
subsection‹Empty semifunctor›
text‹
An empty semifunctor is defined as a semifunctor between an
empty semicategory and an arbitrary semicategory.
›
subsubsection‹Definition and elementary properties›
definition smcf_0 :: "V ⇒ V"
where "smcf_0 𝔄 = [0, 0, smc_0, 𝔄]⇩∘"
text‹Components.›
lemma smcf_0_components:
shows "smcf_0 𝔄⦇ObjMap⦈ = 0"
and "smcf_0 𝔄⦇ArrMap⦈ = 0"
and "smcf_0 𝔄⦇HomDom⦈ = smc_0"
and "smcf_0 𝔄⦇HomCod⦈ = 𝔄"
unfolding smcf_0_def dghm_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma smcf_dghm_smcf_0: "smcf_dghm (smcf_0 𝔄) = dghm_0 (smc_dg 𝔄)"
unfolding
smcf_dghm_def smcf_0_def dg_0_def smc_0_def dghm_0_def smc_dg_def
dg_field_simps dghm_field_simps
by (simp add: nat_omega_simps)
text‹Opposite empty semicategory homomorphism.›
lemma op_smcf_smcf_0: "op_smcf (smcf_0 ℭ) = smcf_0 (op_smc ℭ)"
unfolding
smcf_0_def op_smc_def op_smcf_def smc_0_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map›
lemma smcf_0_ObjMap_vsv[smc_cs_intros]: "vsv (smcf_0 ℭ⦇ObjMap⦈)"
unfolding smcf_0_components by simp
subsubsection‹Arrow map›
lemma smcf_0_ArrMap_vsv[smc_cs_intros]: "vsv (smcf_0 ℭ⦇ArrMap⦈)"
unfolding smcf_0_components by simp
subsubsection‹Empty semifunctor is a faithful semifunctor›
lemma (in 𝒵) smcf_0_is_ft_semifunctor:
assumes "semicategory α 𝔄"
shows "smcf_0 𝔄 : smc_0 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔄"
proof(rule is_ft_semifunctorI)
show "smcf_0 𝔄 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔄"
proof(rule is_semifunctorI, unfold smc_dg_smc_0 smcf_dghm_smcf_0)
show "vfsequence (smcf_0 𝔄)" unfolding smcf_0_def by simp
show "vcard (smcf_0 𝔄) = 4⇩ℕ"
unfolding smcf_0_def by (simp add: nat_omega_simps)
show "dghm_0 (smc_dg 𝔄) : dg_0 ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔄"
by
(
simp add:
assms
dghm_0_is_ft_dghm
is_ft_dghm.axioms(1)
semicategory.smc_digraph
)
qed (auto simp: assms semicategory_smc_0 smcf_0_components smc_0_is_arr_iff)
show "smcf_dghm (smcf_0 𝔄) : smc_dg smc_0 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ smc_dg 𝔄"
by
(
auto simp:
assms
𝒵.dghm_0_is_ft_dghm
𝒵_axioms
smc_dg_smc_0
semicategory.smc_digraph
smcf_dghm_smcf_0
)
qed
lemma (in 𝒵) smcf_0_is_ft_semifunctor'[smcf_cs_intros]:
assumes "semicategory α 𝔄"
and "𝔅' = 𝔄"
and "𝔄' = smc_0"
shows "smcf_0 𝔄 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule smcf_0_is_ft_semifunctor)
lemmas [smcf_cs_intros] = 𝒵.smcf_0_is_ft_semifunctor'
lemma (in 𝒵) smcf_0_is_semifunctor:
assumes "semicategory α 𝔄"
shows "smcf_0 𝔄 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔄"
using smcf_0_is_ft_semifunctor[OF assms] by auto
lemma (in 𝒵) smcf_0_is_semifunctor'[smc_cs_intros]:
assumes "semicategory α 𝔄"
and "𝔅' = 𝔄"
and "𝔄' = smc_0"
shows "smcf_0 𝔄 : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule smcf_0_is_semifunctor)
lemmas [smc_cs_intros] = 𝒵.smcf_0_is_semifunctor'
subsubsection‹Further properties›
lemma is_semifunctor_is_smcf_0_if_smc_0:
assumes "𝔉 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
shows "𝔉 = smcf_0 ℭ"
proof(rule smcf_dghm_eqI)
interpret 𝔉: is_semifunctor α smc_0 ℭ 𝔉 by (rule assms(1))
show "𝔉 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" by (rule assms(1))
then have dom_lhs: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 0" "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 0"
by (cs_concl cs_simp: smc_cs_simps smc_0_components)+
show "smcf_0 ℭ : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" by (cs_concl cs_intro: smc_cs_intros)
show "smcf_dghm 𝔉 = smcf_dghm (smcf_0 ℭ)"
unfolding smcf_dghm_smcf_0
by
(
rule is_dghm_is_dghm_0_if_dg_0,
rule 𝔉.smcf_is_dghm[unfolded slicing_simps smc_dg_smc_0]
)
qed simp_all
subsection‹Empty natural transformation of semifunctors›
subsubsection‹Definition and elementary properties›
definition ntsmcf_0 :: "V ⇒ V"
where "ntsmcf_0 ℭ = [0, smcf_0 ℭ, smcf_0 ℭ, smc_0, ℭ]⇩∘"
text‹Components.›
lemma ntsmcf_0_components:
shows "ntsmcf_0 ℭ⦇NTMap⦈ = 0"
and [smc_cs_simps]: "ntsmcf_0 ℭ⦇NTDom⦈ = smcf_0 ℭ"
and [smc_cs_simps]: "ntsmcf_0 ℭ⦇NTCod⦈ = smcf_0 ℭ"
and [smc_cs_simps]: "ntsmcf_0 ℭ⦇NTDGDom⦈ = smc_0"
and [smc_cs_simps]: "ntsmcf_0 ℭ⦇NTDGCod⦈ = ℭ"
unfolding ntsmcf_0_def nt_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma ntsmcf_tdghm_ntsmcf_0: "ntsmcf_tdghm (ntsmcf_0 𝔄) = tdghm_0 (smc_dg 𝔄)"
unfolding
ntsmcf_tdghm_def ntsmcf_0_def tdghm_0_def smcf_dghm_def
smcf_0_def smc_dg_def smc_0_def dghm_0_def dg_0_def
dg_field_simps dghm_field_simps nt_field_simps
by (simp add: nat_omega_simps)
text‹Duality.›
lemma op_ntsmcf_ntsmcf_0: "op_ntsmcf (ntsmcf_0 ℭ) = ntsmcf_0 (op_smc ℭ)"
by
(
simp_all add:
op_ntsmcf_def ntsmcf_0_def op_smc_def op_smcf_smcf_0 smc_0_def
nt_field_simps dg_field_simps nat_omega_simps
)
subsubsection‹Natural transformation map›
lemma ntsmcf_0_NTMap_vsv[smc_cs_intros]: "vsv (ntsmcf_0 ℭ⦇NTMap⦈)"
unfolding ntsmcf_0_components by simp
lemma ntsmcf_0_NTMap_vdomain[smc_cs_simps]: "𝒟⇩∘ (ntsmcf_0 ℭ⦇NTMap⦈) = 0"
unfolding ntsmcf_0_components by simp
lemma ntsmcf_0_NTMap_vrange[smc_cs_simps]: "ℛ⇩∘ (ntsmcf_0 ℭ⦇NTMap⦈) = 0"
unfolding ntsmcf_0_components by simp
subsubsection‹
Empty natural transformation of semifunctors
is a natural transformation of semifunctors
›
lemma (in semicategory) smc_ntsmcf_0_is_ntsmcfI:
"ntsmcf_0 ℭ : smcf_0 ℭ ↦⇩S⇩M⇩C⇩F smcf_0 ℭ : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof(intro is_ntsmcfI)
show "vfsequence (ntsmcf_0 ℭ)" unfolding ntsmcf_0_def by simp
show "vcard (ntsmcf_0 ℭ) = 5⇩ℕ"
unfolding ntsmcf_0_def by (simp add: nat_omega_simps)
show "ntsmcf_tdghm (ntsmcf_0 ℭ) :
smcf_dghm (smcf_0 ℭ) ↦⇩D⇩G⇩H⇩M smcf_dghm (smcf_0 ℭ) :
smc_dg smc_0 ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
unfolding ntsmcf_tdghm_ntsmcf_0 smcf_dghm_smcf_0 smc_dg_smc_0
by (cs_concl cs_shallow cs_intro: dg_cs_intros slicing_intros)
show
"ntsmcf_0 ℭ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ smcf_0 ℭ⦇ArrMap⦈⦇f⦈ =
smcf_0 ℭ⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ ntsmcf_0 ℭ⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘smc_0⇙ b" for a b f
using that by (elim is_arrE) (auto simp: smc_0_components)
qed
(
cs_concl cs_shallow
cs_simp: smc_cs_simps smc_0_components(1) cs_intro: smc_cs_intros
)+
lemma (in semicategory) smc_ntsmcf_0_is_ntsmcfI'[smc_cs_intros]:
assumes "𝔉' = smcf_0 ℭ"
and "𝔊' = smcf_0 ℭ"
and "𝔄' = smc_0"
and "𝔅' = ℭ"
and "𝔉' = 𝔉"
and "𝔊' = 𝔊"
shows "ntsmcf_0 ℭ : 𝔉' ↦⇩S⇩M⇩C⇩F 𝔊' : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule smc_ntsmcf_0_is_ntsmcfI)
lemmas [smc_cs_intros] = semicategory.smc_ntsmcf_0_is_ntsmcfI'
lemma is_ntsmcf_is_ntsmcf_0_if_smc_0:
assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
shows "𝔑 = ntsmcf_0 ℭ" and "𝔉 = smcf_0 ℭ" and "𝔊 = smcf_0 ℭ"
proof-
interpret 𝔑: is_ntsmcf α smc_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
note is_tdghm_is_tdghm_0_if_dg_0 = is_tdghm_is_tdghm_0_if_dg_0
[
OF 𝔑.ntsmcf_is_tdghm[unfolded smc_dg_smc_0],
folded smcf_dghm_smcf_0 ntsmcf_tdghm_ntsmcf_0
]
show 𝔉_def: "𝔉 = smcf_0 ℭ" and 𝔊_def: "𝔊 = smcf_0 ℭ"
by (all‹intro is_semifunctor_is_smcf_0_if_smc_0›)
(cs_concl cs_shallow cs_intro: smc_cs_intros)+
show "𝔑 = ntsmcf_0 ℭ"
proof(rule ntsmcf_tdghm_eqI)
show "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" by (rule assms(1))
show "ntsmcf_0 ℭ : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: 𝔉_def 𝔊_def cs_intro: smc_cs_intros)
qed (simp_all add: 𝔉_def 𝔊_def is_tdghm_is_tdghm_0_if_dg_0)
qed
subsubsection‹Further properties›
lemma ntsmcf_vcomp_ntsmcf_ntsmcf_0[smc_cs_simps]:
assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
shows "𝔑 ∙⇩N⇩T⇩S⇩M⇩C⇩F ntsmcf_0 ℭ = ntsmcf_0 ℭ"
proof-
interpret 𝔑: is_ntsmcf α smc_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
show ?thesis
unfolding is_ntsmcf_is_ntsmcf_0_if_smc_0[OF assms]
proof(rule ntsmcf_eqI)
show "ntsmcf_0 ℭ ∙⇩N⇩T⇩S⇩M⇩C⇩F ntsmcf_0 ℭ :
smcf_0 ℭ ↦⇩S⇩M⇩C⇩F smcf_0 ℭ : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (cs_concl cs_intro: smc_cs_intros)
then have dom_lhs: "𝒟⇩∘ ((ntsmcf_0 ℭ ∙⇩N⇩T⇩S⇩M⇩C⇩F ntsmcf_0 ℭ)⦇NTMap⦈) = 0"
by
(
cs_concl
cs_simp: smc_cs_simps smc_0_components cs_intro: smc_cs_intros
)
show "ntsmcf_0 ℭ : smcf_0 ℭ ↦⇩S⇩M⇩C⇩F smcf_0 ℭ : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (cs_concl cs_intro: smc_cs_intros)
then have dom_rhs: "𝒟⇩∘ (ntsmcf_0 ℭ⦇NTMap⦈) = 0"
by
(
cs_concl
cs_simp: smc_cs_simps smc_0_components cs_intro: smc_cs_intros
)
show "(ntsmcf_0 ℭ ∙⇩N⇩T⇩S⇩M⇩C⇩F ntsmcf_0 ℭ)⦇NTMap⦈ = ntsmcf_0 ℭ⦇NTMap⦈"
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: smc_cs_intros)
qed simp_all
qed
lemma ntsmcf_vcomp_ntsmcf_0_ntsmcf[smc_cs_simps]:
assumes "𝔑 : 𝔉 ↦⇩S⇩M⇩C⇩F 𝔊 : smc_0 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
shows "ntsmcf_0 ℭ ∙⇩N⇩T⇩S⇩M⇩C⇩F 𝔑 = ntsmcf_0 ℭ"
proof-
interpret 𝔑: is_ntsmcf α smc_0 ℭ 𝔉 𝔊 𝔑 by (rule assms(1))
show ?thesis
unfolding is_ntsmcf_is_ntsmcf_0_if_smc_0[OF assms]
by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
qed
subsection‹‹10›: semicategory with one object and no arrows›
subsubsection‹Definition and elementary properties›
definition smc_10 :: "V ⇒ V"
where "smc_10 𝔞 = [set {𝔞}, 0, 0, 0, 0]⇩∘"
text‹Components.›
lemma smc_10_components:
shows "smc_10 𝔞⦇Obj⦈ = set {𝔞}"
and "smc_10 𝔞⦇Arr⦈ = 0"
and "smc_10 𝔞⦇Dom⦈ = 0"
and "smc_10 𝔞⦇Cod⦈ = 0"
and "smc_10 𝔞⦇Comp⦈ = 0"
unfolding smc_10_def dg_field_simps by (auto simp: nat_omega_simps)
text‹Slicing.›
lemma smc_dg_smc_10: "smc_dg (smc_10 𝔞) = (dg_10 𝔞)"
unfolding smc_dg_def smc_10_def dg_10_def dg_field_simps
by (simp add: nat_omega_simps)
lemmas_with (in 𝒵) [folded smc_dg_smc_10, unfolded slicing_simps]:
smc_10_is_arr_iff = dg_10_is_arr_iff
subsubsection‹‹10› is a semicategory›
lemma (in 𝒵) semicategory_smc_10:
assumes "𝔞 ∈⇩∘ Vset α"
shows "semicategory α (smc_10 𝔞)"
proof(intro semicategoryI)
show "vfsequence (smc_10 𝔞)"
unfolding smc_10_def by (simp add: nat_omega_simps)
show "vcard (smc_10 𝔞) = 5⇩ℕ"
unfolding smc_10_def by (simp add: nat_omega_simps)
show "digraph α (smc_dg (smc_10 𝔞))"
unfolding smc_dg_smc_10 by (rule digraph_dg_10[OF assms])
qed (auto simp: smc_10_components smc_10_is_arr_iff vsubset_vsingleton_leftI)
subsubsection‹Arrow with a domain and a codomain›
lemma smc_10_is_arr_iff: "𝔉 : 𝔄 ↦⇘smc_10 𝔞⇙ 𝔅 ⟷ False"
unfolding is_arr_def smc_10_components by simp
subsection‹‹1›: semicategory with one object and one arrow›
subsubsection‹Definition and elementary properties›
definition smc_1 :: "V ⇒ V ⇒ V"
where "smc_1 𝔞 𝔣 =
[set {𝔞}, set {𝔣}, set {⟨𝔣, 𝔞⟩}, set {⟨𝔣, 𝔞⟩}, set {⟨[𝔣, 𝔣]⇩∘, 𝔣⟩}]⇩∘"
text‹Components.›
lemma smc_1_components:
shows "smc_1 𝔞 𝔣⦇Obj⦈ = set {𝔞}"
and "smc_1 𝔞 𝔣⦇Arr⦈ = set {𝔣}"
and "smc_1 𝔞 𝔣⦇Dom⦈ = set {⟨𝔣, 𝔞⟩}"
and "smc_1 𝔞 𝔣⦇Cod⦈ = set {⟨𝔣, 𝔞⟩}"
and "smc_1 𝔞 𝔣⦇Comp⦈ = set {⟨[𝔣, 𝔣]⇩∘, 𝔣⟩}"
unfolding smc_1_def dg_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma dg_smc_1: "smc_dg (smc_1 𝔞 𝔣) = dg_1 𝔞 𝔣"
unfolding smc_dg_def smc_1_def dg_1_def dg_field_simps
by (simp add: nat_omega_simps)
lemmas_with [folded dg_smc_1, unfolded slicing_simps]:
smc_1_is_arrI = dg_1_is_arrI
and smc_1_is_arrD = dg_1_is_arrD
and smc_1_is_arrE = dg_1_is_arrE
and smc_1_is_arr_iff = dg_1_is_arr_iff
subsubsection‹Composition›
lemma smc_1_Comp_app[simp]: "𝔣 ∘⇩A⇘smc_1 𝔞 𝔣⇙ 𝔣 = 𝔣"
unfolding smc_1_components by simp
subsubsection‹‹1› is a semicategory›
lemma (in 𝒵) semicategory_smc_1:
assumes "𝔞 ∈⇩∘ Vset α" and "𝔣 ∈⇩∘ Vset α"
shows "semicategory α (smc_1 𝔞 𝔣)"
proof(intro semicategoryI, unfold dg_smc_1)
show "vfsequence (smc_1 𝔞 𝔣)"
unfolding smc_1_def by (simp add: nat_omega_simps)
show "vcard (smc_1 𝔞 𝔣) = 5⇩ℕ"
unfolding smc_1_def by (simp add: nat_omega_simps)
qed
(
auto simp:
assms
digraph_dg_1
smc_1_is_arr_iff
smc_1_components
vsubset_vsingleton_leftI
)
text‹\newpage›
end