Theory CZH_ECAT_Functor
section‹Functor›
theory CZH_ECAT_Functor
imports
CZH_ECAT_Category
CZH_Foundations.CZH_SMC_Semifunctor
begin
subsection‹Background›
named_theorems cf_cs_simps
named_theorems cf_cs_intros
named_theorems cat_cn_cs_simps
named_theorems cat_cn_cs_intros
lemmas [cat_cs_simps] = dg_shared_cs_simps
lemmas [cat_cs_intros] = dg_shared_cs_intros
subsubsection‹Slicing›
definition cf_smcf :: "V ⇒ V"
where "cf_smcf ℭ =
[ℭ⦇ObjMap⦈, ℭ⦇ArrMap⦈, cat_smc (ℭ⦇HomDom⦈), cat_smc (ℭ⦇HomCod⦈)]⇩∘"
text‹Components.›
lemma cf_smcf_components:
shows [slicing_simps]: "cf_smcf 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and [slicing_simps]: "cf_smcf 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and [slicing_commute]: "cf_smcf 𝔉⦇HomDom⦈ = cat_smc (𝔉⦇HomDom⦈)"
and [slicing_commute]: "cf_smcf 𝔉⦇HomCod⦈ = cat_smc (𝔉⦇HomCod⦈)"
unfolding cf_smcf_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"›.›
locale is_functor =
𝒵 α + vfsequence 𝔉 + HomDom: category α 𝔄 + HomCod: category α 𝔅
for α 𝔄 𝔅 𝔉 +
assumes cf_length[cat_cs_simps]: "vcard 𝔉 = 4⇩ℕ"
and cf_is_semifunctor[slicing_intros]:
"cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔅"
and cf_HomDom[cat_cs_simps]: "𝔉⦇HomDom⦈ = 𝔄"
and cf_HomCod[cat_cs_simps]: "𝔉⦇HomCod⦈ = 𝔅"
and cf_ObjMap_CId[cat_cs_intros]:
"c ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈"
syntax "_is_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩Cı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" ⇌ "CONST is_functor α 𝔄 𝔅 𝔉"
abbreviation (input) is_cn_cf :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "is_cn_cf α 𝔄 𝔅 𝔉 ≡ 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
syntax "_is_cn_cf" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ⇩C↦↦ı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅" ⇀ "CONST is_cn_cf α 𝔄 𝔅 𝔉"
abbreviation all_cfs :: "V ⇒ V"
where "all_cfs α ≡ set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
abbreviation cfs :: "V ⇒ V ⇒ V ⇒ V"
where "cfs α 𝔄 𝔅 ≡ set {𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
lemmas [cat_cs_simps] =
is_functor.cf_length
is_functor.cf_HomDom
is_functor.cf_HomCod
is_functor.cf_ObjMap_CId
lemma cn_cf_ObjMap_CId[cat_cn_cs_simps]:
assumes "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅" and "c ∈⇩∘ 𝔄⦇Obj⦈"
shows "𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈"
proof-
interpret is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(1))
from assms(2) have c: "c ∈⇩∘ op_cat 𝔄⦇Obj⦈" unfolding cat_op_simps by simp
show ?thesis by (rule cf_ObjMap_CId[OF c, unfolded cat_op_simps])
qed
lemma (in is_functor) cf_is_semifunctor':
assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule cf_is_semifunctor)
lemmas [slicing_intros] = is_functor.cf_is_semifunctor'
lemma cn_smcf_comp_is_semifunctor:
assumes "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "cf_smcf 𝔉 : cat_smc 𝔄 ⇩S⇩M⇩C↦↦⇘α⇙cat_smc 𝔅"
using assms
unfolding slicing_simps slicing_commute
by (rule is_functor.cf_is_semifunctor)
lemma cn_smcf_comp_is_semifunctor'[slicing_intros]:
assumes "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
and "𝔄' = op_smc (cat_smc 𝔄)"
and "𝔅' = cat_smc 𝔅"
shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇘α⇙ 𝔅'"
using assms(1) unfolding assms(2,3) by (rule cn_smcf_comp_is_semifunctor)
text‹Rules.›
lemma (in is_functor) is_functor_axioms'[cat_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩C⇘α'⇙ 𝔅'"
unfolding assms by (rule is_functor_axioms)
mk_ide rf is_functor_def[unfolded is_functor_axioms_def]
|intro is_functorI|
|dest is_functorD[dest]|
|elim is_functorE[elim]|
lemmas [cat_cs_intros] = is_functorD(3,4)
lemma is_functorI':
assumes "𝒵 α"
and "vfsequence 𝔉"
and "category α 𝔄"
and "category α 𝔅"
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⦈"
and "(⋀c. c ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈)"
shows "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by
(
intro is_functorI is_semifunctorI',
unfold cf_smcf_components slicing_simps
)
(simp_all add: assms cf_smcf_def nat_omega_simps category.cat_semicategory)
lemma is_functorD':
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝒵 α"
and "vfsequence 𝔉"
and "category α 𝔄"
and "category α 𝔅"
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⦈"
and "(⋀c. c ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈)"
by
(
simp_all add:
is_functorD(2-9)[OF assms]
is_semifunctorD'[OF is_functorD(6)[OF assms], unfolded slicing_simps]
)
lemma is_functorE':
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
obtains "𝒵 α"
and "vfsequence 𝔉"
and "category α 𝔄"
and "category α 𝔅"
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⦈"
and "(⋀c. c ∈⇩∘ 𝔄⦇Obj⦈ ⟹ 𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈)"
using assms by (simp add: is_functorD')
text‹A functor is a semifunctor.›
context is_functor
begin
interpretation smcf: is_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
by (rule cf_is_semifunctor)
sublocale ObjMap: vsv ‹𝔉⦇ObjMap⦈›
by (rule smcf.ObjMap.vsv_axioms[unfolded slicing_simps])
sublocale ArrMap: vsv ‹𝔉⦇ArrMap⦈›
by (rule smcf.ArrMap.vsv_axioms[unfolded slicing_simps])
lemmas_with [unfolded slicing_simps]:
cf_ObjMap_vsv = smcf.smcf_ObjMap_vsv
and cf_ArrMap_vsv = smcf.smcf_ArrMap_vsv
and cf_ObjMap_vdomain[cat_cs_simps] = smcf.smcf_ObjMap_vdomain
and cf_ObjMap_vrange = smcf.smcf_ObjMap_vrange
and cf_ArrMap_vdomain[cat_cs_simps] = smcf.smcf_ArrMap_vdomain
and cf_ArrMap_is_arr = smcf.smcf_ArrMap_is_arr
and cf_ArrMap_is_arr''[cat_cs_intros] = smcf.smcf_ArrMap_is_arr''
and cf_ArrMap_is_arr'[cat_cs_intros] = smcf.smcf_ArrMap_is_arr'
and cf_ObjMap_app_in_HomCod_Obj[cat_cs_intros] =
smcf.smcf_ObjMap_app_in_HomCod_Obj
and cf_ArrMap_vrange = smcf.smcf_ArrMap_vrange
and cf_ArrMap_app_in_HomCod_Arr[cat_cs_intros] =
smcf.smcf_ArrMap_app_in_HomCod_Arr
and cf_ObjMap_vsubset_Vset = smcf.smcf_ObjMap_vsubset_Vset
and cf_ArrMap_vsubset_Vset = smcf.smcf_ArrMap_vsubset_Vset
and cf_ObjMap_in_Vset = smcf.smcf_ObjMap_in_Vset
and cf_ArrMap_in_Vset = smcf.smcf_ArrMap_in_Vset
and cf_is_semifunctor_if_ge_Limit = smcf.smcf_is_semifunctor_if_ge_Limit
and cf_is_arr_HomCod = smcf.smcf_is_arr_HomCod
and cf_vimage_dghm_ArrMap_vsubset_Hom =
smcf.smcf_vimage_dghm_ArrMap_vsubset_Hom
lemmas_with [unfolded slicing_simps]:
cf_ArrMap_Comp = smcf.smcf_ArrMap_Comp
end
lemmas [cat_cs_simps] =
is_functor.cf_ObjMap_vdomain
is_functor.cf_ArrMap_vdomain
is_functor.cf_ArrMap_Comp
lemmas [cat_cs_intros] =
is_functor.cf_ObjMap_app_in_HomCod_Obj
is_functor.cf_ArrMap_app_in_HomCod_Arr
is_functor.cf_ArrMap_is_arr'
text‹Elementary properties.›
lemma cn_cf_ArrMap_Comp[cat_cn_cs_simps]:
assumes "category α 𝔄"
and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
and "g : c ↦⇘𝔄⇙ b"
and "f : b ↦⇘𝔄⇙ a"
shows "𝔉⦇ArrMap⦈⦇f ∘⇩A⇘𝔄⇙ g⦈ = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈"
proof-
interpret 𝔄: category α 𝔄 by (rule assms(1))
interpret 𝔉: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule cn_smcf_ArrMap_Comp
[
OF
𝔄.cat_semicategory
𝔉.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_simps,
OF assms(3,4)
]
)
qed
lemma cf_eqI:
assumes "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
shows "𝔊 = 𝔉"
proof(rule vsv_eqI)
interpret L: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_functor α ℭ 𝔇 𝔉 by (rule assms(2))
from assms(1) show "vsv 𝔊" by auto
from assms(2) show "vsv 𝔉" by auto
have dom: "𝒟⇩∘ 𝔊 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
show "𝒟⇩∘ 𝔊 = 𝒟⇩∘ 𝔉" by (cs_concl cs_shallow cs_simp: cat_cs_simps V_cs_simps)
from assms(5,6) have sup: "𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by (simp_all add: cat_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
lemma cf_smcf_eqI:
assumes "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
and "cf_smcf 𝔊 = cf_smcf 𝔉"
shows "𝔊 = 𝔉"
proof(rule cf_eqI)
from assms(5) have
"cf_smcf 𝔊⦇ObjMap⦈ = cf_smcf 𝔉⦇ObjMap⦈"
"cf_smcf 𝔊⦇ArrMap⦈ = cf_smcf 𝔉⦇ArrMap⦈"
by simp_all
then show "𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
unfolding slicing_simps by simp_all
qed (auto intro: assms(1,2) simp: assms(3-5))
lemma (in is_functor) cf_def: "𝔉 = [𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, 𝔉⦇HomDom⦈, 𝔉⦇HomCod⦈]⇩∘"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ 𝔉 = 4⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_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)
text‹Size.›
lemma (in is_functor) cf_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 ∈⇩∘ Vset β"
proof-
interpret β: 𝒵 β by (rule assms(1))
note [cat_cs_intros] =
cf_ObjMap_in_Vset
cf_ArrMap_in_Vset
HomDom.cat_in_Vset
HomCod.cat_in_Vset
from assms(2) show ?thesis
by (subst cf_def)
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros
)
qed
lemma (in is_functor) cf_is_functor_if_ge_Limit:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "𝔉 : 𝔄 ↦↦⇩C⇘β⇙ 𝔅"
by (rule is_functorI)
(
auto simp:
cat_cs_simps
assms
vfsequence_axioms
cf_is_semifunctor_if_ge_Limit
HomDom.cat_category_if_ge_Limit
HomCod.cat_category_if_ge_Limit
intro: cat_cs_intros
)
lemma small_all_cfs[simp]: "small {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
proof(cases ‹𝒵 α›)
case True
from is_functor.cf_in_Vset show ?thesis
by (intro down[of _ ‹Vset (α + ω)›])
(auto simp: True 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
case False
then have "{𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅} = {}" by auto
then show ?thesis by simp
qed
lemma (in is_functor) cf_in_Vset_7: "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)"
proof-
note [folded VPow_iff, folded Vset_succ[OF Ord_α], cat_cs_intros] =
cf_ObjMap_vsubset_Vset
cf_ArrMap_vsubset_Vset
from HomDom.cat_category_in_Vset_4 have [cat_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.cat_category_in_Vset_4 have [cat_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 cf_def, succ_of_numeral)
(
cs_concl
cs_simp: plus_V_succ_right V_cs_simps cat_cs_simps
cs_intro: cat_cs_intros V_cs_intros
)
qed
lemma (in 𝒵) all_cfs_in_Vset:
assumes "𝒵 β" and "α ∈⇩∘ β"
shows "all_cfs α ∈⇩∘ Vset β"
proof(rule vsubset_in_VsetI)
interpret β: 𝒵 β by (rule assms(1))
show "all_cfs α ⊆⇩∘ Vset (α + 7⇩ℕ)"
proof(intro vsubsetI)
fix 𝔉 assume "𝔉 ∈⇩∘ all_cfs α"
then obtain 𝔄 𝔅 where 𝔉: "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" by clarsimp
interpret is_functor α 𝔄 𝔅 𝔉 using 𝔉 by simp
show "𝔉 ∈⇩∘ Vset (α + 7⇩ℕ)" by (rule cf_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_cfs[simp]: "small {𝔉. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}"
by (rule down[of _ ‹set {𝔉. ∃𝔄 𝔅. 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅}›]) auto
subsubsection‹Further properties›
lemma (in is_functor) cf_ArrMap_is_iso_arr:
assumes "f : a ↦⇩i⇩s⇩o⇘𝔄⇙ b"
shows "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
proof-
note f = is_iso_arrD(1)[OF assms(1)]
note HomDom.cat_the_inverse_is_iso_arr[OF assms]
note inv_f = this is_iso_arrD(1)[OF this]
show ?thesis
proof(intro is_iso_arrI is_inverseI)
from inv_f(2) show 𝔉_inv_f:
"𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ : 𝔉⦇ObjMap⦈⦇b⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
by (cs_concl cs_intro: cat_cs_intros)
note cf_ArrMap_Comp is_functor.cf_ArrMap_Comp[cat_cs_simps del]
from assms f(1) inv_f show
"𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
"𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇b⦈⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cf_ArrMap_Comp[symmetric]
cs_intro: cat_cs_intros
)+
qed (intro cf_ArrMap_is_arr[OF f(1)])+
qed
lemma (in is_functor) cf_ArrMap_is_iso_arr'[cat_arrow_cs_intros]:
assumes "f : a ↦⇩i⇩s⇩o⇘𝔄⇙ b" and "𝔉a = 𝔉⦇ObjMap⦈⦇a⦈" and "𝔉b = 𝔉⦇ObjMap⦈⦇b⦈"
shows "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉a ↦⇩i⇩s⇩o⇘𝔅⇙ 𝔉b"
using assms(1) unfolding assms(2,3) by (rule cf_ArrMap_is_iso_arr)
lemmas [cat_arrow_cs_intros] = is_functor.cf_ArrMap_is_iso_arr'
subsection‹Opposite functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter II-2 in \<^cite>‹"mac_lane_categories_2010"›.›
definition op_cf :: "V ⇒ V"
where "op_cf 𝔉 =
[𝔉⦇ObjMap⦈, 𝔉⦇ArrMap⦈, op_cat (𝔉⦇HomDom⦈), op_cat (𝔉⦇HomCod⦈)]⇩∘"
text‹Components.›
lemma op_cf_components[cat_op_simps]:
shows "op_cf 𝔉⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
and "op_cf 𝔉⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
and "op_cf 𝔉⦇HomDom⦈ = op_cat (𝔉⦇HomDom⦈)"
and "op_cf 𝔉⦇HomCod⦈ = op_cat (𝔉⦇HomCod⦈)"
unfolding op_cf_def dghm_field_simps by (auto simp: nat_omega_simps)
text‹Slicing.›
lemma cf_smcf_op_cf[slicing_commute]: "op_smcf (cf_smcf 𝔉) = cf_smcf (op_cf 𝔉)"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ (op_smcf (cf_smcf 𝔉)) = 4⇩ℕ"
unfolding op_smcf_def by (auto simp: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ (cf_smcf (op_cf 𝔉)) = 4⇩ℕ"
unfolding cf_smcf_def by (auto simp: nat_omega_simps)
show "𝒟⇩∘ (op_smcf (cf_smcf 𝔉)) = 𝒟⇩∘ (cf_smcf (op_cf 𝔉))"
unfolding dom_lhs dom_rhs by simp
show "a ∈⇩∘ 𝒟⇩∘ (op_smcf (cf_smcf 𝔉)) ⟹
op_smcf (cf_smcf 𝔉)⦇a⦈ = cf_smcf (op_cf 𝔉)⦇a⦈"
for a
by
(
unfold dom_lhs,
elim_in_numeral,
unfold cf_smcf_def op_cf_def op_smcf_def dghm_field_simps
)
(auto simp: nat_omega_simps slicing_commute)
qed (auto simp: cf_smcf_def op_smcf_def)
text‹Elementary properties.›
lemma op_cf_vsv[cat_op_intros]: "vsv (op_cf 𝔉)" unfolding op_cf_def by auto
subsubsection‹Further properties›
lemma (in is_functor) is_functor_op: "op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇘α⇙ op_cat 𝔅"
proof(intro is_functorI, unfold cat_op_simps)
show "vfsequence (op_cf 𝔉)" unfolding op_cf_def by simp
show "vcard (op_cf 𝔉) = 4⇩ℕ"
unfolding op_cf_def by (auto simp: nat_omega_simps)
fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
then show "𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇c⦈⦈"
unfolding cat_op_simps by (auto intro: cat_cs_intros)
qed
(
auto simp:
cat_cs_simps
slicing_commute[symmetric]
is_semifunctor.is_semifunctor_op
cf_is_semifunctor
HomCod.category_op
HomDom.category_op
)
lemma (in is_functor) is_functor_op'[cat_op_intros]:
assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
shows "op_cf 𝔉 : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms(1,2) by (rule is_functor_op)
lemmas is_functor_op[cat_op_intros] = is_functor.is_functor_op'
lemma (in is_functor) cf_op_cf_op_cf[cat_op_simps]: "op_cf (op_cf 𝔉) = 𝔉"
proof(rule cf_eqI[of α 𝔄 𝔅 _ 𝔄 𝔅], unfold cat_op_simps)
show "op_cf (op_cf 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
by
(
metis
HomCod.cat_op_cat_op_cat
HomDom.cat_op_cat_op_cat
is_functor.is_functor_op
is_functor_op
)
qed (auto simp: cat_cs_intros)
lemmas cf_op_cf_op_cf[cat_op_simps] = is_functor.cf_op_cf_op_cf
lemma eq_op_cf_iff[cat_op_simps]:
assumes "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
shows "op_cf 𝔊 = op_cf 𝔉 ⟷ 𝔊 = 𝔉"
proof
interpret L: is_functor α 𝔄 𝔅 𝔊 by (rule assms(1))
interpret R: is_functor α ℭ 𝔇 𝔉 by (rule assms(2))
assume prems: "op_cf 𝔊 = op_cf 𝔉"
show "𝔊 = 𝔉"
proof(rule cf_eqI[OF assms])
from prems R.cf_op_cf_op_cf L.cf_op_cf_op_cf show
"𝔊⦇ObjMap⦈ = 𝔉⦇ObjMap⦈" "𝔊⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
by metis+
from prems R.cf_op_cf_op_cf L.cf_op_cf_op_cf have
"𝔊⦇HomDom⦈ = 𝔉⦇HomDom⦈" "𝔊⦇HomCod⦈ = 𝔉⦇HomCod⦈"
by auto
then show "𝔄 = ℭ" "𝔅 = 𝔇" by (simp_all add: cat_cs_simps)
qed
qed auto
subsection‹Composition of covariant functors›
subsubsection‹Definition and elementary properties›
abbreviation (input) cf_comp :: "V ⇒ V ⇒ V" (infixl "∘⇩C⇩F" 55)
where "cf_comp ≡ dghm_comp"
text‹Slicing.›
lemma cf_smcf_smcf_comp[slicing_commute]:
"cf_smcf 𝔊 ∘⇩S⇩M⇩C⇩F cf_smcf 𝔉 = cf_smcf (𝔊 ∘⇩C⇩F 𝔉)"
unfolding dghm_comp_def cf_smcf_def dghm_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map›
lemma cf_comp_ObjMap_vsv[cat_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ObjMap_vsv
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ObjMap_vdomain[cat_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ObjMap_vdomain
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ObjMap_vrange
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ObjMap_app[cat_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and [simp]: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ObjMap_app
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute,
OF assms(3)
]
)
qed
subsubsection‹Arrow map›
lemma cf_comp_ArrMap_vsv[cat_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ArrMap_vsv
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ArrMap_vdomain[cat_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ArrMap_vdomain
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ArrMap_vrange
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute
]
)
qed
lemma cf_comp_ArrMap_app[cat_cs_simps]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and [simp]: "f ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_comp_ArrMap_app
[
OF L.cf_is_semifunctor R.cf_is_semifunctor,
unfolded slicing_simps slicing_commute,
OF assms(3)
]
)
qed
subsubsection‹Further properties›
lemma cf_comp_is_functorI[cat_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
interpret L: is_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof(rule is_functorI, unfold dghm_comp_components(3,4))
show "vfsequence (𝔊 ∘⇩C⇩F 𝔉)" by (simp add: dghm_comp_def)
show "vcard (𝔊 ∘⇩C⇩F 𝔉) = 4⇩ℕ"
unfolding dghm_comp_def by (simp add: nat_omega_simps)
show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
unfolding cf_smcf_smcf_comp[symmetric]
by
(
cs_concl
cs_intro: smc_cs_intros slicing_intros cat_cs_intros
)
fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
with assms show "(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇c⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (auto simp: cat_cs_simps intro: cat_cs_intros)
qed
lemma cf_comp_assoc[cat_cs_simps]:
assumes "ℌ : ℭ ↦↦⇩C⇘α⇙ 𝔇" and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "(ℌ ∘⇩C⇩F 𝔊) ∘⇩C⇩F 𝔉 = ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉)"
proof(rule cf_eqI[of α 𝔄 𝔇 _ 𝔄 𝔇])
interpret ℌ: is_functor α ℭ 𝔇 ℌ by (rule assms(1))
interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(3))
from 𝔉.is_functor_axioms 𝔊.is_functor_axioms ℌ.is_functor_axioms
show "ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉) : 𝔄 ↦↦⇩C⇘α⇙ 𝔇" and "ℌ ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔇"
by (auto simp: cat_cs_simps intro: cat_cs_intros)
qed (simp_all add: dghm_comp_components vcomp_assoc)
text‹The opposite of the covariant composition of functors.›
lemma op_cf_cf_comp[cat_op_simps]: "op_cf (𝔊 ∘⇩C⇩F 𝔉) = op_cf 𝔊 ∘⇩C⇩F op_cf 𝔉"
unfolding dghm_comp_def op_cf_def dghm_field_simps
by (simp add: nat_omega_simps)
text‹Composition helper.›
lemma cf_comp_assoc_helper:
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "ℌ : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "ℌ ∘⇩C⇩F 𝔊 = 𝒬"
shows "ℌ ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔉) = 𝒬 ∘⇩C⇩F 𝔉"
proof-
interpret 𝔉: is_functor α 𝔄 𝔅 𝔉 by (rule assms(1))
interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
interpret ℌ: is_functor α ℭ 𝔇 ℌ by (rule assms(3))
show ?thesis
using assms(1-3) unfolding assms(4)[symmetric]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
subsection‹Composition of contravariant functors›
subsubsection‹Definition and elementary properties›
text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›.›
definition cf_cn_comp :: "V ⇒ V ⇒ V" (infixl "⇩C⇩F∘" 55)
where "𝔊 ⇩C⇩F∘ 𝔉 =
[
𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈,
𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈,
op_cat (𝔉⦇HomDom⦈),
𝔊⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma cf_cn_comp_components:
shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈ = 𝔊⦇ObjMap⦈ ∘⇩∘ 𝔉⦇ObjMap⦈"
and "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈ = 𝔊⦇ArrMap⦈ ∘⇩∘ 𝔉⦇ArrMap⦈"
and [cat_cn_cs_simps]: "(𝔊 ⇩C⇩F∘ 𝔉)⦇HomDom⦈ = op_cat (𝔉⦇HomDom⦈)"
and [cat_cn_cs_simps]: "(𝔊 ⇩C⇩F∘ 𝔉)⦇HomCod⦈ = 𝔊⦇HomCod⦈"
unfolding cf_cn_comp_def dghm_field_simps by (simp_all add: nat_omega_simps)
text‹Slicing.›
lemma cf_smcf_cf_cn_comp[slicing_commute]:
"cf_smcf 𝔊 ⇩S⇩M⇩C⇩F∘ cf_smcf 𝔉 = cf_smcf (𝔊 ⇩C⇩F∘ 𝔉)"
unfolding smcf_cn_comp_def cf_cn_comp_def cf_smcf_def
by (simp add: nat_omega_simps slicing_commute dghm_field_simps)
subsubsection‹Object map: two contravariant functors›
lemma cf_cn_comp_ObjMap_vsv[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ObjMap_vsv
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ObjMap_vdomain[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ObjMap_vdomain
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ObjMap_vrange
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ObjMap_app[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ObjMap_app
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Arrow map: two contravariant functors›
lemma cf_cn_comp_ArrMap_vsv[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ArrMap_vsv
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ArrMap_vdomain[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ArrMap_vdomain
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ArrMap_vrange
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_comp_ArrMap_app[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_comp_ArrMap_app
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Object map: contravariant and covariant functor›
lemma cf_cn_cov_comp_ObjMap_vsv[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈)"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ObjMap_vsv
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ObjMap_vdomain[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ObjMap_vdomain
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ObjMap_vrange:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ObjMap_vrange
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ObjMap_app[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇a⦈ = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇a⦈⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ObjMap_app
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Arrow map: contravariant and covariant functors›
lemma cf_cn_cov_comp_ArrMap_vsv[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "vsv ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈)"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ArrMap_vsv
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor[unfolded slicing_commute[symmetric]],
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ArrMap_vdomain[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝒟⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ArrMap_vdomain
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ArrMap_vrange:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "ℛ⇩∘ ((𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ArrMap_vrange
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps
]
)
qed
lemma cf_cn_cov_comp_ArrMap_app[cat_cn_cs_simps]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅" and "a ∈⇩∘ 𝔄⦇Arr⦈"
shows "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇a⦈⦈"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by
(
rule smcf_cn_cov_comp_ArrMap_app
[
OF
L.cf_is_semifunctor[unfolded slicing_commute[symmetric]]
R.cf_is_semifunctor,
unfolded slicing_commute slicing_simps,
OF assms(3)
]
)
qed
subsubsection‹Further properties›
lemma cf_cn_comp_is_functorI[cat_cn_cs_intros]:
assumes "category α 𝔄" and "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "𝔊 ⇩C⇩F∘ 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(2))
interpret R: is_functor α ‹op_cat 𝔄› 𝔅 𝔉 by (rule assms(3))
interpret 𝔄: category α 𝔄 by (rule assms(1))
show ?thesis
proof(rule is_functorI, unfold cf_cn_comp_components(3,4) cat_op_simps)
show "vfsequence (𝔊 ⇩C⇩F∘ 𝔉)"
unfolding cf_cn_comp_def by (simp add: nat_omega_simps)
show "vcard (𝔊 ⇩C⇩F∘ 𝔉) = 4⇩ℕ"
unfolding cf_cn_comp_def by (simp add: nat_omega_simps)
from assms(1) L.cf_is_semifunctor R.cf_is_semifunctor show
"cf_smcf (𝔊 ⇩C⇩F∘ 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
unfolding cf_smcf_cf_cn_comp[symmetric]
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros slicing_intros smc_cn_cs_intros
)
fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
with assms show
"(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇c⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cat_cn_cs_simps cs_intro: cat_cs_intros
)
qed (auto simp: cat_cs_simps cat_cs_intros cat_op_simps)
qed
text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›).›
lemma cf_cn_cov_comp_is_functor[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ⇩C↦↦⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
shows "𝔊 ⇩C⇩F∘ 𝔉 : 𝔄 ⇩C↦↦⇘α⇙ ℭ"
proof-
interpret L: is_functor α ‹op_cat 𝔅› ℭ 𝔊 by (rule assms(1))
interpret R: is_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
proof
(
rule is_functorI,
unfold cf_cn_comp_components(3,4) cat_op_simps slicing_commute[symmetric]
)
show "vfsequence (𝔊 ⇩C⇩F∘ 𝔉)" unfolding cf_cn_comp_def by simp
show "vcard (𝔊 ⇩C⇩F∘ 𝔉) = 4⇩ℕ"
unfolding cf_cn_comp_def by (auto simp: nat_omega_simps)
from L.cf_is_semifunctor show
"cf_smcf 𝔊 ⇩S⇩M⇩C⇩F∘ cf_smcf 𝔉 : op_smc (cat_smc 𝔄) ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros slicing_intros smc_cs_intros
)
fix c assume "c ∈⇩∘ 𝔄⦇Obj⦈"
with assms show "(𝔊 ⇩C⇩F∘ 𝔉)⦇ArrMap⦈⦇𝔄⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇(𝔊 ⇩C⇩F∘ 𝔉)⦇ObjMap⦈⦇c⦈⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_cn_cs_simps
cs_intro: cat_cs_intros
)
qed (auto simp: cat_cs_simps cat_cs_intros)
qed
text‹See section 1.2 in \<^cite>‹"bodo_categories_1970"›.›
lemma cf_cov_cn_comp_is_functor[cat_cn_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔉 : 𝔄 ⇩C↦↦⇘α⇙ 𝔅"
shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ⇩C↦↦⇘α⇙ ℭ"
using assms by (rule cf_comp_is_functorI)
text‹The opposite of the contravariant composition of functors.›
lemma op_cf_cf_cn_comp[cat_op_simps]: "op_cf (𝔊 ⇩C⇩F∘ 𝔉) = op_cf 𝔊 ⇩C⇩F∘ op_cf 𝔉"
unfolding op_cf_def cf_cn_comp_def dghm_field_simps
by (auto simp: nat_omega_simps)
subsection‹Identity functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›.›
abbreviation (input) cf_id :: "V ⇒ V" where "cf_id ≡ dghm_id"
text‹Slicing.›
lemma cf_smcf_cf_id[slicing_commute]: "smcf_id (cat_smc ℭ) = cf_smcf (cf_id ℭ)"
unfolding dghm_id_def cat_smc_def cf_smcf_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
context category
begin
interpretation smc: semicategory α ‹cat_smc ℭ› by (rule cat_semicategory)
lemmas_with [unfolded slicing_simps]:
cat_smcf_id_is_semifunctor = smc.smc_smcf_id_is_semifunctor
end
subsubsection‹Object map›
lemmas [cat_cs_simps] = dghm_id_ObjMap_app
subsubsection‹Arrow map›
lemmas [cat_cs_simps] = dghm_id_ArrMap_app
subsubsection‹Opposite of an identity functor.›
lemma op_cf_cf_id[cat_op_simps]: "op_cf (cf_id ℭ) = cf_id (op_cat ℭ)"
unfolding dghm_id_def op_cat_def op_cf_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹An identity functor is a functor›
lemma (in category) cat_cf_id_is_functor: "cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
proof(rule is_functorI, unfold dghm_id_components)
from cat_smcf_id_is_semifunctor show
"cf_smcf (cf_id ℭ) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc ℭ"
by (simp add: slicing_commute)
from cat_CId_is_arr show
"c ∈⇩∘ ℭ⦇Obj⦈ ⟹ vid_on (ℭ⦇Arr⦈)⦇ℭ⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇vid_on (ℭ⦇Obj⦈)⦇c⦈⦈"
for c
by auto
qed (auto simp: dghm_id_def nat_omega_simps cat_cs_intros)
lemma (in category) cat_cf_id_is_functor':
assumes "𝔄 = ℭ" and "𝔅 = ℭ"
shows "cf_id ℭ : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
unfolding assms by (rule cat_cf_id_is_functor)
lemmas [cat_cs_intros] = category.cat_cf_id_is_functor'
subsubsection‹Further properties›
lemma (in is_functor) cf_cf_comp_cf_id_left[cat_cs_simps]: "cf_id 𝔅 ∘⇩C⇩F 𝔉 = 𝔉"
by
(
rule cf_eqI,
unfold dghm_id_components dghm_comp_components dghm_id_components
)
(auto intro: cat_cs_intros simp: cf_ArrMap_vrange cf_ObjMap_vrange)
lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_left
lemma (in is_functor) cf_cf_comp_cf_id_right[cat_cs_simps]: "𝔉 ∘⇩C⇩F cf_id 𝔄 = 𝔉"
by
(
rule cf_eqI,
unfold dghm_id_components dghm_comp_components dghm_id_components
)
(
auto
intro: cat_cs_intros
simp: cat_cs_simps cf_ArrMap_vrange cf_ObjMap_vrange
)
lemmas [cat_cs_simps] = is_functor.cf_cf_comp_cf_id_right
subsection‹Constant functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›
abbreviation cf_const :: "V ⇒ V ⇒ V ⇒ V"
where "cf_const ℭ 𝔇 a ≡ smcf_const ℭ 𝔇 a (𝔇⦇CId⦈⦇a⦈)"
text‹Slicing.›
lemma cf_smcf_cf_const[slicing_commute]:
"smcf_const (cat_smc ℭ) (cat_smc 𝔇) a (𝔇⦇CId⦈⦇a⦈) = cf_smcf (cf_const ℭ 𝔇 a)"
unfolding
dghm_const_def cat_smc_def cf_smcf_def dghm_field_simps dg_field_simps
by (simp add: nat_omega_simps)
subsubsection‹Object map and arrow map›
context
fixes 𝔇 a :: V
begin
lemmas_with [where 𝔇=𝔇 and a=a and f=‹𝔇⦇CId⦈⦇a⦈›, cat_cs_simps]:
dghm_const_ObjMap_app
dghm_const_ArrMap_app
end
subsubsection‹Opposite constant functor›
lemma op_cf_cf_const[cat_op_simps]:
"op_cf (cf_const ℭ 𝔇 a) = cf_const (op_cat ℭ) (op_cat 𝔇) a"
unfolding dghm_const_def op_cat_def op_cf_def dghm_field_simps dg_field_simps
by (auto simp: nat_omega_simps)
subsubsection‹A constant functor is a functor›
lemma cf_const_is_functor:
assumes "category α ℭ" and "category α 𝔇" and "a ∈⇩∘ 𝔇⦇Obj⦈"
shows "cf_const ℭ 𝔇 a : ℭ ↦↦⇩C⇘α⇙ 𝔇"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
show ?thesis
proof(intro is_functorI, tactic‹distinct_subgoals_tac›)
show "vfsequence (dghm_const ℭ 𝔇 a (𝔇⦇CId⦈⦇a⦈))"
unfolding dghm_const_def by simp
show "vcard (cf_const ℭ 𝔇 a) = 4⇩ℕ"
unfolding dghm_const_def by (simp add: nat_omega_simps)
from assms show "cf_smcf (cf_const ℭ 𝔇 a) : cat_smc ℭ ↦↦⇩S⇩M⇩C⇘α⇙ cat_smc 𝔇"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps slicing_simps slicing_commute[symmetric]
cs_intro: smc_cs_intros cat_cs_intros slicing_intros
)
fix c assume "c ∈⇩∘ ℭ⦇Obj⦈"
with assms show
"cf_const ℭ 𝔇 a⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 𝔇⦇CId⦈⦇cf_const ℭ 𝔇 a⦇ObjMap⦈⦇c⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (auto simp: dghm_const_components assms)
qed
lemma cf_const_is_functor'[cat_cs_intros]:
assumes "category α ℭ"
and "category α 𝔇"
and "a ∈⇩∘ 𝔇⦇Obj⦈"
and "𝔄 = ℭ"
and "𝔅 = 𝔇"
and "f = (𝔇⦇CId⦈⦇a⦈)"
shows "dghm_const ℭ 𝔇 a f : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
using assms(1-3) unfolding assms(4-6) by (rule cf_const_is_functor)
subsubsection‹Further properties›
lemma cf_comp_cf_const_right[cat_cs_simps]:
assumes "category α 𝔄"
and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
shows "𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)"
proof(rule cf_eqI)
interpret 𝔄: category α 𝔄 by (rule assms(1))
interpret 𝔊: is_functor α 𝔅 ℭ 𝔊 by (rule assms(2))
from assms(3) show "𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_intro: cat_cs_intros)
from assms(3) show "cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈) : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(3) have ObjMap_dom_lhs:
"𝒟⇩∘ ((𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(3) have ObjMap_dom_rhs:
"𝒟⇩∘ (cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps)
show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈ = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈"
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
with assms(3) show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ObjMap⦈⦇a⦈ =
cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ObjMap⦈⦇a⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (auto intro: assms(3) cat_cs_intros)
from assms(3) have ArrMap_dom_lhs:
"𝒟⇩∘ ((𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(3) have ArrMap_dom_rhs:
"𝒟⇩∘ (cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈ = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈"
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
fix a assume "a ∈⇩∘ 𝔄⦇Arr⦈"
with assms(3) show "(𝔊 ∘⇩C⇩F cf_const 𝔄 𝔅 b)⦇ArrMap⦈⦇a⦈ =
cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)⦇ArrMap⦈⦇a⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (auto intro: assms(3) cat_cs_intros)
qed simp_all
lemma cf_comp_cf_const_right'[cat_cs_simps]:
assumes "category α 𝔄"
and "𝔊 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
and "f = 𝔅⦇CId⦈⦇b⦈"
shows "𝔊 ∘⇩C⇩F dghm_const 𝔄 𝔅 b f = cf_const 𝔄 ℭ (𝔊⦇ObjMap⦈⦇b⦈)"
using assms(1-3) unfolding assms(4) by (rule cf_comp_cf_const_right)
lemma (in is_functor) cf_comp_cf_const_left[cat_cs_simps]:
assumes "category α ℭ" and "a ∈⇩∘ ℭ⦇Obj⦈"
shows "cf_const 𝔅 ℭ a ∘⇩C⇩F 𝔉 = cf_const 𝔄 ℭ a"
proof(rule cf_smcf_eqI)
interpret ℭ: category α ℭ by (rule assms(1))
from assms(2) show "cf_const 𝔅 ℭ a ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms(2) show "cf_const 𝔄 ℭ a : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms(2) have CId_a: "ℭ⦇CId⦈⦇a⦈ : a ↦⇘ℭ⇙ a"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms(2) have CId_CId_a: "ℭ⦇CId⦈⦇a⦈ ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇a⦈ = ℭ⦇CId⦈⦇a⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from
is_semifunctor.smcf_smcf_comp_smcf_const
[
OF cf_is_semifunctor ℭ.cat_semicategory,
unfolded slicing_simps,
OF CId_a CId_CId_a
]
show "cf_smcf (cf_const 𝔅 ℭ a ∘⇩D⇩G⇩H⇩M 𝔉) = cf_smcf (cf_const 𝔄 ℭ a)"
by (cs_prems cs_shallow cs_simp: slicing_simps slicing_commute)
qed simp_all
lemma (in is_functor) cf_comp_cf_const_left'[cat_cs_simps]:
assumes "category α ℭ"
and "a ∈⇩∘ ℭ⦇Obj⦈"
and "f = ℭ⦇CId⦈⦇a⦈"
shows "dghm_const 𝔅 ℭ a f ∘⇩C⇩F 𝔉 = cf_const 𝔄 ℭ a"
using assms(1,2) unfolding assms(3) by (rule cf_comp_cf_const_left)
lemmas [cat_cs_simps] = is_functor.cf_comp_cf_const_left'
subsection‹Faithful functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale is_ft_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes ft_cf_is_ft_semifunctor[slicing_intros]:
"cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ cat_smc 𝔅"
syntax "_is_ft_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩lı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅" ⇌ "CONST is_ft_functor α 𝔄 𝔅 𝔉"
lemma (in is_ft_functor) ft_cf_is_ft_functor':
assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule ft_cf_is_ft_semifunctor)
lemmas [slicing_intros] = is_ft_functor.ft_cf_is_ft_functor'
text‹Rules.›
lemma (in is_ft_functor) is_ft_functor_axioms'[cf_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α'⇙ 𝔅'"
unfolding assms by (rule is_ft_functor_axioms)
mk_ide rf is_ft_functor_def[unfolded is_ft_functor_axioms_def]
|intro is_ft_functorI|
|dest is_ft_functorD[dest]|
|elim is_ft_functorE[elim]|
lemmas [cf_cs_intros] = is_ft_functorD(1)
lemma is_ft_functorI':
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
using assms
by (intro is_ft_functorI)
(
simp_all add:
assms(1)
is_ft_semifunctorI'[OF is_functorD(6)[
OF assms(1)], unfolded slicing_simps
]
)
lemma is_ft_functorD':
assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
by
(
simp_all add:
is_ft_functorD[OF assms(1)]
is_ft_semifunctorD'(2)[
OF is_ft_functorD(2)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_ft_functorE':
assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
obtains "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹ v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
using assms by (simp_all add: is_ft_functorD')
lemma is_ft_functorI'':
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b g f.
⟦ g : a ↦⇘𝔄⇙ b; f : a ↦⇘𝔄⇙ b; 𝔉⦇ArrMap⦈⦇g⦈ = 𝔉⦇ArrMap⦈⦇f⦈ ⟧ ⟹ g = f"
shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
by
(
intro is_ft_functorI assms,
rule is_ft_semifunctorI'',
unfold slicing_simps,
rule is_functor.cf_is_semifunctor[OF assms(1)],
rule assms(2)
)
text‹Elementary properties.›
context is_ft_functor
begin
interpretation smcf: is_ft_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
by (rule ft_cf_is_ft_semifunctor)
lemmas_with [unfolded slicing_simps]:
ft_cf_v11_on_Hom = smcf.ft_smcf_v11_on_Hom
and ft_cf_ArrMap_eqD = smcf.ft_smcf_ArrMap_eqD
end
subsubsection‹Opposite faithful functor.›
lemma (in is_ft_functor) is_ft_functor_op':
"op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_cat 𝔅"
by (rule is_ft_functorI, unfold slicing_commute[symmetric])
(
simp_all add:
is_functor_op is_ft_semifunctor.is_ft_semifunctor_op
ft_cf_is_ft_semifunctor
)
lemma (in is_ft_functor) is_ft_functor_op:
assumes "𝔄' = op_cat 𝔄" and "𝔅' = op_cat 𝔅"
shows "op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ op_cat 𝔅"
unfolding assms by (rule is_ft_functor_op')
lemmas is_ft_functor_op[cat_op_intros] = is_ft_functor.is_ft_functor_op'
subsubsection‹The composition of faithful functors is a faithful functor›
lemma cf_comp_is_ft_functor[cf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ ℭ"
proof(intro is_ft_functorI)
interpret 𝔊: is_ft_functor α 𝔅 ℭ 𝔊 by (simp add: assms(1))
interpret 𝔉: is_ft_functor α 𝔄 𝔅 𝔉 by (simp add: assms(2))
from 𝔉.is_functor_axioms 𝔊.is_functor_axioms show "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
then interpret is_functor α 𝔄 ℭ ‹𝔊 ∘⇩C⇩F 𝔉› .
show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩a⇩i⇩t⇩h⇩f⇩u⇩l⇘α⇙ cat_smc ℭ"
by
(
cs_concl
cs_simp: slicing_commute[symmetric]
cs_intro: cf_cs_intros smcf_cs_intros slicing_intros
)
qed
subsection‹Full functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale is_fl_functor = is_functor α 𝔄 𝔅 𝔉 for α 𝔄 𝔅 𝔉 +
assumes fl_cf_is_fl_semifunctor:
"cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ cat_smc 𝔅"
syntax "_is_fl_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩C⇩.⇩f⇩u⇩l⇩lı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅" ⇌ "CONST is_fl_functor α 𝔄 𝔅 𝔉"
lemma (in is_fl_functor) fl_cf_is_fl_functor'[slicing_intros]:
assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅'"
unfolding assms by (rule fl_cf_is_fl_semifunctor)
lemmas [slicing_intros] = is_fl_functor.fl_cf_is_fl_semifunctor
text‹Rules.›
lemma (in is_fl_functor) is_fl_functor_axioms'[cf_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α'⇙ 𝔅'"
unfolding assms by (rule is_fl_functor_axioms)
mk_ide rf is_fl_functor_def[unfolded is_fl_functor_axioms_def]
|intro is_fl_functorI|
|dest is_fl_functorD[dest]|
|elim is_fl_functorE[elim]|
lemmas [cf_cs_intros] = is_fl_functorD(1)
lemma is_fl_functorI':
assumes "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
shows "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
using assms
by (intro is_fl_functorI)
(
simp_all add:
assms(1)
is_fl_semifunctorI'[
OF is_functorD(6)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_fl_functorD':
assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
shows "𝔉 : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
and "⋀a b. ⟦ a ∈⇩∘ 𝔄⦇Obj⦈; b ∈⇩∘ 𝔄⦇Obj⦈ ⟧ ⟹
𝔉⦇ArrMap⦈ `⇩∘ (Hom 𝔄 a b) = Hom 𝔅 (𝔉⦇ObjMap⦈⦇a⦈) (𝔉⦇ObjMap⦈⦇b⦈)"
by
(
simp_all add:
is_fl_functorD[OF assms(1)]
is_fl_semifunctorD'(2)[
OF is_fl_functorD(2)[OF assms(1)], unfolded slicing_simps
]
)
lemma is_fl_functorE':
assumes "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
obtains "𝔉 : 𝔄 ↦↦⇩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_functorD')
text‹Elementary properties.›
context is_fl_functor
begin
interpretation smcf: is_fl_semifunctor α ‹cat_smc 𝔄› ‹cat_smc 𝔅› ‹cf_smcf 𝔉›
by (rule fl_cf_is_fl_semifunctor)
lemmas_with [unfolded slicing_simps]:
fl_cf_surj_on_Hom = smcf.fl_smcf_surj_on_Hom
end
subsubsection‹Opposite full functor›
lemma (in is_fl_functor) is_fl_functor_op[cat_op_intros]:
"op_cf 𝔉 : op_cat 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ op_cat 𝔅"
by (rule is_fl_functorI, unfold slicing_commute[symmetric])
(simp_all add: cat_op_intros smc_op_intros slicing_intros)
lemmas is_fl_functor_op[cat_op_intros] = is_fl_functor.is_fl_functor_op
subsubsection‹The composition of full functor is a full functor›
lemma cf_comp_is_fl_functor[cf_cs_intros]:
assumes "𝔊 : 𝔅 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ" and "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ 𝔅"
shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ ℭ"
proof(intro is_fl_functorI)
interpret 𝔉: is_fl_functor α 𝔄 𝔅 𝔉 using assms(2) by simp
interpret 𝔊: is_fl_functor α 𝔅 ℭ 𝔊 using assms(1) by simp
from 𝔉.is_functor_axioms 𝔊.is_functor_axioms show "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show "cf_smcf (𝔊 ∘⇩C⇩F 𝔉) : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩u⇩l⇩l⇘α⇙ cat_smc ℭ"
by
(
cs_concl
cs_simp: slicing_commute[symmetric]
cs_intro: cf_cs_intros smcf_cs_intros slicing_intros
)
qed
subsection‹Fully faithful functor›
subsubsection‹Definition and elementary properties›
text‹See Chapter I-3 in \<^cite>‹"mac_lane_categories_2010"›).›
locale is_ff_functor = is_ft_functor α 𝔄 𝔅 𝔉 + is_fl_functor α 𝔄 𝔅 𝔉
for α 𝔄 𝔅 𝔉
syntax "_is_ff_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ↦↦⇩C⇩.⇩f⇩fı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ↦↦⇩C⇩.⇩f⇩f⇘α⇙ 𝔅" ⇌ "CONST is_ff_functor α 𝔄 𝔅 𝔉"
text‹Rules.›
mk_ide rf is_ff_functor_def
|intro is_ff_functorI|
|dest is_ff_functorD[dest]|
|elim is_ff_functorE[elim]|
lemmas [cf_cs_intros] = is_ff_functorD
text‹Elementary properties.›
lemma (in is_ff_functor) ff_cf_is_ff_semifunctor:
"cf_smcf 𝔉 : cat_smc 𝔄 ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ cat_smc 𝔅"
by (rule is_ff_semifunctorI) (auto intro: slicing_intros)
lemma (in is_ff_functor) ff_cf_is_ff_semifunctor'[slicing_intros]:
assumes "𝔄' = cat_smc 𝔄" and "𝔅' = cat_smc 𝔅"
shows "cf_smcf 𝔉 : 𝔄' ↦↦⇩S⇩M⇩C⇩.⇩f⇩f⇘α⇙ 𝔅'"
unfolding assms by (rule ff_cf_is_ff_semifunctor)