Theory CZH_UCAT_PWKan_Example
section‹Pointwise Kan extensions: application example›
theory CZH_UCAT_PWKan_Example
imports
CZH_Elementary_Categories.CZH_ECAT_Ordinal
CZH_UCAT_PWKan
begin
subsection‹Background›
text‹
The application example presented in this section is based on
Exercise 6.1.ii in \<^cite>‹"riehl_category_2016"›. The primary purpose
of this section is the instantiation of the locales associated
with the pointwise Kan extensions.
›
lemma cat_ordinal_2_is_arrE:
assumes "f : a ↦⇘cat_ordinal (2⇩ℕ)⇙ b"
obtains "f = [0, 0]⇩∘" and "a = 0" and "b = 0"
| "f = [0, 1⇩ℕ]⇩∘" and "a = 0" and "b = 1⇩ℕ"
| "f = [1⇩ℕ, 1⇩ℕ]⇩∘" and "a = 1⇩ℕ" and "b = 1⇩ℕ"
using cat_ordinal_is_arrD[OF assms] unfolding two by auto
lemma cat_ordinal_3_is_arrE:
assumes "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b"
obtains "f = [0, 0]⇩∘" and " a = 0" and "b = 0"
| "f = [0, 1⇩ℕ]⇩∘" and "a = 0" and "b = 1⇩ℕ"
| "f = [0, 2⇩ℕ]⇩∘" and "a = 0" and "b = 2⇩ℕ"
| "f = [1⇩ℕ, 1⇩ℕ]⇩∘" and "a = 1⇩ℕ" and "b = 1⇩ℕ"
| "f = [1⇩ℕ, 2⇩ℕ]⇩∘" and "a = 1⇩ℕ" and "b = 2⇩ℕ"
| "f = [2⇩ℕ, 2⇩ℕ]⇩∘" and "a = 2⇩ℕ" and "b = 2⇩ℕ"
using cat_ordinal_is_arrD[OF assms] unfolding three by auto
lemma 0123: "0 ∈⇩∘ 2⇩ℕ" "1⇩ℕ ∈⇩∘ 2⇩ℕ" "0 ∈⇩∘ 3⇩ℕ" "1⇩ℕ ∈⇩∘ 3⇩ℕ" "2⇩ℕ ∈⇩∘ 3⇩ℕ" by auto
subsection‹‹𝔎23››
subsubsection‹Definition and elementary properties›
definition 𝔎23 :: V
where "𝔎23 =
[
(λa∈⇩∘cat_ordinal (2⇩ℕ)⦇Obj⦈. if a = 0 then 0 else 2⇩ℕ),
(
λf∈⇩∘cat_ordinal (2⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ [0, 0]⇩∘
| f = [0, 1⇩ℕ]⇩∘ ⇒ [0, 2⇩ℕ]⇩∘
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ [2⇩ℕ, 2⇩ℕ]⇩∘
| otherwise ⇒ 0
),
cat_ordinal (2⇩ℕ),
cat_ordinal (3⇩ℕ)
]⇩∘"
text‹Components.›
lemma 𝔎23_components:
shows "𝔎23⦇ObjMap⦈ = (λa∈⇩∘cat_ordinal (2⇩ℕ)⦇Obj⦈. if a = 0 then 0 else 2⇩ℕ)"
and "𝔎23⦇ArrMap⦈ =
(
λf∈⇩∘cat_ordinal (2⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ [0, 0]⇩∘
| f = [0, 1⇩ℕ]⇩∘ ⇒ [0, 2⇩ℕ]⇩∘
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ [2⇩ℕ, 2⇩ℕ]⇩∘
| otherwise ⇒ 0
)"
and [cat_Kan_cs_simps]: "𝔎23⦇HomDom⦈ = cat_ordinal (2⇩ℕ)"
and [cat_Kan_cs_simps]: "𝔎23⦇HomCod⦈ = cat_ordinal (3⇩ℕ)"
unfolding 𝔎23_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
mk_VLambda 𝔎23_components(1)
|vsv 𝔎23_ObjMap_vsv[cat_Kan_cs_intros]|
|vdomain 𝔎23_ObjMap_vdomain[cat_Kan_cs_simps]|
|app 𝔎23_ObjMap_app|
lemma 𝔎23_ObjMap_app_0[cat_Kan_cs_simps]:
assumes "x = 0"
shows "𝔎23⦇ObjMap⦈⦇x⦈ = 0"
by
(
cs_concl
cs_simp: 𝔎23_ObjMap_app cat_ordinal_cs_simps V_cs_simps assms
cs_intro: nat_omega_intros
)
lemma 𝔎23_ObjMap_app_1[cat_Kan_cs_simps]:
assumes "x = 1⇩ℕ"
shows "𝔎23⦇ObjMap⦈⦇x⦈ = 2⇩ℕ"
by
(
cs_concl
cs_simp:
cat_ordinal_cs_simps V_cs_simps omega_of_set 𝔎23_ObjMap_app assms
cs_intro: nat_omega_intros V_cs_intros
)
subsubsection‹Arrow map›
mk_VLambda 𝔎23_components(2)
|vsv 𝔎23_ArrMap_vsv[cat_Kan_cs_intros]|
|vdomain 𝔎23_ArrMap_vdomain[cat_Kan_cs_simps]|
|app 𝔎23_ArrMap_app|
lemma 𝔎23_ArrMap_app_00[cat_Kan_cs_simps]:
assumes "f = [0, 0]⇩∘"
shows "𝔎23⦇ArrMap⦈⦇f⦈ = [0, 0]⇩∘"
unfolding assms
by
(
cs_concl
cs_simp: 𝔎23_ArrMap_app cat_ordinal_cs_simps V_cs_simps
cs_intro: cat_ordinal_cs_intros nat_omega_intros
)
lemma 𝔎23_ArrMap_app_01[cat_Kan_cs_simps]:
assumes "f = [0, 1⇩ℕ]⇩∘"
shows "𝔎23⦇ArrMap⦈⦇f⦈ = [0, 2⇩ℕ]⇩∘"
proof-
have "[0, 1⇩ℕ]⇩∘ ∈⇩∘ ordinal_arrs (2⇩ℕ)"
by
(
cs_concl
cs_simp: omega_of_set
cs_intro: cat_ordinal_cs_intros V_cs_intros nat_omega_intros
)
then show ?thesis
unfolding assms by (simp add: 𝔎23_components cat_ordinal_components)
qed
lemma 𝔎23_ArrMap_app_11[cat_Kan_cs_simps]:
assumes "f = [1⇩ℕ, 1⇩ℕ]⇩∘"
shows "𝔎23⦇ArrMap⦈⦇f⦈ = [2⇩ℕ, 2⇩ℕ]⇩∘"
proof-
have "[1⇩ℕ, 1⇩ℕ]⇩∘ ∈⇩∘ ordinal_arrs (2⇩ℕ)"
by
(
cs_concl cs_shallow
cs_simp: omega_of_set
cs_intro: cat_ordinal_cs_intros V_cs_intros nat_omega_intros
)
then show ?thesis
unfolding assms by (simp add: 𝔎23_components cat_ordinal_components)
qed
subsubsection‹‹𝔎23› is a tiny functor›
lemma (in 𝒵) 𝔎23_is_functor: "𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_ordinal (3⇩ℕ)"
proof-
from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
show ?thesis
proof(intro is_tiny_functorI' is_functorI')
show "vfsequence 𝔎23" unfolding 𝔎23_def by auto
show "vcard 𝔎23 = 4⇩ℕ" unfolding 𝔎23_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (𝔎23⦇ObjMap⦈) ⊆⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈"
proof
(
rule vsv.vsv_vrange_vsubset,
unfold cat_Kan_cs_simps cat_ordinal_cs_simps,
intro cat_Kan_cs_intros
)
fix x assume "x ∈⇩∘ 2⇩ℕ"
then consider ‹x = 0› | ‹x = 1⇩ℕ› unfolding two by auto
then show "𝔎23⦇ObjMap⦈⦇x⦈ ∈⇩∘ 3⇩ℕ"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp: cat_Kan_cs_simps omega_of_set cs_intro: nat_omega_intros
)+
qed
show "𝔎23⦇ArrMap⦈⦇f⦈ : 𝔎23⦇ObjMap⦈⦇a⦈ ↦⇘cat_ordinal (3⇩ℕ)⇙ 𝔎23⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘cat_ordinal (2⇩ℕ)⇙ b" for a b f
using that
by (elim cat_ordinal_2_is_arrE; simp only:)
(
cs_concl
cs_simp: omega_of_set cat_Kan_cs_simps
cs_intro: nat_omega_intros V_cs_intros cat_ordinal_cs_intros
)
show
"𝔎23⦇ArrMap⦈⦇g ∘⇩A⇘cat_ordinal (2⇩ℕ)⇙ f⦈ =
𝔎23⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_ordinal (3⇩ℕ)⇙ 𝔎23⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘cat_ordinal (2⇩ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (2⇩ℕ)⇙ b"
for b c g a f
proof-
have "0 ∈⇩∘ 3⇩ℕ" "1⇩ℕ ∈⇩∘ 3⇩ℕ" "2⇩ℕ ∈⇩∘ 3⇩ℕ" by auto
then show ?thesis
using that
by (elim cat_ordinal_2_is_arrE; simp only:)
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_Kan_cs_simps
cs_intro: V_cs_intros cat_ordinal_cs_intros
)+
qed
show
"𝔎23⦇ArrMap⦈⦇cat_ordinal (2⇩ℕ)⦇CId⦈⦇c⦈⦈ =
cat_ordinal (3⇩ℕ)⦇CId⦈⦇𝔎23⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ cat_ordinal (2⇩ℕ)⦇Obj⦈" for c
proof-
from that consider ‹c = 0› | ‹c = 1⇩ℕ›
unfolding cat_ordinal_components(1) two by auto
then show ?thesis
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp: omega_of_set cat_Kan_cs_simps cat_ordinal_cs_simps
cs_intro: nat_omega_intros cat_ordinal_cs_intros
)
qed
qed (auto intro!: cat_cs_intros simp: 𝔎23_components)
qed
lemma (in 𝒵) 𝔎23_is_functor'[cat_Kan_cs_intros]:
assumes "𝔄' = cat_ordinal (2⇩ℕ)"
and "𝔅' = cat_ordinal (3⇩ℕ)"
shows "𝔎23 : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (rule 𝔎23_is_functor)
lemmas [cat_Kan_cs_intros] = 𝒵.𝔎23_is_functor'
lemma (in 𝒵) 𝔎23_is_tiny_functor:
"𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ cat_ordinal (3⇩ℕ)"
proof-
from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
show ?thesis
by (intro is_tiny_functorI' 𝔎23_is_functor)
(auto intro!: cat_small_cs_intros)
qed
lemma (in 𝒵) 𝔎23_is_tiny_functor'[cat_Kan_cs_intros]:
assumes "𝔄' = cat_ordinal (2⇩ℕ)"
and "𝔅' = cat_ordinal (3⇩ℕ)"
shows "𝔎23 : 𝔄' ↦↦⇩C⇩.⇩t⇩i⇩n⇩y⇘α⇙ 𝔅'"
unfolding assms by (rule 𝔎23_is_tiny_functor)
lemmas [cat_Kan_cs_intros] = 𝒵.𝔎23_is_tiny_functor'
subsection‹
‹LK23›: the functor associated with the left Kan extension along \<^const>‹𝔎23›
›
subsubsection‹Definition and elementary properties›
definition LK23 :: "V ⇒ V"
where "LK23 𝔉 =
[
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 2⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
),
(
λf∈⇩∘cat_ordinal (3⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [1⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [2⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
),
cat_ordinal (3⇩ℕ),
𝔉⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma LK23_components:
shows "LK23 𝔉⦇ObjMap⦈ =
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 2⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
)"
and "LK23 𝔉⦇ArrMap⦈ =
(
λf∈⇩∘cat_ordinal (3⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [1⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [2⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
)"
and "LK23 𝔉⦇HomDom⦈ = cat_ordinal (3⇩ℕ)"
and "LK23 𝔉⦇HomCod⦈ = 𝔉⦇HomCod⦈"
unfolding LK23_def dghm_field_simps by (simp_all add: nat_omega_simps)
context is_functor
begin
lemmas LK23_components' = LK23_components[where 𝔉=𝔉, unfolded cat_cs_simps]
lemmas [cat_Kan_cs_simps] = LK23_components'(3,4)
end
lemmas [cat_Kan_cs_simps] = is_functor.LK23_components'(3,4)
subsubsection‹Object map›
mk_VLambda LK23_components(1)
|vsv LK23_ObjMap_vsv[cat_Kan_cs_intros]|
|vdomain LK23_ObjMap_vdomain[cat_Kan_cs_simps]|
|app LK23_ObjMap_app|
lemma LK23_ObjMap_app_0[cat_Kan_cs_simps]:
assumes "a = 0"
shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
unfolding LK23_components assms cat_ordinal_components by simp
lemma LK23_ObjMap_app_1[cat_Kan_cs_simps]:
assumes "a = 1⇩ℕ"
shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
unfolding LK23_components assms cat_ordinal_components by simp
lemma LK23_ObjMap_app_2[cat_Kan_cs_simps]:
assumes "a = 2⇩ℕ"
shows "LK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈"
unfolding LK23_components assms cat_ordinal_components by simp
subsubsection‹Arrow map›
mk_VLambda LK23_components(2)
|vsv LK23_ArrMap_vsv[cat_Kan_cs_intros]|
|vdomain LK23_ArrMap_vdomain[cat_Kan_cs_simps]|
|app LK23_ArrMap_app|
lemma LK23_ArrMap_app_00[cat_Kan_cs_simps]:
assumes "f = [0, 0]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by auto
qed
lemma LK23_ArrMap_app_01[cat_Kan_cs_simps]:
assumes "f = [0, 1⇩ℕ]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by auto
qed
lemma LK23_ArrMap_app_02[cat_Kan_cs_simps]:
assumes "f = [0, 2⇩ℕ]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by auto
qed
lemma LK23_ArrMap_app_11[cat_Kan_cs_simps]:
assumes "f = [1⇩ℕ, 1⇩ℕ]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by auto
qed
lemma LK23_ArrMap_app_12[cat_Kan_cs_simps]:
assumes "f = [1⇩ℕ, 2⇩ℕ]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl
cs_simp: omega_of_set
cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by auto
qed
lemma LK23_ArrMap_app_22[cat_Kan_cs_simps]:
assumes "f = [2⇩ℕ, 2⇩ℕ]⇩∘"
shows "LK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding LK23_components assms by simp
qed
subsubsection‹‹LK23› is a functor›
lemma cat_LK23_is_functor:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
shows "LK23 𝔉 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
proof-
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms(1))
from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms)
show ?thesis
proof(intro is_functorI')
show "vfsequence (LK23 𝔉)" unfolding LK23_def by auto
show "vcard (LK23 𝔉) = 4⇩ℕ" unfolding LK23_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (LK23 𝔉⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cat_Kan_cs_simps)
fix x assume prems: "x ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈"
then consider ‹x = 0› | ‹x = 1⇩ℕ› | ‹x = 2⇩ℕ›
unfolding cat_ordinal_cs_simps three by auto
then show "LK23 𝔉⦇ObjMap⦈⦇x⦈ ∈⇩∘ ℭ⦇Obj⦈"
by cases
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_ordinal_cs_simps omega_of_set
cs_intro: cat_cs_intros nat_omega_intros
)+
qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
show "LK23 𝔉⦇ArrMap⦈⦇f⦈ : LK23 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ LK23 𝔉⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b" for a b f
proof-
from 0123 that show ?thesis
by (elim cat_ordinal_3_is_arrE; simp only:)
(
cs_concl
cs_simp: cat_Kan_cs_simps
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
qed
show
"LK23 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘cat_ordinal (3⇩ℕ)⇙ f⦈ =
LK23 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ LK23 𝔉⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘cat_ordinal (3⇩ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b"
for b c g a f
proof-
from 0123 that show ?thesis
by (elim cat_ordinal_3_is_arrE; simp only:; (solves‹simp›)?)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
𝔉.cf_ArrMap_Comp[symmetric]
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
qed
show "LK23 𝔉⦇ArrMap⦈⦇cat_ordinal (3⇩ℕ)⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇LK23 𝔉⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈" for c
proof-
from that consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ›
unfolding cat_ordinal_components three by auto
moreover have "0 ∈⇩∘ 2⇩ℕ" "1⇩ℕ ∈⇩∘ 2⇩ℕ" "0 ∈⇩∘ 3⇩ℕ" "1⇩ℕ ∈⇩∘ 3⇩ℕ" "2⇩ℕ ∈⇩∘ 3⇩ℕ" by auto
ultimately show ?thesis
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
is_functor.cf_ObjMap_CId[symmetric]
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
qed
qed
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
)+
qed
lemma cat_LK23_is_functor'[cat_Kan_cs_intros]:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
and "𝔄' = cat_ordinal (3⇩ℕ)"
shows "LK23 𝔉 : 𝔄' ↦↦⇩C⇘α⇙ ℭ"
using assms(1) unfolding assms(2) by (rule cat_LK23_is_functor)
subsubsection‹The fundamental property of ‹LK23››
lemma cf_comp_LK23_𝔎23[cat_Kan_cs_simps]:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
shows "LK23 𝔉 ∘⇩C⇩F 𝔎23 = 𝔉"
proof-
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms(1))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret LK23: is_functor α ‹cat_ordinal (3⇩ℕ)› ℭ ‹LK23 𝔉›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
show ?thesis
proof(rule cf_eqI)
show "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ" by (rule assms)
have ObjMap_dom_lhs: "𝒟⇩∘ ((LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈) = 2⇩ℕ"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_ordinal_cs_simps cs_intro: cat_cs_intros
)
have ObjMap_dom_rhs: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 2⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
show "(LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
fix a assume prems: "a ∈⇩∘ 2⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› by force
then show "(LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
omega_of_set cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)+
qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+
have ArrMap_dom_lhs: "𝒟⇩∘ ((LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈) = cat_ordinal (2⇩ℕ)⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have ArrMap_dom_rhs: "𝒟⇩∘ (𝔉⦇ArrMap⦈) = cat_ordinal (2⇩ℕ)⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "(LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
fix f assume prems: "f ∈⇩∘ cat_ordinal (2⇩ℕ)⦇Arr⦈"
then obtain a b where "f : a ↦⇘cat_ordinal (2⇩ℕ)⇙ b" by auto
then show "(LK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
by (elim cat_ordinal_2_is_arrE; simp only:)
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
)+
qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros)+
qed (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
qed
subsection‹
‹RK23›: the functor associated with the right Kan extension along \<^const>‹𝔎23›
›
subsubsection‹Definition and elementary properties›
definition RK23 :: "V ⇒ V"
where "RK23 𝔉 =
[
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| a = 2⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
),
(
λf∈⇩∘cat_ordinal (3⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [0, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| f = [2⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
),
cat_ordinal (3⇩ℕ),
𝔉⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma RK23_components:
shows "RK23 𝔉⦇ObjMap⦈ =
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ 𝔉⦇ObjMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| a = 2⇩ℕ ⇒ 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Obj⦈
)"
and "RK23 𝔉⦇ArrMap⦈ =
(
λf∈⇩∘cat_ordinal (3⇩ℕ)⦇Arr⦈.
if f = [0, 0]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙
| f = [0, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [0, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 1⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| f = [1⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| f = [2⇩ℕ, 2⇩ℕ]⇩∘ ⇒ 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙
| otherwise ⇒ 𝔉⦇HomCod⦈⦇Arr⦈
)"
and "RK23 𝔉⦇HomDom⦈ = cat_ordinal (3⇩ℕ)"
and "RK23 𝔉⦇HomCod⦈ = 𝔉⦇HomCod⦈"
unfolding RK23_def dghm_field_simps by (simp_all add: nat_omega_simps)
context is_functor
begin
lemmas RK23_components' = RK23_components[where 𝔉=𝔉, unfolded cat_cs_simps]
lemmas [cat_Kan_cs_simps] = RK23_components'(3,4)
end
lemmas [cat_Kan_cs_simps] = is_functor.RK23_components'(3,4)
subsubsection‹Object map›
mk_VLambda RK23_components(1)
|vsv RK23_ObjMap_vsv[cat_Kan_cs_intros]|
|vdomain RK23_ObjMap_vdomain[cat_Kan_cs_simps]|
|app RK23_ObjMap_app|
lemma RK23_ObjMap_app_0[cat_Kan_cs_simps]:
assumes "a = 0"
shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇0⦈"
unfolding RK23_components assms cat_ordinal_components by simp
lemma RK23_ObjMap_app_1[cat_Kan_cs_simps]:
assumes "a = 1⇩ℕ"
shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈"
unfolding RK23_components assms cat_ordinal_components by simp
lemma RK23_ObjMap_app_2[cat_Kan_cs_simps]:
assumes "a = 2⇩ℕ"
shows "RK23 𝔉⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇1⇩ℕ⦈"
unfolding RK23_components assms cat_ordinal_components by simp
subsubsection‹Arrow map›
mk_VLambda RK23_components(2)
|vsv RK23_ArrMap_vsv[cat_Kan_cs_intros]|
|vdomain RK23_ArrMap_vdomain[cat_Kan_cs_simps]|
|app RK23_ArrMap_app|
lemma RK23_ArrMap_app_00[cat_Kan_cs_simps]:
assumes "f = [0, 0]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 0⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow cs_intro:
V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by auto
qed
lemma RK23_ArrMap_app_01[cat_Kan_cs_simps]:
assumes "f = [0, 1⇩ℕ]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow cs_intro:
V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by auto
qed
lemma RK23_ArrMap_app_02[cat_Kan_cs_simps]:
assumes "f = [0, 2⇩ℕ]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow cs_intro:
V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by auto
qed
lemma RK23_ArrMap_app_11[cat_Kan_cs_simps]:
assumes "f = [1⇩ℕ, 1⇩ℕ]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow cs_intro:
V_cs_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by auto
qed
lemma RK23_ArrMap_app_12[cat_Kan_cs_simps]:
assumes "f = [1⇩ℕ, 2⇩ℕ]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl
cs_simp: omega_of_set
cs_intro: nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by auto
qed
lemma RK23_ArrMap_app_22[cat_Kan_cs_simps]:
assumes "f = [2⇩ℕ, 2⇩ℕ]⇩∘"
shows "RK23 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙"
proof-
from 0123 have f: "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow cs_intro:
nat_omega_intros cat_ordinal_cs_intros cat_cs_intros assms
)
then show ?thesis unfolding RK23_components assms by simp
qed
subsubsection‹‹RK23› is a functor›
lemma cat_RK23_is_functor:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
shows "RK23 𝔉 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
proof-
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms(1))
from ord_of_nat_ω interpret cat_ordinal_2: finite_category α ‹cat_ordinal (2⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms)
show ?thesis
proof(intro is_functorI')
show "vfsequence (RK23 𝔉)" unfolding RK23_def by auto
show "vcard (RK23 𝔉) = 4⇩ℕ" unfolding RK23_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (RK23 𝔉⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cat_Kan_cs_simps)
fix x assume prems: "x ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈"
then consider ‹x = 0› | ‹x = 1⇩ℕ› | ‹x = 2⇩ℕ›
unfolding cat_ordinal_cs_simps three by auto
then show "RK23 𝔉⦇ObjMap⦈⦇x⦈ ∈⇩∘ ℭ⦇Obj⦈"
by cases
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_ordinal_cs_simps omega_of_set
cs_intro: cat_cs_intros nat_omega_intros
)+
qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
show "RK23 𝔉⦇ArrMap⦈⦇f⦈ : RK23 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ RK23 𝔉⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b" for a b f
proof-
from 0123 that show ?thesis
by (elim cat_ordinal_3_is_arrE; simp only:)
(
cs_concl
cs_simp: cat_Kan_cs_simps
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
qed
show
"RK23 𝔉⦇ArrMap⦈⦇g ∘⇩A⇘cat_ordinal (3⇩ℕ)⇙ f⦈ =
RK23 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙ RK23 𝔉⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘cat_ordinal (3⇩ℕ)⇙ c" and "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b"
for b c g a f
using 0123 that
by (elim cat_ordinal_3_is_arrE; simp only:; (solves‹simp›)?)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
𝔉.cf_ArrMap_Comp[symmetric]
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
show "RK23 𝔉⦇ArrMap⦈⦇cat_ordinal (3⇩ℕ)⦇CId⦈⦇c⦈⦈ = ℭ⦇CId⦈⦇RK23 𝔉⦇ObjMap⦈⦇c⦈⦈"
if "c ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈" for c
proof-
from that consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ›
unfolding cat_ordinal_components three by auto
then show ?thesis
by (cases, use 0123 in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
is_functor.cf_ObjMap_CId[symmetric]
cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
)+
qed
qed
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
)+
qed
lemma cat_RK23_is_functor'[cat_Kan_cs_intros]:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
and "𝔄' = cat_ordinal (3⇩ℕ)"
shows "RK23 𝔉 : 𝔄' ↦↦⇩C⇘α⇙ ℭ"
using assms(1) unfolding assms(2) by (rule cat_RK23_is_functor)
subsubsection‹The fundamental property of ‹RK23››
lemma cf_comp_RK23_𝔎23[cat_Kan_cs_simps]:
assumes "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ"
shows "RK23 𝔉 ∘⇩C⇩F 𝔎23 = 𝔉"
proof-
interpret 𝔉: is_functor α ‹cat_ordinal (2⇩ℕ)› ℭ 𝔉 by (rule assms(1))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret RK23: is_functor α ‹cat_ordinal (3⇩ℕ)› ℭ ‹RK23 𝔉›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
show ?thesis
proof(rule cf_eqI)
show "𝔉 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ ℭ" by (rule assms)
have ObjMap_dom_lhs: "𝒟⇩∘ ((RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈) = 2⇩ℕ"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_ordinal_cs_simps cs_intro: cat_cs_intros
)
have ObjMap_dom_rhs: "𝒟⇩∘ (𝔉⦇ObjMap⦈) = 2⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
show "(RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈ = 𝔉⦇ObjMap⦈"
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
fix a assume prems: "a ∈⇩∘ 2⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› by force
then show "(RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ObjMap⦈⦇a⦈ = 𝔉⦇ObjMap⦈⦇a⦈"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
omega_of_set cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)+
qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+
have ArrMap_dom_lhs: "𝒟⇩∘ ((RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈) = cat_ordinal (2⇩ℕ)⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have ArrMap_dom_rhs: "𝒟⇩∘ (𝔉⦇ArrMap⦈) = cat_ordinal (2⇩ℕ)⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "(RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈ = 𝔉⦇ArrMap⦈"
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
fix f assume prems: "f ∈⇩∘ cat_ordinal (2⇩ℕ)⦇Arr⦈"
then obtain a b where "f : a ↦⇘cat_ordinal (2⇩ℕ)⇙ b" by auto
then show "(RK23 𝔉 ∘⇩C⇩F 𝔎23)⦇ArrMap⦈⦇f⦈ = 𝔉⦇ArrMap⦈⦇f⦈"
by (elim cat_ordinal_2_is_arrE; simp only:)
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cs_intro: cat_cs_intros
)+
qed (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros V_cs_intros)+
qed (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
qed
subsection‹
‹RK_σ23›: towards the universal property of the right Kan extension along ‹𝔎23›
›
subsubsection‹Definition and elementary properties›
definition RK_σ23 :: "V ⇒ V ⇒ V ⇒ V"
where "RK_σ23 𝔗 ε' 𝔉' =
[
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ ε'⦇NTMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ ε'⦇NTMap⦈⦇1⇩ℕ⦈ ∘⇩A⇘𝔗⦇HomCod⦈⇙ 𝔉'⦇ArrMap⦈⦇1⇩ℕ, 2⇩ℕ⦈⇩∙
| a = 2⇩ℕ ⇒ ε'⦇NTMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
),
𝔉',
RK23 𝔗,
cat_ordinal (3⇩ℕ),
𝔉'⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma RK_σ23_components:
shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈ =
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ ε'⦇NTMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ ε'⦇NTMap⦈⦇1⇩ℕ⦈ ∘⇩A⇘𝔗⦇HomCod⦈⇙ 𝔉'⦇ArrMap⦈⦇1⇩ℕ, 2⇩ℕ⦈⇩∙
| a = 2⇩ℕ ⇒ ε'⦇NTMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
)"
and "RK_σ23 𝔗 ε' 𝔉'⦇NTDom⦈ = 𝔉'"
and "RK_σ23 𝔗 ε' 𝔉'⦇NTCod⦈ = RK23 𝔗"
and "RK_σ23 𝔗 ε' 𝔉'⦇NTDGDom⦈ = cat_ordinal (3⇩ℕ)"
and "RK_σ23 𝔗 ε' 𝔉'⦇NTDGCod⦈ = 𝔉'⦇HomCod⦈"
unfolding RK_σ23_def nt_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔄 𝔉' 𝔗
assumes 𝔉': "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and 𝔗: "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule 𝔉')
interpretation 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule 𝔗)
lemmas RK_σ23_components' =
RK_σ23_components[where 𝔉'=𝔉' and 𝔗=𝔗, unfolded cat_cs_simps]
lemmas [cat_Kan_cs_simps] = RK_σ23_components'(2-5)
end
subsubsection‹Natural transformation map›
mk_VLambda RK_σ23_components(1)
|vsv RK_σ23_NTMap_vsv[cat_Kan_cs_intros]|
|vdomain RK_σ23_NTMap_vdomain[cat_Kan_cs_simps]|
|app RK_σ23_NTMap_app|
lemma RK_σ23_NTMap_app_0[cat_Kan_cs_simps]:
assumes "a = 0"
shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇0⦈"
using assms unfolding RK_σ23_components cat_ordinal_cs_simps by simp
lemma (in is_functor) RK_σ23_NTMap_app_1[cat_Kan_cs_simps]:
assumes "a = 1⇩ℕ"
shows "RK_σ23 𝔉 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇1⇩ℕ⦈ ∘⇩A⇘𝔅⇙ 𝔉'⦇ArrMap⦈⦇1⇩ℕ, 2⇩ℕ⦈⇩∙"
using assms
unfolding RK_σ23_components cat_ordinal_cs_simps cat_cs_simps
by simp
lemmas [cat_Kan_cs_simps] = is_functor.RK_σ23_NTMap_app_1
lemma RK_σ23_NTMap_app_2[cat_Kan_cs_simps]:
assumes "a = 2⇩ℕ"
shows "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ = ε'⦇NTMap⦈⦇1⇩ℕ⦈"
using assms unfolding RK_σ23_components cat_ordinal_cs_simps by simp
subsubsection‹‹RK_σ23› is a natural transformation›
lemma RK_σ23_is_ntcf:
assumes "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "ε' : 𝔉' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F 𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
proof-
interpret 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule assms(1))
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(2))
interpret ε': is_ntcf α ‹cat_ordinal (2⇩ℕ)› 𝔄 ‹𝔉' ∘⇩C⇩F 𝔎23› 𝔗 ε'
by (rule assms(3))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret RK23: is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹RK23 𝔗›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
from 0123 have [cat_cs_simps]: "𝔗⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙ = 𝔄⦇CId⦈⦇𝔗⦇ObjMap⦈⦇1⇩ℕ⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps is_functor.cf_ObjMap_CId[symmetric]
cs_intro: cat_cs_intros
)
show ?thesis
proof(rule is_ntcfI')
show "vfsequence (RK_σ23 𝔗 ε' 𝔉')" unfolding RK_σ23_def by simp
show "vcard (RK_σ23 𝔗 ε' 𝔉') = 5⇩ℕ"
unfolding RK_σ23_def by (simp_all add: nat_omega_simps)
show "RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈ : 𝔉'⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ RK23 𝔗⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈" for a
proof-
from that consider ‹a = 0› | ‹a = 1⇩ℕ› | ‹a = 2⇩ℕ›
unfolding cat_ordinal_cs_simps three by auto
from this 0123 show ?thesis
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp: cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
cs_intro:
cat_cs_intros
cat_ordinal_cs_intros
cat_Kan_cs_intros
nat_omega_intros
)+
qed
show
"RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔄⇙ 𝔉'⦇ArrMap⦈⦇f⦈ =
RK23 𝔗⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔄⇙ RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b" for a b f
using that 0123
by (elim cat_ordinal_3_is_arrE, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_cs_simps
cat_ordinal_cs_simps
𝔉'.cf_ArrMap_Comp[symmetric]
𝔉'.HomCod.cat_Comp_assoc
ε'.ntcf_Comp_commute[symmetric]
cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
)+
qed
(
cs_concl
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
)+
qed
lemma RK_σ23_is_ntcf'[cat_Kan_cs_intros]:
assumes "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "ε' : 𝔉' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F 𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔊' = 𝔉'"
and "ℌ' = RK23 𝔗"
and "ℭ' = cat_ordinal (3⇩ℕ)"
shows "RK_σ23 𝔗 ε' 𝔉' : 𝔊' ↦⇩C⇩F ℌ': ℭ' ↦↦⇩C⇘α⇙ 𝔄"
using assms(1-3) unfolding assms(4-6) by (rule RK_σ23_is_ntcf)
subsection‹The right Kan extension along ‹𝔎23››
lemma ε23_is_cat_rKe:
assumes "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "ntcf_id 𝔗 :
RK23 𝔗 ∘⇩C⇩F 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 : cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(1))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret RK23: is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹RK23 𝔗›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
from 0123 have [cat_cs_simps]: "𝔗⦇ArrMap⦈⦇1⇩ℕ, 1⇩ℕ⦈⇩∙ = 𝔄⦇CId⦈⦇𝔗⦇ObjMap⦈⦇1⇩ℕ⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps is_functor.cf_ObjMap_CId[symmetric]
cs_intro: cat_cs_intros
)
show ?thesis
proof(intro is_cat_rKeI')
fix 𝔉' ε' assume prems:
"𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
"ε' : 𝔉' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F 𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
interpret 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule prems(1))
interpret ε': is_ntcf α ‹cat_ordinal (2⇩ℕ)› 𝔄 ‹𝔉' ∘⇩C⇩F 𝔎23› 𝔗 ε'
by (rule prems(2))
interpret RK_σ23: is_ntcf α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' ‹RK23 𝔗› ‹RK_σ23 𝔗 ε' 𝔉'›
by (intro RK_σ23_is_ntcf prems assms)
show "∃!σ.
σ : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄 ∧
ε' = ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
proof(intro ex1I conjI; (elim conjE)?)
show "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (intro RK_σ23.is_ntcf_axioms)
show "ε' = ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (RK_σ23 𝔗 ε' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
proof(rule ntcf_eqI)
show "ε' : 𝔉' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F 𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (intro prems)
then have dom_lhs: "𝒟⇩∘ (ε'⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show rhs:
"ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (RK_σ23 𝔗 ε' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23) :
𝔉' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F 𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (RK_σ23 𝔗 ε' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "ε'⦇NTMap⦈ = (ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (RK_σ23 𝔗 ε' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ 2⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› unfolding two by auto
then show
"ε'⦇NTMap⦈⦇a⦈ =
(ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (RK_σ23 𝔗 ε' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈⦇a⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
omega_of_set
cat_Kan_cs_simps
cat_cs_simps
cat_ordinal_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros nat_omega_intros
)+
qed
(
use rhs in
‹cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros›
)+
qed simp_all
fix σ assume prems':
"σ : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
"ε' = ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
interpret σ: is_ntcf α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' ‹RK23 𝔗› σ
by (rule prems'(1))
from prems'(2) have
"ε'⦇NTMap⦈⦇0⦈ = (ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈⦇0⦈"
by auto
then have [cat_cs_simps]: "ε'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)
from prems'(2) have
"ε'⦇NTMap⦈⦇1⇩ℕ⦈ = (ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈⦇1⇩ℕ⦈"
by auto
then have [cat_cs_simps]: "ε'⦇NTMap⦈⦇1⇩ℕ⦈ = σ⦇NTMap⦈⦇2⇩ℕ⦈"
by
(
cs_prems cs_shallow
cs_simp:
omega_of_set cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)
show "σ = RK_σ23 𝔗 ε' 𝔉'"
proof(rule ntcf_eqI)
show "σ : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (rule prems'(1))
then have dom_lhs: "𝒟⇩∘ (σ⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
show "RK_σ23 𝔗 ε' 𝔉' : 𝔉' ↦⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
then have dom_rhs: "𝒟⇩∘ (RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
from 0123 have 013: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (3⇩ℕ)⇙ 1⇩ℕ"
by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
from 0123 have 123: "[1⇩ℕ, 2⇩ℕ]⇩∘ : 1⇩ℕ ↦⇘cat_ordinal (3⇩ℕ)⇙ 2⇩ℕ"
by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
from σ.ntcf_Comp_commute[OF 123] 013 0123
have [symmetric, cat_Kan_cs_simps]:
"σ⦇NTMap⦈⦇2⇩ℕ⦈ ∘⇩A⇘𝔄⇙ 𝔉'⦇ArrMap⦈ ⦇1⇩ℕ, 2⇩ℕ⦈⇩∙ = σ⦇NTMap⦈⦇1⇩ℕ⦈"
by
(
cs_prems
cs_simp: cat_cs_simps cat_Kan_cs_simps RK23_ArrMap_app_12
cs_intro: cat_cs_intros
)
show "σ⦇NTMap⦈ = RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ 3⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› | ‹a = 2⇩ℕ› unfolding three by auto
then show "σ⦇NTMap⦈⦇a⦈ = RK_σ23 𝔗 ε' 𝔉'⦇NTMap⦈⦇a⦈"
by (cases; use nothing in ‹simp_all only:›)
(cs_concl cs_simp: cat_cs_simps cat_Kan_cs_simps)+
qed auto
qed simp_all
qed
qed (cs_concl cs_shallow cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)+
qed
subsection‹
‹LK_σ23›: towards the universal property of the left Kan extension along ‹𝔎23›
›
subsubsection‹Definition and elementary properties›
definition LK_σ23 :: "V ⇒ V ⇒ V ⇒ V"
where "LK_σ23 𝔗 η' 𝔉' =
[
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ η'⦇NTMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉'⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙ ∘⇩A⇘𝔗⦇HomCod⦈⇙ η'⦇NTMap⦈⦇0⦈
| a = 2⇩ℕ ⇒ η'⦇NTMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
),
LK23 𝔗,
𝔉',
cat_ordinal (3⇩ℕ),
𝔉'⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma LK_σ23_components:
shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈ =
(
λa∈⇩∘cat_ordinal (3⇩ℕ)⦇Obj⦈.
if a = 0 ⇒ η'⦇NTMap⦈⦇0⦈
| a = 1⇩ℕ ⇒ 𝔉'⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙ ∘⇩A⇘𝔗⦇HomCod⦈⇙ η'⦇NTMap⦈⦇0⦈
| a = 2⇩ℕ ⇒ η'⦇NTMap⦈⦇1⇩ℕ⦈
| otherwise ⇒ 𝔗⦇HomCod⦈⦇Arr⦈
)"
and "LK_σ23 𝔗 η' 𝔉'⦇NTDom⦈ = LK23 𝔗"
and "LK_σ23 𝔗 η' 𝔉'⦇NTCod⦈ = 𝔉'"
and "LK_σ23 𝔗 η' 𝔉'⦇NTDGDom⦈ = cat_ordinal (3⇩ℕ)"
and "LK_σ23 𝔗 η' 𝔉'⦇NTDGCod⦈ = 𝔉'⦇HomCod⦈"
unfolding LK_σ23_def nt_field_simps by (simp_all add: nat_omega_simps)
context
fixes α 𝔄 𝔉' 𝔗
assumes 𝔉': "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and 𝔗: "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
begin
interpretation 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule 𝔉')
interpretation 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule 𝔗)
lemmas LK_σ23_components' =
LK_σ23_components[where 𝔉'=𝔉' and 𝔗=𝔗, unfolded cat_cs_simps]
lemmas [cat_Kan_cs_simps] = LK_σ23_components'(2-5)
end
subsubsection‹Natural transformation map›
mk_VLambda LK_σ23_components(1)
|vsv LK_σ23_NTMap_vsv[cat_Kan_cs_intros]|
|vdomain LK_σ23_NTMap_vdomain[cat_Kan_cs_simps]|
|app LK_σ23_NTMap_app|
lemma LK_σ23_NTMap_app_0[cat_Kan_cs_simps]:
assumes "a = 0"
shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ = η'⦇NTMap⦈⦇0⦈"
using assms unfolding LK_σ23_components cat_ordinal_cs_simps by simp
lemma (in is_functor) LK_σ23_NTMap_app_1[cat_Kan_cs_simps]:
assumes "a = 1⇩ℕ"
shows "LK_σ23 𝔉 η' 𝔉'⦇NTMap⦈⦇a⦈ = 𝔉'⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙ ∘⇩A⇘𝔅⇙ η'⦇NTMap⦈⦇0⦈"
using assms unfolding LK_σ23_components cat_ordinal_cs_simps cat_cs_simps by simp
lemmas [cat_Kan_cs_simps] = is_functor.LK_σ23_NTMap_app_1
lemma LK_σ23_NTMap_app_2[cat_Kan_cs_simps]:
assumes "a = 2⇩ℕ"
shows "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ = η'⦇NTMap⦈⦇1⇩ℕ⦈"
using assms unfolding LK_σ23_components cat_ordinal_cs_simps by simp
subsubsection‹‹LK_σ23› is a natural transformation›
lemma LK_σ23_is_ntcf:
assumes "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "η' : 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
proof-
interpret 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule assms(1))
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(2))
interpret η': is_ntcf α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 ‹𝔉' ∘⇩C⇩F 𝔎23› η'
by (rule assms(3))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret LK23: is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹LK23 𝔗›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
show ?thesis
proof(rule is_ntcfI')
show "vfsequence (LK_σ23 𝔗 η' 𝔉')" unfolding LK_σ23_def by simp
show "vcard (LK_σ23 𝔗 η' 𝔉') = 5⇩ℕ"
unfolding LK_σ23_def by (simp_all add: nat_omega_simps)
show "LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ : LK23 𝔗⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Obj⦈" for a
proof-
from that consider ‹a = 0› | ‹a = 1⇩ℕ› | ‹a = 2⇩ℕ›
unfolding cat_ordinal_cs_simps three by auto
from this 0123 show
"LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈ : LK23 𝔗⦇ObjMap⦈⦇a⦈ ↦⇘𝔄⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp: cat_cs_simps cat_ordinal_cs_simps cat_Kan_cs_simps
cs_intro:
cat_cs_intros
cat_ordinal_cs_intros
cat_Kan_cs_intros
nat_omega_intros
)+
qed
show
"LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔄⇙ LK23 𝔗⦇ArrMap⦈⦇f⦈ =
𝔉'⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔄⇙ LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘cat_ordinal (3⇩ℕ)⇙ b" for a b f
using that 0123
by (elim cat_ordinal_3_is_arrE, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_cs_simps
cat_ordinal_cs_simps
𝔉'.cf_ArrMap_Comp[symmetric]
𝔉'.HomCod.cat_Comp_assoc[symmetric]
η'.ntcf_Comp_commute
cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
)+
qed
(
cs_concl
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
)+
qed
lemma LK_σ23_is_ntcf'[cat_Kan_cs_intros]:
assumes "𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "η' : 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
and "𝔊' = LK23 𝔗"
and "ℌ' = 𝔉'"
and "ℭ' = cat_ordinal (3⇩ℕ)"
shows "LK_σ23 𝔗 η' 𝔉' : 𝔊' ↦⇩C⇩F ℌ': ℭ' ↦↦⇩C⇘α⇙ 𝔄"
using assms(1-3) unfolding assms(4-6) by (rule LK_σ23_is_ntcf)
subsection‹The left Kan extension along ‹𝔎23››
lemma η23_is_cat_rKe:
assumes "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "ntcf_id 𝔗 :
𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇘α⇙ LK23 𝔗 ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(1))
interpret 𝔎23: is_functor α ‹cat_ordinal (2⇩ℕ)› ‹cat_ordinal (3⇩ℕ)› ‹𝔎23›
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Kan_cs_intros)
interpret LK23: is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹LK23 𝔗›
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
show ?thesis
proof(intro is_cat_lKeI')
fix 𝔉' η' assume prems:
"𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
"η' : 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
interpret 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› 𝔄 𝔉' by (rule prems(1))
interpret η': is_ntcf α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 ‹𝔉' ∘⇩C⇩F 𝔎23› η'
by (rule prems(2))
interpret LK_σ23: is_ntcf α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹LK23 𝔗› 𝔉' ‹LK_σ23 𝔗 η' 𝔉'›
by (intro LK_σ23_is_ntcf prems assms)
show "∃!σ.
σ : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄 ∧
η' = σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗"
proof(intro ex1I conjI; (elim conjE)?)
show "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (intro LK_σ23.is_ntcf_axioms)
show "η' = LK_σ23 𝔗 η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗"
proof(rule ntcf_eqI)
show "η' : 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (intro prems)
then have dom_lhs: "𝒟⇩∘ (η'⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show rhs:
"LK_σ23 𝔗 η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗 :
𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((LK_σ23 𝔗 η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗)⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "η'⦇NTMap⦈ = (LK_σ23 𝔗 η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ 2⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› unfolding two by auto
then show
"η'⦇NTMap⦈⦇a⦈ =
(LK_σ23 𝔗 η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗)⦇NTMap⦈⦇a⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
omega_of_set
cat_Kan_cs_simps
cat_cs_simps
cat_ordinal_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros nat_omega_intros
)+
qed
(
use rhs in
‹cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros›
)+
qed simp_all
fix σ assume prems':
"σ : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
"η' = σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗"
interpret σ: is_ntcf α ‹cat_ordinal (3⇩ℕ)› 𝔄 ‹LK23 𝔗› 𝔉' σ
by (rule prems'(1))
from prems'(2) have
"η'⦇NTMap⦈⦇0⦈ = (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗)⦇NTMap⦈⦇0⦈"
by auto
then have [cat_cs_simps]: "η'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)
from prems'(2) have
"η'⦇NTMap⦈⦇1⇩ℕ⦈ = (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F ntcf_id 𝔗)⦇NTMap⦈⦇1⇩ℕ⦈"
by auto
then have [cat_cs_simps]: "η'⦇NTMap⦈⦇1⇩ℕ⦈ = σ⦇NTMap⦈⦇2⇩ℕ⦈"
by
(
cs_prems cs_shallow
cs_simp:
omega_of_set cat_Kan_cs_simps cat_cs_simps cat_ordinal_cs_simps
cs_intro: cat_cs_intros nat_omega_intros
)
show "σ = LK_σ23 𝔗 η' 𝔉'"
proof(rule ntcf_eqI)
show "σ : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (rule prems'(1))
then have dom_lhs: "𝒟⇩∘ (σ⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
show "LK_σ23 𝔗 η' 𝔉' : LK23 𝔗 ↦⇩C⇩F 𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
then have dom_rhs: "𝒟⇩∘ (LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_ordinal_cs_simps)
from 0123 have 012: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (2⇩ℕ)⇙ 1⇩ℕ"
by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
from 0123 have 013: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (3⇩ℕ)⇙ 1⇩ℕ"
by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
from 0123 have 00: "[0, 0]⇩∘ = (cat_ordinal (2⇩ℕ))⦇CId⦈⦇0⦈"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)
from σ.ntcf_Comp_commute[OF 013] 013 0123
have [symmetric, cat_Kan_cs_simps]:
"σ⦇NTMap⦈⦇1⇩ℕ⦈ = 𝔉'⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙ ∘⇩A⇘𝔄⇙ σ⦇NTMap⦈⦇0⦈"
by
(
cs_prems
cs_simp: cat_cs_simps cat_Kan_cs_simps 00 LK23_ArrMap_app_01
cs_intro: cat_cs_intros cat_ordinal_cs_intros nat_omega_intros
)
show "σ⦇NTMap⦈ = LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ 3⇩ℕ"
then consider ‹a = 0› | ‹a = 1⇩ℕ› | ‹a = 2⇩ℕ› unfolding three by auto
then show "σ⦇NTMap⦈⦇a⦈ = LK_σ23 𝔗 η' 𝔉'⦇NTMap⦈⦇a⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros
)+
qed auto
qed simp_all
qed
qed (cs_concl cs_shallow cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros)+
qed
subsection‹Pointwise Kan extensions along ‹𝔎23››
lemma ε23_is_cat_pw_rKe:
assumes "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "ntcf_id 𝔗 :
RK23 𝔗 ∘⇩C⇩F 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇩.⇩p⇩w⇘α⇙ 𝔗 :
cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(1))
show ?thesis
proof(intro is_cat_pw_rKeI ε23_is_cat_rKe[OF assms])
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
show
"ntcf_id 𝔗 :
RK23 𝔗 ∘⇩C⇩F 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ 𝔗 :
cat_ordinal (2⇩ℕ) ↦⇩C
cat_ordinal (3⇩ℕ) ↦⇩C
(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) : 𝔄 ↦↦⇩C cat_Set α)"
proof(intro is_cat_rKe_preservesI ε23_is_cat_rKe[OF assms])
from prems show "Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 :
(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗) ∘⇩C⇩F 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C cat_Set α"
proof(intro is_cat_rKeI')
show "𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_ordinal (3⇩ℕ)"
by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
from prems show
"Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_intro: cat_cs_intros cat_Kan_cs_intros)
from prems show
"Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 :
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 ∘⇩C⇩F 𝔎23 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros
)
fix 𝔊' ε' assume prems':
"𝔊' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
"ε' :
𝔊' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
interpret 𝔊': is_functor α ‹cat_ordinal (3⇩ℕ)› ‹cat_Set α› 𝔊'
by (rule prems'(1))
interpret ε': is_ntcf
α
‹cat_ordinal (2⇩ℕ)›
‹cat_Set α›
‹𝔊' ∘⇩C⇩F 𝔎23›
‹Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗›
ε'
by (rule prems'(2))
show "∃!σ.
σ :
𝔊' ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α ∧
ε' = Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
proof(intro ex1I conjI; (elim conjE)?)
have [cat_Kan_cs_simps]:
"Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 = RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)"
proof(rule cf_eqI)
from prems show lhs: "Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros
)
from prems show rhs: "RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros
)
from lhs prems have ObjMap_dom_lhs:
"𝒟⇩∘ ((Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ObjMap⦈) = 3⇩ℕ"
by
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
from rhs prems have ObjMap_dom_rhs:
"𝒟⇩∘ ((RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗))⦇ObjMap⦈) = 3⇩ℕ"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros
)
show
"(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ObjMap⦈ =
RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)⦇ObjMap⦈"
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
fix c assume prems'': "c ∈⇩∘ 3⇩ℕ"
with 0123 consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ› by force
from this prems prems'' 0123 show
"(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ObjMap⦈⦇c⦈ =
RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)⦇ObjMap⦈⦇c⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_cs_simps
cat_op_simps
cat_Kan_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)+
qed
(
use prems in ‹
cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros
›
)+
from lhs prems have ArrMap_dom_lhs:
"𝒟⇩∘ ((Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ArrMap⦈) =
cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
from rhs prems have ArrMap_dom_rhs:
"𝒟⇩∘ ((RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗))⦇ArrMap⦈) =
cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cat_cs_simps
cs_intro: cat_Kan_cs_intros
)
show
"(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ArrMap⦈ =
RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)⦇ArrMap⦈"
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
fix f assume prems'': "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
then obtain a' b' where "f : a' ↦⇘cat_ordinal (3⇩ℕ)⇙ b'" by auto
from this 0123 prems show
"(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗)⦇ArrMap⦈⦇f⦈ =
RK23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗)⦇ArrMap⦈⦇f⦈"
by
(
elim cat_ordinal_3_is_arrE;
use nothing in ‹simp_all only:›
)
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
cs_intro:
cat_ordinal_cs_intros
cat_Kan_cs_intros
cat_cs_intros
nat_omega_intros
)+
qed
(
use prems in
‹cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros›
)+
qed simp_all
show "RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' :
𝔊' ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by (intro RK_σ23_is_ntcf')
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros
)+
show "ε' =
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F
ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F
(RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
proof(rule ntcf_eqI)
show "ε' :
𝔊' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by (intro prems')
then have dom_lhs: "𝒟⇩∘ (ε'⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
from prems show
"Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F
ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F
(RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23) :
𝔊' ∘⇩C⇩F 𝔎23 ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘
(
(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F
ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F
(RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)
)⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "ε'⦇NTMap⦈ =
(
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F
ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F
(RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)
)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix c assume prems'': "c ∈⇩∘ 2⇩ℕ"
then consider ‹c = 0› | ‹c = 1⇩ℕ› unfolding two by auto
from this prems 0123 show "ε'⦇NTMap⦈⦇c⦈ =
(
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F
ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F
(RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)
)⦇NTMap⦈⦇c⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_Kan_cs_simps
cat_ordinal_cs_simps
cat_cs_simps
cat_op_simps
RK_σ23_NTMap_app_0
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
𝔗.HomCod.cat_Hom_in_Vset
)+
qed (cs_concl cs_intro: cat_cs_intros V_cs_intros)+
qed simp_all
fix σ assume prems'':
"σ :
𝔊' ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
"ε' = Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)"
interpret σ: is_ntcf
α ‹cat_ordinal (3⇩ℕ)› ‹cat_Set α› 𝔊' ‹Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗› σ
by (rule prems''(1))
from prems''(2) have "ε'⦇NTMap⦈⦇0⦈ =
(Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23))⦇NTMap⦈⦇0⦈"
by auto
from this prems 0123 have ε'_NTMap_app_0: "ε'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
by
(
cs_prems
cs_simp:
cat_ordinal_cs_simps
cat_cs_simps
cat_Kan_cs_simps
cat_op_simps
𝔎23_ObjMap_app_0
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
𝔗.HomCod.cat_Hom_in_Vset
)
from 0123 have 01: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (2⇩ℕ)⇙ 1⇩ℕ"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_ordinal_cs_intros nat_omega_intros
)
from prems''(2) have
"ε'⦇NTMap⦈⦇1⇩ℕ⦈ =
(
Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 ∙⇩N⇩T⇩C⇩F (σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23)
)⦇NTMap⦈⦇1⇩ℕ⦈"
by auto
from this prems 0123 have ε'_NTMap_app_1:
"ε'⦇NTMap⦈⦇1⇩ℕ⦈ = σ⦇NTMap⦈⦇2⇩ℕ⦈"
by
(
cs_prems
cs_simp:
cat_ordinal_cs_simps
cat_cs_simps
cat_Kan_cs_simps
cat_op_simps
𝔎23_ObjMap_app_1
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
𝔗.HomCod.cat_Hom_in_Vset
)
from 0123 have 012: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (2⇩ℕ)⇙ 1⇩ℕ"
by
(
cs_concl cs_intro:
cat_ordinal_cs_intros nat_omega_intros
)
from 0123 have 013: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (3⇩ℕ)⇙ 1⇩ℕ"
by
(
cs_concl cs_intro:
cat_ordinal_cs_intros nat_omega_intros
)
from 0123 have 123: "[1⇩ℕ, 2⇩ℕ]⇩∘ : 1⇩ℕ ↦⇘cat_ordinal (3⇩ℕ)⇙ 2⇩ℕ"
by
(
cs_concl cs_intro:
cat_ordinal_cs_intros nat_omega_intros
)
from 0123 have 11: "[1⇩ℕ, 1⇩ℕ]⇩∘ = (cat_ordinal (2⇩ℕ))⦇CId⦈⦇1⇩ℕ⦈"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)
from σ.ntcf_Comp_commute[OF 123] prems 012 013
have [cat_Kan_cs_simps]:
"ε'⦇NTMap⦈⦇1⇩ℕ⦈ ∘⇩A⇘cat_Set α⇙ 𝔊'⦇ArrMap⦈⦇1⇩ℕ, 2⇩ℕ⦈⇩∙ = σ⦇NTMap⦈⦇1⇩ℕ⦈"
by
(
cs_prems
cs_simp:
cat_cs_simps
cat_Kan_cs_simps
ε'_NTMap_app_1[symmetric]
is_functor.cf_ObjMap_CId
RK23_ArrMap_app_12
11
cs_intro: cat_cs_intros nat_omega_intros
)
show "σ = RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊'"
proof(rule ntcf_eqI)
show σ: "σ :
𝔊' ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by (rule prems''(1))
then have dom_lhs: "𝒟⇩∘ (σ⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊' :
𝔊' ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F RK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ (RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊'⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "σ⦇NTMap⦈ = RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊'⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix c assume "c ∈⇩∘ 3⇩ℕ"
then consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ›
unfolding three by auto
from this 0123 show
"σ⦇NTMap⦈⦇c⦈ = RK_σ23 (Hom⇩O⇩.⇩C⇘α⇙𝔄(a,-) ∘⇩C⇩F 𝔗) ε' 𝔊'⦇NTMap⦈⦇c⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl cs_simp:
cat_Kan_cs_simps ε'_NTMap_app_1 ε'_NTMap_app_0
)+
qed (cs_concl cs_intro: cat_Kan_cs_intros V_cs_intros)+
qed simp_all
qed
qed
qed
qed
qed
lemma η23_is_cat_pw_lKe:
assumes "𝔗 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ 𝔄"
shows "ntcf_id 𝔗 :
𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇩.⇩p⇩w⇘α⇙ LK23 𝔗 ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C 𝔄"
proof-
interpret 𝔗: is_functor α ‹cat_ordinal (2⇩ℕ)› 𝔄 𝔗 by (rule assms(1))
from ord_of_nat_ω interpret cat_ordinal_3: finite_category α ‹cat_ordinal (3⇩ℕ)›
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
from 0123 have 002: "[0, 0]⇩∘ : 0 ↦⇘cat_ordinal (2⇩ℕ)⇙ 0"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cs_intro: cat_cs_intros
)
show ?thesis
proof(intro is_cat_pw_lKeI η23_is_cat_rKe assms, unfold cat_op_simps)
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
show
"op_ntcf (ntcf_id 𝔗) :
op_cf (LK23 𝔗) ∘⇩C⇩F op_cf 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ op_cf 𝔗 :
op_cat (cat_ordinal (2⇩ℕ)) ↦⇩C op_cat (cat_ordinal (3⇩ℕ)) ↦⇩C
(Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) : op_cat 𝔄 ↦↦⇩C cat_Set α)"
proof(intro is_cat_rKe_preservesI)
show
"op_ntcf (ntcf_id 𝔗) :
op_cf (LK23 𝔗) ∘⇩C⇩F op_cf 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙ op_cf 𝔗 :
op_cat (cat_ordinal (2⇩ℕ)) ↦⇩C op_cat (cat_ordinal (3⇩ℕ)) ↦⇩C op_cat 𝔄"
proof(cs_intro_step cat_op_intros)
show "ntcf_id 𝔗 :
𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇘α⇙ LK23 𝔗 ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C 𝔄"
by (intro η23_is_cat_rKe assms)
qed simp_all
from prems show "Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) : op_cat 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
have
"op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗 ↦⇩C⇩F⇩.⇩l⇩K⇩e⇘α⇙
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗) ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦⇩C cat_ordinal (3⇩ℕ) ↦⇩C op_cat (cat_Set α)"
proof(intro is_cat_lKeI')
show "𝔎23 : cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ cat_ordinal (3⇩ℕ)"
by (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
from prems show "op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
from prems show
"op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗 :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗 ↦⇩C⇩F
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
fix 𝔉' η' assume prems':
"𝔉' : cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
"η' :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
interpret 𝔉': is_functor α ‹cat_ordinal (3⇩ℕ)› ‹op_cat (cat_Set α)› 𝔉'
by (rule prems'(1))
interpret η': is_ntcf
α
‹cat_ordinal (2⇩ℕ)›
‹op_cat (cat_Set α)›
‹op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗›
‹𝔉' ∘⇩C⇩F 𝔎23›
η'
by (rule prems'(2))
note [unfolded cat_op_simps, cat_cs_intros] =
η'.ntcf_NTMap_is_arr'
𝔉'.cf_ArrMap_is_arr'
show
"∃!σ.
σ :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ↦⇩C⇩F 𝔉' :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α) ∧
η' = σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗)"
proof(intro ex1I conjI; (elim conjE)?)
have [cat_Kan_cs_simps]:
"op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 =
LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)"
proof(rule cf_eqI)
from prems show lhs: "op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl
cs_simp: cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
from prems show rhs: "LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by (cs_concl cs_intro: cat_Kan_cs_intros cat_cs_intros)
from lhs prems have ObjMap_dom_lhs:
"𝒟⇩∘ ((op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ObjMap⦈) = 3⇩ℕ"
by
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
from rhs prems have ObjMap_dom_rhs:
"𝒟⇩∘ (LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ObjMap⦈) = 3⇩ℕ"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cat_cs_simps
)
show
"(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ObjMap⦈ =
LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ObjMap⦈"
proof(rule vsv_eqI, unfold ObjMap_dom_lhs ObjMap_dom_rhs)
fix c assume prems'': "c ∈⇩∘ 3⇩ℕ"
then consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ›
unfolding three by auto
from this prems 0123 show
"(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ObjMap⦈⦇c⦈ =
LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ObjMap⦈⦇c⦈"
by (cases; use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
cat_cs_simps
cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)+
qed
(
use prems in
‹
cs_concl
cs_simp: cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
›
)+
from lhs prems have ArrMap_dom_lhs:
"𝒟⇩∘ ((op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ArrMap⦈) =
cat_ordinal (3⇩ℕ)⦇Arr⦈"
by
(
cs_concl
cs_simp: cat_ordinal_cs_simps cat_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
from rhs prems have ArrMap_dom_rhs:
"𝒟⇩∘ (LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ArrMap⦈) =
cat_ordinal (3⇩ℕ)⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show
"(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ArrMap⦈ =
LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ArrMap⦈"
proof(rule vsv_eqI, unfold ArrMap_dom_lhs ArrMap_dom_rhs)
fix f assume "f ∈⇩∘ cat_ordinal (3⇩ℕ)⦇Arr⦈"
then obtain a' b' where f: "f : a' ↦⇘cat_ordinal (3⇩ℕ)⇙ b'"
by auto
from f prems 0123 002 show
"(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗)⦇ArrMap⦈⦇f⦈ =
LK23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗)⦇ArrMap⦈⦇f⦈"
by (elim cat_ordinal_3_is_arrE, (simp_all only:)?)
(
cs_concl
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
cs_intro:
cat_ordinal_cs_intros
cat_Kan_cs_intros
cat_cs_intros
cat_op_intros
nat_omega_intros
)+
qed
(
use prems in
‹
cs_concl
cs_simp: cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros›
)+
qed simp_all
show "LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ↦⇩C⇩F 𝔉' :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_Kan_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
show "η' =
LK_σ23
(
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗
)"
proof(rule ntcf_eqI)
show lhs: "η' :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by (rule prems'(2))
from lhs have "𝒟⇩∘ (η'⦇NTMap⦈) = cat_ordinal (2⇩ℕ)⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from prems show rhs:
"LK_σ23
(
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗
) :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗 ↦⇩C⇩F 𝔉' ∘⇩C⇩F 𝔎23 :
cat_ordinal (2⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl
cs_simp: cat_Kan_cs_simps cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
from lhs have dom_lhs: "𝒟⇩∘ (η'⦇NTMap⦈) = 2⇩ℕ"
by
(
cs_concl cs_shallow
cs_simp: cat_ordinal_cs_simps cat_cs_simps
)
from rhs have dom_rhs: "𝒟⇩∘ ((LK_σ23
(
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗
))⦇NTMap⦈) = 2⇩ℕ"
by (cs_concl cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show
"η'⦇NTMap⦈ =
(
LK_σ23
(
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗
)
)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs cat_ordinal_cs_simps)
fix c assume "c ∈⇩∘ 2⇩ℕ"
then consider ‹c = 0› | ‹c = 1⇩ℕ› unfolding two by auto
from this prems 0123 show
"η'⦇NTMap⦈⦇c⦈ =
(
LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗)
)⦇NTMap⦈⦇c⦈"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
cat_cs_simps
cat_op_simps
𝔎23_ObjMap_app_1
𝔎23_ObjMap_app_0
LK_σ23_NTMap_app_0
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
𝔗.HomCod.cat_Hom_in_Vset
)+
qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
qed simp_all
fix σ assume prems'':
"σ :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ↦⇩C⇩F 𝔉' :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
"η' = σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎23 ∙⇩N⇩T⇩C⇩F (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗)"
interpret σ: is_ntcf
α
‹cat_ordinal (3⇩ℕ)› ‹op_cat (cat_Set α)›
‹op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗›
𝔉'
σ
by (rule prems''(1))
note [cat_Kan_cs_intros] = σ.ntcf_NTMap_is_arr'[unfolded cat_op_simps]
from prems''(2) have
"η'⦇NTMap⦈⦇0⦈ =
(
σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗)
)⦇NTMap⦈⦇0⦈"
by simp
from this prems 0123 have η'_NTMap_app_0: "η'⦇NTMap⦈⦇0⦈ = σ⦇NTMap⦈⦇0⦈"
by
(
cs_prems
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
cat_cs_simps
cat_op_simps
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
𝔗.HomCod.cat_Hom_in_Vset
)
from prems''(2) have
"η'⦇NTMap⦈⦇1⇩ℕ⦈ =
(
σ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F
𝔎23 ∙⇩N⇩T⇩C⇩F
(op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ntcf_id 𝔗)
)⦇NTMap⦈⦇1⇩ℕ⦈"
by simp
from this prems 0123 have η'_NTMap_app_1: "η'⦇NTMap⦈⦇1⇩ℕ⦈ = σ⦇NTMap⦈⦇2⇩ℕ⦈"
by
(
cs_prems
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
cat_cs_simps
cat_op_simps
cat_Set_components(1)
cs_intro:
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
𝔗.HomCod.cat_Hom_in_Vset
)+
from 0123 have 013: "[0, 1⇩ℕ]⇩∘ : 0 ↦⇘cat_ordinal (3⇩ℕ)⇙ 1⇩ℕ"
by (cs_concl cs_intro: cat_ordinal_cs_intros nat_omega_intros)
from 0123 have 00: "[0, 0]⇩∘ = (cat_ordinal (2⇩ℕ))⦇CId⦈⦇0⦈"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps)
from σ.ntcf_Comp_commute[OF 013] prems 0123 013
have [cat_Kan_cs_simps]:
"σ⦇NTMap⦈⦇1⇩ℕ⦈ = η'⦇NTMap⦈⦇0⦈ ∘⇩A⇘cat_Set α⇙ 𝔉'⦇ArrMap⦈⦇0, 1⇩ℕ⦈⇩∙"
by
(
cs_prems
cs_simp:
cat_ordinal_cs_simps
cat_Kan_cs_simps
cat_cs_simps
cat_op_simps
LK23_ArrMap_app_01
cs_intro:
cat_ordinal_cs_intros
cat_Kan_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
nat_omega_intros
cs_simp: 00 η'_NTMap_app_0[symmetric]
)
show "σ = LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉'"
proof(rule ntcf_eqI)
show lhs: "σ :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ↦⇩C⇩F 𝔉' :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by (rule prems''(1))
show rhs: "LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉' :
op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F LK23 𝔗 ↦⇩C⇩F 𝔉' :
cat_ordinal (3⇩ℕ) ↦↦⇩C⇘α⇙ op_cat (cat_Set α)"
by
(
cs_concl cs_shallow
cs_simp: cat_Kan_cs_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros
)
from lhs have dom_lhs: "𝒟⇩∘ (σ⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
from rhs have dom_rhs:
"𝒟⇩∘ (LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉'⦇NTMap⦈) = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: cat_ordinal_cs_simps cat_cs_simps)
show "σ⦇NTMap⦈ = LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉'⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix c assume "c ∈⇩∘ 3⇩ℕ"
then consider ‹c = 0› | ‹c = 1⇩ℕ› | ‹c = 2⇩ℕ›
unfolding three by auto
from this 0123 show
"σ⦇NTMap⦈⦇c⦈ =
LK_σ23 (op_cf Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F 𝔗) η' 𝔉'⦇NTMap⦈⦇c⦈"
by (cases, use nothing in ‹simp_all only:›)
(
cs_concl
cs_simp:
cat_ordinal_cs_simps
cat_cs_simps
cat_Kan_cs_simps
cat_op_simps
η'_NTMap_app_0
LK_σ23_NTMap_app_0
η'_NTMap_app_1
cs_intro:
cat_ordinal_cs_intros
cat_Kan_cs_intros
cat_cs_intros
cat_op_intros
nat_omega_intros
)+
qed (cs_concl cs_intro: cat_Kan_cs_intros V_cs_intros)+
qed simp_all
qed
qed
then have
"op_ntcf (Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf (ntcf_id 𝔗)) :
op_cf (Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F op_cf 𝔗) ↦⇩C⇩F⇩.⇩l⇩K⇩e⇘α⇙
op_cf ((Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F op_cf (LK23 𝔗))) ∘⇩C⇩F op_cf (op_cf 𝔎23) :
op_cat (op_cat (cat_ordinal (2⇩ℕ))) ↦⇩C
op_cat (op_cat (cat_ordinal (3⇩ℕ))) ↦⇩C
op_cat (cat_Set α)"
by
(
cs_concl
cs_simp: cat_op_simps
cs_intro: cat_cs_intros cat_Kan_cs_intros cat_op_intros
)
from is_cat_lKe.is_cat_rKe_op[OF this] prems show
"Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf (ntcf_id 𝔗) :
(Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F op_cf (LK23 𝔗)) ∘⇩C⇩F op_cf 𝔎23 ↦⇩C⇩F⇩.⇩r⇩K⇩e⇘α⇙
Hom⇩O⇩.⇩C⇘α⇙𝔄(-,a) ∘⇩C⇩F op_cf 𝔗 :
op_cat (cat_ordinal (2⇩ℕ)) ↦⇩C
op_cat (cat_ordinal (3⇩ℕ)) ↦⇩C
cat_Set α"
by
(
cs_prems
cs_simp: cat_op_simps
cs_intro: cat_Kan_cs_intros cat_cs_intros cat_op_intros
)
qed
qed
qed
text‹\newpage›
end