Theory CZH_SMC_Semifunctor
section‹Semifunctor›
theory CZH_SMC_Semifunctor
imports
CZH_DG_DGHM
CZH_SMC_Semicategory
begin
subsection‹Background›
named_theorems smcf_cs_simps
named_theorems smcf_cs_intros
named_theorems smc_cn_cs_simps
named_theorems smc_cn_cs_intros
lemmas [smc_cs_simps] = dg_shared_cs_simps
lemmas [smc_cs_intros] = dg_shared_cs_intros
subsubsection‹Slicing›
definition smcf_dghm :: "V ⇒ V"
where "smcf_dghm ℭ =
[ℭ⦇ObjMap⦈, ℭ⦇ArrMap⦈, smc_dg (ℭ⦇HomDom⦈), smc_dg (ℭ⦇HomCod⦈)]⇩∘"
text‹Components.›
lemma smcf_dghm_components:
shows [slicing_simps]: "smcf_dghm 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and [slicing_simps]: "smcf_dghm 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and [slicing_commute]: "smcf_dghm 𝔉⦇HomDom⦈ = smc_dg (𝔉⦇HomDom⦈)"
and [slicing_commute]: "smcf_dghm 𝔉⦇HomCod⦈ = smc_dg (𝔉⦇HomCod⦈)"
unfolding smcf_dghm_def dghm_field_simps by (auto simp: nat_omega_simps)
subsection‹Definition and elementary properties›
text‹
See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"› and the description
of the concept of a digraph homomorphism in the previous chapter.
›
locale is_semifunctor =
𝒵 α +
vfsequence 𝔉 +
HomDom: semicategory α 𝔄 +
HomCod: semicategory α 𝔅
for α 𝔄 𝔅 𝔉 +
assumes smcf_length[smc_cs_simps]: "vcard 𝔉 = 4⇩ℕ"
and smcf_is_dghm[slicing_intros]:
"smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔅"
and smcf_HomDom[smc_cs_simps]: "𝔉⦇HomDom⦈ = 𝔄"
and smcf_HomCod[smc_cs_simps]: "𝔉⦇HomCod⦈ = 𝔅"
and smcf_ArrMap_Comp[smc_cs_simps]: "⟦ g : b ↦⇘𝔄⇙ c; f : a ↦⇘𝔄⇙ b ⟧ ⟹
𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
syntax "_is_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩S⇩M⇩Cı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" ⇌ "CONST is_semifunctor α 𝔄 𝔅 𝔉"
abbreviation (input) is_cn_semifunctor :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "is_cn_semifunctor α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
syntax "_is_cn_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ⇩S⇩M⇩C↦↦ı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_semifunctor α 𝔄 𝔅 𝔉"
abbreviation all_smcfs :: "V ⇒ V"
where "all_smcfs α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
abbreviation smcfs :: "V ⇒ V ⇒ V ⇒ V"
where "smcfs α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
lemmas [smc_cs_simps] =
is_semifunctor.smcf_HomDom
is_semifunctor.smcf_HomCod
is_semifunctor.smcf_ArrMap_Comp
lemma smcf_is_dghm'[slicing_intros]:
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "𝔄' = smc_dg 𝔄"
and "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule is_semifunctor.smcf_is_dghm)
lemma cn_dghm_comp_is_dghm:
assumes "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "smcf_dghm 𝔉 : op_dg (smc_dg 𝔄) ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔅"
using assms
unfolding slicing_simps slicing_commute
by (cs_concl cs_shallow cs_intro: slicing_intros)
lemma cn_dghm_comp_is_dghm'[slicing_intros]:
assumes "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "𝔄' = op_dg (smc_dg 𝔄)"
and "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule cn_dghm_comp_is_dghm)
text‹Rules.›
lemma (in is_semifunctor) is_semifunctor_axioms'[smc_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α'⇙ 𝔅'"
unfolding assms by (rule is_semifunctor_axioms)
mk_ide rf is_semifunctor_def[unfolded is_semifunctor_axioms_def]
|intro is_semifunctorI|
|dest is_semifunctorD[dest]|
|elim is_semifunctorE[elim]|
lemmas [smc_cs_intros] =
is_semifunctorD(3,4)
lemma is_semifunctorI':
assumes "𝒵 α"
and "vfsequence 𝔉"
and "semicategory α 𝔄"
and "semicategory α 𝔅"
and "vcard 𝔉 = 4⇩ℕ"
and "𝔉⦇HomDom⦈ = 𝔄"
and "𝔉⦇HomCod⦈ = 𝔅"
and "vsv (𝔉⦇ObjMap⦈)"
and "vsv (𝔉⦇ArrMap⦈)"
and "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔅⦇Obj⦈"
and "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
and "⋀b c g a f. ⟦ g : b ↦⇘𝔄⇙ c; f : a ↦⇘𝔄⇙ b ⟧ ⟹
𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
by (intro is_semifunctorI is_dghmI, unfold smcf_dghm_components slicing_simps)
(simp_all add: assms smcf_dghm_def nat_omega_simps semicategory.smc_digraph)
lemma is_semifunctorD':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝒵 α"
and "vfsequence 𝔉"
and "semicategory α 𝔄"
and "semicategory α 𝔅"
and "vcard 𝔉 = 4⇩ℕ"
and "𝔉⦇HomDom⦈ = 𝔄"
and "𝔉⦇HomCod⦈ = 𝔅"
and "vsv (𝔉⦇ObjMap⦈)"
and "vsv (𝔉⦇ArrMap⦈)"
and "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔅⦇Obj⦈"
and "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
and "⋀b c g a f. ⟦ g : b ↦⇘𝔄⇙ c; f : a ↦⇘𝔄⇙ b ⟧ ⟹
𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
by
(
simp_all add:
is_semifunctorD(2-9)[OF assms]
is_dghmD[OF is_semifunctorD(6)[OF assms], unfolded slicing_simps]
)
lemma is_semifunctorE':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
obtains "𝒵 α"
and "vfsequence 𝔉"
and "semicategory α 𝔄"
and "semicategory α 𝔅"
and "vcard 𝔉 = 4⇩ℕ"
and "𝔉⦇HomDom⦈ = 𝔄"
and "𝔉⦇HomCod⦈ = 𝔅"
and "vsv (𝔉⦇ObjMap⦈)"
and "vsv (𝔉⦇ArrMap⦈)"
and "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔅⦇Obj⦈"
and "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈"
and "⋀a b f. f : a ↦⇘𝔄⇙ b ⟹
𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
and "⋀b c g a f. ⟦ g : b ↦⇘𝔄⇙ c; f : a ↦⇘𝔄⇙ b ⟧ ⟹
𝔉⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
using assms by (simp add: is_semifunctorD')
text‹Slicing.›
context is_semifunctor
begin
interpretation dghm: is_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule smcf_is_dghm)
sublocale ObjMap: vsv ‹𝔉⦇ObjMap⦈›
by (rule dghm.ObjMap.vsv_axioms[unfolded slicing_simps])
sublocale ArrMap: vsv ‹𝔉⦇ArrMap⦈›
by (rule dghm.ArrMap.vsv_axioms[unfolded slicing_simps])
lemmas_with [unfolded slicing_simps]:
smcf_ObjMap_vsv = dghm.dghm_ObjMap_vsv
and smcf_ArrMap_vsv = dghm.dghm_ArrMap_vsv
and smcf_ObjMap_vdomain[smc_cs_simps] = dghm.dghm_ObjMap_vdomain
and smcf_ObjMap_vrange = dghm.dghm_ObjMap_vrange
and smcf_ArrMap_vdomain[smc_cs_simps] = dghm.dghm_ArrMap_vdomain
and smcf_ArrMap_is_arr = dghm.dghm_ArrMap_is_arr
and smcf_ArrMap_is_arr''[smc_cs_intros] = dghm.dghm_ArrMap_is_arr''
and smcf_ArrMap_is_arr'[smc_cs_intros] = dghm.dghm_ArrMap_is_arr'
and smcf_ObjMap_app_in_HomCod_Obj[smc_cs_intros] =
dghm.dghm_ObjMap_app_in_HomCod_Obj
and smcf_ArrMap_vrange = dghm.dghm_ArrMap_vrange
and smcf_ArrMap_app_in_HomCod_Arr[smc_cs_intros] =
dghm.dghm_ArrMap_app_in_HomCod_Arr
and smcf_ObjMap_vsubset_Vset = dghm.dghm_ObjMap_vsubset_Vset
and smcf_ArrMap_vsubset_Vset = dghm.dghm_ArrMap_vsubset_Vset
and smcf_ObjMap_in_Vset = dghm.dghm_ObjMap_in_Vset
and smcf_ArrMap_in_Vset = dghm.dghm_ArrMap_in_Vset
and smcf_is_dghm_if_ge_Limit = dghm.dghm_is_dghm_if_ge_Limit
and smcf_is_arr_HomCod = dghm.dghm_is_arr_HomCod
and smcf_vimage_dghm_ArrMap_vsubset_Hom =
dghm.dghm_vimage_dghm_ArrMap_vsubset_Hom
end
lemmas [smc_cs_simps] =
is_semifunctor.smcf_ObjMap_vdomain
is_semifunctor.smcf_ArrMap_vdomain
lemmas [smc_cs_intros] =
is_semifunctor.smcf_ObjMap_app_in_HomCod_Obj
is_semifunctor.smcf_ArrMap_app_in_HomCod_Arr
is_semifunctor.smcf_ArrMap_is_arr'
text‹Elementary properties.›
lemma cn_smcf_ArrMap_Comp[smc_cs_simps]:
assumes "semicategory α 𝔄"
and "𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "g : c ↦⇘𝔄⇙ b"
and "f : b ↦⇘𝔄⇙ a"
shows "𝔉⦇ArrMap⦈⦇f ∘⇩A⇘𝔄⇙ g⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
proof-
from assms(3,4) have gf:
"𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘op_smc 𝔄⇙ f⦈"
by
(
force
intro: is_semifunctor.smcf_ArrMap_Comp[OF assms(2), symmetric]
simp: slicing_simps smc_op_simps
)
from assms show ?thesis
unfolding gf by (cs_concl cs_shallow cs_simp: smc_op_simps)
qed
lemma smcf_eqI:
assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
and "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
shows "𝔊 = 𝔉"
proof-
interpret L: is_semifunctor α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ℭ 𝔇 𝔉 by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ 𝔊 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
show "𝒟⇩∘ 𝔊 = 𝒟⇩∘ 𝔉"
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
from assms(5,6) have sup: "𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by (simp_all add: smc_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔊 ⟹ 𝔊⦇a⦈ = 𝔉⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert assms(3,4) sup)
(auto simp: dghm_field_simps)
qed auto
qed
lemma smcf_dghm_eqI:
assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
and "smcf_dghm 𝔊 = smcf_dghm 𝔉"
shows "𝔊 = 𝔉"
proof(rule smcf_eqI)
from assms(5) have
"smcf_dghm 𝔊⦇ObjMap⦈ = smcf_dghm 𝔉⦇ObjMap⦈"
"smcf_dghm 𝔊⦇ArrMap⦈ = smcf_dghm 𝔉⦇ArrMap⦈"
by simp_all
then show "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
unfolding slicing_simps by simp_all
qed (auto intro: assms(1,2) simp: assms)
lemma (in is_semifunctor) smcf_def:
"𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ 𝔉 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: smc_cs_simps V_cs_simps)
have dom_rhs: "𝒟⇩∘ [𝔉⦇Obj⦈, 𝔉⦇Arr⦈, 𝔉⦇Dom⦈, 𝔉⦇Cod⦈]⇩∘ = 4⇩ℕ"
by (simp add: nat_omega_simps)
then show "𝒟⇩∘ 𝔉 = 𝒟⇩∘ [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
unfolding dom_lhs dom_rhs by (simp add: nat_omega_simps)
show "a ∈⇩∘ 𝒟⇩∘ 𝔉 ⟹ 𝔉⦇a⦈ = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘⦇a⦈"
for a
by (unfold dom_lhs, elim_in_numeral, unfold dghm_field_simps)
(simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)
lemma (in is_semifunctor) smcf_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 ∈⇩∘ Vset β"
proof-
interpret β: 𝒵 β by (rule assms(1))
note [smc_cs_intros] =
smcf_ObjMap_in_Vset
smcf_ArrMap_in_Vset
HomDom.smc_in_Vset
HomCod.smc_in_Vset
from assms(2) show ?thesis
by (subst smcf_def)
(
cs_concl cs_shallow
cs_simp: smc_cs_simps cs_intro: smc_cs_intros V_cs_intros
)
qed
lemma (in is_semifunctor) smcf_is_semifunctor_if_ge_Limit:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘β⇙ 𝔅"
by (rule is_semifunctorI)
(
simp_all add:
assms
vfsequence_axioms
smcf_is_dghm_if_ge_Limit
HomDom.smc_semicategory_if_ge_Limit
HomCod.smc_semicategory_if_ge_Limit
smc_cs_simps
)
lemma small_all_smcfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
case True
from is_semifunctor.smcf_in_Vset show ?thesis
by (intro down[of _ ‹Vset (α + ω)›])
(auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
case False
then have "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅} = {}" by auto
then show ?thesis by simp
qed
lemma (in is_semifunctor) smcf_in_Vset_7: "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
note [folded VPow_iff, folded Vset_succ[OF Ord_α], smc_cs_intros] =
smcf_ObjMap_vsubset_Vset
smcf_ArrMap_vsubset_Vset
from HomDom.smc_semicategory_in_Vset_4 have [smc_cs_intros]:
"𝔄 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by (succ_of_numeral)
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
from HomCod.smc_semicategory_in_Vset_4 have [smc_cs_intros]:
"𝔅 ∈⇩∘ Vset (succ (succ (succ (succ α))))"
by (succ_of_numeral)
(cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
show ?thesis
by (subst smcf_def, succ_of_numeral)
(
cs_concl
cs_simp: plus_V_succ_right V_cs_simps smc_cs_simps
cs_intro: smc_cs_intros V_cs_intros
)
qed
lemma (in 𝒵) all_smcfs_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "all_smcfs α ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
interpret β: 𝒵 β by (rule assms(1))
show "all_smcfs α ⊆⇩∘ Vset (α + 7⇩ℕ)"
proof(intro vsubsetI)
fix 𝔉 assume "𝔉 ∈⇩∘ all_smcfs α"
then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" by clarsimp
then interpret is_semifunctor α 𝔄 𝔅 𝔉 .
show "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)" by (rule smcf_in_Vset_7)
qed
from assms(2) show "Vset (α + 7⇩ℕ) ∈⇩∘ Vset β"
by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed
lemma small_smcfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}"
by (rule down[of _ ‹set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅}›]) auto
subsection‹Opposite semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.›
definition op_smcf :: "V ⇒ V"
where "op_smcf 𝔉 =
[𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, op_smc (𝔉⦇HomDom⦈), op_smc (𝔉⦇HomCod⦈)]⇩∘"
text‹Components.›
lemma op_smcf_components[smc_op_simps]:
shows "op_smcf 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "op_smcf 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "op_smcf 𝔉⦇HomDom⦈ = op_smc (𝔉⦇HomDom⦈)"
and "op_smcf 𝔉⦇HomCod⦈ = op_smc (𝔉⦇HomCod⦈)"
unfolding op_smcf_def dghm_field_simps by (auto simp: nat_omega_simps)
text‹Slicing.›
lemma op_dghm_smcf_dghm[slicing_commute]:
"op_dghm (smcf_dghm 𝔉) = smcf_dghm (op_smcf 𝔉)"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) = 4⇩ℕ"
unfolding op_dghm_def by (auto simp: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (smcf_dghm (op_smcf 𝔉)) = 4⇩ℕ"
unfolding smcf_dghm_def by (auto simp: nat_omega_simps)
show "𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) = 𝒟⇩∘ (smcf_dghm (op_smcf 𝔉))"
unfolding dom_lhs dom_rhs by simp
show "a ∈⇩∘ 𝒟⇩∘ (op_dghm (smcf_dghm 𝔉)) ⟹
op_dghm (smcf_dghm 𝔉)⦇a⦈ = smcf_dghm (op_smcf 𝔉)⦇a⦈"
for a
by
(
unfold dom_lhs,
elim_in_numeral,
unfold smcf_dghm_def op_smcf_def op_dghm_def dghm_field_simps
)
(auto simp: nat_omega_simps slicing_simps slicing_commute)
qed (auto simp: smcf_dghm_def op_dghm_def)
subsubsection‹Further properties›
lemma (in is_semifunctor) is_semifunctor_op:
"op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ op_smc 𝔅"
proof(intro is_semifunctorI)
show "vfsequence (op_smcf 𝔉)" unfolding op_smcf_def by simp
show "vcard (op_smcf 𝔉) = 4⇩ℕ"
unfolding op_smcf_def by (auto simp: nat_omega_simps)
fix g b c f a assume "g : b ↦⇘op_smc 𝔄⇙ c" "f : a ↦⇘op_smc 𝔄⇙ b"
then have "g : c ↦⇘𝔄⇙ b" and "f : b ↦⇘𝔄⇙ a"
unfolding smc_op_simps by simp_all
with is_semifunctor_axioms show
"op_smcf 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘op_smc 𝔄⇙ f⦈ =
op_smcf 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘op_smc 𝔅⇙ op_smcf 𝔉⦇ArrMap⦈⦇f⦈"
by
(
cs_concl
cs_simp: smc_op_simps smc_cs_simps
cs_intro: smc_op_intros smc_cs_intros
)
qed
(
auto simp:
smc_cs_simps
smc_op_simps
slicing_simps
slicing_commute[symmetric]
is_dghm.is_dghm_op
smcf_is_dghm
HomCod.semicategory_op
HomDom.semicategory_op
)
lemma (in is_semifunctor) is_semifunctor_op':
assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅" and "α' = α"
shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α'⇙ 𝔅'"
unfolding assms by (rule is_semifunctor_op)
lemmas is_semifunctor_op'[smc_op_intros] = is_semifunctor.is_semifunctor_op'
lemma (in is_semifunctor) smcf_op_smcf_op_smcf[smc_op_simps]:
"op_smcf (op_smcf 𝔉) = 𝔉"
proof(rule smcf_eqI, unfold smc_op_simps)
show "op_smcf (op_smcf 𝔉) : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
by
(
metis
HomCod.smc_op_smc_op_smc
HomDom.smc_op_smc_op_smc
is_semifunctor.is_semifunctor_op
is_semifunctor_op
)
qed (simp_all add: is_semifunctor_axioms)
lemmas smcf_op_smcf_op_smcf[smc_op_simps] = is_semifunctor.smcf_op_smcf_op_smcf
lemma eq_op_smcf_iff[smc_op_simps]:
assumes "𝔊 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "𝔉 : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
shows "op_smcf 𝔊 = op_smcf 𝔉 ⟷ 𝔊 = 𝔉"
proof
interpret L: is_semifunctor α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ℭ 𝔇 𝔉 by (rule assms(2))
assume prems: "op_smcf 𝔊 = op_smcf 𝔉"
show "𝔊 = 𝔉"
proof(rule smcf_eqI[OF assms])
from prems R.smcf_op_smcf_op_smcf L.smcf_op_smcf_op_smcf show
"𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
by metis+
from prems R.smcf_op_smcf_op_smcf L.smcf_op_smcf_op_smcf have
"𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by auto
then show "𝔄 = ℭ" "𝔅 = 𝔇" by (simp_all add: smc_cs_simps)
qed
qed auto
subsection‹Composition of covariant semifunctors›
subsubsection‹Definition and elementary properties›
abbreviation (input) smcf_comp :: "V ⇒ V ⇒ V" (infixl "∘⇩S⇩M⇩C⇩F" 55)
where "smcf_comp ≡ dghm_comp"
text‹Slicing.›
lemma smcf_dghm_smcf_comp[slicing_commute]:
"smcf_dghm 𝔊 ∘⇩D⇩G⇩H⇩M smcf_dghm 𝔉 = smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)"
unfolding dghm_comp_def smcf_dghm_def dghm_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map›
lemma smcf_comp_ObjMap_vsv[smc_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ObjMap_vsv
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ObjMap_vdomain[smc_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ObjMap_vdomain
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ObjMap_vrange
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ObjMap_app[smc_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and [simp]: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ObjMap_app
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute,
OF assms(3)
]
)
qed
subsubsection‹Arrow map›
lemma smcf_comp_ArrMap_vsv[smc_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ArrMap_vsv
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ArrMap_vdomain[smc_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ArrMap_vdomain
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ArrMap_vrange
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute
]
)
qed
lemma smcf_comp_ArrMap_app[smc_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and [simp]: "f ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_comp_ArrMap_app
[
OF L.smcf_is_dghm R.smcf_is_dghm,
unfolded slicing_simps slicing_commute,
OF assms(3)
]
)
qed
subsubsection‹Further properties›
lemma smcf_comp_is_semifunctor[smc_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
interpret L: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof(rule is_semifunctorI, unfold dghm_comp_components(3,4))
show "vfsequence (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)" by (simp add: dghm_comp_def)
show "vcard (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) = 4⇩ℕ"
unfolding dghm_comp_def by (simp add: nat_omega_simps)
fix g b c f a assume "g : b ↦⇘𝔄⇙ c" "f : a ↦⇘𝔄⇙ b"
with assms show "(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
(𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈"
by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
qed
(
auto
simp: slicing_commute[symmetric] smc_cs_simps smc_cs_intros
intro: dg_cs_intros slicing_intros
)
qed
lemma smcf_comp_assoc[smc_cs_simps]:
assumes "ℌ : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "(ℌ ∘⇩S⇩M⇩C⇩F 𝔊) ∘⇩S⇩M⇩C⇩F 𝔉 = ℌ ∘⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉)"
proof(rule smcf_eqI[of α 𝔄 𝔇 _ 𝔄 𝔇])
interpret ℌ: is_semifunctor α ℭ 𝔇 ℌ by (rule assms(1))
interpret 𝔊: is_semifunctor α 𝔅 ℭ 𝔊 by (rule assms(2))
interpret 𝔉: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(3))
from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms ℌ.is_semifunctor_axioms
show "ℌ ∘⇩S⇩M⇩C⇩F (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
and "ℌ ∘⇩S⇩M⇩C⇩F 𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
by (auto intro: smc_cs_intros)
qed (simp_all add: dghm_comp_components vcomp_assoc)
lemma op_smcf_smcf_comp[smc_op_simps]:
"op_smcf (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) = op_smcf 𝔊 ∘⇩S⇩M⇩C⇩F op_smcf 𝔉"
unfolding dghm_comp_def op_smcf_def dghm_field_simps
by (simp add: nat_omega_simps)
subsection‹Composition of contravariant semifunctors›
subsubsection‹Definition and elementary properties›
text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›.›
definition smcf_cn_comp :: "V ⇒ V ⇒ V" (infixl ‹⇩S⇩M⇩C⇩F∘› 55)
where "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 =
[
𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈,
𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈,
op_smc (𝔉⦇HomDom⦈),
𝔊⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma smcf_cn_comp_components:
shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
and "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
and [smc_cn_cs_simps]: "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇HomDom⦈ = op_smc (𝔉⦇HomDom⦈)"
and [smc_cn_cs_simps]: "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇HomCod⦈ = 𝔊⦇HomCod⦈"
unfolding smcf_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma smcf_dghm_smcf_cn_comp[slicing_commute]:
"smcf_dghm 𝔊 ⇩D⇩G⇩H⇩M∘ smcf_dghm 𝔉 = smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)"
unfolding dghm_cn_comp_def smcf_cn_comp_def smcf_dghm_def
by (simp add: nat_omega_simps slicing_commute dghm_field_simps)
subsubsection‹Object map: two contravariant semifunctors›
lemma smcf_cn_comp_ObjMap_vsv[smc_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ObjMap_vsv
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ObjMap_vdomain[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ObjMap_vdomain
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ObjMap_vrange
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ObjMap_app[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ObjMap_app
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Arrow map: two contravariant semifunctors›
lemma smcf_cn_comp_ArrMap_vsv[smc_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ArrMap_vsv
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ArrMap_vdomain[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ArrMap_vdomain
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ArrMap_vrange
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_comp_ArrMap_app[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_comp_ArrMap_app
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Object map: contravariant and covariant semifunctors›
lemma smcf_cn_cov_comp_ObjMap_vsv[smc_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ObjMap_vsv
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ObjMap_vdomain[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ObjMap_vdomain
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ObjMap_vrange
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ObjMap_app[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ObjMap_app
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Arrow map: contravariant and covariant semifunctors›
lemma smcf_cn_cov_comp_ArrMap_vsv[smc_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ArrMap_vsv
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ArrMap_vdomain[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ArrMap_vdomain
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ArrMap_vrange
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps
]
)
qed
lemma smcf_cn_cov_comp_ArrMap_app[smc_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅" and "f ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule dghm_cn_cov_comp_ArrMap_app
[
OF
L.smcf_is_dghm[unfolded slicing_commute[symmetric]]
R.smcf_is_dghm,
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Opposite of the contravariant composition of semifunctors›
lemma op_smcf_smcf_cn_comp[smc_op_simps]:
"op_smcf (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) = op_smcf 𝔊 ⇩S⇩M⇩C⇩F∘ op_smcf 𝔉"
unfolding op_smcf_def smcf_cn_comp_def dghm_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹Further properties›
lemma smcf_cn_comp_is_semifunctor[smc_cn_cs_intros]:
assumes "semicategory α 𝔄" and "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊
rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a
by (rule assms(2)) (simp_all add: smc_op_simps)
interpret R: is_semifunctor α ‹op_smc 𝔄› 𝔅 𝔉
rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a
by (rule assms(3)) (simp_all add: smc_op_simps)
interpret 𝔄: semicategory α 𝔄 by (rule assms(1))
show ?thesis
proof(rule is_semifunctorI, unfold smcf_cn_comp_components(3,4) smc_op_simps)
from assms show "smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
by
(
cs_concl cs_shallow
cs_simp: slicing_commute[symmetric]
cs_intro: dg_cn_cs_intros slicing_intros
)
fix g b c f a assume "g : b ↦⇘𝔄⇙ c" "f : a ↦⇘𝔄⇙ b"
with assms show "(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g ∘⇩A⇘𝔄⇙ f⦈ =
(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈"
by
(
cs_concl cs_shallow
cs_simp: smc_cs_simps smc_cn_cs_simps smc_op_simps
cs_intro: smc_cs_intros
)
qed
(
auto simp:
smcf_cn_comp_def
nat_omega_simps
smc_cs_simps
smc_op_simps
smc_cs_intros
)
qed
lemma smcf_cn_cov_comp_is_semifunctor[smc_cs_intros]:
assumes "𝔊 : 𝔅 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
shows "𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ"
proof-
interpret L: is_semifunctor α ‹op_smc 𝔅› ℭ 𝔊
rewrites "f : b ↦⇘op_smc ℭ'⇙ a = f : a ↦⇘ℭ'⇙ b" for ℭ' f b a
by (rule assms(1)) (simp_all add: smc_op_simps)
interpret R: is_semifunctor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof(rule is_semifunctorI, unfold smcf_cn_comp_components(3,4) smc_op_simps)
from assms show
"smcf_dghm (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) : smc_dg (op_smc 𝔄) ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
by
(
cs_concl cs_shallow
cs_simp: slicing_commute[symmetric]
cs_intro: dg_cn_cs_intros slicing_intros
)
show "vfsequence (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)" unfolding smcf_cn_comp_def by simp
show "vcard (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉) = 4⇩ℕ"
unfolding smcf_cn_comp_def by (auto simp: nat_omega_simps)
show "op_smc (𝔉⦇HomDom⦈) = op_smc 𝔄" by (simp add: smc_cs_simps)
show "𝔊⦇HomCod⦈ = ℭ" by (simp add: smc_cs_simps)
fix g b c f a assume "g : c ↦⇘𝔄⇙ b" "f : b ↦⇘𝔄⇙ a"
with assms show
"(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f ∘⇩A⇘𝔄⇙ g⦈ =
(𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ (𝔊 ⇩S⇩M⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇f⦈"
by
(
cs_concl cs_shallow
cs_simp: smc_cs_simps smc_cn_cs_simps smc_op_simps
cs_intro: smc_cs_intros
)
qed (auto intro: smc_cs_intros smc_op_intros)
qed
lemma smcf_cov_cn_comp_is_semifunctor[smc_cn_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙ ℭ"
using assms by (rule smcf_comp_is_semifunctor)
subsection‹Identity semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
abbreviation (input) smcf_id :: "V ⇒ V" where "smcf_id ≡ dghm_id"
text‹Slicing.›
lemma smcf_dghm_smcf_id[slicing_commute]:
"dghm_id (smc_dg ℭ) = smcf_dghm (smcf_id ℭ)"
unfolding dghm_id_def smc_dg_def smcf_dghm_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
context semicategory
begin
interpretation dg: digraph α ‹smc_dg ℭ› by (rule smc_digraph)
lemmas_with [unfolded slicing_simps]:
smc_dghm_id_is_dghm = dg.dg_dghm_id_is_dghm
end
subsubsection‹Object map›
lemmas [smc_cs_simps] = dghm_id_ObjMap_app
subsubsection‹Arrow map›
lemmas [smc_cs_simps] = dghm_id_ArrMap_app
subsubsection‹Opposite identity semifunctor›
lemma op_smcf_smcf_id[smc_op_simps]: "op_smcf (smcf_id ℭ) = smcf_id (op_smc ℭ)"
unfolding dghm_id_def op_smc_def op_smcf_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹An identity semifunctor is a semifunctor›
lemma (in semicategory) smc_smcf_id_is_semifunctor: "smcf_id ℭ : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
proof(rule is_semifunctorI, unfold dghm_id_components)
from smc_dghm_id_is_dghm show
"smcf_dghm (smcf_id ℭ) : smc_dg ℭ ↦↦⇩D⇩G⇘α⇙ smc_dg ℭ"
by (auto simp: slicing_simps slicing_commute)
fix g b c f a assume "g : b ↦⇘ℭ⇙ c" "f : a ↦⇘ℭ⇙ b"
then show "vid_on (ℭ⦇Arr⦈)⦇g ∘⇩A⇘ℭ⇙ f⦈ =
vid_on (ℭ⦇Arr⦈)⦇g⦈ ∘⇩A⇘ℭ⇙ vid_on (ℭ⦇Arr⦈)⦇f⦈"
by (metis smc_is_arrD(1) smc_Comp_is_arr vid_on_eq_atI)
qed (auto simp: semicategory_axioms dghm_id_def nat_omega_simps)
lemma (in semicategory) smc_smcf_id_is_semifunctor':
assumes "𝔄 = ℭ" and "𝔅 = ℭ"
shows "smcf_id ℭ : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
unfolding assms by (rule smc_smcf_id_is_semifunctor)
lemmas [smc_cs_intros] = semicategory.smc_smcf_id_is_semifunctor'
subsubsection‹Further properties›
lemma (in is_semifunctor) smcf_smcf_comp_smcf_id_left[smc_cs_simps]:
"smcf_id 𝔅 ∘⇩S⇩M⇩C⇩F 𝔉 = 𝔉"
by (rule smcf_eqI, unfold dghm_id_components dghm_comp_components)
(auto simp: smcf_ObjMap_vrange smcf_ArrMap_vrange intro: smc_cs_intros)
lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_id_left
lemma (in is_semifunctor) smcf_smcf_comp_smcf_id_right[smc_cs_simps]:
"𝔉 ∘⇩S⇩M⇩C⇩F smcf_id 𝔄 = 𝔉"
by (rule smcf_eqI, unfold dghm_id_components dghm_comp_components)
(
auto
simp: smcf_ObjMap_vrange smcf_ArrMap_vrange smc_cs_simps
intro: smc_cs_intros
)
lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_id_right
subsection‹Constant semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›
abbreviation (input) smcf_const :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "smcf_const ≡ dghm_const"
text‹Slicing.›
lemma smcf_dghm_smcf_const[slicing_commute]:
"dghm_const (smc_dg ℭ) (smc_dg 𝔇) a f = smcf_dghm (smcf_const ℭ 𝔇 a f)"
unfolding
dghm_const_def smc_dg_def smcf_dghm_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map›
lemmas [smc_cs_simps] =
dghm_const_ObjMap_app
subsubsection‹Arrow map›
lemmas [smc_cs_simps] =
dghm_const_ArrMap_app
subsubsection‹Opposite constant semifunctor›
lemma op_smcf_smcf_const[smc_op_simps]:
"op_smcf (smcf_const ℭ 𝔇 a f) = smcf_const (op_smc ℭ) (op_smc 𝔇) a f"
unfolding dghm_const_def op_smc_def op_smcf_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹A constant semifunctor is a semifunctor›
lemma smcf_const_is_semifunctor:
assumes "semicategory α ℭ"
and "semicategory α 𝔇"
and "f : a ↦⇘𝔇⇙ a"
and [simp]: "f ∘⇩A⇘𝔇⇙ f = f"
shows "smcf_const ℭ 𝔇 a f : ℭ ↦↦⇩S⇩M⇩C⇘α⇙ 𝔇"
proof-
interpret ℭ: semicategory α ℭ by (rule assms(1))
interpret 𝔇: semicategory α 𝔇 by (rule assms(2))
show ?thesis
proof(intro is_semifunctorI, tactic‹distinct_subgoals_tac›)
from assms show
"smcf_dghm (dghm_const ℭ 𝔇 a f) : smc_dg ℭ ↦↦⇩D⇩G⇘α⇙ smc_dg 𝔇"
by
(
cs_concl cs_shallow
cs_simp: slicing_commute[symmetric]
cs_intro: dg_cs_intros slicing_intros
)
show "vfsequence (smcf_const ℭ 𝔇 a f)" unfolding dghm_const_def by simp
show "vcard (smcf_const ℭ 𝔇 a f) = 4⇩ℕ"
unfolding dghm_const_def by (simp add: nat_omega_simps)
fix g' b c f' a' assume "g' : b ↦⇘ℭ⇙ c" "f' : a' ↦⇘ℭ⇙ b"
with assms(1-3) show "smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇g' ∘⇩A⇘ℭ⇙ f'⦈ =
smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇g'⦈ ∘⇩A⇘𝔇⇙ smcf_const ℭ 𝔇 a f⦇ArrMap⦈⦇f'⦈"
by (cs_concl cs_simp: assms(4) smc_cs_simps cs_intro: smc_cs_intros)
qed (auto simp: assms(1,2) dghm_const_components)
qed
lemma smcf_const_is_semifunctor'[smc_cs_intros]:
assumes "semicategory α ℭ"
and "semicategory α 𝔇"
and "f : a ↦⇘𝔇⇙ a"
and "f ∘⇩A⇘𝔇⇙ f = f"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
shows "smcf_const ℭ 𝔇 a f : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
using assms(1-4) unfolding assms(5,6) by (rule smcf_const_is_semifunctor)
subsubsection‹Further properties›
lemma (in is_semifunctor) smcf_smcf_comp_smcf_const[smc_cs_simps]:
assumes "semicategory α ℭ" and "f : a ↦⇘ℭ⇙ a" and "f ∘⇩A⇘ℭ⇙ f = f"
shows "smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉 = smcf_const 𝔄 ℭ a f"
proof(rule smcf_dghm_eqI)
interpret ℭ: semicategory α ℭ by (rule assms(1))
from assms(2) show "smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by
(
cs_concl cs_shallow
cs_simp: smc_cs_simps assms(3) cs_intro: smc_cs_intros
)
from assms(2) show "smcf_const 𝔄 ℭ a f : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by
(
cs_concl cs_shallow
cs_simp: smc_cs_simps assms(3) cs_intro: smc_cs_intros
)
from is_dghm.dghm_dghm_comp_dghm_const[
OF smcf_is_dghm ℭ.smc_digraph, unfolded slicing_simps, OF assms(2)
]
show "smcf_dghm (smcf_const 𝔅 ℭ a f ∘⇩S⇩M⇩C⇩F 𝔉) = smcf_dghm (smcf_const 𝔄 ℭ a f)"
by (cs_prems cs_shallow cs_simp: slicing_simps slicing_commute)
qed simp_all
lemmas [smc_cs_simps] = is_semifunctor.smcf_smcf_comp_smcf_const
subsection‹Faithful semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_ft_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes ft_smcf_is_ft_dghm:
"smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ smc_dg 𝔅"
syntax "_is_ft_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩lı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅" ⇌ "CONST is_ft_semifunctor α 𝔄 𝔅 𝔉"
lemma (in is_ft_semifunctor) ft_smcf_is_ft_dghm'[slicing_intros]:
assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule ft_smcf_is_ft_dghm)
lemmas [slicing_intros] = is_ft_semifunctor.ft_smcf_is_ft_dghm'
text‹Rules.›
lemma (in is_ft_semifunctor) is_ft_semifunctor_axioms'[smcf_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α'⇙ 𝔅'"
unfolding assms by (rule is_ft_semifunctor_axioms)
mk_ide rf is_ft_semifunctor_def[unfolded is_ft_semifunctor_axioms_def]
|intro is_ft_semifunctorI|
|dest is_ft_semifunctorD[dest]|
|elim is_ft_semifunctorE[elim]|
lemmas [smcf_cs_intros] = is_ft_semifunctorD(1)
lemma is_ft_semifunctorI':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
using assms
by (intro is_ft_semifunctorI)
(
simp_all add:
assms(1)
is_ft_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
)
lemma is_ft_semifunctorD':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
by
(
simp_all add:
is_ft_semifunctorD[OF assms(1)]
is_ft_dghmD(2)[
OF is_ft_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_ft_semifunctorE':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
using assms by (simp_all add: is_ft_semifunctorD')
lemma is_ft_semifunctorI'':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b g f.
⟦ g : a ↦⇘𝔄⇙ b; f : a ↦⇘𝔄⇙ b; 𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ⟧ ⟹ g = f"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
by
(
intro is_ft_semifunctorI assms,
rule is_ft_dghmI'',
unfold slicing_simps,
rule is_semifunctor.smcf_is_dghm[OF assms(1)],
rule assms(2)
)
text‹Elementary properties.›
context is_ft_semifunctor
begin
interpretation dghm: is_ft_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule ft_smcf_is_ft_dghm)
lemmas_with [unfolded slicing_simps]:
ft_smcf_v11_on_Hom = dghm.ft_dghm_v11_on_Hom
and ft_smcf_ArrMap_eqD = dghm.ft_dghm_ArrMap_eqD
end
subsubsection‹Opposite faithful semifunctor›
lemma (in is_ft_semifunctor) is_ft_semifunctor_op:
"op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_smc 𝔅"
by
(
rule is_ft_semifunctorI,
unfold smc_op_simps slicing_simps slicing_commute[symmetric]
)
(
simp_all add:
is_semifunctor_op is_ft_dghm.ft_dghm_op_dghm_is_ft_dghm
ft_smcf_is_ft_dghm
)
lemma (in is_ft_semifunctor) is_ft_semifunctor_op'[smc_op_intros]:
assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule is_ft_semifunctor_op)
lemmas is_ft_semifunctor_op[smc_op_intros] =
is_ft_semifunctor.is_ft_semifunctor_op'
subsubsection‹
The composition of faithful semifunctors is a faithful semifunctor
›
lemma smcf_comp_is_ft_semifunctor[smcf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
proof(intro is_ft_semifunctorI)
interpret 𝔊: is_ft_semifunctor α 𝔅 ℭ 𝔊 by (simp add: assms(1))
interpret 𝔉: is_ft_semifunctor α 𝔄 𝔅 𝔉 by (simp add: assms(2))
from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show 𝔊𝔉:
"𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (auto intro: smc_cs_intros)
then interpret is_semifunctor α 𝔄 ℭ ‹𝔊 ∘⇩S⇩M⇩C⇩F 𝔉› .
show "smcf_dghm (𝔊 ∘⇩S⇩M⇩C⇩F 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ smc_dg ℭ"
unfolding slicing_simps slicing_commute[symmetric]
by (auto intro: dghm_cs_intros slicing_intros)
qed
subsection‹Full semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_fl_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes fl_smcf_is_fl_dghm:
"smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ smc_dg 𝔅"
syntax "_is_fl_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩lı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" ⇌ "CONST is_fl_semifunctor α 𝔄 𝔅 𝔉"
lemma (in is_fl_semifunctor) fl_smcf_is_fl_dghm'[slicing_intros]:
assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule fl_smcf_is_fl_dghm)
lemmas [slicing_intros] = is_fl_semifunctor.fl_smcf_is_fl_dghm'
text‹Rules.›
mk_ide rf is_fl_semifunctor_def[unfolded is_fl_semifunctor_axioms_def]
|intro is_fl_semifunctorI|
|dest is_fl_semifunctorD[dest]|
|elim is_fl_semifunctorE[elim]|
lemmas [smcf_cs_intros] = is_fl_semifunctorD(1)
lemma is_fl_semifunctorI':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
using assms
by (intro is_fl_semifunctorI)
(
simp_all add:
assms(1)
is_fl_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
)
lemma is_fl_semifunctorD':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
by
(
simp_all add:
is_fl_semifunctorD[OF assms(1)]
is_fl_dghmD(2)[
OF is_fl_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_fl_semifunctorE':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
using assms by (simp_all add: is_fl_semifunctorD')
text‹Elementary properties.›
context is_fl_semifunctor
begin
interpretation dghm: is_fl_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule fl_smcf_is_fl_dghm)
lemmas_with [unfolded slicing_simps]:
fl_smcf_surj_on_Hom = dghm.fl_dghm_surj_on_Hom
end
subsubsection‹Opposite full semifunctor›
lemma (in is_fl_semifunctor) is_fl_semifunctor_op:
"op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ op_smc 𝔅"
by
(
rule is_fl_semifunctorI,
unfold smc_op_simps slicing_simps slicing_commute[symmetric]
)
(
simp_all add:
is_semifunctor_op
is_fl_dghm.fl_dghm_op_dghm_is_fl_dghm
fl_smcf_is_fl_dghm
)
lemma (in is_fl_semifunctor) is_fl_semifunctor_op'[smc_op_intros]:
assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule is_fl_semifunctor_op)
lemmas is_fl_semifunctor_op[smc_op_intros] =
is_fl_semifunctor.is_fl_semifunctor_op
subsubsection‹The composition of full semifunctors is a full semifunctor›
lemma smcf_comp_is_fl_semifunctor[smcf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ"
proof(intro is_fl_semifunctorI)
interpret 𝔉: is_fl_semifunctor α 𝔄 𝔅 𝔉 using assms(2) by simp
interpret 𝔊: is_fl_semifunctor α 𝔅 ℭ 𝔊 using assms(1) by simp
from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show
"𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (auto intro: smc_cs_intros)
show "smcf_dghm (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩u⇩l⇩l⇘α⇙ smc_dg ℭ"
unfolding slicing_commute[symmetric]
by (auto intro: dghm_cs_intros slicing_intros)
qed
subsection‹Fully faithful semifunctor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale is_ff_semifunctor =
is_ft_semifunctor α 𝔄 𝔅 𝔉 + is_fl_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉
syntax "_is_ff_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩f⇩fı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" ⇌ "CONST is_ff_semifunctor α 𝔄 𝔅 𝔉"
text‹Rules.›
mk_ide rf is_ff_semifunctor_def
|intro is_ff_semifunctorI|
|dest is_ff_semifunctorD[dest]|
|elim is_ff_semifunctorE[elim]|
lemmas [smcf_cs_intros] = is_ff_semifunctorD
text‹Elementary properties.›
lemma (in is_ff_semifunctor) ff_smcf_is_ff_dghm:
"smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ smc_dg 𝔅"
by (rule is_ff_dghmI) (auto intro: slicing_intros)
lemma (in is_ff_semifunctor) ff_smcf_is_ff_dghm'[slicing_intros]:
assumes "𝔄' = smc_dg 𝔄" and "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩f⇩f⇘α⇙ 𝔅'"
unfolding assms by (rule ff_smcf_is_ff_dghm)
lemmas [slicing_intros] = is_ff_semifunctor.ff_smcf_is_ff_dghm'
subsubsection‹Opposite fully faithful semifunctor›
lemma (in is_ff_semifunctor) is_ff_semifunctor_op:
"op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ op_smc 𝔅"
by (rule is_ff_semifunctorI)
(auto simp: is_fl_semifunctor_op is_ft_semifunctor_op)
lemma (in is_ff_semifunctor) is_ff_semifunctor_op'[smc_op_intros]:
assumes "𝔄' = op_smc 𝔄" and "𝔅' = op_smc 𝔅"
shows "op_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅'"
unfolding assms by (rule is_ff_semifunctor_op)
lemmas is_ff_semifunctor_op[smc_op_intros] =
is_ff_semifunctor.is_ff_semifunctor_op'
subsubsection‹
The composition of fully faithful semifunctors is a fully faithful
semifunctor
›
lemma smcf_comp_is_ff_semifunctor[smcf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ ℭ"
using assms
by (intro is_ff_semifunctorI, elim is_ff_semifunctorE)
(auto intro: smcf_cs_intros)
subsection‹Isomorphism of semicategories›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
locale is_iso_semifunctor = is_semifunctor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes iso_smcf_is_iso_dghm:
"smcf_dghm 𝔉 : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg 𝔅"
syntax "_is_iso_semifunctor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩oı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅" ⇌ "CONST is_iso_semifunctor α 𝔄 𝔅 𝔉"
lemma (in is_iso_semifunctor) iso_smcf_is_iso_dghm'[slicing_intros]:
assumes "𝔄' = smc_dg 𝔄" "𝔅' = smc_dg 𝔅"
shows "smcf_dghm 𝔉 : 𝔄' ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ 𝔅'"
unfolding assms by (rule iso_smcf_is_iso_dghm)
lemmas [slicing_intros] = is_iso_semifunctor.iso_smcf_is_iso_dghm'
text‹Rules.›
lemma (in is_iso_semifunctor) is_iso_semifunctor_axioms'[smcf_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α'⇙ 𝔅'"
unfolding assms by (rule is_iso_semifunctor_axioms)
mk_ide rf is_iso_semifunctor_def[unfolded is_iso_semifunctor_axioms_def]
|intro is_iso_semifunctorI|
|dest is_iso_semifunctorD[dest]|
|elim is_iso_semifunctorE[elim]|
lemma is_iso_semifunctorI':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "v11 (𝔉⦇ObjMap⦈)"
and "v11 (𝔉⦇ArrMap⦈)"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
using assms
by (intro is_iso_semifunctorI)
(
simp_all add:
assms(1)
is_iso_dghmI[OF is_semifunctorD(6)[OF assms(1)], unfolded slicing_simps]
)
lemma is_iso_semifunctorD':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "v11 (𝔉⦇ObjMap⦈)"
and "v11 (𝔉⦇ArrMap⦈)"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
by
(
simp_all add:
is_iso_semifunctorD[OF assms(1)]
is_iso_dghmD(2-5)[
OF is_iso_semifunctorD(2)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_iso_semifunctorE':
assumes "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
obtains "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅"
and "v11 (𝔉⦇ObjMap⦈)"
and "v11 (𝔉⦇ArrMap⦈)"
and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
using assms by (simp_all add: is_iso_semifunctorD')
text‹Elementary properties.›
context is_iso_semifunctor
begin
interpretation dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule iso_smcf_is_iso_dghm)
lemmas_with [unfolded slicing_simps]:
iso_smcf_ObjMap_vrange[smcf_cs_simps] = dghm.iso_dghm_ObjMap_vrange
and iso_smcf_ArrMap_vrange[smcf_cs_simps] = dghm.iso_dghm_ArrMap_vrange
sublocale ObjMap: v11 ‹𝔉⦇ObjMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 𝔄⦇Obj⦈" and "ℛ⇩∘ (𝔉⦇ObjMap⦈) = 𝔅⦇Obj⦈"
by (rule dghm.iso_dghm_ObjMap_v11[unfolded slicing_simps])
(simp_all add: smc_cs_simps smcf_cs_simps)
sublocale ArrMap: v11 ‹𝔉⦇ArrMap⦈›
rewrites "𝒟⇩∘ (𝔉⦇ArrMap⦈) = 𝔄⦇Arr⦈" and "ℛ⇩∘ (𝔉⦇ArrMap⦈) = 𝔅⦇Arr⦈"
by (rule dghm.iso_dghm_ArrMap_v11[unfolded slicing_simps])
(simp_all add: smc_cs_simps smcf_cs_simps)
lemmas_with [unfolded slicing_simps]:
iso_smcf_Obj_HomDom_if_Obj_HomCod[elim] =
dghm.iso_dghm_Obj_HomDom_if_Obj_HomCod
and iso_smcf_Arr_HomDom_if_Arr_HomCod[elim] =
dghm.iso_dghm_Arr_HomDom_if_Arr_HomCod
and iso_smcf_ObjMap_eqE[elim] = dghm.iso_dghm_ObjMap_eqE
and iso_smcf_ArrMap_eqE[elim] = dghm.iso_dghm_ArrMap_eqE
end
sublocale is_iso_semifunctor ⊆ is_ff_semifunctor
proof-
interpret dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule iso_smcf_is_iso_dghm)
show "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" by unfold_locales
qed
lemmas (in is_iso_semifunctor) iso_smcf_is_ff_semifunctor =
is_ff_semifunctor_axioms
lemmas [smcf_cs_intros] = is_iso_semifunctor.iso_smcf_is_ff_semifunctor
subsubsection‹Opposite isomorphism of semicategories›
lemma (in is_iso_semifunctor) is_iso_semifunctor_op:
"op_smcf 𝔉 : op_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ op_smc 𝔅"
by
(
rule is_iso_semifunctorI,
unfold smc_op_simps slicing_simps slicing_commute[symmetric]
)
(
simp_all add:
is_semifunctor_op is_iso_dghm.is_iso_dghm_op iso_smcf_is_iso_dghm
)
lemmas is_iso_semifunctor_op[smc_op_intros] =
is_iso_semifunctor.is_iso_semifunctor_op
subsubsection‹
The composition of isomorphisms of semicategories is an isomorphism of
semicategories
›
lemma smcf_comp_is_iso_semifunctor[smcf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ 𝔅"
shows "𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ ℭ"
proof(intro is_iso_semifunctorI)
interpret 𝔉: is_iso_semifunctor α 𝔄 𝔅 𝔉 using assms by auto
interpret 𝔊: is_iso_semifunctor α 𝔅 ℭ 𝔊 using assms by auto
from 𝔉.is_semifunctor_axioms 𝔊.is_semifunctor_axioms show
"𝔊 ∘⇩S⇩M⇩C⇩F 𝔉 : 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ ℭ"
by (auto intro: smcf_cs_intros)
show "smcf_dghm (𝔊 ∘⇩D⇩G⇩H⇩M 𝔉) : smc_dg 𝔄 ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ smc_dg ℭ"
by
(
auto
intro: dghm_cs_intros slicing_intros
simp: slicing_commute[symmetric]
)
qed
subsection‹Inverse semifunctor›
abbreviation (input) inv_smcf :: "V ⇒ V"
where "inv_smcf ≡ inv_dghm"
lemmas [smc_cs_simps] = inv_dghm_components(3,4)
text‹Slicing.›
lemma dghm_inv_smcf[slicing_commute]:
"inv_dghm (smcf_dghm 𝔉) = smcf_dghm (inv_smcf 𝔉)"
unfolding smcf_dghm_def inv_dghm_def dghm_field_simps
by (simp_all add: nat_omega_simps)
context is_iso_semifunctor
begin
interpretation dghm: is_iso_dghm α ‹smc_dg 𝔄› ‹smc_dg 𝔅› ‹smcf_dghm 𝔉›
by (rule iso_smcf_is_iso_dghm)
lemmas_with [unfolded slicing_simps slicing_commute]:
inv_smcf_ObjMap_v11 = dghm.inv_dghm_ObjMap_v11
and inv_smcf_ObjMap_vdomain = dghm.inv_dghm_ObjMap_vdomain
and inv_smcf_ObjMap_app = dghm.inv_dghm_ObjMap_app
and inv_smcf_ObjMap_vrange = dghm.inv_dghm_ObjMap_vrange
and inv_smcf_ArrMap_v11 = dghm.inv_dghm_ArrMap_v11
and inv_smcf_ArrMap_vdomain = dghm.inv_dghm_ArrMap_vdomain
and inv_smcf_ArrMap_app = dghm.inv_dghm_ArrMap_app
and inv_smcf_ArrMap_vrange = dghm.inv_dghm_ArrMap_vrange
and iso_smcf_ObjMap_inv_smcf_ObjMap_app[smcf_cs_simps] =
dghm.iso_dghm_ObjMap_inv_dghm_ObjMap_app
and