Theory CZH_UCAT_Universal
section‹Universal arrow›
theory CZH_UCAT_Universal
imports
CZH_UCAT_Introduction
CZH_Elementary_Categories.CZH_ECAT_FUNCT
CZH_Elementary_Categories.CZH_ECAT_Hom
begin
subsection‹Background›
text‹
The following section is based, primarily, on the elements of the content
of Chapter III-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
named_theorems ua_field_simps
definition UObj :: V where [ua_field_simps]: "UObj = 0"
definition UArr :: V where [ua_field_simps]: "UArr = 1⇩ℕ"
lemma [cat_cs_simps]:
shows UObj_simp: "[a, b]⇩∘⦇UObj⦈ = a"
and UArr_simp: "[a, b]⇩∘⦇UArr⦈ = b"
unfolding ua_field_simps by (simp_all add: nat_omega_simps)
subsection‹Universal map›
text‹
The universal map is a convenience utility that allows treating
a part of the definition of the universal arrow as an arrow in the
category ‹Set›.
›
subsubsection‹Definition and elementary properties›
definition umap_of :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "umap_of 𝔉 c r u d =
[
(λf'∈⇩∘Hom (𝔉⦇HomDom⦈) r d. 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔉⦇HomCod⦈⇙ u),
Hom (𝔉⦇HomDom⦈) r d,
Hom (𝔉⦇HomCod⦈) c (𝔉⦇ObjMap⦈⦇d⦈)
]⇩∘"
definition umap_fo :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "umap_fo 𝔉 c r u d = umap_of (op_cf 𝔉) c r u d"
text‹Components.›
lemma (in is_functor) umap_of_components:
assumes "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "umap_of 𝔉 c r u d⦇ArrVal⦈ = (λf'∈⇩∘Hom 𝔄 r d. 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ u)"
and "umap_of 𝔉 c r u d⦇ArrDom⦈ = Hom 𝔄 r d"
and "umap_of 𝔉 c r u d⦇ArrCod⦈ = Hom 𝔅 c (𝔉⦇ObjMap⦈⦇d⦈)"
unfolding umap_of_def arr_field_simps
by (simp_all add: cat_cs_simps nat_omega_simps)
lemma (in is_functor) umap_fo_components:
assumes "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "umap_fo 𝔉 c r u d⦇ArrVal⦈ = (λf'∈⇩∘Hom 𝔄 d r. u ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f'⦈)"
and "umap_fo 𝔉 c r u d⦇ArrDom⦈ = Hom 𝔄 d r"
and "umap_fo 𝔉 c r u d⦇ArrCod⦈ = Hom 𝔅 (𝔉⦇ObjMap⦈⦇d⦈) c"
unfolding
umap_fo_def
is_functor.umap_of_components[
OF is_functor_op, unfolded cat_op_simps, OF assms
]
proof(rule vsv_eqI)
fix f' assume "f' ∈⇩∘ 𝒟⇩∘ (λf'∈⇩∘Hom 𝔄 d r. 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘op_cat 𝔅⇙ u)"
then have f': "f' : d ↦⇘𝔄⇙ r" by simp
then have 𝔉f': "𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇d⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
by (auto intro: cat_cs_intros)
from f' show
"(λf'∈⇩∘Hom 𝔄 d r. 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘op_cat 𝔅⇙ u)⦇f'⦈ =
(λf'∈⇩∘Hom 𝔄 d r. u ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f'⦈)⦇f'⦈"
by (simp add: HomCod.op_cat_Comp[OF assms 𝔉f'])
qed simp_all
text‹Universal maps for the opposite functor.›
lemma (in is_functor) op_umap_of[cat_op_simps]: "umap_of (op_cf 𝔉) = umap_fo 𝔉"
unfolding umap_fo_def by simp
lemma (in is_functor) op_umap_fo[cat_op_simps]: "umap_fo (op_cf 𝔉) = umap_of 𝔉"
unfolding umap_fo_def by (simp add: cat_op_simps)
lemmas [cat_op_simps] =
is_functor.op_umap_of
is_functor.op_umap_fo
subsubsection‹Arrow value›
lemma umap_of_ArrVal_vsv[cat_cs_intros]: "vsv (umap_of 𝔉 c r u d⦇ArrVal⦈)"
unfolding umap_of_def arr_field_simps by (simp add: nat_omega_simps)
lemma umap_fo_ArrVal_vsv[cat_cs_intros]: "vsv (umap_fo 𝔉 c r u d⦇ArrVal⦈)"
unfolding umap_fo_def by (rule umap_of_ArrVal_vsv)
lemma (in is_functor) umap_of_ArrVal_vdomain:
assumes "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "𝒟⇩∘ (umap_of 𝔉 c r u d⦇ArrVal⦈) = Hom 𝔄 r d"
unfolding umap_of_components[OF assms] by simp
lemmas [cat_cs_simps] = is_functor.umap_of_ArrVal_vdomain
lemma (in is_functor) umap_fo_ArrVal_vdomain:
assumes "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "𝒟⇩∘ (umap_fo 𝔉 c r u d⦇ArrVal⦈) = Hom 𝔄 d r"
unfolding umap_fo_components[OF assms] by simp
lemmas [cat_cs_simps] = is_functor.umap_fo_ArrVal_vdomain
lemma (in is_functor) umap_of_ArrVal_app:
assumes "f' : r ↦⇘𝔄⇙ d" and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "umap_of 𝔉 c r u d⦇ArrVal⦈⦇f'⦈ = 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ u"
using assms(1) unfolding umap_of_components[OF assms(2)] by simp
lemmas [cat_cs_simps] = is_functor.umap_of_ArrVal_app
lemma (in is_functor) umap_fo_ArrVal_app:
assumes "f' : d ↦⇘𝔄⇙ r" and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "umap_fo 𝔉 c r u d⦇ArrVal⦈⦇f'⦈ = u ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f'⦈"
proof-
from assms have "𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇d⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
by (auto intro: cat_cs_intros)
from this assms(2) have 𝔉f'[simp]:
"𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘op_cat 𝔅⇙ u = u ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f'⦈"
by (simp add: cat_op_simps)
from
is_functor_axioms
is_functor.umap_of_ArrVal_app[
OF is_functor_op, unfolded cat_op_simps,
OF assms
]
show ?thesis
by (simp add: cat_op_simps cat_cs_simps)
qed
lemmas [cat_cs_simps] = is_functor.umap_fo_ArrVal_app
lemma (in is_functor) umap_of_ArrVal_vrange:
assumes "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "ℛ⇩∘ (umap_of 𝔉 c r u d⦇ArrVal⦈) ⊆⇩∘ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇d⦈)"
proof(intro vsubset_antisym vsubsetI)
interpret vsv ‹umap_of 𝔉 c r u d⦇ArrVal⦈›
unfolding umap_of_components[OF assms] by simp
fix g assume "g ∈⇩∘ ℛ⇩∘ (umap_of 𝔉 c r u d⦇ArrVal⦈)"
then obtain f'
where g_def: "g = umap_of 𝔉 c r u d⦇ArrVal⦈⦇f'⦈"
and f': "f' ∈⇩∘ 𝒟⇩∘ (umap_of 𝔉 c r u d⦇ArrVal⦈)"
unfolding umap_of_components[OF assms] by auto
then have f': "f' : r ↦⇘𝔄⇙ d"
unfolding umap_of_ArrVal_vdomain[OF assms] by simp
then have 𝔉f': "𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇d⦈"
by (auto intro!: cat_cs_intros)
have g_def: "g = 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ u"
unfolding g_def umap_of_ArrVal_app[OF f' assms]..
from 𝔉f' assms show "g ∈⇩∘ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇d⦈)"
unfolding g_def by (auto intro: cat_cs_intros)
qed
lemma (in is_functor) umap_fo_ArrVal_vrange:
assumes "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "ℛ⇩∘ (umap_fo 𝔉 c r u d⦇ArrVal⦈) ⊆⇩∘ Hom 𝔅 (𝔉⦇ObjMap⦈⦇d⦈) c"
by
(
rule is_functor.umap_of_ArrVal_vrange[
OF is_functor_op, unfolded cat_op_simps, OF assms, folded umap_fo_def
]
)
subsubsection‹Universal map is an arrow in the category ‹Set››
lemma (in is_functor) cf_arr_Set_umap_of:
assumes "category α 𝔄"
and "category α 𝔅"
and r: "r ∈⇩∘ 𝔄⦇Obj⦈"
and d: "d ∈⇩∘ 𝔄⦇Obj⦈"
and u: "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "arr_Set α (umap_of 𝔉 c r u d)"
proof(intro arr_SetI)
interpret HomDom: category α 𝔄 by (rule assms(1))
interpret HomCod: category α 𝔅 by (rule assms(2))
note umap_of_components = umap_of_components[OF u]
from u d have c: "c ∈⇩∘ 𝔅⦇Obj⦈" and 𝔉d: "(𝔉⦇ObjMap⦈⦇d⦈) ∈⇩∘ 𝔅⦇Obj⦈"
by (auto intro: cat_cs_intros)
show "vfsequence (umap_of 𝔉 c r u d)" unfolding umap_of_def by simp
show "vcard (umap_of 𝔉 c r u d) = 3⇩ℕ"
unfolding umap_of_def by (simp add: nat_omega_simps)
from umap_of_ArrVal_vrange[OF u] show
"ℛ⇩∘ (umap_of 𝔉 c r u d⦇ArrVal⦈) ⊆⇩∘ umap_of 𝔉 c r u d⦇ArrCod⦈"
unfolding umap_of_components by simp
from r d show "umap_of 𝔉 c r u d⦇ArrDom⦈ ∈⇩∘ Vset α"
unfolding umap_of_components by (intro HomDom.cat_Hom_in_Vset)
from c 𝔉d show "umap_of 𝔉 c r u d⦇ArrCod⦈ ∈⇩∘ Vset α"
unfolding umap_of_components by (intro HomCod.cat_Hom_in_Vset)
qed (auto simp: umap_of_components[OF u])
lemma (in is_functor) cf_arr_Set_umap_fo:
assumes "category α 𝔄"
and "category α 𝔅"
and r: "r ∈⇩∘ 𝔄⦇Obj⦈"
and d: "d ∈⇩∘ 𝔄⦇Obj⦈"
and u: "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "arr_Set α (umap_fo 𝔉 c r u d)"
proof-
from assms(1) have 𝔄: "category α (op_cat 𝔄)"
by (auto intro: cat_cs_intros)
from assms(2) have 𝔅: "category α (op_cat 𝔅)"
by (auto intro: cat_cs_intros)
show ?thesis
by
(
rule
is_functor.cf_arr_Set_umap_of[
OF is_functor_op, unfolded cat_op_simps, OF 𝔄 𝔅 r d u
]
)
qed
lemma (in is_functor) cf_umap_of_is_arr:
assumes "category α 𝔄"
and "category α 𝔅"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "d ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "umap_of 𝔉 c r u d : Hom 𝔄 r d ↦⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇d⦈)"
proof(intro cat_Set_is_arrI)
show "arr_Set α (umap_of 𝔉 c r u d)"
by (rule cf_arr_Set_umap_of[OF assms])
qed (simp_all add: umap_of_components[OF assms(5)])
lemma (in is_functor) cf_umap_of_is_arr':
assumes "category α 𝔄"
and "category α 𝔅"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "d ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
and "A = Hom 𝔄 r d"
and "B = Hom 𝔅 c (𝔉⦇ObjMap⦈⦇d⦈)"
and "ℭ = cat_Set α"
shows "umap_of 𝔉 c r u d : A ↦⇘ℭ⇙ B"
using assms(1-5) unfolding assms(6-8) by (rule cf_umap_of_is_arr)
lemmas [cat_cs_intros] = is_functor.cf_umap_of_is_arr'
lemma (in is_functor) cf_umap_fo_is_arr:
assumes "category α 𝔄"
and "category α 𝔅"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "d ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "umap_fo 𝔉 c r u d : Hom 𝔄 d r ↦⇘cat_Set α⇙ Hom 𝔅 (𝔉⦇ObjMap⦈⦇d⦈) c"
proof(intro cat_Set_is_arrI)
show "arr_Set α (umap_fo 𝔉 c r u d)"
by (rule cf_arr_Set_umap_fo[OF assms])
qed (simp_all add: umap_fo_components[OF assms(5)])
lemma (in is_functor) cf_umap_fo_is_arr':
assumes "category α 𝔄"
and "category α 𝔅"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "d ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
and "A = Hom 𝔄 d r"
and "B = Hom 𝔅 (𝔉⦇ObjMap⦈⦇d⦈) c"
and "ℭ = cat_Set α"
shows "umap_fo 𝔉 c r u d : A ↦⇘ℭ⇙ B"
using assms(1-5) unfolding assms(6-8) by (rule cf_umap_fo_is_arr)
lemmas [cat_cs_intros] = is_functor.cf_umap_fo_is_arr'
subsection‹Universal arrow: definition and elementary properties›
text‹See Chapter III-1 in \<^cite>‹"mac_lane_categories_2010"›.›
definition universal_arrow_of :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "universal_arrow_of 𝔉 c r u ⟷
(
r ∈⇩∘ 𝔉⦇HomDom⦈⦇Obj⦈ ∧
u : c ↦⇘𝔉⦇HomCod⦈⇙ 𝔉⦇ObjMap⦈⦇r⦈ ∧
(
∀r' u'.
r' ∈⇩∘ 𝔉⦇HomDom⦈⦇Obj⦈ ⟶
u' : c ↦⇘𝔉⦇HomCod⦈⇙ 𝔉⦇ObjMap⦈⦇r'⦈ ⟶
(∃!f'. f' : r ↦⇘𝔉⦇HomDom⦈⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈)
)
)"
definition universal_arrow_fo :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "universal_arrow_fo 𝔉 c r u ≡ universal_arrow_of (op_cf 𝔉) c r u"
text‹Rules.›
mk_ide (in is_functor) rf
universal_arrow_of_def[where 𝔉=𝔉, unfolded cf_HomDom cf_HomCod]
|intro universal_arrow_ofI|
|dest universal_arrow_ofD[dest]|
|elim universal_arrow_ofE[elim]|
lemma (in is_functor) universal_arrow_foI:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
and "⋀r' u'. ⟦ r' ∈⇩∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔅⇙ c ⟧ ⟹
∃!f'. f' : r' ↦⇘𝔄⇙ r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
shows "universal_arrow_fo 𝔉 c r u"
by
(
simp add:
is_functor.universal_arrow_ofI
[
OF is_functor_op,
folded universal_arrow_fo_def,
unfolded cat_op_simps,
OF assms
]
)
lemma (in is_functor) universal_arrow_foD[dest]:
assumes "universal_arrow_fo 𝔉 c r u"
shows "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
and "⋀r' u'. ⟦ r' ∈⇩∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔅⇙ c ⟧ ⟹
∃!f'. f' : r' ↦⇘𝔄⇙ r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
by
(
auto simp:
is_functor.universal_arrow_ofD
[
OF is_functor_op,
folded universal_arrow_fo_def,
unfolded cat_op_simps,
OF assms
]
)
lemma (in is_functor) universal_arrow_foE[elim]:
assumes "universal_arrow_fo 𝔉 c r u"
obtains "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
and "⋀r' u'. ⟦ r' ∈⇩∘ 𝔄⦇Obj⦈; u' : 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔅⇙ c ⟧ ⟹
∃!f'. f' : r' ↦⇘𝔄⇙ r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
using assms by (auto simp: universal_arrow_foD)
text‹Elementary properties.›
lemma (in is_functor) op_cf_universal_arrow_of[cat_op_simps]:
"universal_arrow_of (op_cf 𝔉) c r u ⟷ universal_arrow_fo 𝔉 c r u"
unfolding universal_arrow_fo_def ..
lemma (in is_functor) op_cf_universal_arrow_fo[cat_op_simps]:
"universal_arrow_fo (op_cf 𝔉) c r u ⟷ universal_arrow_of 𝔉 c r u"
unfolding universal_arrow_fo_def cat_op_simps ..
lemmas (in is_functor) [cat_op_simps] =
is_functor.op_cf_universal_arrow_of
is_functor.op_cf_universal_arrow_fo
subsection‹Uniqueness›
text‹
The following properties are related to the uniqueness of the
universal arrow. These properties can be inferred from the content of
Chapter III-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
lemma (in is_functor) cf_universal_arrow_of_ex_is_iso_arr:
assumes "universal_arrow_of 𝔉 c r u" and "universal_arrow_of 𝔉 c r' u'"
obtains f where "f : r ↦⇩i⇩s⇩o⇘𝔄⇙ r'" and "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
proof-
note ua1 = universal_arrow_ofD[OF assms(1)]
note ua2 = universal_arrow_ofD[OF assms(2)]
from ua1(1) have 𝔄r: "𝔄⦇CId⦈⦇r⦈ : r ↦⇘𝔄⇙ r" by (auto intro: cat_cs_intros)
from ua1(1) have "𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇r⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇r⦈⦈"
by (auto intro: cat_cs_intros)
with ua1(1,2) have u_def: "u = umap_of 𝔉 c r u r⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈"
unfolding umap_of_ArrVal_app[OF 𝔄r ua1(2)] by (auto simp: cat_cs_simps)
from ua2(1) have 𝔄r': "𝔄⦇CId⦈⦇r'⦈ : r' ↦⇘𝔄⇙ r'" by (auto intro: cat_cs_intros)
from ua2(1) have "𝔉⦇ArrMap⦈⦇𝔄⦇CId⦈⦇r'⦈⦈ = 𝔅⦇CId⦈⦇𝔉⦇ObjMap⦈⦇r'⦈⦈"
by (auto intro: cat_cs_intros)
with ua2(1,2) have u'_def: "u' = umap_of 𝔉 c r' u' r'⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r'⦈⦈"
unfolding umap_of_ArrVal_app[OF 𝔄r' ua2(2)] by (auto simp: cat_cs_simps)
from 𝔄r u_def universal_arrow_ofD(3)[OF assms(1) ua1(1,2)] have eq_CId_rI:
"⟦ f' : r ↦⇘𝔄⇙ r; u = umap_of 𝔉 c r u r⦇ArrVal⦈⦇f'⦈ ⟧ ⟹ f' = 𝔄⦇CId⦈⦇r⦈"
for f'
by blast
from 𝔄r' u'_def universal_arrow_ofD(3)[OF assms(2) ua2(1,2)] have eq_CId_r'I:
"⟦ f' : r' ↦⇘𝔄⇙ r'; u' = umap_of 𝔉 c r' u' r'⦇ArrVal⦈⦇f'⦈ ⟧ ⟹
f' = 𝔄⦇CId⦈⦇r'⦈"
for f'
by blast
from ua1(3)[OF ua2(1,2)] obtain f
where f: "f : r ↦⇘𝔄⇙ r'"
and u'_def: "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
and "g : r ↦⇘𝔄⇙ r' ⟹ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇g⦈ ⟹ f = g"
for g
by metis
from ua2(3)[OF ua1(1,2)] obtain f'
where f': "f' : r' ↦⇘𝔄⇙ r"
and u_def: "u = umap_of 𝔉 c r' u' r⦇ArrVal⦈⦇f'⦈"
and "g : r' ↦⇘𝔄⇙ r ⟹ u = umap_of 𝔉 c r' u' r⦇ArrVal⦈⦇g⦈ ⟹ f' = g"
for g
by metis
have "f : r ↦⇩i⇩s⇩o⇘𝔄⇙ r'"
proof(intro is_iso_arrI is_inverseI)
show f: "f : r ↦⇘𝔄⇙ r'" by (rule f)
show f': "f' : r' ↦⇘𝔄⇙ r" by (rule f')
show "f : r ↦⇘𝔄⇙ r'" by (rule f)
from f' have 𝔉f': "𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇r'⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
by (auto intro: cat_cs_intros)
from f have 𝔉f: "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
by (auto intro: cat_cs_intros)
note u'_def' = u'_def[symmetric, unfolded umap_of_ArrVal_app[OF f ua1(2)]]
and u_def' = u_def[symmetric, unfolded umap_of_ArrVal_app[OF f' ua2(2)]]
show "f' ∘⇩A⇘𝔄⇙ f = 𝔄⦇CId⦈⦇r⦈"
proof(rule eq_CId_rI)
from f f' show f'f: "f' ∘⇩A⇘𝔄⇙ f : r ↦⇘𝔄⇙ r"
by (auto intro: cat_cs_intros)
from ua1(2) 𝔉f' 𝔉f show "u = umap_of 𝔉 c r u r⦇ArrVal⦈⦇f' ∘⇩A⇘𝔄⇙ f⦈"
unfolding umap_of_ArrVal_app[OF f'f ua1(2)] cf_ArrMap_Comp[OF f' f]
by (simp add: HomCod.cat_Comp_assoc u'_def' u_def')
qed
show "f ∘⇩A⇘𝔄⇙ f' = 𝔄⦇CId⦈⦇r'⦈"
proof(rule eq_CId_r'I)
from f f' show ff': "f ∘⇩A⇘𝔄⇙ f' : r' ↦⇘𝔄⇙ r'"
by (auto intro: cat_cs_intros)
from ua2(2) 𝔉f' 𝔉f show "u' = umap_of 𝔉 c r' u' r'⦇ArrVal⦈⦇f ∘⇩A⇘𝔄⇙ f'⦈"
unfolding umap_of_ArrVal_app[OF ff' ua2(2)] cf_ArrMap_Comp[OF f f']
by (simp add: HomCod.cat_Comp_assoc u'_def' u_def')
qed
qed
with u'_def that show ?thesis by auto
qed
lemma (in is_functor) cf_universal_arrow_fo_ex_is_iso_arr:
assumes "universal_arrow_fo 𝔉 c r u"
and "universal_arrow_fo 𝔉 c r' u'"
obtains f where "f : r' ↦⇩i⇩s⇩o⇘𝔄⇙ r" and "u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
by
(
elim
is_functor.cf_universal_arrow_of_ex_is_iso_arr[
OF is_functor_op, unfolded cat_op_simps, OF assms
]
)
lemma (in is_functor) cf_universal_arrow_of_unique:
assumes "universal_arrow_of 𝔉 c r u"
and "universal_arrow_of 𝔉 c r' u'"
shows "∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
proof-
note ua1 = universal_arrow_ofD[OF assms(1)]
note ua2 = universal_arrow_ofD[OF assms(2)]
from ua1(3)[OF ua2(1,2)] show ?thesis .
qed
lemma (in is_functor) cf_universal_arrow_fo_unique:
assumes "universal_arrow_fo 𝔉 c r u"
and "universal_arrow_fo 𝔉 c r' u'"
shows "∃!f'. f' : r' ↦⇘𝔄⇙ r ∧ u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
proof-
note ua1 = universal_arrow_foD[OF assms(1)]
note ua2 = universal_arrow_foD[OF assms(2)]
from ua1(3)[OF ua2(1,2)] show ?thesis .
qed
lemma (in is_functor) cf_universal_arrow_of_is_iso_arr:
assumes "universal_arrow_of 𝔉 c r u"
and "universal_arrow_of 𝔉 c r' u'"
and "f : r ↦⇘𝔄⇙ r'"
and "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
shows "f : r ↦⇩i⇩s⇩o⇘𝔄⇙ r'"
proof-
from assms(3,4) cf_universal_arrow_of_unique[OF assms(1,2)] have eq:
"g : r ↦⇘𝔄⇙ r' ⟹ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇g⦈ ⟹ f = g" for g
by blast
from assms(1,2) obtain f'
where iso_f': "f' : r ↦⇩i⇩s⇩o⇘𝔄⇙ r'"
and u'_def: "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
by (auto elim: cf_universal_arrow_of_ex_is_iso_arr)
then have f': "f' : r ↦⇘𝔄⇙ r'" by auto
from iso_f' show ?thesis unfolding eq[OF f' u'_def, symmetric].
qed
lemma (in is_functor) cf_universal_arrow_fo_is_iso_arr:
assumes "universal_arrow_fo 𝔉 c r u"
and "universal_arrow_fo 𝔉 c r' u'"
and "f : r' ↦⇘𝔄⇙ r"
and "u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
shows "f : r' ↦⇩i⇩s⇩o⇘𝔄⇙ r"
by
(
rule
is_functor.cf_universal_arrow_of_is_iso_arr[
OF is_functor_op, unfolded cat_op_simps, OF assms
]
)
lemma (in is_functor) universal_arrow_of_if_universal_arrow_of:
assumes "universal_arrow_of 𝔉 c r u"
and "f : r ↦⇩i⇩s⇩o⇘𝔄⇙ r'"
and "u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
shows "universal_arrow_of 𝔉 c r' u'"
proof(intro universal_arrow_ofI assms(2))
note ua = universal_arrow_ofD[OF assms(1)]
note f = is_iso_arrD(1)[OF assms(2)]
from assms(3) ua(1,2) f have u'_def: "u' = 𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ u"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from ua(2) f show u': "u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
unfolding u'_def by (cs_concl cs_intro: cat_cs_intros)
from f(1) show "r' ∈⇩∘ 𝔄⦇Obj⦈" by auto
fix r'' u'' assume prems: "r'' ∈⇩∘ 𝔄⦇Obj⦈" "u'' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r''⦈"
from ua(3)[OF prems] obtain f'
where f': "f' : r ↦⇘𝔄⇙ r''"
and u''_def: "u'' = umap_of 𝔉 c r u r''⦇ArrVal⦈⦇f'⦈"
and f'_unique: "⋀f''.
⟦ f'' : r ↦⇘𝔄⇙ r''; u'' = umap_of 𝔉 c r u r''⦇ArrVal⦈⦇f''⦈ ⟧ ⟹
f'' = f'"
by metis
from u''_def f' ua(2) have [cat_cs_simps]: "𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ u = u''"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros) simp
show "∃!f'. f' : r' ↦⇘𝔄⇙ r'' ∧ u'' = umap_of 𝔉 c r' u' r''⦇ArrVal⦈⦇f'⦈"
proof(intro ex1I conjI; (elim conjE)?)
from f' assms(2) f show "f' ∘⇩A⇘𝔄⇙ f¯⇩C⇘𝔄⇙ : r' ↦⇘𝔄⇙ r''"
by (cs_concl cs_intro: cat_cs_intros cat_arrow_cs_intros)
have
"𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ ∘⇩A⇘𝔅⇙ u') =
𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ u))"
unfolding u'_def ..
also from f' assms(2) u' f ua(2) have
"… = 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙ ∘⇩A⇘𝔄⇙ f⦈) ∘⇩A⇘𝔅⇙ u"
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_arrow_cs_intros cat_cs_intros
)
also from f' assms(2) f ua(2) have "… = u''"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
finally have [cat_cs_simps]:
"𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ (𝔉⦇ArrMap⦈⦇f¯⇩C⇘𝔄⇙⦈ ∘⇩A⇘𝔅⇙ u') = u''".
from f' assms(2) u' f show
"u'' = umap_of 𝔉 c r' u' r''⦇ArrVal⦈⦇f' ∘⇩A⇘𝔄⇙ f¯⇩C⇘𝔄⇙⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_arrow_cs_intros
)
fix g assume prems':
"g : r' ↦⇘𝔄⇙ r''" "u'' = umap_of 𝔉 c r' u' r''⦇ArrVal⦈⦇g⦈"
from prems'(1) f have gf: "g ∘⇩A⇘𝔄⇙ f : r ↦⇘𝔄⇙ r''"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from prems'(2,1) assms(2) u' have "u'' = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ u'"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
also from prems'(1) f ua(2) have
"… = 𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ 𝔉⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔅⇙ u"
by (cs_concl cs_simp: cat_cs_simps u'_def u''_def cs_intro: cat_cs_intros)
also from prems'(1) f ua(2) have
"… = umap_of 𝔉 c r u r''⦇ArrVal⦈⦇g ∘⇩A⇘𝔄⇙ f⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
finally have "u'' = umap_of 𝔉 c r u r''⦇ArrVal⦈⦇g ∘⇩A⇘𝔄⇙ f⦈".
from f'_unique[OF gf this] have "g ∘⇩A⇘𝔄⇙ f = f'".
then have "(g ∘⇩A⇘𝔄⇙ f) ∘⇩A⇘𝔄⇙ f¯⇩C⇘𝔄⇙ = f' ∘⇩A⇘𝔄⇙ f¯⇩C⇘𝔄⇙" by simp
from this assms(2) prems'(1) u' f ua(2) show "g = f' ∘⇩A⇘𝔄⇙ f¯⇩C⇘𝔄⇙"
by
(
cs_prems
cs_simp: cat_cs_simps cs_intro: cat_arrow_cs_intros cat_cs_intros
)
qed
qed
lemma (in is_functor) universal_arrow_fo_if_universal_arrow_fo:
assumes "universal_arrow_fo 𝔉 c r u"
and "f : r' ↦⇩i⇩s⇩o⇘𝔄⇙ r"
and "u' = umap_fo 𝔉 c r u r'⦇ArrVal⦈⦇f⦈"
shows "universal_arrow_fo 𝔉 c r' u'"
by
(
rule is_functor.universal_arrow_of_if_universal_arrow_of[
OF is_functor_op, unfolded cat_op_simps, OF assms
]
)
subsection‹Universal natural transformation›
subsubsection‹Definition and elementary properties›
text‹
The concept of the universal natural transformation is introduced for the
statement of the elements of a variant of Proposition 1 in Chapter III-2
in \<^cite>‹"mac_lane_categories_2010"›.
›
definition ntcf_ua_of :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "ntcf_ua_of α 𝔉 c r u =
[
(λd∈⇩∘𝔉⦇HomDom⦈⦇Obj⦈. umap_of 𝔉 c r u d),
Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomDom⦈(r,-),
Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomCod⦈(c,-) ∘⇩C⇩F 𝔉,
𝔉⦇HomDom⦈,
cat_Set α
]⇩∘"
definition ntcf_ua_fo :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "ntcf_ua_fo α 𝔉 c r u = ntcf_ua_of α (op_cf 𝔉) c r u"
text‹Components.›
lemma ntcf_ua_of_components:
shows "ntcf_ua_of α 𝔉 c r u⦇NTMap⦈ = (λd∈⇩∘𝔉⦇HomDom⦈⦇Obj⦈. umap_of 𝔉 c r u d)"
and "ntcf_ua_of α 𝔉 c r u⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomDom⦈(r,-)"
and "ntcf_ua_of α 𝔉 c r u⦇NTCod⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomCod⦈(c,-) ∘⇩C⇩F 𝔉"
and "ntcf_ua_of α 𝔉 c r u⦇NTDGDom⦈ = 𝔉⦇HomDom⦈"
and "ntcf_ua_of α 𝔉 c r u⦇NTDGCod⦈ = cat_Set α"
unfolding ntcf_ua_of_def nt_field_simps by (simp_all add: nat_omega_simps)
lemma ntcf_ua_fo_components:
shows "ntcf_ua_fo α 𝔉 c r u⦇NTMap⦈ = (λd∈⇩∘𝔉⦇HomDom⦈⦇Obj⦈. umap_fo 𝔉 c r u d)"
and "ntcf_ua_fo α 𝔉 c r u⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙op_cat (𝔉⦇HomDom⦈)(r,-)"
and "ntcf_ua_fo α 𝔉 c r u⦇NTCod⦈ =
Hom⇩O⇩.⇩C⇘α⇙op_cat (𝔉⦇HomCod⦈)(c,-) ∘⇩C⇩F op_cf 𝔉"
and "ntcf_ua_fo α 𝔉 c r u⦇NTDGDom⦈ = op_cat (𝔉⦇HomDom⦈)"
and "ntcf_ua_fo α 𝔉 c r u⦇NTDGCod⦈ = cat_Set α"
unfolding ntcf_ua_fo_def ntcf_ua_of_components umap_fo_def cat_op_simps
by simp_all
context is_functor
begin
lemmas ntcf_ua_of_components' =
ntcf_ua_of_components[where α=α and 𝔉=𝔉, unfolded cat_cs_simps]
lemmas [cat_cs_simps] = ntcf_ua_of_components'(2-5)
lemma ntcf_ua_fo_components':
assumes "c ∈⇩∘ 𝔅⦇Obj⦈" and "r ∈⇩∘ 𝔄⦇Obj⦈"
shows "ntcf_ua_fo α 𝔉 c r u⦇NTMap⦈ = (λd∈⇩∘𝔄⦇Obj⦈. umap_fo 𝔉 c r u d)"
and [cat_cs_simps]:
"ntcf_ua_fo α 𝔉 c r u⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔄(-,r)"
and [cat_cs_simps]:
"ntcf_ua_fo α 𝔉 c r u⦇NTCod⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔅(-,c) ∘⇩C⇩F op_cf 𝔉"
and [cat_cs_simps]: "ntcf_ua_fo α 𝔉 c r u⦇NTDGDom⦈ = op_cat 𝔄"
and [cat_cs_simps]: "ntcf_ua_fo α 𝔉 c r u⦇NTDGCod⦈ = cat_Set α"
unfolding
ntcf_ua_fo_components cat_cs_simps
HomDom.cat_op_cat_cf_Hom_snd[OF assms(2)]
HomCod.cat_op_cat_cf_Hom_snd[OF assms(1)]
by simp_all
end
lemmas [cat_cs_simps] =
is_functor.ntcf_ua_of_components'(2-5)
is_functor.ntcf_ua_fo_components'(2-5)
subsubsection‹Natural transformation map›
mk_VLambda (in is_functor)
ntcf_ua_of_components(1)[where α=α and 𝔉=𝔉, unfolded cf_HomDom]
|vsv ntcf_ua_of_NTMap_vsv|
|vdomain ntcf_ua_of_NTMap_vdomain|
|app ntcf_ua_of_NTMap_app|
context is_functor
begin
context
fixes c r
assumes r: "r ∈⇩∘ 𝔄⦇Obj⦈" and c: "c ∈⇩∘ 𝔅⦇Obj⦈"
begin
mk_VLambda ntcf_ua_fo_components'(1)[OF c r]
|vsv ntcf_ua_fo_NTMap_vsv|
|vdomain ntcf_ua_fo_NTMap_vdomain|
|app ntcf_ua_fo_NTMap_app|
end
end
lemmas [cat_cs_intros] =
is_functor.ntcf_ua_fo_NTMap_vsv
is_functor.ntcf_ua_of_NTMap_vsv
lemmas [cat_cs_simps] =
is_functor.ntcf_ua_fo_NTMap_vdomain
is_functor.ntcf_ua_fo_NTMap_app
is_functor.ntcf_ua_of_NTMap_vdomain
is_functor.ntcf_ua_of_NTMap_app
lemma (in is_functor) ntcf_ua_of_NTMap_vrange:
assumes "category α 𝔄"
and "category α 𝔅"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "ℛ⇩∘ (ntcf_ua_of α 𝔉 c r u⦇NTMap⦈) ⊆⇩∘ cat_Set α⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold ntcf_ua_of_NTMap_vdomain)
show "vsv (ntcf_ua_of α 𝔉 c r u⦇NTMap⦈)" by (rule ntcf_ua_of_NTMap_vsv)
fix d assume prems: "d ∈⇩∘ 𝔄⦇Obj⦈"
with category_cat_Set is_functor_axioms assms show
"ntcf_ua_of α 𝔉 c r u⦇NTMap⦈⦇d⦈ ∈⇩∘ cat_Set α⦇Arr⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
subsubsection‹Commutativity of the universal maps and ‹hom›-functions›
lemma (in is_functor) cf_umap_of_cf_hom_commute:
assumes "category α 𝔄"
and "category α 𝔅"
and "c ∈⇩∘ 𝔅⦇Obj⦈"
and "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
and "f : a ↦⇘𝔄⇙ b"
shows
"umap_of 𝔉 c r u b ∘⇩A⇘cat_Set α⇙ cf_hom 𝔄 [𝔄⦇CId⦈⦇r⦈, f]⇩∘ =
cf_hom 𝔅 [𝔅⦇CId⦈⦇c⦈, 𝔉⦇ArrMap⦈⦇f⦈]⇩∘ ∘⇩A⇘cat_Set α⇙ umap_of 𝔉 c r u a"
(is ‹?uof_b ∘⇩A⇘cat_Set α⇙ ?rf = ?cf ∘⇩A⇘cat_Set α⇙ ?uof_a›)
proof-
from is_functor_axioms category_cat_Set assms(1,2,4-6) have b_rf:
"?uof_b ∘⇩A⇘cat_Set α⇙ ?rf : Hom 𝔄 r a ↦⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇b⦈)"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
from is_functor_axioms category_cat_Set assms(1,2,4-6) have cf_a:
"?cf ∘⇩A⇘cat_Set α⇙ ?uof_a : Hom 𝔄 r a ↦⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇b⦈)"
by (cs_concl cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros)
show ?thesis
proof(rule arr_Set_eqI[of α])
from b_rf show arr_Set_b_rf: "arr_Set α (?uof_b ∘⇩A⇘cat_Set α⇙ ?rf)"
by (auto dest: cat_Set_is_arrD(1))
from b_rf have dom_lhs:
"𝒟⇩∘ ((?uof_b ∘⇩A⇘cat_Set α⇙ ?rf)⦇ArrVal⦈) = Hom 𝔄 r a"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
from cf_a show arr_Set_cf_a: "arr_Set α (?cf ∘⇩A⇘cat_Set α⇙ ?uof_a)"
by (auto dest: cat_Set_is_arrD(1))
from cf_a have dom_rhs:
"𝒟⇩∘ ((?cf ∘⇩A⇘cat_Set α⇙ ?uof_a)⦇ArrVal⦈) = Hom 𝔄 r a"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "(?uof_b ∘⇩A⇘cat_Set α⇙ ?rf)⦇ArrVal⦈ = (?cf ∘⇩A⇘cat_Set α⇙ ?uof_a)⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix q assume "q : r ↦⇘𝔄⇙ a"
with is_functor_axioms category_cat_Set assms show
"(?uof_b ∘⇩A⇘cat_Set α⇙ ?rf)⦇ArrVal⦈⦇q⦈ =
(?cf ∘⇩A⇘cat_Set α⇙ ?uof_a)⦇ArrVal⦈⦇q⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
qed (use arr_Set_b_rf arr_Set_cf_a in auto)
qed (use b_rf cf_a in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
lemma cf_umap_of_cf_hom_unit_commute:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
and "g : c' ↦⇘ℭ⇙ c"
and "f : d ↦⇘𝔇⇙ d'"
shows
"umap_of 𝔊 c' (𝔉⦇ObjMap⦈⦇c'⦈) (η⦇NTMap⦈⦇c'⦈) d' ∘⇩A⇘cat_Set α⇙
cf_hom 𝔇 [𝔉⦇ArrMap⦈⦇g⦈, f]⇩∘ =
cf_hom ℭ [g, 𝔊⦇ArrMap⦈⦇f⦈]⇩∘ ∘⇩A⇘cat_Set α⇙
umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
(is ‹?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf = ?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd›)
proof-
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› η by (rule assms(5))
from assms have c'd'_𝔉gf: "?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇c⦈) d ↦⇘cat_Set α⇙ Hom ℭ c' (𝔊⦇ObjMap⦈⦇d'⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇c⦈) d"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms have g𝔊f_cd: "?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇c⦈) d ↦⇘cat_Set α⇙ Hom ℭ c' (𝔊⦇ObjMap⦈⦇d'⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇c⦈) d"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI[of α])
from c'd'_𝔉gf show arr_Set_c'd'_𝔉gf:
"arr_Set α (?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf)"
by (auto dest: cat_Set_is_arrD(1))
from g𝔊f_cd show arr_Set_g𝔊f_cd:
"arr_Set α (?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd)"
by (auto dest: cat_Set_is_arrD(1))
show
"(?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf)⦇ArrVal⦈ =
(?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd)⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix h assume prems: "h : 𝔉⦇ObjMap⦈⦇c⦈ ↦⇘𝔇⇙ d"
from η.ntcf_Comp_commute[OF assms(6)] assms have [cat_cs_simps]:
"η⦇NTMap⦈⦇c⦈ ∘⇩A⇘ℭ⇙ g = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇g⦈⦈ ∘⇩A⇘ℭ⇙ η⦇NTMap⦈⦇c'⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
from assms prems show
"(?uof_c'd' ∘⇩A⇘cat_Set α⇙ ?𝔉gf)⦇ArrVal⦈⦇h⦈ =
(?g𝔊f ∘⇩A⇘cat_Set α⇙ ?uof_cd)⦇ArrVal⦈⦇h⦈"
by
(
cs_concl
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
cs_simp: cat_cs_simps
)
qed (use arr_Set_c'd'_𝔉gf arr_Set_g𝔊f_cd in auto)
qed (use c'd'_𝔉gf g𝔊f_cd in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
subsubsection‹Universal natural transformation is a natural transformation›
lemma (in is_functor) cf_ntcf_ua_of_is_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
shows "ntcf_ua_of α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
proof(intro is_ntcfI')
let ?ua = ‹ntcf_ua_of α 𝔉 c r u›
show "vfsequence (ntcf_ua_of α 𝔉 c r u)" unfolding ntcf_ua_of_def by simp
show "vcard ?ua = 5⇩ℕ" unfolding ntcf_ua_of_def by (simp add: nat_omega_simps)
from assms(1) show "Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from is_functor_axioms assms(2) show
"Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_intro: cat_cs_intros)
from is_functor_axioms assms show "𝒟⇩∘ (?ua⦇NTMap⦈) = 𝔄⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "?ua⦇NTMap⦈⦇a⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)⦇ObjMap⦈⦇a⦈ ↦⇘cat_Set α⇙ (Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ 𝔄⦇Obj⦈" for a
using is_functor_axioms assms that
by (cs_concl cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros)
show "?ua⦇NTMap⦈⦇b⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)⦇ArrMap⦈⦇f⦈ =
(Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ ?ua⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘𝔄⇙ b" for a b f
using is_functor_axioms assms that
by
(
cs_concl
cs_simp: cf_umap_of_cf_hom_commute cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed (auto simp: ntcf_ua_of_components cat_cs_simps)
lemma (in is_functor) cf_ntcf_ua_fo_is_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈" and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
shows "ntcf_ua_fo α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(-,r) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔅(-,c) ∘⇩C⇩F op_cf 𝔉 :
op_cat 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
from assms(2) have c: "c ∈⇩∘ 𝔅⦇Obj⦈" by auto
show ?thesis
by
(
rule is_functor.cf_ntcf_ua_of_is_ntcf
[
OF is_functor_op,
unfolded cat_op_simps,
OF assms(1,2),
unfolded
HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)]
HomCod.cat_op_cat_cf_Hom_snd[OF c]
ntcf_ua_fo_def[symmetric]
]
)
qed
subsubsection‹Universal natural transformation and universal arrow›
text‹
The lemmas in this subsection correspond to
variants of elements of Proposition 1 in Chapter III-2 in
\<^cite>‹"mac_lane_categories_2010"›.
›
lemma (in is_functor) cf_ntcf_ua_of_is_iso_ntcf:
assumes "universal_arrow_of 𝔉 c r u"
shows "ntcf_ua_of α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
have r: "r ∈⇩∘ 𝔄⦇Obj⦈"
and u: "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
and bij: "⋀r' u'.
⟦
r' ∈⇩∘ 𝔄⦇Obj⦈;
u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈
⟧ ⟹ ∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
by (auto intro!: universal_arrow_ofD[OF assms(1)])
show ?thesis
proof(intro is_iso_ntcfI)
show "ntcf_ua_of α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
by (rule cf_ntcf_ua_of_is_ntcf[OF r u])
fix a assume prems: "a ∈⇩∘ 𝔄⦇Obj⦈"
from is_functor_axioms prems r u have [simp]:
"umap_of 𝔉 c r u a : Hom 𝔄 r a ↦⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇a⦈)"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
then have dom: "𝒟⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈) = Hom 𝔄 r a"
by (cs_concl cs_simp: cat_cs_simps)
have "umap_of 𝔉 c r u a : Hom 𝔄 r a ↦⇩i⇩s⇩o⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇a⦈)"
proof(intro cat_Set_is_iso_arrI, unfold dom)
show umof_a: "v11 (umap_of 𝔉 c r u a⦇ArrVal⦈)"
proof(intro vsv.vsv_valeq_v11I, unfold dom in_Hom_iff)
fix g f assume prems':
"g : r ↦⇘𝔄⇙ a"
"f : r ↦⇘𝔄⇙ a"
"umap_of 𝔉 c r u a⦇ArrVal⦈⦇g⦈ = umap_of 𝔉 c r u a⦇ArrVal⦈⦇f⦈"
from is_functor_axioms r u prems'(1) have 𝔉g:
"𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from bij[OF prems 𝔉g] have unique:
"⟦
f' : r ↦⇘𝔄⇙ a;
𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ u = umap_of 𝔉 c r u a⦇ArrVal⦈⦇f'⦈
⟧ ⟹ g = f'"
for f' by (metis prems'(1) u umap_of_ArrVal_app)
from is_functor_axioms prems'(1,2) u have 𝔉g_u:
"𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔅⇙ u = umap_of 𝔉 c r u a⦇ArrVal⦈⦇f⦈"
by (cs_concl cs_simp: prems'(3)[symmetric] cat_cs_simps)
show "g = f" by (rule unique[OF prems'(2) 𝔉g_u])
qed (auto simp: cat_cs_simps cat_cs_intros)
interpret umof_a: v11 ‹umap_of 𝔉 c r u a⦇ArrVal⦈› by (rule umof_a)
show "ℛ⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈) = Hom 𝔅 c (𝔉⦇ObjMap⦈⦇a⦈)"
proof(intro vsubset_antisym)
from u show "ℛ⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈) ⊆⇩∘ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇a⦈)"
by (rule umap_of_ArrVal_vrange)
show "Hom 𝔅 c (𝔉⦇ObjMap⦈⦇a⦈) ⊆⇩∘ ℛ⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
proof(rule vsubsetI, unfold in_Hom_iff )
fix f assume prems': "f : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇a⦈"
from bij[OF prems prems'] obtain f'
where f': "f' : r ↦⇘𝔄⇙ a"
and f_def: "f = umap_of 𝔉 c r u a⦇ArrVal⦈⦇f'⦈"
by auto
from is_functor_axioms prems prems' u f' have
"f' ∈⇩∘ 𝒟⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from this show "f ∈⇩∘ ℛ⇩∘ (umap_of 𝔉 c r u a⦇ArrVal⦈)"
unfolding f_def by (rule umof_a.vsv_vimageI2)
qed
qed
qed simp_all
from is_functor_axioms prems r u this show
"ntcf_ua_of α 𝔉 c r u⦇NTMap⦈⦇a⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set α⇙
(Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
qed
qed
lemmas [cat_cs_intros] = is_functor.cf_ntcf_ua_of_is_iso_ntcf
lemma (in is_functor) cf_ntcf_ua_fo_is_iso_ntcf:
assumes "universal_arrow_fo 𝔉 c r u"
shows "ntcf_ua_fo α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(-,r) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(-,c) ∘⇩C⇩F op_cf 𝔉 :
op_cat 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
from universal_arrow_foD[OF assms] have r: "r ∈⇩∘ 𝔄⦇Obj⦈" and c: "c ∈⇩∘ 𝔅⦇Obj⦈"
by auto
show ?thesis
by
(
rule is_functor.cf_ntcf_ua_of_is_iso_ntcf
[
OF is_functor_op,
unfolded cat_op_simps,
OF assms,
unfolded
HomDom.cat_op_cat_cf_Hom_snd[OF r]
HomCod.cat_op_cat_cf_Hom_snd[OF c]
ntcf_ua_fo_def[symmetric]
]
)
qed
lemmas [cat_cs_intros] = is_functor.cf_ntcf_ua_fo_is_iso_ntcf
lemma (in is_functor) cf_ua_of_if_ntcf_ua_of_is_iso_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
and "ntcf_ua_of α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
shows "universal_arrow_of 𝔉 c r u"
proof(rule universal_arrow_ofI)
interpret ua_of_u: is_iso_ntcf
α
𝔄
‹cat_Set α›
‹Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)›
‹Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉›
‹ntcf_ua_of α 𝔉 c r u›
by (rule assms(3))
fix r' u' assume prems: "r' ∈⇩∘ 𝔄⦇Obj⦈" "u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
have "ntcf_ua_of α 𝔉 c r u⦇NTMap⦈⦇r'⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)⦇ObjMap⦈⦇r'⦈ ↦⇩i⇩s⇩o⇘cat_Set α⇙
(Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇r'⦈"
by (rule is_iso_ntcf.iso_ntcf_is_iso_arr[OF assms(3) prems(1)])
from this is_functor_axioms assms(1-2) prems have uof_r':
"umap_of 𝔉 c r u r' : Hom 𝔄 r r' ↦⇩i⇩s⇩o⇘cat_Set α⇙ Hom 𝔅 c (𝔉⦇ObjMap⦈⦇r'⦈)"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros)
note uof_r' = cat_Set_is_iso_arrD[OF uof_r']
interpret uof_r': v11 ‹umap_of 𝔉 c r u r'⦇ArrVal⦈› by (rule uof_r'(2))
from
uof_r'.v11_vrange_ex1_eq[
THEN iffD1, unfolded uof_r'(3,4) in_Hom_iff, OF prems(2)
]
show "∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r u r'⦇ArrVal⦈⦇f'⦈"
by metis
qed (intro assms)+
lemma (in is_functor) cf_ua_fo_if_ntcf_ua_fo_is_iso_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "u : 𝔉⦇ObjMap⦈⦇r⦈ ↦⇘𝔅⇙ c"
and "ntcf_ua_fo α 𝔉 c r u :
Hom⇩O⇩.⇩C⇘α⇙𝔄(-,r) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(-,c) ∘⇩C⇩F op_cf 𝔉 :
op_cat 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
shows "universal_arrow_fo 𝔉 c r u"
proof-
from assms(2) have c: "c ∈⇩∘ 𝔅⦇Obj⦈" by auto
show ?thesis
by
(
rule is_functor.cf_ua_of_if_ntcf_ua_of_is_iso_ntcf
[
OF is_functor_op,
unfolded cat_op_simps,
OF assms(1,2),
unfolded
HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)]
HomCod.cat_op_cat_cf_Hom_snd[OF c]
ntcf_ua_fo_def[symmetric],
OF assms(3)
]
)
qed
lemma (in is_functor) cf_universal_arrow_of_if_is_iso_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "c ∈⇩∘ 𝔅⦇Obj⦈"
and "φ :
Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉 : 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
shows "universal_arrow_of 𝔉 c r (φ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈)"
(is ‹universal_arrow_of 𝔉 c r ?u›)
proof-
interpret φ: is_iso_ntcf
α 𝔄 ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)› ‹Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉› φ
by (rule assms(3))
show ?thesis
proof(intro universal_arrow_ofI assms)
from assms(1,2) show u: "?u : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
fix r' u' assume prems: "r' ∈⇩∘ 𝔄⦇Obj⦈" "u' : c ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇r'⦈"
have φr'_ArrVal_app[symmetric, cat_cs_simps]:
"φ⦇NTMap⦈⦇r'⦈⦇ArrVal⦈⦇f'⦈ =
𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ φ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈"
if "f' : r ↦⇘𝔄⇙ r'" for f'
proof-
have "φ⦇NTMap⦈⦇r'⦈ ∘⇩A⇘cat_Set α⇙ Hom⇩O⇩.⇩C⇘α⇙𝔄(r,-)⦇ArrMap⦈⦇f'⦈ =
(Hom⇩O⇩.⇩C⇘α⇙𝔅(c,-) ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘cat_Set α⇙ φ⦇NTMap⦈⦇r⦈"
using that by (intro φ.ntcf_Comp_commute)
then have
"φ⦇NTMap⦈⦇r'⦈ ∘⇩A⇘cat_Set α⇙ cf_hom 𝔄 [𝔄⦇CId⦈⦇r⦈, f']⇩∘ =
cf_hom 𝔅 [𝔅⦇CId⦈⦇c⦈, 𝔉⦇ArrMap⦈⦇f'⦈]⇩∘ ∘⇩A⇘cat_Set α⇙ φ⦇NTMap⦈⦇r⦈"
using assms(1,2) that prems
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_op_simps cs_intro: cat_cs_intros
)
then have
"(φ⦇NTMap⦈⦇r'⦈ ∘⇩A⇘cat_Set α⇙
cf_hom 𝔄 [𝔄⦇CId⦈⦇r⦈, f']⇩∘)⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈ =
(cf_hom 𝔅 [𝔅⦇CId⦈⦇c⦈, 𝔉⦇ArrMap⦈⦇f'⦈]⇩∘ ∘⇩A⇘cat_Set α⇙
φ⦇NTMap⦈⦇r⦈)⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈"
by simp
from this assms(1,2) u that show ?thesis
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
qed
show "∃!f'. f' : r ↦⇘𝔄⇙ r' ∧ u' = umap_of 𝔉 c r ?u r'⦇ArrVal⦈⦇f'⦈"
proof(intro ex1I conjI; (elim conjE)?)
from assms prems show
"(φ⦇NTMap⦈⦇r'⦈)¯⇩C⇘cat_Set α⇙⦇ArrVal⦈⦇u'⦈ : r ↦⇘𝔄⇙ r'"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_arrow_cs_intros
)
with assms(1,2) prems show "u' =
umap_of 𝔉 c r ?u r'⦇ArrVal⦈⦇(φ⦇NTMap⦈⦇r'⦈)¯⇩C⇘cat_Set α⇙⦇ArrVal⦈⦇u'⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
)
fix f' assume prems':
"f' : r ↦⇘𝔄⇙ r'"
"u' = umap_of 𝔉 c r (φ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈) r'⦇ArrVal⦈⦇f'⦈"
from prems'(2,1) assms(1,2) have u'_def:
"u' = 𝔉⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘𝔅⇙ φ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
from prems' show "f' = (φ⦇NTMap⦈⦇r'⦈)¯⇩C⇘cat_Set α⇙⦇ArrVal⦈⦇u'⦈"
unfolding u'_def φr'_ArrVal_app[OF prems'(1)]
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_arrow_cs_intros cat_cs_intros cat_op_intros
)
qed
qed
qed
lemma (in is_functor) cf_universal_arrow_fo_if_is_iso_ntcf:
assumes "r ∈⇩∘ 𝔄⦇Obj⦈"
and "c ∈⇩∘ 𝔅⦇Obj⦈"
and "φ :
Hom⇩O⇩.⇩C⇘α⇙𝔄(-,r) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙𝔅(-,c) ∘⇩C⇩F op_cf 𝔉 :
op_cat 𝔄 ↦↦⇩C⇘α⇙ cat_Set α"
shows "universal_arrow_fo 𝔉 c r (φ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇𝔄⦇CId⦈⦇r⦈⦈)"
by
(
rule is_functor.cf_universal_arrow_of_if_is_iso_ntcf
[
OF is_functor_op,
unfolded cat_op_simps,
OF assms(1,2),
unfolded
HomDom.cat_op_cat_cf_Hom_snd[OF assms(1)]
HomCod.cat_op_cat_cf_Hom_snd[OF assms(2)]
ntcf_ua_fo_def[symmetric],
OF assms(3)
]
)
text‹\newpage›
end