Theory CZH_UCAT_PWKan
section‹Pointwise Kan extensions›
theory CZH_UCAT_PWKan
imports CZH_UCAT_Kan
begin
subsection‹Pointwise Kan extensions›
text‹
The following subsection is based on elements of the
content of section 6.3 in \<^cite>‹"riehl_category_2016"› and
Chapter X-5 in \<^cite>‹"mac_lane_categories_2010"›.
›
locale is_cat_pw_rKe = is_cat_rKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε
for α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε +
assumes cat_pw_rKe_preserved: "a ∈⇩∘ 𝔄⦇Obj⦈ ⟹
ε :
𝔊 ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 :
𝔅 ↦⇩C ℭ ↦⇩C (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) : 𝔄 ↦↦⇩C cat_Set α)"
syntax "_is_cat_pw_rKe" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
(
‹(_ :/ _ ∘⇩C⇩F _ ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩wı _ :/ _ ↦⇩C _ ↦⇩C _)›
[51, 51, 51, 51, 51, 51, 51] 51
)
translations "ε : 𝔊 ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩w⇘α⇙ 𝔗 : 𝔅 ↦⇩C ℭ ↦⇩C 𝔄" ⇌
"CONST is_cat_pw_rKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔊 ε"
locale is_cat_pw_lKe = is_cat_lKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η
for α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η +
assumes cat_pw_lKe_preserved: "a ∈⇩∘ op_cat 𝔄⦇Obj⦈ ⟹
op_ntcf η :
op_cf 𝔉 ∘⇩C⇩F op_cf 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ op_cf 𝔗 :
op_cat 𝔅 ↦⇩C op_cat ℭ ↦⇩C (Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) : op_cat 𝔄 ↦↦⇩C cat_Set α)"
syntax "_is_cat_pw_lKe" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
(
‹(_ :/ _ ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩wı _ ∘⇩C⇩F _ :/ _ ↦⇩C _ ↦⇩C _)›
[51, 51, 51, 51, 51, 51, 51] 51
)
translations "η : 𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩w⇘α⇙ 𝔉 ∘⇩C⇩F 𝔎 : 𝔅 ↦⇩C ℭ ↦⇩C 𝔄" ⇌
"CONST is_cat_pw_lKe α 𝔅 ℭ 𝔄 𝔎 𝔗 𝔉 η"
lemma (in is_cat_pw_rKe) cat_pw_rKe_preserved'[cat_Kan_cs_intros]:
assumes "a ∈⇩∘ 𝔄⦇Obj⦈"
and "𝔄' = 𝔄"
and "ℌ' = Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-)"
and "𝔈' = cat_Set α"
shows "ε : 𝔊 ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 : 𝔅 ↦⇩C ℭ ↦⇩C (ℌ' : 𝔄' ↦↦⇩C 𝔈')"
using assms(1) unfolding assms(2-4) by (rule cat_pw_rKe_preserved)
lemmas [cat_Kan_cs_intros] = is_cat_pw_rKe.cat_pw_rKe_preserved'
lemma (in is_cat_pw_lKe) cat_pw_lKe_preserved'[cat_Kan_cs_intros]:
assumes "a ∈⇩∘ op_cat 𝔄⦇Obj⦈"
and "𝔉' = op_cf 𝔉"
and "𝔎' = op_cf 𝔎"
and "𝔗' = op_cf 𝔗"
and "𝔅' = op_cat 𝔅"
and "ℭ' = op_cat ℭ"
and "𝔄' = op_cat 𝔄"
and "ℌ' = Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a)"
and "𝔈' = cat_Set α"
shows "op_ntcf η :
𝔉' ∘⇩C⇩F 𝔎' ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗' : 𝔅' ↦⇩C ℭ' ↦⇩C (ℌ' : 𝔄' ↦↦⇩C 𝔈')"
using assms(1) unfolding assms by (rule cat_pw_lKe_preserved)
lemmas [cat_Kan_cs_intros] = is_cat_pw_lKe.cat_pw_lKe_preserved'
text‹Rules.›
lemma (in is_cat_pw_rKe) is_cat_pw_rKe_axioms'[cat_Kan_cs_intros]:
assumes "α' = α"
and "𝔊' = 𝔊"
and "𝔎' = 𝔎"
and "𝔗' = 𝔗"
and "𝔅' = 𝔅"
and "𝔄' = 𝔄"
and "ℭ' = ℭ"
shows "ε : 𝔊' ∘⇩C⇩F 𝔎' ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩w⇘α'⇙ 𝔗' : 𝔅' ↦⇩C ℭ' ↦⇩C 𝔄'"
unfolding assms by (rule is_cat_pw_rKe_axioms)
mk_ide rf is_cat_pw_rKe_def[unfolded is_cat_pw_rKe_axioms_def]
|intro is_cat_pw_rKeI|
|dest is_cat_pw_rKeD[dest]|
|elim is_cat_pw_rKeE[elim]|
lemmas [cat_Kan_cs_intros] = is_cat_pw_rKeD(1)
lemma (in is_cat_pw_lKe) is_cat_pw_lKe_axioms'[cat_Kan_cs_intros]:
assumes "α' = α"
and "𝔉' = 𝔉"
and "𝔎' = 𝔎"
and "𝔗' = 𝔗"
and "𝔅' = 𝔅"
and "𝔄' = 𝔄"
and "ℭ' = ℭ"
shows "η : 𝔗' ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩w⇘α'⇙ 𝔉' ∘⇩C⇩F 𝔎' : 𝔅' ↦⇩C ℭ' ↦⇩C 𝔄'"
unfolding assms by (rule is_cat_pw_lKe_axioms)
mk_ide rf is_cat_pw_lKe_def[unfolded is_cat_pw_lKe_axioms_def]
|intro is_cat_pw_lKeI|
|dest is_cat_pw_lKeD[dest]|
|elim is_cat_pw_lKeE[elim]|
lemmas [cat_Kan_cs_intros] = is_cat_pw_lKeD(1)
text‹Duality.›
lemma (in is_cat_pw_rKe) is_cat_pw_lKe_op:
"op_ntcf ε :
op_cf 𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩w⇘α⇙ op_cf 𝔊 ∘⇩C⇩F op_cf 𝔎 :
op_cat 𝔅 ↦⇩C op_cat ℭ ↦⇩C op_cat 𝔄"
proof(intro is_cat_pw_lKeI, unfold cat_op_simps)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
from cat_pw_rKe_preserved[OF prems] prems show
"ε :
𝔊 ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 :
𝔅 ↦⇩C ℭ ↦⇩C (Hom⇩O⇩.⇩C⇘α⇙op_cat 𝔄(-,a) : 𝔄 ↦↦⇩C cat_Set α)"
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
qed (cs_concl cs_shallow cs_intro: cat_op_intros)
lemma (in is_cat_pw_rKe) is_cat_pw_lKe_op'[cat_op_intros]:
assumes "𝔗' = op_cf 𝔗"
and "𝔊' = op_cf 𝔊"
and "𝔎' = op_cf 𝔎"
and "𝔅' = op_cat 𝔅"
and "𝔄' = op_cat 𝔄"
and "ℭ' = op_cat ℭ"
shows "op_ntcf ε : 𝔗' ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩w⇘α⇙ 𝔊' ∘⇩C⇩F 𝔎' : 𝔅' ↦⇩C ℭ' ↦⇩C 𝔄'"
unfolding assms by (rule is_cat_pw_lKe_op)
lemmas [cat_op_intros] = is_cat_pw_rKe.is_cat_pw_lKe_op'
lemma (in is_cat_pw_lKe) is_cat_pw_rKe_op:
"op_ntcf η :
op_cf 𝔉 ∘⇩C⇩F op_cf 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩w⇘α⇙ op_cf 𝔗 :
op_cat 𝔅 ↦⇩C op_cat ℭ ↦⇩C op_cat 𝔄"
proof(intro is_cat_pw_rKeI, unfold cat_op_simps)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
from cat_pw_lKe_preserved[unfolded cat_op_simps, OF prems] prems show
"op_ntcf η :
op_cf 𝔉 ∘⇩C⇩F op_cf 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ op_cf 𝔗 :
op_cat 𝔅 ↦⇩C op_cat ℭ ↦⇩C
(Hom⇩O⇩.⇩C⇘α⇙op_cat 𝔄(a,-) : op_cat 𝔄 ↦↦⇩C cat_Set α)"
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_cs_intros)
qed (cs_concl cs_shallow cs_intro: cat_op_intros)
lemma (in is_cat_pw_lKe) is_cat_pw_lKe_op'[cat_op_intros]:
assumes "𝔗' = op_cf 𝔗"
and "𝔉' = op_cf 𝔉"
and "𝔎' = op_cf 𝔎"
and "𝔅' = op_cat 𝔅"
and "𝔄' = op_cat 𝔄"
and "ℭ' = op_cat ℭ"
shows "op_ntcf η : 𝔉' ∘⇩C⇩F 𝔎' ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩w⇘α⇙ 𝔗' : 𝔅' ↦⇩C ℭ' ↦⇩C 𝔄'"
unfolding assms by (rule is_cat_pw_rKe_op)
lemmas [cat_op_intros] = is_cat_pw_lKe.is_cat_pw_lKe_op'
subsection‹Lemma X.5: ‹L_10_5_N›\label{sec:lem_X_5_start}›
text‹
This subsection and several further subsections
(\ref{sec:lem_X_5_start}-\ref{sec:lem_X_5_end})
expose definitions that are used in the proof of the technical lemma that
was used in the proof of Theorem 3 from Chapter X-5
in \<^cite>‹"mac_lane_categories_2010"›.
›
definition L_10_5_N :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "L_10_5_N α β 𝔗 𝔎 c =
[
(
λa∈⇩∘𝔗⦇HomCod⦈⦇Obj⦈.
cf_nt α β 𝔎⦇ObjMap⦈⦇cf_map (Hom⇩O⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(a,-) ∘⇩C⇩F 𝔗), c⦈⇩∙
),
(
λf∈⇩∘𝔗⦇HomCod⦈⦇Arr⦈.
cf_nt α β 𝔎⦇ArrMap⦈⦇
ntcf_arrow (Hom⇩A⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(f,-) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗), 𝔎⦇HomCod⦈⦇CId⦈⦇c⦈
⦈⇩∙
),
op_cat (𝔗⦇HomCod⦈),
cat_Set β
]⇩∘"
text‹Components.›
lemma L_10_5_N_components:
shows "L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈ =
(
λa∈⇩∘𝔗⦇HomCod⦈⦇Obj⦈.
cf_nt α β 𝔎⦇ObjMap⦈⦇cf_map (Hom⇩O⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(a,-) ∘⇩C⇩F 𝔗), c⦈⇩∙
)"
and "L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈ =
(
λf∈⇩∘𝔗⦇HomCod⦈⦇Arr⦈.
cf_nt α β 𝔎⦇ArrMap⦈⦇
ntcf_arrow (Hom⇩A⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(f,-) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗), 𝔎⦇HomCod⦈⦇CId⦈⦇c⦈
⦈⇩∙
)"
and "L_10_5_N α β 𝔗 𝔎 c⦇HomDom⦈ = op_cat (𝔗⦇HomCod⦈)"
and "L_10_5_N α β 𝔗 𝔎 c⦇HomCod⦈ = cat_Set β"
unfolding L_10_5_N_def dghm_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
lemmas L_10_5_N_components' = L_10_5_N_components[
where 𝔗=𝔗 and 𝔎=𝔎, unfolded cat_cs_simps
]
lemmas [cat_Kan_cs_simps] = L_10_5_N_components'(3,4)
end
subsubsection‹Object map›
mk_VLambda L_10_5_N_components(1)
|vsv L_10_5_N_ObjMap_vsv[cat_Kan_cs_intros]|
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗 c
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
mk_VLambda L_10_5_N_components'(1)[OF 𝔎 𝔗]
|vdomain L_10_5_N_ObjMap_vdomain[cat_Kan_cs_simps]|
|app L_10_5_N_ObjMap_app[cat_Kan_cs_simps]|
end
subsubsection‹Arrow map›
mk_VLambda L_10_5_N_components(2)
|vsv L_10_5_N_ArrMap_vsv[cat_Kan_cs_intros]|
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗 c
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
mk_VLambda L_10_5_N_components'(2)[OF 𝔎 𝔗]
|vdomain L_10_5_N_ArrMap_vdomain[cat_Kan_cs_simps]|
|app L_10_5_N_ArrMap_app[cat_Kan_cs_simps]|
end
subsubsection‹‹L_10_5_N› is a functor›
lemma L_10_5_N_is_functor:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
shows "L_10_5_N α β 𝔗 𝔎 c : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
proof-
let ?FUNCT = ‹λ𝔄. cat_FUNCT α 𝔄 (cat_Set α)›
interpret β: 𝒵 β by (rule assms(1))
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(3))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(4))
from assms(2) interpret FUNCT_𝔅: tiny_category β ‹?FUNCT 𝔅›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
interpret β𝔎: is_tiny_functor β 𝔅 ℭ 𝔎
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔗: is_tiny_functor β 𝔅 𝔄 𝔗
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
from assms(2) interpret cf_nt:
is_functor β ‹?FUNCT 𝔅 ×⇩C ℭ› ‹cat_Set β› ‹cf_nt α β 𝔎›
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(intro is_functorI')
show "vfsequence (L_10_5_N α β 𝔗 𝔎 c)" unfolding L_10_5_N_def by simp
show "vcard (L_10_5_N α β 𝔗 𝔎 c) = 4⇩ℕ"
unfolding L_10_5_N_def by (simp add: nat_omega_simps)
show "vsv (L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈)"
by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
from assms(3,4) show "vsv (L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈)"
by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
from assms show "𝒟⇩∘ (L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈) = op_cat 𝔄⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
show "ℛ⇩∘ (L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈) ⊆⇩∘ cat_Set β⦇Obj⦈"
unfolding L_10_5_N_components'[OF 𝔎.is_functor_axioms 𝔗.is_functor_axioms]
proof(rule vrange_VLambda_vsubset)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
from prems assms show
"cf_nt α β 𝔎⦇ObjMap⦈⦇cf_map (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗), c⦈⇩∙ ∈⇩∘
cat_Set β⦇Obj⦈"
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps cat_FUNCT_cs_simps
cs_intro:
cat_cs_intros FUNCT_𝔅.cat_Hom_in_Vset cat_FUNCT_cs_intros
)
qed
from assms show "𝒟⇩∘ (L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈) = op_cat 𝔄⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
show "L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇f⦈ :
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘op_cat 𝔄⇙ b" for a b f
using that assms
unfolding cat_op_simps
by
(
cs_concl
cs_simp: L_10_5_N_ArrMap_app L_10_5_N_ObjMap_app
cs_intro: cat_cs_intros cat_prod_cs_intros cat_FUNCT_cs_intros
)
show
"L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇g ∘⇩A⇘op_cat 𝔄⇙ f⦈ =
L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set β⇙ L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇f⦈"
if "g : b' ↦⇘op_cat 𝔄⇙ c'" and "f : a' ↦⇘op_cat 𝔄⇙ b'" for b' c' g a' f
proof-
from that assms(5) show ?thesis
unfolding cat_op_simps
by
(
cs_concl
cs_intro:
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
cat_FUNCT_cs_simps
cat_prod_cs_simps
cat_op_simps
cf_nt.cf_ArrMap_Comp[symmetric]
)
qed
show
"L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇op_cat 𝔄⦇CId⦈⦇a⦈⦈ =
cat_Set β⦇CId⦈⦇L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
proof-
note [cat_cs_simps] =
ntcf_id_cf_comp[symmetric]
ntcf_arrow_id_ntcf_id[symmetric]
cat_FUNCT_CId_app[symmetric]
from that[unfolded cat_op_simps] assms show ?thesis
by
(
cs_concl
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
cs_simp:
cat_FUNCT_cs_simps cat_cs_simps cat_Kan_cs_simps cat_op_simps
)
qed
qed (cs_concl cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)+
qed
lemma L_10_5_N_is_functor'[cat_Kan_cs_intros]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "𝔄' = op_cat 𝔄"
and "𝔅' = cat_Set β"
and "β' = β"
shows "L_10_5_N α β 𝔗 𝔎 c : 𝔄' ↦↦⇩C⇘β'⇙ 𝔅'"
using assms(1-5) unfolding assms(6-8) by (rule L_10_5_N_is_functor)
subsection‹Lemma X.5: ‹L_10_5_υ_arrow››
subsubsection‹Definition and elementary properties›
definition L_10_5_υ_arrow :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "L_10_5_υ_arrow 𝔗 𝔎 c τ a b =
[
(λf∈⇩∘Hom (𝔎⦇HomCod⦈) c (𝔎⦇ObjMap⦈⦇b⦈). τ⦇NTMap⦈⦇0, b, f⦈⇩∙),
Hom (𝔎⦇HomCod⦈) c (𝔎⦇ObjMap⦈⦇b⦈),
Hom (𝔗⦇HomCod⦈) a (𝔗⦇ObjMap⦈⦇b⦈)
]⇩∘"
text‹Components.›
lemma L_10_5_υ_arrow_components:
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ a b⦇ArrVal⦈ =
(λf∈⇩∘Hom (𝔎⦇HomCod⦈) c (𝔎⦇ObjMap⦈⦇b⦈). τ⦇NTMap⦈⦇0, b, f⦈⇩∙)"
and "L_10_5_υ_arrow 𝔗 𝔎 c τ a b⦇ArrDom⦈ = Hom (𝔎⦇HomCod⦈) c (𝔎⦇ObjMap⦈⦇b⦈)"
and "L_10_5_υ_arrow 𝔗 𝔎 c τ a b⦇ArrCod⦈ = Hom (𝔗⦇HomCod⦈) a (𝔗⦇ObjMap⦈⦇b⦈)"
unfolding L_10_5_υ_arrow_def arr_field_simps
by (simp_all add: nat_omega_simps)
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
lemmas L_10_5_υ_arrow_components' = L_10_5_υ_arrow_components[
where 𝔗=𝔗 and 𝔎=𝔎, unfolded cat_cs_simps
]
lemmas [cat_Kan_cs_simps] = L_10_5_υ_arrow_components'(2,3)
end
subsubsection‹Arrow value›
mk_VLambda L_10_5_υ_arrow_components(1)
|vsv L_10_5_υ_arrow_ArrVal_vsv[cat_Kan_cs_intros]|
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
mk_VLambda L_10_5_υ_arrow_components'(1)[OF 𝔎 𝔗]
|vdomain L_10_5_υ_arrow_ArrVal_vdomain[cat_Kan_cs_simps]|
|app L_10_5_υ_arrow_ArrVal_app[unfolded in_Hom_iff]|
end
lemma L_10_5_υ_arrow_ArrVal_app':
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ a b⦇ArrVal⦈⦇f⦈ = τ⦇NTMap⦈⦇0, b, f⦈⇩∙"
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
from assms(3) have c: "c ∈⇩∘ ℭ⦇Obj⦈" by auto
show ?thesis by (rule L_10_5_υ_arrow_ArrVal_app[OF assms(1,2,3)])
qed
subsubsection‹‹L_10_5_υ_arrow› is an arrow›
lemma L_10_5_υ_arrow_ArrVal_is_arr:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "τ' = ntcf_arrow τ"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrVal⦈⦇f⦈ : a ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇b⦈"
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ by (rule assms(4))
from assms(5,6) show ?thesis
unfolding assms(3)
by
(
cs_concl
cs_simp:
cat_cs_simps
L_10_5_υ_arrow_ArrVal_app
cat_comma_cs_simps
cat_FUNCT_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
qed
lemma L_10_5_υ_arrow_ArrVal_is_arr'[cat_Kan_cs_intros]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "τ' = ntcf_arrow τ"
and "a' = a"
and "b' = 𝔗⦇ObjMap⦈⦇b⦈"
and "𝔄' = 𝔄"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrVal⦈⦇f⦈ : a' ↦⇘𝔄⇙ b'"
using assms(1-3, 7-9)
unfolding assms(3-6)
by (rule L_10_5_υ_arrow_ArrVal_is_arr)
subsubsection‹Further properties›
lemma L_10_5_υ_arrow_is_arr:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "τ' = ntcf_arrow τ"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ' a b :
Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b⦈)"
proof-
note L_10_5_υ_arrow_components = L_10_5_υ_arrow_components'[OF assms(1,2)]
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ by (rule assms(5))
show ?thesis
proof(intro cat_Set_is_arrI)
show "arr_Set α (L_10_5_υ_arrow 𝔗 𝔎 c τ' a b)"
proof(intro arr_SetI)
show "vfsequence (L_10_5_υ_arrow 𝔗 𝔎 c τ' a b)"
unfolding L_10_5_υ_arrow_def by simp
show "vcard (L_10_5_υ_arrow 𝔗 𝔎 c τ' a b) = 3⇩ℕ"
unfolding L_10_5_υ_arrow_def by (simp add: nat_omega_simps)
show
"ℛ⇩∘ (L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrVal⦈) ⊆⇩∘
L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrCod⦈"
unfolding L_10_5_υ_arrow_components
proof(intro vrange_VLambda_vsubset, unfold in_Hom_iff)
fix f assume "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
from L_10_5_υ_arrow_ArrVal_is_arr[OF assms(1,2,4,5) this assms(6)] this
show "τ'⦇NTMap⦈⦇0, b, f⦈⇩∙ : a ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇b⦈"
by
(
cs_prems cs_shallow
cs_simp: L_10_5_υ_arrow_ArrVal_app' cat_cs_simps
cs_intro: cat_cs_intros
)
qed
from assms(3,6) show "L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrDom⦈ ∈⇩∘ Vset α"
by (cs_concl cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)
from assms(1-3,6) τ.cat_cone_obj show
"L_10_5_υ_arrow 𝔗 𝔎 c τ' a b⦇ArrCod⦈ ∈⇩∘ Vset α"
by (cs_concl cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)
qed (auto simp: L_10_5_υ_arrow_components)
qed (simp_all add: L_10_5_υ_arrow_components)
qed
lemma L_10_5_υ_arrow_is_arr'[cat_Kan_cs_intros]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "τ' = ntcf_arrow τ"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "b ∈⇩∘ 𝔅⦇Obj⦈"
and "A = Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈)"
and "B = Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b⦈)"
and "ℭ' = cat_Set α"
shows "L_10_5_υ_arrow 𝔗 𝔎 c τ' a b : A ↦⇘ℭ'⇙ B"
using assms(1-6) unfolding assms(7-9) by (rule L_10_5_υ_arrow_is_arr)
lemma L_10_5_υ_cf_hom[cat_Kan_cs_simps]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "τ' = ntcf_arrow τ"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
and "f : a' ↦⇘𝔅⇙ b'"
shows
"L_10_5_υ_arrow 𝔗 𝔎 c τ' a b' ∘⇩A⇘cat_Set α⇙
cf_hom ℭ [ℭ⦇CId⦈⦇c⦈, 𝔎⦇ArrMap⦈⦇f⦈]⇩∘ =
cf_hom 𝔄 [𝔄⦇CId⦈⦇a⦈, 𝔗⦇ArrMap⦈⦇f⦈]⇩∘ ∘⇩A⇘cat_Set α⇙
L_10_5_υ_arrow 𝔗 𝔎 c τ' a a'"
(is "?lhs = ?rhs")
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ by (rule assms(5))
have [cat_Kan_cs_simps]:
"τ⦇NTMap⦈⦇a'', b'', 𝔎⦇ArrMap⦈⦇h'⦈ ∘⇩A⇘ℭ⇙ f'⦈⇩∙ =
𝔗⦇ArrMap⦈⦇h'⦈ ∘⇩A⇘𝔄⇙ τ⦇NTMap⦈⦇a', b', f'⦈⇩∙"
if F_def: "F = [[a', b', f']⇩∘, [a'', b'', f'']⇩∘, [g', h']⇩∘]⇩∘"
and A_def: "A = [a', b', f']⇩∘"
and B_def: "B = [a'', b'', f'']⇩∘"
and F: "F : A ↦⇘c ↓⇩C⇩F 𝔎⇙ B"
for F A B a' b' f' a'' b'' f'' g' h'
proof-
from F[unfolded F_def A_def B_def] assms(3) have a'_def: "a' = 0"
and a''_def: "a'' = 0"
and g'_def: "g' = 0"
and h': "h' : b' ↦⇘𝔅⇙ b''"
and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
and f'': "f'' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b''⦈"
and f''_def: "𝔎⦇ArrMap⦈⦇h'⦈ ∘⇩A⇘ℭ⇙ f' = f''"
by auto
note τ.cat_cone_Comp_commute[cat_cs_simps del]
from
τ.ntcf_Comp_commute[OF F]
that(2) F g' h' f' f''
𝔎.is_functor_axioms
𝔗.is_functor_axioms
show
"τ⦇NTMap⦈⦇a'', b'', 𝔎⦇ArrMap⦈⦇h'⦈ ∘⇩A⇘ℭ⇙ f'⦈⇩∙ =
𝔗⦇ArrMap⦈⦇h'⦈ ∘⇩A⇘𝔄⇙ τ⦇NTMap⦈⦇a', b', f'⦈⇩∙"
unfolding F_def A_def B_def a'_def a''_def g'_def
by
(
cs_prems
cs_simp: cat_cs_simps cat_comma_cs_simps f''_def[symmetric]
cs_intro: cat_cs_intros cat_comma_cs_intros
)
qed
from assms(3) assms(6,7) 𝔎.HomCod.category_axioms have lhs_is_arr:
"?lhs : Hom ℭ c (𝔎⦇ObjMap⦈⦇a'⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b'⦈)"
unfolding assms(4)
by
(
cs_concl cs_intro:
cat_lim_cs_intros
cat_cs_intros
cat_Kan_cs_intros
cat_prod_cs_intros
cat_op_intros
)
then have dom_lhs: "𝒟⇩∘ ((?lhs)⦇ArrVal⦈) = Hom ℭ c (𝔎⦇ObjMap⦈⦇a'⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms(3) assms(6,7) 𝔎.HomCod.category_axioms 𝔗.HomCod.category_axioms
have rhs_is_arr:
"?rhs : Hom ℭ c (𝔎⦇ObjMap⦈⦇a'⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b'⦈)"
unfolding assms(4)
by
(
cs_concl cs_intro:
cat_lim_cs_intros
cat_cs_intros
cat_Kan_cs_intros
cat_prod_cs_intros
cat_op_intros
)
then have dom_rhs: "𝒟⇩∘ ((?rhs)⦇ArrVal⦈) = Hom ℭ c (𝔎⦇ObjMap⦈⦇a'⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from lhs_is_arr show arr_Set_lhs: "arr_Set α ?lhs"
by (auto dest: cat_Set_is_arrD(1))
from rhs_is_arr show arr_Set_rhs: "arr_Set α ?rhs"
by (auto dest: cat_Set_is_arrD(1))
show "?lhs⦇ArrVal⦈ = ?rhs⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix g assume prems: "g : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇a'⦈"
from prems assms(7) have 𝔎f:
"𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ g : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b'⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
with assms(6,7) prems 𝔎.HomCod.category_axioms 𝔗.HomCod.category_axioms
show "?lhs⦇ArrVal⦈⦇g⦈ = ?rhs⦇ArrVal⦈⦇g⦈"
by
(
cs_concl
cs_intro:
cat_lim_cs_intros
cat_cs_intros
cat_Kan_cs_intros
cat_comma_cs_intros
cat_prod_cs_intros
cat_op_intros
cat_1_is_arrI
cs_simp:
L_10_5_υ_arrow_ArrVal_app'
cat_cs_simps
cat_Kan_cs_simps
cat_op_simps
cat_FUNCT_cs_simps
cat_comma_cs_simps
assms(4)
)+
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed
(
use lhs_is_arr rhs_is_arr in
‹cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros›
)+
qed
subsection‹Lemma X.5: ‹L_10_5_τ››
subsubsection‹Definition and elementary properties›
definition L_10_5_τ where "L_10_5_τ 𝔗 𝔎 c υ a =
[
(λbf∈⇩∘c ↓⇩C⇩F 𝔎⦇Obj⦈. υ⦇NTMap⦈⦇bf⦇1⇩ℕ⦈⦈⦇ArrVal⦈⦇bf⦇2⇩ℕ⦈⦈),
cf_const (c ↓⇩C⇩F 𝔎) (𝔗⦇HomCod⦈) a,
𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎,
c ↓⇩C⇩F 𝔎,
(𝔗⦇HomCod⦈)
]⇩∘"
text‹Components.›
lemma L_10_5_τ_components:
shows "L_10_5_τ 𝔗 𝔎 c υ a⦇NTMap⦈ =
(λbf∈⇩∘c ↓⇩C⇩F 𝔎⦇Obj⦈. υ⦇NTMap⦈⦇bf⦇1⇩ℕ⦈⦈⦇ArrVal⦈⦇bf⦇2⇩ℕ⦈⦈)"
and "L_10_5_τ 𝔗 𝔎 c υ a⦇NTDom⦈ = cf_const (c ↓⇩C⇩F 𝔎) (𝔗⦇HomCod⦈) a"
and "L_10_5_τ 𝔗 𝔎 c υ a⦇NTCod⦈ = 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎"
and "L_10_5_τ 𝔗 𝔎 c υ a⦇NTDGDom⦈ = c ↓⇩C⇩F 𝔎"
and "L_10_5_τ 𝔗 𝔎 c υ a⦇NTDGCod⦈ = (𝔗⦇HomCod⦈)"
unfolding L_10_5_τ_def nt_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
lemmas L_10_5_τ_components' = L_10_5_τ_components[
where 𝔗=𝔗 and 𝔎=𝔎, unfolded cat_cs_simps
]
lemmas [cat_Kan_cs_simps] = L_10_5_τ_components'(2-5)
end
subsubsection‹Natural transformation map›
mk_VLambda L_10_5_τ_components(1)
|vsv L_10_5_τ_NTMap_vsv[cat_Kan_cs_intros]|
|vdomain L_10_5_τ_NTMap_vdomain[cat_Kan_cs_simps]|
lemma L_10_5_τ_NTMap_app[cat_Kan_cs_simps]:
assumes "bf = [0, b, f]⇩∘" and "bf ∈⇩∘ c ↓⇩C⇩F 𝔎⦇Obj⦈"
shows "L_10_5_τ 𝔗 𝔎 c υ a⦇NTMap⦈⦇bf⦈ = υ⦇NTMap⦈⦇b⦈⦇ArrVal⦈⦇f⦈"
using assms unfolding L_10_5_τ_components by (simp add: nat_omega_simps)
subsubsection‹‹L_10_5_τ› is a cone›
lemma L_10_5_τ_is_cat_cone[cat_cs_intros]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and υ'_def: "υ' = ntcf_arrow υ"
and υ: "υ :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_τ 𝔗 𝔎 c υ' a : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
proof-
let ?H_ℭ = ‹λc. Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-)›
let ?H_𝔄 = ‹λa. Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-)›
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
from assms(3) interpret c𝔎: category α ‹c ↓⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from assms(3) interpret Πc: is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by
(
cs_concl cs_shallow
cs_simp: cat_comma_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
interpret υ: is_ntcf α 𝔅 ‹cat_Set α› ‹?H_ℭ c ∘⇩C⇩F 𝔎› ‹?H_𝔄 a ∘⇩C⇩F 𝔗› υ
by (rule υ)
show ?thesis
proof(intro is_cat_coneI is_ntcfI')
show "vfsequence (L_10_5_τ 𝔗 𝔎 c υ' a)" unfolding L_10_5_τ_def by simp
show "vcard (L_10_5_τ 𝔗 𝔎 c υ' a) = 5⇩ℕ"
unfolding L_10_5_τ_def by (simp add: nat_omega_simps)
from a interpret cf_const:
is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a›
by (cs_concl cs_intro: cat_cs_intros)
show "L_10_5_τ 𝔗 𝔎 c υ' a⦇NTMap⦈⦇bf⦈ :
cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a⦇ObjMap⦈⦇bf⦈ ↦⇘𝔄⇙ (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇bf⦈"
if "bf ∈⇩∘ c ↓⇩C⇩F 𝔎⦇Obj⦈" for bf
proof-
from that assms(3) obtain b f
where bf_def: "bf = [0, b, f]⇩∘"
and b: "b ∈⇩∘ 𝔅⦇Obj⦈"
and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
by auto
from υ.ntcf_NTMap_is_arr[OF b] a b assms(3) f have "υ⦇NTMap⦈⦇b⦈ :
Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b⦈)"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
with that b f show "L_10_5_τ 𝔗 𝔎 c υ' a⦇NTMap⦈⦇bf⦈ :
cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a⦇ObjMap⦈⦇bf⦈ ↦⇘𝔄⇙ (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇bf⦈"
unfolding bf_def υ'_def
by
(
cs_concl
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
cat_comma_cs_simps
cat_FUNCT_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
qed
show
"L_10_5_τ 𝔗 𝔎 c υ' a⦇NTMap⦈⦇B⦈ ∘⇩A⇘𝔄⇙ cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a⦇ArrMap⦈⦇F⦈ =
(𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ArrMap⦈⦇F⦈ ∘⇩A⇘𝔄⇙ L_10_5_τ 𝔗 𝔎 c υ' a⦇NTMap⦈⦇A⦈"
if "F : A ↦⇘c ↓⇩C⇩F 𝔎⇙ B" for A B F
proof-
from 𝔎.is_functor_axioms that assms(3) obtain a' f a'' f' g
where F_def: "F = [[0, a', f]⇩∘, [0, a'', f']⇩∘, [0, g]⇩∘]⇩∘"
and A_def: "A = [0, a', f]⇩∘"
and B_def: "B = [0, a'', f']⇩∘"
and g: "g : a' ↦⇘𝔅⇙ a''"
and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇a'⦈"
and f': "f' : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇a''⦈"
and f'_def: "𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ f = f'"
by auto
from υ.ntcf_Comp_commute[OF g] have
"(υ⦇NTMap⦈⦇a''⦈ ∘⇩A⇘cat_Set α⇙ (?H_ℭ c ∘⇩C⇩F 𝔎)⦇ArrMap⦈⦇g⦈)⦇ArrVal⦈⦇f⦈ =
((?H_𝔄 a ∘⇩C⇩F 𝔗)⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ υ⦇NTMap⦈⦇a'⦈)⦇ArrVal⦈⦇f⦈"
by simp
from this a g f f' 𝔎.HomCod.category_axioms 𝔗.HomCod.category_axioms
have [cat_cs_simps]:
"υ⦇NTMap⦈⦇a''⦈⦇ArrVal⦈⦇𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ f⦈ =
𝔗⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔄⇙ υ⦇NTMap⦈⦇a'⦈⦇ArrVal⦈⦇f⦈"
by
(
cs_prems
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_prod_cs_intros cat_op_intros
)
from that a g f f' 𝔎.HomCod.category_axioms 𝔗.HomCod.category_axioms
show ?thesis
unfolding F_def A_def B_def υ'_def
by
(
cs_concl
cs_simp:
f'_def[symmetric]
cat_cs_simps
cat_Kan_cs_simps
cat_comma_cs_simps
cat_FUNCT_cs_simps
cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed
qed
(
use assms in
‹
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros a
›
)+
qed
lemma L_10_5_τ_is_cat_cone'[cat_Kan_cs_intros]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "υ' = ntcf_arrow υ"
and "𝔉' = 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎"
and "c𝔎 = c ↓⇩C⇩F 𝔎"
and "𝔄' = 𝔄"
and "α' = α"
and "υ :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_τ 𝔗 𝔎 c υ' a : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉' : c𝔎 ↦↦⇩C⇘α'⇙ 𝔄'"
using assms(1-4,9,10) unfolding assms(5-8) by (rule L_10_5_τ_is_cat_cone)
subsection‹Lemma X.5: ‹L_10_5_υ››
subsubsection‹Definition and elementary properties›
definition L_10_5_υ :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "L_10_5_υ α 𝔗 𝔎 c τ a =
[
(λb∈⇩∘𝔗⦇HomDom⦈⦇Obj⦈. L_10_5_υ_arrow 𝔗 𝔎 c τ a b),
Hom⇩O⇩.⇩C⇘α⇙𝔎⦇HomCod⦈(c,-) ∘⇩C⇩F 𝔎,
Hom⇩O⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(a,-) ∘⇩C⇩F 𝔗,
𝔗⦇HomDom⦈,
cat_Set α
]⇩∘"
text‹Components.›
lemma L_10_5_υ_components:
shows "L_10_5_υ α 𝔗 𝔎 c τ a⦇NTMap⦈ =
(λb∈⇩∘𝔗⦇HomDom⦈⦇Obj⦈. L_10_5_υ_arrow 𝔗 𝔎 c τ a b)"
and "L_10_5_υ α 𝔗 𝔎 c τ a⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔎⦇HomCod⦈(c,-) ∘⇩C⇩F 𝔎"
and "L_10_5_υ α 𝔗 𝔎 c τ a⦇NTCod⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔗⦇HomCod⦈(a,-) ∘⇩C⇩F 𝔗"
and "L_10_5_υ α 𝔗 𝔎 c τ a⦇NTDGDom⦈ = 𝔗⦇HomDom⦈"
and "L_10_5_υ α 𝔗 𝔎 c τ a⦇NTDGCod⦈ = cat_Set α"
unfolding L_10_5_υ_def nt_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
lemmas L_10_5_υ_components' = L_10_5_υ_components[
where 𝔗=𝔗 and 𝔎=𝔎, unfolded cat_cs_simps
]
lemmas [cat_Kan_cs_simps] = L_10_5_υ_components'(2-5)
end
subsubsection‹Natural transformation map›
mk_VLambda L_10_5_υ_components(1)
|vsv L_10_5_υ_NTMap_vsv[cat_Kan_cs_intros]|
context
fixes α 𝔅 ℭ 𝔄 𝔎 𝔗
assumes 𝔎: "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule 𝔎)
interpretation 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
mk_VLambda L_10_5_υ_components'(1)[OF 𝔎 𝔗]
|vdomain L_10_5_υ_NTMap_vdomain[cat_Kan_cs_simps]|
|app L_10_5_υ_NTMap_app[cat_Kan_cs_simps]|
end
subsubsection‹‹L_10_5_υ› is a natural transformation›
lemma L_10_5_υ_is_ntcf:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and τ'_def: "τ' = ntcf_arrow τ"
and τ: "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_υ α 𝔗 𝔎 c τ' a :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
(is ‹?L_10_5_υ : ?H_ℭ c ∘⇩C⇩F 𝔎 ↦⇩C⇩F ?H_𝔄 a ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α›)
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ
by (rule assms(5))
from assms(3) interpret c𝔎: category α ‹c ↓⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from assms(3) interpret Πc: is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by
(
cs_concl cs_shallow
cs_simp: cat_comma_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
show "?L_10_5_υ : ?H_ℭ c ∘⇩C⇩F 𝔎 ↦⇩C⇩F ?H_𝔄 a ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
proof(intro is_ntcfI')
show "vfsequence ?L_10_5_υ" unfolding L_10_5_υ_def by auto
show "vcard ?L_10_5_υ = 5⇩ℕ"
unfolding L_10_5_υ_def by (simp add: nat_omega_simps)
show "?L_10_5_υ⦇NTMap⦈⦇b⦈ :
(?H_ℭ c ∘⇩C⇩F 𝔎)⦇ObjMap⦈⦇b⦈ ↦⇘cat_Set α⇙ (?H_𝔄 a ∘⇩C⇩F 𝔗)⦇ObjMap⦈⦇b⦈"
if "b ∈⇩∘ 𝔅⦇Obj⦈" for b
proof-
from a that assms(3) show ?thesis
unfolding τ'_def
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Kan_cs_simps
cs_intro:
cat_Kan_cs_intros
cat_lim_cs_intros
cat_cs_intros
cat_op_intros
)
qed
show
"?L_10_5_υ⦇NTMap⦈⦇b'⦈ ∘⇩A⇘cat_Set α⇙ (?H_ℭ c ∘⇩C⇩F 𝔎)⦇ArrMap⦈⦇f⦈ =
(?H_𝔄 a ∘⇩C⇩F 𝔗)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?L_10_5_υ⦇NTMap⦈⦇a'⦈"
if "f : a' ↦⇘𝔅⇙ b'" for a' b' f
proof-
from that a assms(3) show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps τ'_def
cs_intro: cat_lim_cs_intros cat_cs_intros
)
qed
qed
(
use assms(3,6) in
‹
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros
›
)+
qed
lemma L_10_5_υ_is_ntcf'[cat_Kan_cs_intros]:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "τ' = ntcf_arrow τ"
and "𝔉' = Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎"
and "𝔊' = Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗"
and "𝔅' = 𝔅"
and "ℭ' = cat_Set α"
and "α' = α"
and "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_υ α 𝔗 𝔎 c τ' a : 𝔉' ↦⇩C⇩F 𝔊' : 𝔅' ↦↦⇩C⇘α'⇙ ℭ'"
using assms(1-4,10,11) unfolding assms(5-9) by (rule L_10_5_υ_is_ntcf)
subsection‹Lemma X.5: ‹L_10_5_χ_arrow››
subsubsection‹Definition and elementary properties›
definition L_10_5_χ_arrow
where "L_10_5_χ_arrow α β 𝔗 𝔎 c a =
[
(λυ∈⇩∘L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈. ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υ a)),
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈,
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈
]⇩∘"
text‹Components.›
lemma L_10_5_χ_arrow_components:
shows "L_10_5_χ_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈ =
(λυ∈⇩∘L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈. ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υ a))"
and "L_10_5_χ_arrow α β 𝔗 𝔎 c a⦇ArrDom⦈ = L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
and "L_10_5_χ_arrow α β 𝔗 𝔎 c a⦇ArrCod⦈ =
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
unfolding L_10_5_χ_arrow_def arr_field_simps
by (simp_all add: nat_omega_simps)
lemmas [cat_Kan_cs_simps] = L_10_5_χ_arrow_components(2,3)
subsubsection‹Arrow value›
mk_VLambda L_10_5_χ_arrow_components(1)
|vsv L_10_5_χ_arrow_vsv[cat_Kan_cs_intros]|
|vdomain L_10_5_χ_arrow_vdomain|
|app L_10_5_χ_arrow_app|
lemma L_10_5_χ_arrow_vdomain'[cat_Kan_cs_simps]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "𝒟⇩∘ (L_10_5_χ_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈) = Hom
(cat_FUNCT α 𝔅 (cat_Set α))
(cf_map (Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎))
(cf_map (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗))"
using assms
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps L_10_5_χ_arrow_vdomain
cs_intro: cat_cs_intros
)
lemma L_10_5_χ_arrow_app'[cat_Kan_cs_simps]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and υ'_def: "υ' = ntcf_arrow υ"
and υ: "υ :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows
"L_10_5_χ_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈⦇υ'⦈ =
ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υ' a)"
using assms
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Kan_cs_simps L_10_5_χ_arrow_app
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
lemma υτa_def:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and υτa'_def: "υτa' = ntcf_arrow υτa"
and υτa: "υτa :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "υτa = L_10_5_υ α 𝔗 𝔎 c (ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υτa' a)) a"
(is ‹υτa = ?L_10_5_υ (ntcf_arrow ?L_10_5_τ) a›)
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
interpret υτa: is_ntcf
α 𝔅 ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎› ‹Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗› υτa
by (rule υτa)
show ?thesis
proof(rule ntcf_eqI)
show "υτa :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by (rule υτa)
from assms(1-3) a show
"?L_10_5_υ (ntcf_arrow ?L_10_5_τ) a :
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps υτa'_def
cs_intro: cat_cs_intros cat_Kan_cs_intros
)
have dom_lhs: "𝒟⇩∘ (υτa⦇NTMap⦈) = 𝔅⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
have dom_rhs: "𝒟⇩∘ (?L_10_5_υ (ntcf_arrow (?L_10_5_τ)) a⦇NTMap⦈) = 𝔅⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)
show "υτa⦇NTMap⦈ = ?L_10_5_υ (ntcf_arrow ?L_10_5_τ) a⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix b assume prems: "b ∈⇩∘ 𝔅⦇Obj⦈"
from prems assms(3) a have lhs: "υτa⦇NTMap⦈⦇b⦈ :
Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b⦈)"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
)
then have dom_lhs: "𝒟⇩∘ (υτa⦇NTMap⦈⦇b⦈⦇ArrVal⦈) = Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from prems assms(3) a have rhs:
"L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a b :
Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈) ↦⇘cat_Set α⇙ Hom 𝔄 a (𝔗⦇ObjMap⦈⦇b⦈)"
unfolding υτa'_def
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ (L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a b⦇ArrVal⦈) =
Hom ℭ c (𝔎⦇ObjMap⦈⦇b⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
have [cat_cs_simps]:
"υτa⦇NTMap⦈⦇b⦈ = L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a b"
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs: "arr_Set α (υτa⦇NTMap⦈⦇b⦈)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs:
"arr_Set α (L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow (?L_10_5_τ)) a b)"
by (auto dest: cat_Set_is_arrD(1))
show "υτa⦇NTMap⦈⦇b⦈⦇ArrVal⦈ =
L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a b⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix f assume "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
with assms prems show
"υτa⦇NTMap⦈⦇b⦈⦇ArrVal⦈⦇f⦈ =
L_10_5_υ_arrow 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a b⦇ArrVal⦈⦇f⦈"
unfolding υτa'_def
by
(
cs_concl cs_shallow
cs_simp:
cat_Kan_cs_simps cat_FUNCT_cs_simps L_10_5_υ_arrow_ArrVal_app
cs_intro: cat_cs_intros cat_comma_cs_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
from prems show
"υτa⦇NTMap⦈⦇b⦈ = L_10_5_υ α 𝔗 𝔎 c (ntcf_arrow ?L_10_5_τ) a⦇NTMap⦈⦇b⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
)
qed (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros V_cs_intros)+
qed simp_all
qed
subsection‹Lemma X.5: ‹L_10_5_χ'_arrow››
subsubsection‹Definition and elementary properties›
definition L_10_5_χ'_arrow :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "L_10_5_χ'_arrow α β 𝔗 𝔎 c a =
[
(
λτ∈⇩∘cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈.
ntcf_arrow (L_10_5_υ α 𝔗 𝔎 c τ a)
),
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈,
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈
]⇩∘"
text‹Components.›
lemma L_10_5_χ'_arrow_components:
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈ =
(
λτ∈⇩∘cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈.
ntcf_arrow (L_10_5_υ α 𝔗 𝔎 c τ a)
)"
and [cat_Kan_cs_simps]: "L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrDom⦈ =
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
and [cat_Kan_cs_simps]: "L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrCod⦈ =
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
unfolding L_10_5_χ'_arrow_def arr_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Arrow value›
mk_VLambda L_10_5_χ'_arrow_components(1)
|vsv L_10_5_χ'_arrow_ArrVal_vsv[cat_Kan_cs_intros]|
|vdomain L_10_5_χ'_arrow_ArrVal_vdomain|
|app L_10_5_χ'_arrow_ArrVal_app|
lemma L_10_5_χ'_arrow_ArrVal_vdomain'[cat_Kan_cs_simps]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and τ: "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "𝒟⇩∘ (L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈) = Hom
(cat_FUNCT α (c ↓⇩C⇩F 𝔎) 𝔄)
(cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a))
(cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎))"
proof-
interpret β: 𝒵 β by (rule assms(1))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ
by (rule assms(3))
from assms(1,2,4) show ?thesis
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps L_10_5_χ'_arrow_ArrVal_vdomain
cs_intro: cat_cs_intros
)
qed
lemma L_10_5_χ'_arrow_ArrVal_app'[cat_cs_simps]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and τ'_def: "τ' = ntcf_arrow τ"
and τ: "τ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
and a: "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈⦇τ'⦈ =
ntcf_arrow (L_10_5_υ α 𝔗 𝔎 c τ' a)"
proof-
interpret β: 𝒵 β by (rule assms(1))
interpret τ: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› τ
by (rule assms(4))
from assms(2,5) have "τ' ∈⇩∘ cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
unfolding τ'_def
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_FUNCT_cs_intros cat_cs_intros
)
then show
"L_10_5_χ'_arrow α β 𝔗 𝔎 c a⦇ArrVal⦈⦇τ'⦈ =
ntcf_arrow (L_10_5_υ α 𝔗 𝔎 c τ' a)"
unfolding L_10_5_χ'_arrow_components by auto
qed
subsubsection‹‹L_10_5_χ'_arrow› is an isomorphism in the category ‹Set››
lemma L_10_5_χ'_arrow_is_iso_arr:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a :
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set β⇙
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
(
is
‹
?L_10_5_χ'_arrow :
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set β⇙
?L_10_5_N⦇ObjMap⦈⦇a⦈
›
)
proof-
let ?FUNCT = ‹λ𝔄. cat_FUNCT α 𝔄 (cat_Set α)›
let ?c𝔎_𝔄 = ‹cat_FUNCT α (c ↓⇩C⇩F 𝔎) 𝔄›
let ?H_ℭ = ‹λc. Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-)›
let ?H_𝔄 = ‹λc. Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-)›
from assms(1,2) interpret β: 𝒵 β by simp
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(3))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(4))
from 𝔎.vempty_is_zet assms interpret c𝔎: category α ‹c ↓⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from assms(2,6) interpret c𝔎_𝔄: category β ?c𝔎_𝔄
by
(
cs_concl cs_intro:
cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
from 𝔎.vempty_is_zet assms interpret Πc:
is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from assms(2) interpret FUNCT_𝔄: tiny_category β ‹?FUNCT 𝔄›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from assms(2) interpret FUNCT_𝔅: tiny_category β ‹?FUNCT 𝔅›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from assms(2) interpret FUNCT_ℭ: tiny_category β ‹?FUNCT ℭ›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
have 𝔗Π: "𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by (cs_concl cs_intro: cat_cs_intros)
from assms(5,6) have [cat_cs_simps]:
"cf_of_cf_map (c ↓⇩C⇩F 𝔎) 𝔄 (cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a)) =
cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a"
"cf_of_cf_map (c ↓⇩C⇩F 𝔎) 𝔄 (cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)) = 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎"
"cf_of_cf_map 𝔅 (cat_Set α) (cf_map (Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎)) =
Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-) ∘⇩C⇩F 𝔎"
"cf_of_cf_map 𝔅 (cat_Set α) (cf_map (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)) =
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗"
by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)+
note cf_Cone_ObjMap_app = is_functor.cf_Cone_ObjMap_app[OF 𝔗Π assms(1,2,6)]
show ?thesis
proof
(
intro cat_Set_is_iso_arrI cat_Set_is_arrI arr_SetI,
unfold L_10_5_χ'_arrow_components(3) cf_Cone_ObjMap_app
)
show "vfsequence ?L_10_5_χ'_arrow"
unfolding L_10_5_χ'_arrow_def by auto
show χ'_arrow_ArrVal_vsv: "vsv (?L_10_5_χ'_arrow⦇ArrVal⦈)"
unfolding L_10_5_χ'_arrow_components by auto
show "vcard ?L_10_5_χ'_arrow = 3⇩ℕ"
unfolding L_10_5_χ'_arrow_def by (simp add: nat_omega_simps)
show [cat_cs_simps]:
"𝒟⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈) = ?L_10_5_χ'_arrow⦇ArrDom⦈"
unfolding L_10_5_χ'_arrow_components by simp
show vrange_χ'_arrow_vsubset_N'':
"ℛ⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈) ⊆⇩∘ ?L_10_5_N⦇ObjMap⦈⦇a⦈"
unfolding L_10_5_χ'_arrow_components
proof(rule vrange_VLambda_vsubset)
fix τ assume prems: "τ ∈⇩∘ cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
from this assms c𝔎_𝔄.category_axioms have τ_is_arr:
"τ : cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a) ↦⇘?c𝔎_𝔄⇙ cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)"
by
(
cs_prems
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_FUNCT_components(1)
cs_intro: cat_cs_intros
)
note τ = cat_FUNCT_is_arrD(1,2)[OF τ_is_arr, unfolded cat_cs_simps]
have "cf_of_cf_map (c ↓⇩C⇩F 𝔎) 𝔄 (cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)) = 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎"
by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
from prems assms τ(1) show
"ntcf_arrow (L_10_5_υ α 𝔗 𝔎 c τ a) ∈⇩∘ ?L_10_5_N⦇ObjMap⦈⦇a⦈"
by (subst τ(2))
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps
cs_intro:
is_cat_coneI cat_cs_intros cat_Kan_cs_intros cat_FUNCT_cs_intros
)
qed
show "ℛ⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈) = ?L_10_5_N⦇ObjMap⦈⦇a⦈"
proof
(
intro vsubset_antisym[OF vrange_χ'_arrow_vsubset_N''],
intro vsubsetI
)
fix υτa assume "υτa ∈⇩∘ ?L_10_5_N⦇ObjMap⦈⦇a⦈"
from this assms have υτa:
"υτa : cf_map (?H_ℭ c ∘⇩C⇩F 𝔎) ↦⇘?FUNCT 𝔅⇙ cf_map (?H_𝔄 a ∘⇩C⇩F 𝔗)"
by
(
cs_prems
cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
)
note υτa = cat_FUNCT_is_arrD[OF this, unfolded cat_cs_simps]
interpret τ:
is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› ‹L_10_5_τ 𝔗 𝔎 c υτa a›
by (rule L_10_5_τ_is_cat_cone[OF assms(3,4,5) υτa(2,1) assms(6)])
show "υτa ∈⇩∘ ℛ⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈)"
proof(rule vsv.vsv_vimageI2')
show "vsv (?L_10_5_χ'_arrow⦇ArrVal⦈)" by (rule χ'_arrow_ArrVal_vsv)
from τ.is_cat_cone_axioms assms show
"ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υτa a) ∈⇩∘ 𝒟⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈)"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
from assms υτa(1,2) show
"υτa = ?L_10_5_χ'_arrow⦇ArrVal⦈⦇ntcf_arrow (L_10_5_τ 𝔗 𝔎 c υτa a)⦈"
by
(
subst υτa(2),
cs_concl_step υτa_def[OF assms(3,4,5) υτa(2,1) assms(6)]
)
(cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
qed
from assms show "?L_10_5_χ'_arrow⦇ArrDom⦈ ∈⇩∘ Vset β"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_FUNCT_components(1) cf_Cone_ObjMap_app
cs_intro: cat_cs_intros cat_FUNCT_cs_intros c𝔎_𝔄.cat_Hom_in_Vset
)
with assms(2) have "?L_10_5_χ'_arrow⦇ArrDom⦈ ∈⇩∘ Vset β"
by (meson Vset_in_mono Vset_trans)
from assms show "?L_10_5_N⦇ObjMap⦈⦇a⦈ ∈⇩∘ Vset β"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_cs_intros FUNCT_𝔅.cat_Hom_in_Vset cat_FUNCT_cs_intros
)
show dom_χ'_arrow: "𝒟⇩∘ (?L_10_5_χ'_arrow⦇ArrVal⦈) =
Hom ?c𝔎_𝔄 (cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a)) (cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎))"
unfolding L_10_5_χ'_arrow_components cf_Cone_ObjMap_app by simp
show "?L_10_5_χ'_arrow⦇ArrDom⦈ =
Hom ?c𝔎_𝔄 (cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a)) (cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎))"
unfolding L_10_5_χ'_arrow_components cf_Cone_ObjMap_app by simp
show "v11 (?L_10_5_χ'_arrow⦇ArrVal⦈)"
proof(rule vsv.vsv_valeq_v11I, unfold dom_χ'_arrow in_Hom_iff)
fix τ' τ'' assume prems:
"τ' : cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a) ↦⇘?c𝔎_𝔄⇙ cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)"
"τ'' : cf_map (cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a) ↦⇘?c𝔎_𝔄⇙ cf_map (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)"
"?L_10_5_χ'_arrow⦇ArrVal⦈⦇τ'⦈ = ?L_10_5_χ'_arrow⦇ArrVal⦈⦇τ''⦈"
note τ' = cat_FUNCT_is_arrD[OF prems(1), unfolded cat_cs_simps]
and τ'' = cat_FUNCT_is_arrD[OF prems(2), unfolded cat_cs_simps]
interpret τ': is_cat_cone
α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› ‹ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'›
by (rule is_cat_coneI[OF τ'(1) assms(6)])
interpret τ'': is_cat_cone
α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎› ‹ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ''›
by (rule is_cat_coneI[OF τ''(1) assms(6)])
have τ'τ': "ntcf_arrow (ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ') = τ'"
by (subst (2) τ'(2)) (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)
have τ''τ'': "ntcf_arrow (ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'') = τ''"
by (subst (2) τ''(2)) (cs_concl cs_shallow cs_simp: cat_FUNCT_cs_simps)
from prems(3) τ'(1) τ''(1) assms have
"L_10_5_υ α 𝔗 𝔎 c τ' a = L_10_5_υ α 𝔗 𝔎 c τ'' a"
by (subst (asm) τ'(2), use nothing in ‹subst (asm) τ''(2)›)
(
cs_prems cs_shallow
cs_simp: τ'τ' τ''τ'' cat_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_lim_cs_intros cat_Kan_cs_intros cat_cs_intros
)
from this have υτ'a_υτ''a:
"L_10_5_υ α 𝔗 𝔎 c τ' a⦇NTMap⦈⦇b⦈⦇ArrVal⦈⦇f⦈ =
L_10_5_υ α 𝔗 𝔎 c τ'' a⦇NTMap⦈⦇b⦈⦇ArrVal⦈⦇f⦈"
if "b ∈⇩∘ 𝔅⦇Obj⦈" and "f : c ↦⇘ℭ⇙ (𝔎⦇ObjMap⦈⦇b⦈)" for b f
by simp
have [cat_cs_simps]: "τ'⦇NTMap⦈⦇0, b, f⦈⇩∙ = τ''⦇NTMap⦈⦇0, b, f⦈⇩∙"
if "b ∈⇩∘ 𝔅⦇Obj⦈" and "f : c ↦⇘ℭ⇙ (𝔎⦇ObjMap⦈⦇b⦈)" for b f
using υτ'a_υτ''a[OF that] that
by
(
cs_prems cs_shallow
cs_simp: cat_Kan_cs_simps L_10_5_υ_arrow_ArrVal_app
cs_intro: cat_cs_intros
)
have
"ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ' =
ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ''"
proof(rule ntcf_eqI)
show "ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ' :
cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a ↦⇩C⇩F 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by (rule τ'.is_ntcf_axioms)
then have dom_lhs:
"𝒟⇩∘ (ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'⦇NTMap⦈) = c ↓⇩C⇩F 𝔎⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'' :
cf_const (c ↓⇩C⇩F 𝔎) 𝔄 a ↦⇩C⇩F 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by (rule τ''.is_ntcf_axioms)
then have dom_rhs:
"𝒟⇩∘ (ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ''⦇NTMap⦈) = c ↓⇩C⇩F 𝔎⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show
"ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'⦇NTMap⦈ =
ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ''⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix A assume "A ∈⇩∘ c ↓⇩C⇩F 𝔎⦇Obj⦈"
with assms(5) obtain b f
where A_def: "A = [0, b, f]⇩∘"
and b: "b ∈⇩∘ 𝔅⦇Obj⦈"
and f: "f : c ↦⇘ℭ⇙ 𝔎⦇ObjMap⦈⦇b⦈"
by auto
from b f show
"ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ'⦇NTMap⦈⦇A⦈ =
ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 τ''⦇NTMap⦈⦇A⦈"
unfolding A_def
by (cs_concl cs_simp: cat_cs_simps cat_map_extra_cs_simps)
qed (cs_concl cs_shallow cs_intro: V_cs_intros)+
qed simp_all
then show "τ' = τ''"
proof(rule inj_onD[OF bij_betw_imp_inj_on[OF bij_betw_ntcf_of_ntcf_arrow]])
show "τ' ∈⇩∘ ntcf_arrows α (c ↓⇩C⇩F 𝔎) 𝔄"
by (subst τ'(2))
(
cs_concl cs_intro:
cat_lim_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
show "τ'' ∈⇩∘ ntcf_arrows α (c ↓⇩C⇩F 𝔎) 𝔄"
by (subst τ''(2))
(
cs_concl cs_intro:
cat_lim_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
qed
qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
qed auto
qed
lemma L_10_5_χ'_arrow_is_iso_arr'[cat_Kan_cs_intros]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
and "A = cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
and "B = L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
and "ℭ' = cat_Set β"
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a : A ↦⇩i⇩s⇩o⇘ℭ'⇙ B"
using assms(1-6)
unfolding assms(7-9)
by (rule L_10_5_χ'_arrow_is_iso_arr)
lemma L_10_5_χ'_arrow_is_arr:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a :
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙
L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
by
(
rule cat_Set_is_iso_arrD(1)[
OF L_10_5_χ'_arrow_is_iso_arr[OF assms(1-6)]
]
)
lemma L_10_5_χ'_arrow_is_arr'[cat_Kan_cs_intros]:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔄⦇Obj⦈"
and "A = cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)⦇ObjMap⦈⦇a⦈"
and "B = L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
and "ℭ' = cat_Set β"
shows "L_10_5_χ'_arrow α β 𝔗 𝔎 c a : A ↦⇘ℭ'⇙ B"
using assms(1-6) unfolding assms(7-9) by (rule L_10_5_χ'_arrow_is_arr)
subsection‹Lemma X.5: ‹L_10_5_χ›\label{sec:lem_X_5_end}›
subsubsection‹Definition and elementary properties›
definition L_10_5_χ :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "L_10_5_χ α β 𝔗 𝔎 c =
[
(λa∈⇩∘𝔗⦇HomCod⦈⦇Obj⦈. L_10_5_χ'_arrow α β 𝔗 𝔎 c a),
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎),
L_10_5_N α β 𝔗 𝔎 c,
op_cat (𝔗⦇HomCod⦈),
cat_Set β
]⇩∘"
text‹Components.›
lemma L_10_5_χ_components:
shows "L_10_5_χ α β 𝔗 𝔎 c⦇NTMap⦈ =
(λa∈⇩∘𝔗⦇HomCod⦈⦇Obj⦈. L_10_5_χ'_arrow α β 𝔗 𝔎 c a)"
and [cat_Kan_cs_simps]:
"L_10_5_χ α β 𝔗 𝔎 c⦇NTDom⦈ = cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎)"
and [cat_Kan_cs_simps]:
"L_10_5_χ α β 𝔗 𝔎 c⦇NTCod⦈ = L_10_5_N α β 𝔗 𝔎 c"
and "L_10_5_χ α β 𝔗 𝔎 c⦇NTDGDom⦈ = op_cat (𝔗⦇HomCod⦈)"
and [cat_Kan_cs_simps]: "L_10_5_χ α β 𝔗 𝔎 c⦇NTDGCod⦈ = cat_Set β"
unfolding L_10_5_χ_def nt_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔄 𝔅 𝔗
assumes 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
lemmas L_10_5_χ_components' =
L_10_5_χ_components[where 𝔗=𝔗, unfolded cat_cs_simps]
lemmas [cat_Kan_cs_simps] = L_10_5_χ_components'(4)
end
subsubsection‹Natural transformation map›
mk_VLambda L_10_5_χ_components(1)
|vsv L_10_5_χ_NTMap_vsv[cat_Kan_cs_intros]|
context
fixes α 𝔄 𝔅 𝔗
assumes 𝔗: "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation is_functor α 𝔅 𝔄 𝔗 by (rule 𝔗)
mk_VLambda L_10_5_χ_components(1)[where 𝔗=𝔗, unfolded cat_cs_simps]
|vdomain L_10_5_χ_NTMap_vdomain[cat_Kan_cs_simps]|
|app L_10_5_χ_NTMap_app[cat_Kan_cs_simps]|
end
subsubsection‹‹L_10_5_χ› is a natural isomorphism›
lemma L_10_5_χ_is_iso_ntcf:
assumes "𝒵 β"
and "α ∈⇩∘ β"
and "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
shows "L_10_5_χ α β 𝔗 𝔎 c :
cf_Cone α β (𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎) ↦⇩C⇩F⇩.⇩i⇩s⇩o L_10_5_N α β 𝔗 𝔎 c :
op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
(is ‹?L_10_5_χ : ?cf_Cone ↦⇩C⇩F⇩.⇩i⇩s⇩o ?L_10_5_N : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β›)
proof-
let ?FUNCT = ‹λ𝔄. cat_FUNCT α 𝔄 (cat_Set α)›
let ?c𝔎_𝔄 = ‹cat_FUNCT α (c ↓⇩C⇩F 𝔎) 𝔄›
let ?ntcf_c𝔎_𝔄 = ‹ntcf_const (c ↓⇩C⇩F 𝔎) 𝔄›
let ?𝔗_c𝔎 = ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎›
let ?H_ℭ = ‹λc. Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-)›
let ?H_𝔄 = ‹λa. Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-)›
let ?L_10_5_χ'_arrow = ‹L_10_5_χ'_arrow α β 𝔗 𝔎 c›
let ?cf_c𝔎_𝔄 = ‹cf_const (c ↓⇩C⇩F 𝔎) 𝔄›
let ?L_10_5_υ = ‹L_10_5_υ α 𝔗 𝔎 c›
let ?L_10_5_υ_arrow = ‹L_10_5_υ_arrow 𝔗 𝔎 c›
interpret β: 𝒵 β by (rule assms(1))
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(3))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(4))
from 𝔎.vempty_is_zet assms(5) interpret c𝔎: category α ‹c ↓⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from assms(1,2,5) interpret c𝔎_𝔄: category β ?c𝔎_𝔄
by
(
cs_concl cs_intro:
cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
interpret β_c𝔎_𝔄: category β ?c𝔎_𝔄
by (cs_concl cs_shallow cs_intro: cat_cs_intros assms(2))+
from assms(2,5) interpret Δ: is_functor β 𝔄 ?c𝔎_𝔄 ‹Δ⇩C⇩F α (c ↓⇩C⇩F 𝔎) 𝔄›
by (cs_concl cs_intro: cat_cs_intros cat_op_intros)+
from 𝔎.vempty_is_zet assms(5) interpret Πc:
is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by
(
cs_concl cs_shallow
cs_simp: cat_comma_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
interpret βΠc: is_tiny_functor β ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by (rule Πc.cf_is_tiny_functor_if_ge_Limit[OF assms(1,2)])
interpret E: is_functor β ‹?FUNCT ℭ ×⇩C ℭ› ‹cat_Set β› ‹cf_eval α β ℭ›
by (rule 𝔎.HomCod.cat_cf_eval_is_functor[OF assms(1,2)])
from assms(2) interpret FUNCT_𝔄: tiny_category β ‹?FUNCT 𝔄›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from assms(2) interpret FUNCT_𝔅: tiny_category β ‹?FUNCT 𝔅›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from assms(2) interpret FUNCT_ℭ: tiny_category β ‹?FUNCT ℭ›
by (cs_concl cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
interpret β𝔄: tiny_category β 𝔄
by (rule category.cat_tiny_category_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔅: tiny_category β 𝔅
by (rule category.cat_tiny_category_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret βℭ: tiny_category β ℭ
by (rule category.cat_tiny_category_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔎: is_tiny_functor β 𝔅 ℭ 𝔎
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔗: is_tiny_functor β 𝔅 𝔄 𝔗
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use assms(2) in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret cat_Set_αβ: subcategory β ‹cat_Set α› ‹cat_Set β›
by (rule 𝔎.subcategory_cat_Set_cat_Set[OF assms(1,2)])
show ?thesis
proof(intro is_iso_ntcfI is_ntcfI', unfold cat_op_simps)
show "vfsequence (?L_10_5_χ)" unfolding L_10_5_χ_def by auto
show "vcard (?L_10_5_χ) = 5⇩ℕ"
unfolding L_10_5_χ_def by (simp add: nat_omega_simps)
from assms(2) show "?cf_Cone : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (intro is_functor.tm_cf_cf_Cone_is_functor_if_ge_Limit)
(cs_concl cs_intro: cat_cs_intros)+
from assms show "?L_10_5_N : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
show "?L_10_5_χ⦇NTMap⦈⦇a⦈ :
?cf_Cone⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set β⇙ ?L_10_5_N⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using assms(2,3,4,5) that
by
(
cs_concl
cs_simp: L_10_5_χ_NTMap_app
cs_intro: cat_cs_intros L_10_5_χ'_arrow_is_iso_arr
)
from cat_Set_is_iso_arrD[OF this] show
"?L_10_5_χ⦇NTMap⦈⦇a⦈ : ?cf_Cone⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ ?L_10_5_N⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using that by auto
have [cat_cs_simps]:
"?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙
cf_hom ?c𝔎_𝔄 [ntcf_arrow (?ntcf_c𝔎_𝔄 f), ntcf_arrow (ntcf_id ?𝔗_c𝔎)]⇩∘ =
cf_hom (?FUNCT 𝔅)
[
ntcf_arrow (ntcf_id (?H_ℭ c ∘⇩C⇩F 𝔎)),
ntcf_arrow (Hom⇩A⇩.⇩C⇘α⇙𝔄(f,-) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗)
]⇩∘ ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a"
(
is
"?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs =
?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a"
)
if "f : b ↦⇘𝔄⇙ a" for a b f
proof-
let ?H_f = ‹Hom⇩A⇩.⇩C⇘α⇙𝔄(f,-)›
from that assms c𝔎_𝔄.category_axioms c𝔎_𝔄.category_axioms have lhs:
"?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs :
Hom ?c𝔎_𝔄 (cf_map (?cf_c𝔎_𝔄 a)) (cf_map ?𝔗_c𝔎) ↦⇘cat_Set β⇙
?L_10_5_N⦇ObjMap⦈⦇b⦈"
by
(
cs_concl
cs_simp:
cat_Kan_cs_simps
cat_cs_simps
cat_FUNCT_cs_simps
cat_FUNCT_components(1)
cat_op_simps
cs_intro:
cat_Kan_cs_intros
cat_FUNCT_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
)
then have dom_lhs:
"𝒟⇩∘ ((?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈) =
Hom ?c𝔎_𝔄 (cf_map (?cf_c𝔎_𝔄 a)) (cf_map ?𝔗_c𝔎)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from that assms c𝔎_𝔄.category_axioms c𝔎_𝔄.category_axioms have rhs:
"?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a :
Hom ?c𝔎_𝔄 (cf_map (?cf_c𝔎_𝔄 a)) (cf_map ?𝔗_c𝔎) ↦⇘cat_Set β⇙
?L_10_5_N⦇ObjMap⦈⦇b⦈"
by
(
cs_concl
cs_simp:
cat_Kan_cs_simps
cat_cs_simps
cat_FUNCT_components(1)
cat_op_simps
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
then have dom_rhs:
"𝒟⇩∘ ((?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a)⦇ArrVal⦈) =
Hom ?c𝔎_𝔄 (cf_map (?cf_c𝔎_𝔄 a)) (cf_map ?𝔗_c𝔎)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from lhs show arr_Set_lhs:
"arr_Set β (?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)"
by (auto dest: cat_Set_is_arrD(1))
from rhs show arr_Set_rhs:
"arr_Set β (?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a)"
by (auto dest: cat_Set_is_arrD(1))
show
"(?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈ =
(?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a)⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix F assume prems: "F : cf_map (?cf_c𝔎_𝔄 a) ↦⇘?c𝔎_𝔄⇙ cf_map ?𝔗_c𝔎"
let ?F = ‹ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 F›
from that have [cat_cs_simps]:
"cf_of_cf_map (c ↓⇩C⇩F 𝔎) 𝔄 (cf_map (?cf_c𝔎_𝔄 a)) = ?cf_c𝔎_𝔄 a"
"cf_of_cf_map (c ↓⇩C⇩F 𝔎) 𝔄 (cf_map (?𝔗_c𝔎)) = ?𝔗_c𝔎"
by (cs_concl cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros)
note F = cat_FUNCT_is_arrD[OF prems, unfolded cat_cs_simps]
from that F(1) have F_const_is_cat_cone:
"?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f : b <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ?𝔗_c𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: is_cat_coneI cat_cs_intros
)
have [cat_cs_simps]:
"?L_10_5_υ (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b =
?H_f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?L_10_5_υ (ntcf_arrow ?F) a"
proof(rule ntcf_eqI)
from assms that F(1) show
"?L_10_5_υ (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b :
?H_ℭ c ∘⇩C⇩F 𝔎 ↦⇩C⇩F ?H_𝔄 b ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_intro:
cat_Kan_cs_intros cat_cs_intros is_cat_coneI
)
then have dom_υ:
"𝒟⇩∘ (?L_10_5_υ (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b⦇NTMap⦈) =
𝔅⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms that F(1) show
"?H_f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?L_10_5_υ (ntcf_arrow ?F) a :
?H_ℭ c ∘⇩C⇩F 𝔎 ↦⇩C⇩F ?H_𝔄 b ∘⇩C⇩F 𝔗 : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_intro:
cat_Kan_cs_intros cat_cs_intros is_cat_coneI
)
then have dom_f𝔗υ:
"𝒟⇩∘ ((?H_f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?L_10_5_υ (ntcf_arrow ?F) a)⦇NTMap⦈) =
𝔅⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps)
show
"?L_10_5_υ (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b⦇NTMap⦈ =
(?H_f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?L_10_5_υ (ntcf_arrow ?F) a)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_υ dom_f𝔗υ)
fix b' assume prems': "b' ∈⇩∘ 𝔅⦇Obj⦈"
let ?Y = ‹Yoneda_component (?H_𝔄 b) a f (𝔗⦇ObjMap⦈⦇b'⦈)›
let ?𝔎b' = ‹𝔎⦇ObjMap⦈⦇b'⦈›
let ?𝔗b' = ‹𝔗⦇ObjMap⦈⦇b'⦈›
have [cat_cs_simps]:
"?L_10_5_υ_arrow (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b b' =
?Y ∘⇩A⇘cat_Set α⇙ ?L_10_5_υ_arrow (ntcf_arrow ?F) a b'"
(is ‹?υ_Ffbb' = ?Yυ›)
proof-
from assms prems' F_const_is_cat_cone have υ_Ffbb':
"?υ_Ffbb' : Hom ℭ c ?𝔎b' ↦⇘cat_Set α⇙ Hom 𝔄 b ?𝔗b'"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros L_10_5_υ_arrow_is_arr
)
then have dom_υ_Ffbb': "𝒟⇩∘ (?υ_Ffbb'⦇ArrVal⦈) = Hom ℭ c (?𝔎b')"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms that 𝔗.HomCod.category_axioms prems' F(1) have Yυ:
"?Yυ : Hom ℭ c ?𝔎b' ↦⇘cat_Set α⇙ Hom 𝔄 b ?𝔗b'"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_cs_simps cat_op_simps
cs_intro: is_cat_coneI cat_Kan_cs_intros cat_cs_intros
)
then have dom_Yυ: "𝒟⇩∘ (?Yυ⦇ArrVal⦈) = Hom ℭ c (?𝔎b')"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from υ_Ffbb' show arr_Set_υ_Ffbb': "arr_Set α ?υ_Ffbb'"
by (auto dest: cat_Set_is_arrD(1))
from Yυ show arr_Set_Yυ: "arr_Set α ?Yυ"
by (auto dest: cat_Set_is_arrD(1))
show "?υ_Ffbb'⦇ArrVal⦈ = ?Yυ⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_υ_Ffbb' dom_Yυ in_Hom_iff)
fix g assume "g : c ↦⇘ℭ⇙ ?𝔎b'"
with
assms(2-)
𝔎.is_functor_axioms
𝔗.is_functor_axioms
𝔗.HomCod.category_axioms
𝔎.HomCod.category_axioms
that prems' F(1)
show "?υ_Ffbb'⦇ArrVal⦈⦇g⦈ = ?Yυ⦇ArrVal⦈⦇g⦈"
by
(
cs_concl
cs_simp:
cat_Kan_cs_simps
cat_cs_simps
L_10_5_υ_arrow_ArrVal_app
cat_comma_cs_simps
cat_op_simps
cs_intro:
cat_Kan_cs_intros
is_cat_coneI
cat_cs_intros
cat_comma_cs_intros
cat_op_intros
cs_simp: cat_FUNCT_cs_simps
)
qed (use arr_Set_υ_Ffbb' arr_Set_Yυ in auto)
qed
(
use υ_Ffbb' Yυ in
‹cs_concl cs_shallow cs_simp: cat_cs_simps›
)+
qed
from assms prems' that F(1) show
"?L_10_5_υ (ntcf_arrow (?F ∙⇩N⇩T⇩C⇩F ?ntcf_c𝔎_𝔄 f)) b⦇NTMap⦈⦇b'⦈ =
(?H_f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?L_10_5_υ (ntcf_arrow ?F) a)⦇NTMap⦈⦇b'⦈"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_cs_simps
cs_intro: is_cat_coneI cat_Kan_cs_intros cat_cs_intros
)
qed (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)+
qed simp_all
from that F(1) interpret F: is_cat_cone α a ‹c ↓⇩C⇩F 𝔎› 𝔄 ‹?𝔗_c𝔎› ?F
by (cs_concl cs_shallow cs_intro: is_cat_coneI cat_cs_intros)
from
assms(2-) prems F(1) that
𝔗.HomCod.cat_ntcf_Hom_snd_is_ntcf[OF that]
c𝔎_𝔄.category_axioms
show
"(?L_10_5_χ'_arrow b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈⦇F⦈ =
(?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ'_arrow a)⦇ArrVal⦈⦇F⦈"
by (subst (1 2) F(2))
(
cs_concl
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
cat_FUNCT_cs_simps
cat_FUNCT_components(1)
cat_op_simps
cs_intro:
is_cat_coneI
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
qed (use arr_Set_lhs arr_Set_rhs in auto)
qed (use lhs rhs in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
show
"?L_10_5_χ⦇NTMap⦈⦇b⦈ ∘⇩A⇘cat_Set β⇙ ?cf_Cone⦇ArrMap⦈⦇f⦈ =
?L_10_5_N⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set β⇙ ?L_10_5_χ⦇NTMap⦈⦇a⦈"
if "f : b ↦⇘𝔄⇙ a" for a b f
using that assms
by
(
cs_concl
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
cat_FUNCT_components(1)
cat_FUNCT_cs_simps
cat_op_simps
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
qed
(
cs_concl
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
)+
qed
subsection‹
The existence of a canonical limit or a canonical colimit for the
pointwise Kan extensions
›
lemma (in is_cat_pw_rKe) cat_pw_rKe_ex_cat_limit:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
obtains UA
where "UA : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
proof-
define β where "β = α + ω"
have β: "𝒵 β" and αβ: "α ∈⇩∘ β"
by (simp_all add: β_def AG.𝒵_Limit_αω AG.𝒵_ω_αω 𝒵_def AG.𝒵_α_αω)
then interpret β: 𝒵 β by simp
let ?FUNCT = ‹λ𝔄. cat_FUNCT α 𝔄 (cat_Set α)›
let ?H_A = ‹λf. Hom⇩A⇩.⇩C⇘α⇙𝔄(f,-)›
let ?H_A𝔊 = ‹λf. ?H_A f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊›
let ?H_𝔄 = ‹λa. Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-)›
let ?H_𝔄𝔗 = ‹λa. ?H_𝔄 a ∘⇩C⇩F 𝔗›
let ?H_𝔄𝔊 = ‹λa. ?H_𝔄 a ∘⇩C⇩F 𝔊›
let ?H_ℭ = ‹λc. Hom⇩O⇩.⇩C⇘α⇙ℭ(c,-)›
let ?H_ℭ𝔎 = ‹λc. ?H_ℭ c ∘⇩C⇩F 𝔎›
let ?H_𝔄ε = ‹λb. ?H_𝔄 b ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ε›
let ?SET_𝔎 = ‹exp_cat_cf α (cat_Set α) 𝔎›
let ?H_FUNCT = ‹λℭ 𝔉. Hom⇩O⇩.⇩C⇘β⇙?FUNCT ℭ(-,cf_map 𝔉)›
let ?ua_NTDGDom = ‹op_cat (?FUNCT ℭ)›
let ?ua_NTDom = ‹λa. ?H_FUNCT ℭ (?H_𝔄𝔊 a)›
let ?ua_NTCod = ‹λa. ?H_FUNCT 𝔅 (?H_𝔄𝔗 a) ∘⇩C⇩F op_cf ?SET_𝔎›
let ?c𝔎_𝔄 = ‹cat_FUNCT α (c ↓⇩C⇩F 𝔎) 𝔄›
let ?ua =
‹
λa. ntcf_ua_fo
β
?SET_𝔎
(cf_map (?H_𝔄𝔗 a))
(cf_map (?H_𝔄𝔊 a))
(ntcf_arrow (?H_𝔄ε a))
›
let ?cf_nt = ‹cf_nt α β (cf_id ℭ)›
let ?cf_eval = ‹cf_eval α β ℭ›
let ?𝔗_c𝔎 = ‹𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎›
let ?cf_c𝔎_𝔄 = ‹cf_const (c ↓⇩C⇩F 𝔎) 𝔄›
let ?𝔊c = ‹𝔊⦇ObjMap⦈⦇c⦈›
let ?Δ = ‹Δ⇩C⇩F α (c ↓⇩C⇩F 𝔎) 𝔄›
let ?ntcf_ua_fo =
‹
λa. ntcf_ua_fo
β
?SET_𝔎
(cf_map (?H_𝔄𝔗 a))
(cf_map (?H_𝔄𝔊 a))
(ntcf_arrow (?H_𝔄ε a))
›
let ?umap_fo =
‹
λb. umap_fo
?SET_𝔎
(cf_map (?H_𝔄𝔗 b))
(cf_map (?H_𝔄𝔊 b))
(ntcf_arrow (?H_𝔄ε b))
(cf_map (?H_ℭ c))
›
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
from AG.vempty_is_zet assms(3) interpret c𝔎: category α ‹c ↓⇩C⇩F 𝔎›
by (cs_concl cs_shallow cs_intro: cat_comma_cs_intros)
from αβ assms(3) interpret c𝔎_𝔄: category β ?c𝔎_𝔄
by
(
cs_concl cs_intro:
cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
from αβ assms(3) interpret Δ: is_functor β 𝔄 ?c𝔎_𝔄 ?Δ
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)+
from AG.vempty_is_zet assms(3) interpret Πc:
is_functor α ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by
(
cs_concl cs_shallow
cs_simp: cat_comma_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
interpret βΠc: is_tiny_functor β ‹c ↓⇩C⇩F 𝔎› 𝔅 ‹c ⇩O⨅⇩C⇩F 𝔎›
by (rule Πc.cf_is_tiny_functor_if_ge_Limit[OF β αβ])
interpret E: is_functor β ‹?FUNCT ℭ ×⇩C ℭ› ‹cat_Set β› ?cf_eval
by (rule AG.HomCod.cat_cf_eval_is_functor[OF β αβ])
from αβ interpret FUNCT_𝔄: tiny_category β ‹?FUNCT 𝔄›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from αβ interpret FUNCT_𝔅: tiny_category β ‹?FUNCT 𝔅›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
from αβ interpret FUNCT_ℭ: tiny_category β ‹?FUNCT ℭ›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_FUNCT_cs_intros)
interpret β𝔄: tiny_category β 𝔄
by (rule category.cat_tiny_category_if_ge_Limit)
(use αβ in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔅: tiny_category β 𝔅
by (rule category.cat_tiny_category_if_ge_Limit)
(use αβ in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret βℭ: tiny_category β ℭ
by (rule category.cat_tiny_category_if_ge_Limit)
(use αβ in ‹cs_concl cs_intro: cat_cs_intros›)+
interpret β𝔎: is_tiny_functor β 𝔅 ℭ 𝔎
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use αβ in ‹cs_concl cs_shallow cs_intro: cat_cs_intros›)+
interpret β𝔊: is_tiny_functor β ℭ 𝔄 𝔊
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use αβ in ‹cs_concl cs_shallow cs_intro: cat_cs_intros›)+
interpret β𝔗: is_tiny_functor β 𝔅 𝔄 𝔗
by (rule is_functor.cf_is_tiny_functor_if_ge_Limit)
(use αβ in ‹cs_concl cs_shallow cs_intro: cat_cs_intros›)+
interpret cat_Set_αβ: subcategory β ‹cat_Set α› ‹cat_Set β›
by (rule AG.subcategory_cat_Set_cat_Set[OF β αβ])
from assms(3) αβ interpret Hom_c: is_functor α ℭ ‹cat_Set α› ‹?H_ℭ c›
by (cs_concl cs_intro: cat_cs_intros)
define E' :: V where "E' =
[
(λa∈⇩∘𝔄⦇Obj⦈. ?cf_eval⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙),
(λf∈⇩∘𝔄⦇Arr⦈. ?cf_eval⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙),
op_cat 𝔄,
cat_Set β
]⇩∘ "
have E'_components:
"E'⦇ObjMap⦈ = (λa∈⇩∘𝔄⦇Obj⦈. ?cf_eval⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙)"
"E'⦇ArrMap⦈ =
(λf∈⇩∘𝔄⦇Arr⦈. ?cf_eval⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙)"
"E'⦇HomDom⦈ = op_cat 𝔄"
"E'⦇HomCod⦈ = cat_Set β"
unfolding E'_def dghm_field_simps by (simp_all add: nat_omega_simps)
note [cat_cs_simps] = E'_components(3,4)
have E'_ObjMap_app[cat_cs_simps]:
"E'⦇ObjMap⦈⦇a⦈ = ?cf_eval⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using that unfolding E'_components by simp
have E'_ArrMap_app[cat_cs_simps]:
"E'⦇ArrMap⦈⦇f⦈ = ?cf_eval⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙"
if "f ∈⇩∘ 𝔄⦇Arr⦈" for f
using that unfolding E'_components by simp
have E': "E' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
proof(intro is_functorI')
show "vfsequence E'" unfolding E'_def by auto
show "vcard E' = 4⇩ℕ" unfolding E'_def by (simp add: nat_omega_simps)
show "vsv (E'⦇ObjMap⦈)" unfolding E'_components by simp
show "vsv (E'⦇ArrMap⦈)" unfolding E'_components by simp
show "𝒟⇩∘ (E'⦇ObjMap⦈) = op_cat 𝔄⦇Obj⦈"
unfolding E'_components by (simp add: cat_op_simps)
show "ℛ⇩∘ (E'⦇ObjMap⦈) ⊆⇩∘ cat_Set β⦇Obj⦈"
unfolding E'_components
proof(rule vrange_VLambda_vsubset)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
then have "?H_𝔄𝔊 a : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
with assms(3) prems show
"?cf_eval⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙ ∈⇩∘ cat_Set β⦇Obj⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Set_components(1)
cs_intro: cat_cs_intros cat_op_intros Ran.HomCod.cat_Hom_in_Vset
)
qed
show "𝒟⇩∘ (E'⦇ArrMap⦈) = op_cat 𝔄⦇Arr⦈"
unfolding E'_components by (simp add: cat_op_simps)
show "E'⦇ArrMap⦈⦇f⦈ : E'⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ E'⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘op_cat 𝔄⇙ b" for a b f
proof-
from that[unfolded cat_op_simps] assms(3) show ?thesis
by (intro cat_Set_αβ.subcat_is_arrD)
(
cs_concl
cs_simp:
category.cf_eval_ObjMap_app
category.cf_eval_ArrMap_app
E'_ObjMap_app
E'_ArrMap_app
cs_intro: cat_cs_intros
)
qed
then have [cat_cs_intros]: "E'⦇ArrMap⦈⦇f⦈ : A ↦⇘cat_Set β⇙ B"
if "A = E'⦇ObjMap⦈⦇a⦈" and "B = E'⦇ObjMap⦈⦇b⦈" and "f : b ↦⇘𝔄⇙ a"
for a b f A B
using that by (simp add: cat_op_simps)
show
"E'⦇ArrMap⦈⦇g ∘⇩A⇘op_cat 𝔄⇙ f⦈ = E'⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set β⇙ E'⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘op_cat 𝔄⇙ c" and "f : a ↦⇘op_cat 𝔄⇙ b" for b c g a f
proof-
note g = that(1)[unfolded cat_op_simps]
and f = that(2)[unfolded cat_op_simps]
from g f assms(3) αβ show ?thesis
by
(
cs_concl
cs_intro:
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
cs_simp:
cat_cs_simps
cat_FUNCT_cs_simps
cat_prod_cs_simps
cat_op_simps
E.cf_ArrMap_Comp[symmetric]
)+
qed
show "E'⦇ArrMap⦈⦇op_cat 𝔄⦇CId⦈⦇a⦈⦈ = cat_Set β⦇CId⦈⦇E'⦇ObjMap⦈⦇a⦈⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
proof(cs_concl_step cat_Set_αβ.subcat_CId[symmetric])
from that[unfolded cat_op_simps] assms(3) show
"E'⦇ObjMap⦈⦇a⦈ ∈⇩∘ cat_Set α⦇Obj⦈"
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros
)
from that[unfolded cat_op_simps] assms(3) show
"E'⦇ArrMap⦈⦇op_cat 𝔄⦇CId⦈⦇a⦈⦈ = cat_Set α⦇CId⦈⦇E'⦇ObjMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_intro: cat_cs_intros
cs_simp:
cat_Set_components(1)
cat_cs_simps
cat_op_simps
ntcf_id_cf_comp[symmetric]
)
qed
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
then interpret E': is_functor β ‹op_cat 𝔄› ‹cat_Set β› E' by simp
define N' :: V where "N' =
[
(λa∈⇩∘𝔄⦇Obj⦈. ?cf_nt⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙),
(λf∈⇩∘𝔄⦇Arr⦈. ?cf_nt⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙),
op_cat 𝔄,
cat_Set β
]⇩∘ "
have N'_components:
"N'⦇ObjMap⦈ = (λa∈⇩∘𝔄⦇Obj⦈. ?cf_nt⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙)"
"N'⦇ArrMap⦈ =
(λf∈⇩∘𝔄⦇Arr⦈. ?cf_nt⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙)"
"N'⦇HomDom⦈ = op_cat 𝔄"
"N'⦇HomCod⦈ = cat_Set β"
unfolding N'_def dghm_field_simps by (simp_all add: nat_omega_simps)
note [cat_cs_simps] = N'_components(3,4)
have N'_ObjMap_app[cat_cs_simps]:
"N'⦇ObjMap⦈⦇a⦈ = ?cf_nt⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using that unfolding N'_components by simp
have N'_ArrMap_app[cat_cs_simps]:
"N'⦇ArrMap⦈⦇f⦈ = ?cf_nt⦇ArrMap⦈⦇ntcf_arrow (?H_A𝔊 f), ℭ⦇CId⦈⦇c⦈⦈⇩∙"
if "f ∈⇩∘ 𝔄⦇Arr⦈" for f
using that unfolding N'_components by simp
from αβ interpret cf_nt_ℭ: is_functor β ‹?FUNCT ℭ ×⇩C ℭ› ‹cat_Set β› ‹?cf_nt›
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have N': "N' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
proof(intro is_functorI')
show "vfsequence N'" unfolding N'_def by simp
show "vcard N' = 4⇩ℕ" unfolding N'_def by (simp add: nat_omega_simps)
show "vsv (N'⦇ObjMap⦈)" unfolding N'_components by simp
show "vsv (N'⦇ArrMap⦈)" unfolding N'_components by simp
show "𝒟⇩∘ (N'⦇ObjMap⦈) = op_cat 𝔄⦇Obj⦈"
unfolding N'_components by (simp add: cat_op_simps)
show "ℛ⇩∘ (N'⦇ObjMap⦈) ⊆⇩∘ cat_Set β⦇Obj⦈"
unfolding N'_components
proof(rule vrange_VLambda_vsubset)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
with assms(3) αβ show
"?cf_nt⦇ObjMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙ ∈⇩∘ cat_Set β⦇Obj⦈"
by
(
cs_concl
cs_simp: cat_Set_components(1) cat_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_cs_intros FUNCT_ℭ.cat_Hom_in_Vset cat_FUNCT_cs_intros
)
qed
show "𝒟⇩∘ (N'⦇ArrMap⦈) = op_cat 𝔄⦇Arr⦈"
unfolding N'_components by (simp add: cat_op_simps)
show "N'⦇ArrMap⦈⦇f⦈ : N'⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ N'⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘op_cat 𝔄⇙ b" for a b f
using that[unfolded cat_op_simps] assms(3)
by
(
cs_concl
cs_simp: N'_ObjMap_app N'_ArrMap_app
cs_intro: cat_cs_intros cat_prod_cs_intros cat_FUNCT_cs_intros
)
show
"N'⦇ArrMap⦈⦇g ∘⇩A⇘op_cat 𝔄⇙ f⦈ = N'⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set β⇙ N'⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘op_cat 𝔄⇙ c" and "f : a ↦⇘op_cat 𝔄⇙ b" for b c g a f
proof-
from that assms(3) αβ show ?thesis
unfolding cat_op_simps
by
(
cs_concl
cs_intro:
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
cs_simp:
cat_cs_simps
cat_FUNCT_cs_simps
cat_prod_cs_simps
cat_op_simps
cf_nt_ℭ.cf_ArrMap_Comp[symmetric]
)
qed
show "N'⦇ArrMap⦈⦇op_cat 𝔄⦇CId⦈⦇a⦈⦈ = cat_Set β⦇CId⦈⦇N'⦇ObjMap⦈⦇a⦈⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
proof-
note [cat_cs_simps] =
ntcf_id_cf_comp[symmetric]
ntcf_arrow_id_ntcf_id[symmetric]
cat_FUNCT_CId_app[symmetric]
from that[unfolded cat_op_simps] assms(3) αβ show ?thesis
by
(
cs_concl
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
cs_simp: cat_FUNCT_cs_simps cat_cs_simps cat_op_simps
)+
qed
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
then interpret N': is_functor β ‹op_cat 𝔄› ‹cat_Set β› N' by simp
define Y' :: V where "Y' =
[
(λa∈⇩∘𝔄⦇Obj⦈. ntcf_Yoneda α β ℭ⦇NTMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙),
N',
E',
op_cat 𝔄,
cat_Set β
]⇩∘"
have Y'_components:
"Y'⦇NTMap⦈ = (λa∈⇩∘𝔄⦇Obj⦈. ntcf_Yoneda α β ℭ⦇NTMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙)"
"Y'⦇NTDom⦈ = N'"
"Y'⦇NTCod⦈ = E'"
"Y'⦇NTDGDom⦈ = op_cat 𝔄"
"Y'⦇NTDGCod⦈ = cat_Set β"
unfolding Y'_def nt_field_simps by (simp_all add: nat_omega_simps)
note [cat_cs_simps] = Y'_components(2-5)
have Y'_NTMap_app[cat_cs_simps]:
"Y'⦇NTMap⦈⦇a⦈ = ntcf_Yoneda α β ℭ⦇NTMap⦈⦇cf_map (?H_𝔄𝔊 a), c⦈⇩∙"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using that unfolding Y'_components by simp
from β αβ interpret Y:
is_iso_ntcf β ‹?FUNCT ℭ ×⇩C ℭ› ‹cat_Set β› ?cf_nt ?cf_eval ‹ntcf_Yoneda α β ℭ›
by (rule AG.HomCod.cat_ntcf_Yoneda_is_ntcf)
have Y': "Y' : N' ↦⇩C⇩F⇩.⇩i⇩s⇩o E' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence Y'" unfolding Y'_def by simp
show "vcard Y' = 5⇩ℕ"
unfolding Y'_def by (simp add: nat_omega_simps)
show "vsv (Y'⦇NTMap⦈)" unfolding Y'_components by auto
show "𝒟⇩∘ (Y'⦇NTMap⦈) = op_cat 𝔄⦇Obj⦈"
unfolding Y'_components by (simp add: cat_op_simps)
show Y'_NTMap_a: "Y'⦇NTMap⦈⦇a⦈ : N'⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set β⇙ E'⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
using that[unfolded cat_op_simps] assms(3) αβ
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
)
then show "Y'⦇NTMap⦈⦇a⦈ : N'⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ E'⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
by (intro cat_Set_is_iso_arrD[OF Y'_NTMap_a[OF that]])
show
"Y'⦇NTMap⦈⦇b⦈ ∘⇩A⇘cat_Set β⇙ N'⦇ArrMap⦈⦇f⦈ =
E'⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set β⇙ Y'⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘op_cat 𝔄⇙ b" for a b f
proof-
note f = that[unfolded cat_op_simps]
from f assms(3) show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps Y.ntcf_Comp_commute
cs_intro: cat_cs_intros cat_prod_cs_intros cat_FUNCT_cs_intros
)+
qed
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
have E'_def: "E' = Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)"
proof(rule cf_eqI)
show "E' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms(3) show
"Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c) : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have dom_lhs: "𝒟⇩∘ (E'⦇ObjMap⦈) = 𝔄⦇Obj⦈" unfolding E'_components by simp
from assms(3) have dom_rhs:
"𝒟⇩∘ (Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ObjMap⦈) = 𝔄⦇Obj⦈"
unfolding E'_components
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
show "E'⦇ObjMap⦈ = Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ObjMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume "a ∈⇩∘ 𝔄⦇Obj⦈"
with assms(3) show "E'⦇ObjMap⦈⦇a⦈ = Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ObjMap⦈⦇a⦈"
by
(
cs_concl
cs_simp: cat_op_simps cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed (auto simp: E'_components cat_cs_intros assms(3))
have dom_lhs: "𝒟⇩∘ (E'⦇ArrMap⦈) = 𝔄⦇Arr⦈" unfolding E'_components by simp
from assms(3) have dom_rhs:
"𝒟⇩∘ (Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ArrMap⦈) = 𝔄⦇Arr⦈"
unfolding E'_components
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
show "E'⦇ArrMap⦈ = Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ArrMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix f assume prems: "f ∈⇩∘ 𝔄⦇Arr⦈"
then obtain a b where f: "f : a ↦⇘𝔄⇙ b" by auto
have [cat_cs_simps]:
"cf_eval_arrow ℭ (ntcf_arrow (?H_A𝔊 f)) (ℭ⦇CId⦈⦇c⦈) =
cf_hom 𝔄 [f, 𝔄⦇CId⦈⦇?𝔊c⦈]⇩∘"
(is ‹?cf_eval_arrow = ?cf_hom_f𝔊c›)
proof-
have cf_eval_arrow_f_CId_𝔊c:
"?cf_eval_arrow :
Hom 𝔄 b ?𝔊c ↦⇘cat_Set α⇙ Hom 𝔄 a ?𝔊c"
proof(rule cf_eval_arrow_is_arr')
from f show "?H_A𝔊 f : ?H_𝔄𝔊 b ↦⇩C⇩F ?H_𝔄𝔊 a : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_intro: cat_cs_intros)
qed
(
use f assms(3) in
‹
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
›
)+
from f assms(3) have dom_lhs:
"𝒟⇩∘ (?cf_eval_arrow⦇ArrVal⦈) = Hom 𝔄 b ?𝔊c"
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
)
from assms(3) f Ran.HomCod.category_axioms have cf_hom_f𝔊c:
"?cf_hom_f𝔊c :
Hom 𝔄 b ?𝔊c ↦⇘cat_Set α⇙ Hom 𝔄 a ?𝔊c"
by
(
cs_concl cs_shallow cs_intro:
cat_cs_intros cat_prod_cs_intros cat_op_intros
)
from f assms(3) have dom_rhs:
"𝒟⇩∘ (?cf_hom_f𝔊c⦇ArrVal⦈) = Hom 𝔄 b ?𝔊c"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
)
show ?thesis
proof(rule arr_Set_eqI)
from cf_eval_arrow_f_CId_𝔊c show "arr_Set α ?cf_eval_arrow"
by (auto dest: cat_Set_is_arrD(1))
from cf_hom_f𝔊c show "arr_Set α ?cf_hom_f𝔊c"
by (auto dest: cat_Set_is_arrD(1))
show "?cf_eval_arrow⦇ArrVal⦈ = ?cf_hom_f𝔊c⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs, unfold in_Hom_iff)
from f assms(3) show "vsv (?cf_eval_arrow⦇ArrVal⦈)"
by (cs_concl cs_intro: cat_cs_intros)
from f assms(3) show "vsv (?cf_hom_f𝔊c⦇ArrVal⦈)"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
fix g assume "g : b ↦⇘𝔄⇙ ?𝔊c"
with f assms(3) show
"?cf_eval_arrow⦇ArrVal⦈⦇g⦈ = ?cf_hom_f𝔊c⦇ArrVal⦈⦇g⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed simp
qed
(
use cf_eval_arrow_f_CId_𝔊c cf_hom_f𝔊c in
‹cs_concl cs_simp: cat_cs_simps›
)+
qed
from f prems assms(3) show "E'⦇ArrMap⦈⦇f⦈ = Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)⦇ArrMap⦈⦇f⦈"
by
(
cs_concl
cs_simp: cat_op_simps cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed (auto simp: E'_components cat_cs_intros assms(3))
qed simp_all
from Y' have inv_Y': "inv_ntcf Y' :
Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c) ↦⇩C⇩F⇩.⇩i⇩s⇩o N' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
unfolding E'_def by (auto intro: iso_ntcf_is_iso_arr)
interpret N'': is_functor β ‹op_cat 𝔄› ‹cat_Set β› ‹L_10_5_N α β 𝔗 𝔎 c›
by (rule L_10_5_N_is_functor[OF β αβ assms])
define ψ :: V
where "ψ =
[
(λa∈⇩∘𝔄⦇Obj⦈. ?ntcf_ua_fo a⦇NTMap⦈⦇cf_map (?H_ℭ c)⦈),
N',
L_10_5_N α β 𝔗 𝔎 c,
op_cat 𝔄,
cat_Set β
]⇩∘"
have ψ_components:
"ψ⦇NTMap⦈ = (λa∈⇩∘𝔄⦇Obj⦈. ?ntcf_ua_fo a⦇NTMap⦈⦇cf_map (?H_ℭ c)⦈)"
"ψ⦇NTDom⦈ = N'"
"ψ⦇NTCod⦈ = L_10_5_N α β 𝔗 𝔎 c"
"ψ⦇NTDGDom⦈ = op_cat 𝔄"
"ψ⦇NTDGCod⦈ = cat_Set β"
unfolding ψ_def nt_field_simps by (simp_all add: nat_omega_simps)
note [cat_cs_simps] = Y'_components(2-5)
have ψ_NTMap_app[cat_cs_simps]:
"ψ⦇NTMap⦈⦇a⦈ = ?ntcf_ua_fo a⦇NTMap⦈⦇cf_map (?H_ℭ c)⦈"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using that unfolding ψ_components by simp
have ψ: "ψ : N' ↦⇩C⇩F⇩.⇩i⇩s⇩o L_10_5_N α β 𝔗 𝔎 c : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
proof-
show ?thesis
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence ψ" unfolding ψ_def by auto
show "vcard ψ = 5⇩ℕ" unfolding ψ_def by (simp_all add: nat_omega_simps)
show "N' : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β" by (rule N')
show "L_10_5_N α β 𝔗 𝔎 c : op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "ψ⦇NTDom⦈ = N'" unfolding ψ_components by simp
show "ψ⦇NTCod⦈ = L_10_5_N α β 𝔗 𝔎 c" unfolding ψ_components by simp
show "ψ⦇NTDGDom⦈ = op_cat 𝔄" unfolding ψ_components by simp
show "ψ⦇NTDGCod⦈ = cat_Set β" unfolding ψ_components by simp
show "vsv (ψ⦇NTMap⦈)" unfolding ψ_components by simp
show "𝒟⇩∘ (ψ⦇NTMap⦈) = op_cat 𝔄⦇Obj⦈"
unfolding ψ_components by (simp add: cat_op_simps)
show ψ_NTMap_is_iso_arr[unfolded cat_op_simps]:
"ψ⦇NTMap⦈⦇a⦈ : N'⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set β⇙ L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
proof-
note a = that[unfolded cat_op_simps]
interpret ε:
is_cat_rKe_preserves α 𝔅 ℭ 𝔄 ‹cat_Set α› 𝔎 𝔗 𝔊 ‹?H_𝔄 a› ε
by (rule cat_pw_rKe_preserved[OF a])
interpret aε:
is_cat_rKe α 𝔅 ℭ ‹cat_Set α› 𝔎 ‹?H_𝔄𝔗 a› ‹?H_𝔄𝔊 a› ‹?H_𝔄ε a›
by (rule ε.cat_rKe_preserves)
interpret is_iso_ntcf
β
‹op_cat (?FUNCT ℭ)›
‹cat_Set β›
‹?H_FUNCT ℭ (?H_𝔄𝔊 a)›
‹?H_FUNCT 𝔅 (?H_𝔄𝔗 a) ∘⇩C⇩F op_cf ?SET_𝔎›
‹?ntcf_ua_fo a›
by (rule aε.cat_rKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit[OF β αβ])
have "cf_map (?H_ℭ c) ∈⇩∘ ?FUNCT ℭ⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
from
iso_ntcf_is_iso_arr[unfolded cat_op_simps, OF this]
a assms αβ
show ?thesis
by
(
cs_prems
cs_simp:
cat_cs_simps cat_Kan_cs_simps cat_FUNCT_cs_simps cat_op_simps
cs_intro:
cat_small_cs_intros
cat_Kan_cs_intros
cat_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
qed
show ψ_NTMap_is_arr[unfolded cat_op_simps]:
"ψ⦇NTMap⦈⦇a⦈ : N'⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set β⇙ L_10_5_N α β 𝔗 𝔎 c⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ op_cat 𝔄⦇Obj⦈" for a
by
(
rule cat_Set_is_iso_arrD[
OF ψ_NTMap_is_iso_arr[OF that[unfolded cat_op_simps]]
]
)
show
"ψ⦇NTMap⦈⦇b⦈ ∘⇩A⇘cat_Set β⇙ N'⦇ArrMap⦈⦇f⦈ =
L_10_5_N α β 𝔗 𝔎 c⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set β⇙ ψ⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘op_cat 𝔄⇙ b" for a b f
proof-
note f = that[unfolded cat_op_simps]
from f have a: "a ∈⇩∘ 𝔄⦇Obj⦈" and b: "b ∈⇩∘ 𝔄⦇Obj⦈" by auto
interpret p_a_ε:
is_cat_rKe_preserves α 𝔅 ℭ 𝔄 ‹cat_Set α› 𝔎 𝔗 𝔊 ‹?H_𝔄 a› ε
by (rule cat_pw_rKe_preserved[OF a])
interpret a_ε: is_cat_rKe
α 𝔅 ℭ ‹cat_Set α› 𝔎 ‹?H_𝔄𝔗 a› ‹?H_𝔄𝔊 a› ‹?H_𝔄ε a›
by (rule p_a_ε.cat_rKe_preserves)
interpret ntcf_ua_fo_a_ε: is_iso_ntcf
β ?ua_NTDGDom ‹cat_Set β› ‹?ua_NTDom a› ‹?ua_NTCod a› ‹?ua a›
by (rule a_ε.cat_rKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit[OF β αβ])
interpret p_b_ε:
is_cat_rKe_preserves α 𝔅 ℭ 𝔄 ‹cat_Set α› 𝔎 𝔗 𝔊 ‹?H_𝔄 b› ε
by (rule cat_pw_rKe_preserved[OF b])
interpret b_ε: is_cat_rKe
α 𝔅 ℭ ‹cat_Set α› 𝔎 ‹?H_𝔄𝔗 b› ‹?H_𝔄𝔊 b› ‹?H_𝔄ε b›
by (rule p_b_ε.cat_rKe_preserves)
interpret ntcf_ua_fo_b_ε: is_iso_ntcf
β ?ua_NTDGDom ‹cat_Set β› ‹?ua_NTDom b› ‹?ua_NTCod b› ‹?ua b›
by (rule b_ε.cat_rKe_ntcf_ua_fo_is_iso_ntcf_if_ge_Limit[OF β αβ])
interpret 𝔎_SET: is_tiny_functor β ‹?FUNCT ℭ› ‹?FUNCT 𝔅› ?SET_𝔎
by
(
rule exp_cat_cf_is_tiny_functor[
OF β αβ AG.category_cat_Set AG.is_functor_axioms
]
)
from f interpret Hom_f:
is_ntcf α 𝔄 ‹cat_Set α› ‹?H_𝔄 a› ‹?H_𝔄 b› ‹?H_A f›
by (cs_concl cs_intro: cat_cs_intros)
let ?cf_hom_lhs =
‹
cf_hom
(?FUNCT ℭ)
[ntcf_arrow (ntcf_id (?H_ℭ c)), ntcf_arrow (?H_A𝔊 f)]⇩∘
›
let ?cf_hom_rhs =
‹
cf_hom
(?FUNCT 𝔅)
[
ntcf_arrow (ntcf_id (?H_ℭ c ∘⇩C⇩F 𝔎)),
ntcf_arrow (?H_A f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗)
]⇩∘
›
let ?dom =
‹Hom (?FUNCT ℭ) (cf_map (?H_ℭ c)) (cf_map (?H_𝔄𝔊 a))›
let ?cod = ‹Hom (?FUNCT 𝔅) (cf_map (?H_ℭ𝔎 c)) (cf_map (?H_𝔄𝔗 b))›
let ?cf_hom_lhs_umap_fo_inter =
‹Hom (?FUNCT ℭ) (cf_map (?H_ℭ c)) (cf_map (?H_𝔄𝔊 b))›
let ?umap_fo_cf_hom_rhs_inter =
‹Hom (?FUNCT 𝔅) (cf_map (?H_ℭ𝔎 c)) (cf_map (?H_𝔄𝔗 a))›
have [cat_cs_simps]:
"?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs =
?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a"
proof-
from f assms(3) αβ have cf_hom_lhs:
"?cf_hom_lhs : ?dom ↦⇘cat_Set β⇙ ?cf_hom_lhs_umap_fo_inter"
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from f assms(3) αβ have umap_fo_b:
"?umap_fo b : ?cf_hom_lhs_umap_fo_inter ↦⇘cat_Set β⇙ ?cod"
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from cf_hom_lhs umap_fo_b have umap_fo_cf_hom_lhs:
"?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs : ?dom ↦⇘cat_Set β⇙ ?cod"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
then have dom_umap_fo_cf_hom_lhs:
"𝒟⇩∘ ((?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈) = ?dom"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
from f assms(3) αβ have cf_hom_rhs:
"?cf_hom_rhs : ?umap_fo_cf_hom_rhs_inter ↦⇘cat_Set β⇙ ?cod"
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from f assms(3) αβ have umap_fo_a:
"?umap_fo a : ?dom ↦⇘cat_Set β⇙ ?umap_fo_cf_hom_rhs_inter"
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro:
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from cf_hom_rhs umap_fo_a have cf_hom_rhs_umap_fo_a:
"?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a : ?dom ↦⇘cat_Set β⇙ ?cod"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
then have dom_cf_hom_rhs_umap_fo_a:
"𝒟⇩∘ ((?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a)⦇ArrVal⦈) = ?dom"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
show ?thesis
proof(rule arr_Set_eqI)
from umap_fo_cf_hom_lhs show arr_Set_umap_fo_cf_hom_lhs:
"arr_Set β (?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)"
by (auto dest: cat_Set_is_arrD(1))
from cf_hom_rhs_umap_fo_a show arr_Set_cf_hom_rhs_umap_fo_a:
"arr_Set β (?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a)"
by (auto dest: cat_Set_is_arrD(1))
show
"(?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈ =
(?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a)⦇ArrVal⦈"
proof
(
rule vsv_eqI,
unfold
dom_umap_fo_cf_hom_lhs dom_cf_hom_rhs_umap_fo_a in_Hom_iff;
(rule refl)?
)
fix ℌ assume prems:
"ℌ : cf_map (?H_ℭ c) ↦⇘?FUNCT ℭ⇙ cf_map (?H_𝔄𝔊 a)"
let ?ℌ = ‹ntcf_of_ntcf_arrow ℭ (cat_Set α) ℌ›
let ?lhs = ‹?H_𝔄ε b ∙⇩N⇩T⇩C⇩F ((?H_A𝔊 f ∙⇩N⇩T⇩C⇩F ?ℌ) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎)›
let ?rhs =
‹(?H_A f ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F ?H_𝔄ε a ∙⇩N⇩T⇩C⇩F (?ℌ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎))›
let ?cf_hom_𝔄ε = ‹λb b'. cf_hom 𝔄 [𝔄⦇CId⦈⦇b⦈, ε⦇NTMap⦈⦇b'⦈]⇩∘›
let ?Yc = ‹λQ. Yoneda_component (?H_𝔄 b) a f Q›
let ?ℌ𝔎 = ‹λb'. ?ℌ⦇NTMap⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈›
let ?𝔊𝔎 = ‹λb'. 𝔊⦇ObjMap⦈⦇𝔎⦇ObjMap⦈⦇b'⦈⦈›
have [cat_cs_simps]:
"cf_of_cf_map ℭ (cat_Set α) (cf_map (?H_ℭ c)) = ?H_ℭ c"
by
(
cs_concl cs_shallow
cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
)
have [cat_cs_simps]:
"cf_of_cf_map ℭ (cat_Set α) (cf_map (?H_𝔄𝔊 a)) = ?H_𝔄𝔊 a"
by
(
cs_concl cs_shallow
cs_simp: cat_FUNCT_cs_simps cs_intro: cat_cs_intros
)
note ℌ = cat_FUNCT_is_arrD[OF prems, unfolded cat_cs_simps]
have Hom_c: "?H_ℭ𝔎 c : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have [cat_cs_simps]: "?lhs = ?rhs"
proof(rule ntcf_eqI)
from ℌ(1) f show lhs:
"?lhs : ?H_ℭ𝔎 c ↦⇩C⇩F ?H_𝔄𝔗 b : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_simp: cs_intro: cat_cs_intros)
then have dom_lhs: "𝒟⇩∘ (?lhs⦇NTMap⦈) = 𝔅⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps)+
from ℌ(1) f show rhs:
"?rhs : ?H_ℭ𝔎 c ↦⇩C⇩F ?H_𝔄𝔗 b : 𝔅 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_intro: cat_cs_intros)
then have dom_rhs: "𝒟⇩∘ (?rhs⦇NTMap⦈) = 𝔅⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps)+
have [cat_cs_simps]:
"?cf_hom_𝔄ε b b' ∘⇩A⇘cat_Set α⇙
(?Yc (?𝔊𝔎 b') ∘⇩A⇘cat_Set α⇙ ?ℌ𝔎 b') =
?Yc (𝔗⦇ObjMap⦈⦇b'⦈) ∘⇩A⇘cat_Set α⇙
(?cf_hom_𝔄ε a b' ∘⇩A⇘cat_Set α⇙ ?ℌ𝔎 b')"
(is ‹?lhs_Set = ?rhs_Set›)
if "b' ∈⇩∘ 𝔅⦇Obj⦈" for b'
proof-
let ?𝔎b' = ‹𝔎⦇ObjMap⦈⦇b'⦈›
from ℌ(1) f that assms(3) Ran.HomCod.category_axioms
have lhs_Set_is_arr: "?lhs_Set :
Hom ℭ c (?𝔎b') ↦⇘cat_Set α⇙ Hom 𝔄 b (𝔗⦇ObjMap⦈⦇b'⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_cs_intros cat_prod_cs_intros cat_op_intros
)
then have dom_lhs_Set: "𝒟⇩∘ (?lhs_Set⦇ArrVal⦈) = Hom ℭ c ?𝔎b'"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from ℌ(1) f that assms(3) Ran.HomCod.category_axioms
have rhs_Set_is_arr: "?rhs_Set :
Hom ℭ c (?𝔎b') ↦⇘cat_Set α⇙ Hom 𝔄 b (𝔗⦇ObjMap⦈⦇b'⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_cs_intros cat_prod_cs_intros cat_op_intros
)
then have dom_rhs_Set: "𝒟⇩∘ (?rhs_Set⦇ArrVal⦈) = Hom ℭ c ?𝔎b'"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI)
from lhs_Set_is_arr show arr_Set_lhs_Set: "arr_Set α ?lhs_Set"
by (auto dest: cat_Set_is_arrD(1))
from rhs_Set_is_arr show arr_Set_rhs_Set: "arr_Set α ?rhs_Set"
by (auto dest: cat_Set_is_arrD(1))
show "?lhs_Set⦇ArrVal⦈ = ?rhs_Set⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs_Set dom_rhs_Set in_Hom_iff)
fix h assume "h : c ↦⇘ℭ⇙ ?𝔎b'"
with ℌ(1) f that assms Ran.HomCod.category_axioms show
"?lhs_Set⦇ArrVal⦈⦇h⦈ = ?rhs_Set⦇ArrVal⦈⦇h⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_cs_intros cat_prod_cs_intros cat_op_intros
)
qed (use arr_Set_lhs_Set arr_Set_rhs_Set in auto)
qed
(
use lhs_Set_is_arr rhs_Set_is_arr in
‹cs_concl cs_shallow cs_simp: cat_cs_simps›
)+
qed
show "?lhs⦇NTMap⦈ = ?rhs⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix b' assume "b' ∈⇩∘ 𝔅⦇Obj⦈"
with ℌ(1) f assms(3) show "?lhs⦇NTMap⦈⦇b'⦈ = ?rhs⦇NTMap⦈⦇b'⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros
)
qed (cs_concl cs_intro: cat_cs_intros)
qed simp_all
from
assms(3) f ℌ(1) prems αβ
Ran.HomCod.category_axioms
FUNCT_ℭ.category_axioms
FUNCT_𝔅.category_axioms
AG.is_functor_axioms
Ran.is_functor_axioms
Hom_f.is_ntcf_axioms
show
"(?umap_fo b ∘⇩A⇘cat_Set β⇙ ?cf_hom_lhs)⦇ArrVal⦈⦇ℌ⦈ =
(?cf_hom_rhs ∘⇩A⇘cat_Set β⇙ ?umap_fo a)⦇ArrVal⦈⦇ℌ⦈"
by (subst (1 2) ℌ(2))
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps cat_op_simps
cs_intro:
cat_cs_intros
cat_prod_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
qed
(
use arr_Set_umap_fo_cf_hom_lhs arr_Set_cf_hom_rhs_umap_fo_a in
auto
)
qed
(
use umap_fo_cf_hom_lhs cf_hom_rhs_umap_fo_a in
‹cs_concl cs_shallow cs_simp: cat_cs_simps›
)+
qed
from f assms αβ show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
qed
qed auto
qed
from L_10_5_χ_is_iso_ntcf[OF β αβ assms] have inv_χ:
"inv_ntcf (L_10_5_χ α β 𝔗 𝔎 c) :
L_10_5_N α β 𝔗 𝔎 c ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_Cone α β ?𝔗_c𝔎 :
op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
by (auto intro: iso_ntcf_is_iso_arr)
define φ where "φ = inv_ntcf (L_10_5_χ α β 𝔗 𝔎 c) ∙⇩N⇩T⇩C⇩F ψ ∙⇩N⇩T⇩C⇩F inv_ntcf Y'"
from inv_Y' ψ inv_χ have φ: "φ :
Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c) ↦⇩C⇩F⇩.⇩i⇩s⇩o cf_Cone α β ?𝔗_c𝔎 :
op_cat 𝔄 ↦↦⇩C⇘β⇙ cat_Set β"
unfolding φ_def by (cs_concl cs_shallow cs_intro: cat_cs_intros)
interpret φ: is_iso_ntcf
β ‹op_cat 𝔄› ‹cat_Set β› ‹Hom⇩O⇩.⇩C⇘β⇙𝔄(-,?𝔊c)› ‹cf_Cone α β ?𝔗_c𝔎› φ
by (rule φ)
let ?φ_𝔊c_CId = ‹φ⦇NTMap⦈⦇?𝔊c⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇?𝔊c⦈⦈›
let ?ntcf_φ_𝔊c_CId = ‹ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 ?φ_𝔊c_CId›
from AG.vempty_is_zet assms(3) have Δ: "?Δ : 𝔄 ↦↦⇩C⇘β⇙ ?c𝔎_𝔄"
by
(
cs_concl cs_shallow
cs_simp: cat_comma_cs_simps
cs_intro: cat_cs_intros cat_comma_cs_intros
)
from assms(3) have 𝔊c: "?𝔊c ∈⇩∘ 𝔄⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from AG.vempty_is_zet have 𝔗_c𝔎: "cf_map (?𝔗_c𝔎) ∈⇩∘ ?c𝔎_𝔄⦇Obj⦈"
by
(
cs_concl
cs_simp: cat_FUNCT_components(1)
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
from
φ.ntcf_NTMap_is_arr[unfolded cat_op_simps, OF 𝔊c]
assms(3)
AG.vempty_is_zet
β.vempty_is_zet
αβ
have φ_𝔊c: "φ⦇NTMap⦈⦇?𝔊c⦈ :
Hom 𝔄 ?𝔊c?𝔊c ↦⇘cat_Set β⇙
Hom ?c𝔎_𝔄 (cf_map (?cf_c𝔎_𝔄 ?𝔊c)) (cf_map ?𝔗_c𝔎)"
by
(
cs_prems
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
cat_comma_cs_simps
cat_op_simps
cat_FUNCT_components(1)
cs_intro:
cat_Kan_cs_intros
cat_comma_cs_intros
cat_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
)
with assms(3) have φ_𝔊c_CId:
"?φ_𝔊c_CId : cf_map (?cf_c𝔎_𝔄 ?𝔊c) ↦⇘?c𝔎_𝔄⇙ cf_map ?𝔗_c𝔎"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
have ntcf_arrow_φ_𝔊c_CId: "ntcf_arrow ?ntcf_φ_𝔊c_CId = ?φ_𝔊c_CId"
by (rule cat_FUNCT_is_arrD(2)[OF φ_𝔊c_CId, symmetric])
have ua: "universal_arrow_fo ?Δ (cf_map (?𝔗_c𝔎)) ?𝔊c ?φ_𝔊c_CId"
by
(
rule is_functor.cf_universal_arrow_fo_if_is_iso_ntcf[
OF Δ 𝔊c 𝔗_c𝔎 φ[unfolded cf_Cone_def cat_cs_simps]
]
)
moreover have ntcf_φ_𝔊c_CId:
"?ntcf_φ_𝔊c_CId : ?𝔊c <⇩C⇩F⇩.⇩c⇩o⇩n⇩e ?𝔗_c𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
proof(intro is_cat_coneI)
from cat_FUNCT_is_arrD(1)[OF φ_𝔊c_CId] assms(3) AG.vempty_is_zet show
"ntcf_of_ntcf_arrow (c ↓⇩C⇩F 𝔎) 𝔄 ?φ_𝔊c_CId :
?cf_c𝔎_𝔄 ?𝔊c ↦⇩C⇩F ?𝔗_c𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by
(
cs_prems
cs_simp: cat_cs_simps cat_FUNCT_cs_simps
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
qed (rule 𝔊c)
ultimately have "?ntcf_φ_𝔊c_CId : ?𝔊c <⇩C⇩F⇩.⇩l⇩i⇩m ?𝔗_c𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by (intro is_cat_cone.cat_cone_is_cat_limit)
(simp_all add: ntcf_arrow_φ_𝔊c_CId)
then show ?thesis using that by auto
qed
lemma (in is_cat_pw_lKe) cat_pw_lKe_ex_cat_colimit:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ"
and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
and "c ∈⇩∘ ℭ⦇Obj⦈"
obtains UA
where "UA : 𝔗 ∘⇩C⇩F 𝔎 ⇩C⇩F⨅⇩O c >⇩C⇩F⇩.⇩c⇩o⇩l⇩i⇩m 𝔉⦇ObjMap⦈⦇c⦈ : 𝔎 ⇩C⇩F↓ c ↦↦⇩C⇘α⇙ 𝔄"
proof-
from
is_cat_pw_rKe.cat_pw_rKe_ex_cat_limit
[
OF is_cat_pw_rKe_op AG.is_functor_op ntcf_lKe.NTDom.is_functor_op,
unfolded cat_op_simps,
OF assms(3)
]
obtain UA where UA: "UA :
𝔉⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩l⇩i⇩m op_cf 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F (op_cf 𝔎) :
c ↓⇩C⇩F (op_cf 𝔎) ↦↦⇩C⇘α⇙ op_cat 𝔄"
by auto
from assms(3) have [cat_cs_simps]:
"op_cf 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F (op_cf 𝔎) ∘⇩C⇩F op_cf_obj_comma 𝔎 c =
op_cf 𝔗 ∘⇩C⇩F op_cf (𝔎 ⇩C⇩F⨅⇩O c)"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps AG.op_cf_cf_obj_comma_proj[OF assms(3)]
cs_intro: cat_cs_intros cat_comma_cs_intros cat_op_intros
)
from assms(3) have [cat_op_simps]:
"𝔗 ∘⇩C⇩F op_cf (c ⇩O⨅⇩C⇩F (op_cf 𝔎)) ∘⇩C⇩F op_cf (op_cf_obj_comma 𝔎 c) =
𝔗 ∘⇩C⇩F 𝔎 ⇩C⇩F⨅⇩O c"
by
(
cs_concl cs_shallow
cs_simp:
cat_cs_simps cat_op_simps
op_cf_cf_comp[symmetric] AG.op_cf_cf_obj_comma_proj[symmetric]
cs_intro: cat_cs_intros cat_comma_cs_intros cat_op_intros
)
from assms(3) have [cat_op_simps]: "op_cat (op_cat (𝔎 ⇩C⇩F↓ c)) = 𝔎 ⇩C⇩F↓ c"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_comma_cs_intros
)
note ntcf_cf_comp_is_cat_limit_if_is_iso_functor =
ntcf_cf_comp_is_cat_limit_if_is_iso_functor
[
OF UA AG.op_cf_obj_comma_is_iso_functor[OF assms(3)],
unfolded cat_op_simps
]
have "op_ntcf UA ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F op_cf (op_cf_obj_comma 𝔎 c) :
𝔗 ∘⇩C⇩F 𝔎 ⇩C⇩F⨅⇩O c >⇩C⇩F⇩.⇩c⇩o⇩l⇩i⇩m 𝔉⦇ObjMap⦈⦇c⦈ : 𝔎 ⇩C⇩F↓ c ↦↦⇩C⇘α⇙ 𝔄"
by
(
rule is_cat_limit.is_cat_colimit_op
[
OF ntcf_cf_comp_is_cat_limit_if_is_iso_functor,
unfolded cat_op_simps
]
)
then show ?thesis using that by auto
qed
subsection‹The limit and the colimit for the pointwise Kan extensions›
subsubsection‹Definition and elementary properties›
text‹See Theorem 3 in Chapter X-5 in \<^cite>‹"mac_lane_categories_2010"›.›
definition the_pw_cat_rKe_limit :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊 c =
[
𝔊⦇ObjMap⦈⦇c⦈,
(
SOME UA.
UA : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔗⦇HomCod⦈
)
]⇩∘"
definition the_pw_cat_lKe_colimit :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c =
[
𝔉⦇ObjMap⦈⦇c⦈,
op_ntcf
(
the_pw_cat_rKe_limit α (op_cf 𝔎) (op_cf 𝔗) (op_cf 𝔉) c⦇UArr⦈ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
op_cf_obj_comma 𝔎 c
)
]⇩∘"
text‹Components.›
lemma the_pw_cat_rKe_limit_components:
shows "the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊 c⦇UObj⦈ = 𝔊⦇ObjMap⦈⦇c⦈"
and "the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊 c⦇UArr⦈ =
(
SOME UA.
UA : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔗⦇HomCod⦈
)"
unfolding the_pw_cat_rKe_limit_def ua_field_simps
by (simp_all add: nat_omega_simps)
lemma the_pw_cat_lKe_colimit_components:
shows "the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c⦇UObj⦈ = 𝔉⦇ObjMap⦈⦇c⦈"
and "the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c⦇UArr⦈ = op_ntcf
(
the_pw_cat_rKe_limit α (op_cf 𝔎) (op_cf 𝔗) (op_cf 𝔉) c⦇UArr⦈ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
op_cf_obj_comma 𝔎 c
)"
unfolding the_pw_cat_lKe_colimit_def ua_field_simps
by (simp_all add: nat_omega_simps)
context is_functor
begin
lemmas the_pw_cat_rKe_limit_components' =
the_pw_cat_rKe_limit_components[where 𝔗=𝔉, unfolded cat_cs_simps]
end
subsubsection‹
The limit for the pointwise right Kan extension is a limit,
the colimit for the pointwise left Kan extension is a colimit
›
lemma (in is_cat_pw_rKe) cat_pw_rKe_the_pw_cat_rKe_limit_is_cat_limit:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄" and "c ∈⇩∘ ℭ⦇Obj⦈"
shows "the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊 c⦇UArr⦈ :
the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊 c⦇UObj⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 :
c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
proof-
from cat_pw_rKe_ex_cat_limit[OF assms] obtain UA
where UA: "UA : 𝔊⦇ObjMap⦈⦇c⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F 𝔎 : c ↓⇩C⇩F 𝔎 ↦↦⇩C⇘α⇙ 𝔄"
by auto
show ?thesis
unfolding the_pw_cat_rKe_limit_components
by (rule someI2, unfold cat_cs_simps, rule UA)
qed
lemma (in is_cat_pw_lKe) cat_pw_lKe_the_pw_cat_lKe_colimit_is_cat_colimit:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄" and "c ∈⇩∘ ℭ⦇Obj⦈"
shows "the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c⦇UArr⦈ :
𝔗 ∘⇩C⇩F 𝔎 ⇩C⇩F⨅⇩O c >⇩C⇩F⇩.⇩c⇩o⇩l⇩i⇩m the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c⦇UObj⦈ :
𝔎 ⇩C⇩F↓ c ↦↦⇩C⇘α⇙ 𝔄"
proof-
interpret 𝔎: is_functor α 𝔅 ℭ 𝔎 by (rule assms(1))
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
note cat_pw_rKe_the_pw_cat_rKe_limit_is_cat_limit =
is_cat_pw_rKe.cat_pw_rKe_the_pw_cat_rKe_limit_is_cat_limit
[
OF is_cat_pw_rKe_op AG.is_functor_op ntcf_lKe.NTDom.is_functor_op,
unfolded cat_op_simps,
OF assms(3)
]
from assms(3) have
"op_cf 𝔗 ∘⇩C⇩F c ⇩O⨅⇩C⇩F (op_cf 𝔎) ∘⇩C⇩F op_cf_obj_comma 𝔎 c =
op_cf 𝔗 ∘⇩C⇩F op_cf (𝔎 ⇩C⇩F⨅⇩O c)"
by
(
cs_concl cs_shallow
cs_simp:
cat_cs_simps cat_comma_cs_simps cat_op_simps
AG.op_cf_cf_obj_comma_proj[OF assms(3)]
cs_intro: cat_cs_intros cat_comma_cs_intros cat_op_intros
)
note ntcf_cf_comp_is_cat_limit_if_is_iso_functor =
ntcf_cf_comp_is_cat_limit_if_is_iso_functor
[
OF
cat_pw_rKe_the_pw_cat_rKe_limit_is_cat_limit
AG.op_cf_obj_comma_is_iso_functor[OF assms(3)],
unfolded this, folded op_cf_cf_comp
]
from assms(3) have [cat_op_simps]: "op_cat (op_cat (𝔎 ⇩C⇩F↓ c)) = 𝔎 ⇩C⇩F↓ c"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_comma_cs_intros
)
from assms(3) have [cat_op_simps]: "op_cf (op_cf (𝔎 ⇩C⇩F⨅⇩O c)) = 𝔎 ⇩C⇩F⨅⇩O c"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_comma_cs_intros
)
have [cat_op_simps]:
"the_pw_cat_rKe_limit α (op_cf 𝔎) (op_cf 𝔗) (op_cf 𝔉) c⦇UObj⦈ =
the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉 c⦇UObj⦈"
unfolding
the_pw_cat_lKe_colimit_components
the_pw_cat_rKe_limit_components
cat_op_simps
by simp
show ?thesis
by
(
rule is_cat_limit.is_cat_colimit_op
[
OF ntcf_cf_comp_is_cat_limit_if_is_iso_functor,
folded the_pw_cat_lKe_colimit_components,
unfolded cat_op_simps
]
)
qed
lemma (in is_cat_pw_rKe) cat_pw_rKe_the_ntcf_rKe_is_cat_rKe:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
shows "the_ntcf_rKe α 𝔗 𝔎 (the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊) :
the_cf_rKe α 𝔗 𝔎 (the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊) ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 :
𝔅 ↦⇩C ℭ ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
show "the_ntcf_rKe α 𝔗 𝔎 (the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊) :
the_cf_rKe α 𝔗 𝔎 (the_pw_cat_rKe_limit α 𝔎 𝔗 𝔊) ∘⇩C⇩F 𝔎 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 :
𝔅 ↦⇩C ℭ ↦⇩C 𝔄"
by
(
rule
the_ntcf_rKe_is_cat_rKe
[
OF
assms(1)
ntcf_rKe.NTCod.is_functor_axioms
cat_pw_rKe_the_pw_cat_rKe_limit_is_cat_limit[OF assms]
]
)
qed
lemma (in is_cat_pw_lKe) cat_pw_lKe_the_ntcf_lKe_is_cat_lKe:
assumes "𝔎 : 𝔅 ↦↦⇩C⇘α⇙ ℭ" and "𝔗 : 𝔅 ↦↦⇩C⇘α⇙ 𝔄"
shows "the_ntcf_lKe α 𝔗 𝔎 (the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉) :
𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇘α⇙ the_cf_lKe α 𝔗 𝔎 (the_pw_cat_lKe_colimit α 𝔎 𝔗 𝔉) ∘⇩C⇩F 𝔎 :
𝔅 ↦⇩C ℭ ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α 𝔅 𝔄 𝔗 by (rule assms(2))
show ?thesis
by
(
rule the_ntcf_lKe_is_cat_lKe
[
OF
assms(1,2)
cat_pw_lKe_the_pw_cat_lKe_colimit_is_cat_colimit[OF assms],
simplified
]
)
qed
text‹\newpage›
end