Theory CZH_UCAT_Representable
section‹Representable and corepresentable functors›
theory CZH_UCAT_Representable
imports
CZH_Elementary_Categories.CZH_ECAT_Yoneda
CZH_UCAT_Pointed
CZH_UCAT_Limit
begin
subsection‹Representable and corepresentable functors›
subsubsection‹Definitions and elementary properties›
text‹
See Chapter III-2 in \<^cite>‹"mac_lane_categories_2010"›
or Section 2.1 in \<^cite>‹"riehl_category_2016"›.
›
definition cat_representation :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "cat_representation α 𝔉 c ψ ⟷
c ∈⇩∘ 𝔉⦇HomDom⦈⦇Obj⦈ ∧
ψ : Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomDom⦈(c,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔉⦇HomDom⦈ ↦↦⇩C⇘α⇙ cat_Set α"
definition cat_corepresentation :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
where "cat_corepresentation α 𝔉 c ψ ⟷
c ∈⇩∘ 𝔉⦇HomDom⦈⦇Obj⦈ ∧
ψ : Hom⇩O⇩.⇩C⇘α⇙op_cat (𝔉⦇HomDom⦈)(-,c) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : 𝔉⦇HomDom⦈ ↦↦⇩C⇘α⇙ cat_Set α"
text‹Rules.›
context
fixes α ℭ 𝔉
assumes 𝔉: "𝔉 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
begin
interpretation 𝔉: is_functor α ℭ ‹cat_Set α› 𝔉 by (rule 𝔉)
mk_ide rf cat_representation_def[where α=α and 𝔉=𝔉, unfolded cat_cs_simps]
|intro cat_representationI|
|dest cat_representationD'|
|elim cat_representationE'|
end
lemmas cat_representationD[dest] = cat_representationD'[rotated]
and cat_representationE[elim] = cat_representationE'[rotated]
lemma cat_corepresentationI:
assumes "category α ℭ"
and "𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "ψ : Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
shows "cat_corepresentation α 𝔉 c ψ"
proof-
interpret category α ℭ by (rule assms(1))
interpret 𝔉: is_functor α ‹op_cat ℭ› ‹cat_Set α› 𝔉 by (rule assms(2))
note [cat_op_simps] = 𝔉.HomDom.cat_op_cat_cf_Hom_snd[
symmetric, unfolded cat_op_simps, OF assms(3)
]
show ?thesis
unfolding cat_corepresentation_def
by (intro conjI, unfold cat_cs_simps cat_op_simps; intro assms)
qed
lemma cat_corepresentationD:
assumes "cat_corepresentation α 𝔉 c ψ"
and "category α ℭ"
and "𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
shows "c ∈⇩∘ ℭ⦇Obj⦈"
and "ψ : Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
proof-
interpret category α ℭ by (rule assms(2))
interpret 𝔉: is_functor α ‹op_cat ℭ› ‹cat_Set α› 𝔉 by (rule assms(3))
note cψ = cat_corepresentation_def[
THEN iffD1, OF assms(1), unfolded cat_cs_simps cat_op_simps
]
from cψ(1) show c: "c ∈⇩∘ ℭ⦇Obj⦈" by auto
note [cat_op_simps] = 𝔉.HomDom.cat_op_cat_cf_Hom_snd[
symmetric, unfolded cat_op_simps, OF c
]
show "ψ : Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (rule conjunct2[OF cψ, unfolded cat_op_simps])
qed
lemma cat_corepresentationE:
assumes "cat_corepresentation α 𝔉 c ψ"
and "category α ℭ"
and "𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
obtains "c ∈⇩∘ ℭ⦇Obj⦈"
and "ψ : Hom⇩O⇩.⇩C⇘α⇙ℭ(-,c) ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (simp add: cat_corepresentationD[OF assms])
subsubsection‹Representable functors and universal arrows›
lemma universal_arrow_of_if_cat_representation:
assumes "𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
and "cat_representation α 𝔎 r ψ"
and "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
shows "universal_arrow_of
𝔎 (set {𝔞}) r (ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇r⦈) (ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈))"
proof-
note rψ = cat_representationD[OF assms(2,1)]
interpret 𝔎: is_functor α ℭ ‹cat_Set α› 𝔎 by (rule assms(1))
interpret ψ: is_iso_ntcf α ℭ ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)› 𝔎 ψ
by (rule rψ(2))
from assms(3) have set_𝔞: "set {𝔞} ∈⇩∘ cat_Set α⦇Obj⦈"
by (simp add: Limit_vsingleton_in_VsetI cat_Set_components(1))
from
ntcf_cf_comp_is_iso_ntcf[
OF 𝔎.ntcf_pointed_inv_is_iso_ntcf[OF assms(3)] assms(1)
]
have 𝔞𝔎: "ntcf_pointed_inv α 𝔞 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 :
𝔎 ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙cat_Set α (set {𝔞},-) ∘⇩C⇩F 𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_prems cs_simp: cat_cs_simps)
from iso_ntcf_is_iso_arr(1)[OF 𝔞𝔎] rψ assms(3) have [cat_cs_simps]:
"((ntcf_pointed_inv α 𝔞 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔎 ∙⇩N⇩T⇩C⇩F ψ)⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈) =
ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇r⦈) (ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_Set_cs_intros cat_cs_intros cat_op_intros
)
show "universal_arrow_of
𝔎 (set {𝔞}) r (ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇r⦈) (ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈))"
by
(
rule 𝔎.cf_universal_arrow_of_if_is_iso_ntcf
[
OF rψ(1) set_𝔞 ntcf_vcomp_is_iso_ntcf[OF 𝔞𝔎 rψ(2)],
unfolded cat_cs_simps
]
)
qed
lemma universal_arrow_of_if_cat_corepresentation:
assumes "category α ℭ"
and "𝔎 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
and "cat_corepresentation α 𝔎 r ψ"
and "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
shows "universal_arrow_of
𝔎 (set {𝔞}) r (ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇r⦈) (ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈))"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
note rψ = cat_corepresentationD[OF assms(3,1,2)]
note [cat_op_simps] = ℭ.cat_op_cat_cf_Hom_snd[OF rψ(1)]
have rep: "cat_representation α 𝔎 r ψ"
by (intro cat_representationI, rule assms(2), unfold cat_op_simps; rule rψ)
show ?thesis
by
(
rule universal_arrow_of_if_cat_representation[
OF assms(2) rep assms(4), unfolded cat_op_simps
]
)
qed
lemma cat_representation_if_universal_arrow_of:
assumes "𝔎 : ℭ ↦↦⇩C⇘α⇙ cat_Set α"
and "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
and "universal_arrow_of 𝔎 (set {𝔞}) r u"
shows "cat_representation α 𝔎 r (Yoneda_arrow α 𝔎 r (u⦇ArrVal⦈⦇𝔞⦈))"
proof-
let ?Y = ‹Yoneda_component 𝔎 r (u⦇ArrVal⦈⦇𝔞⦈)›
interpret 𝔎: is_functor α ℭ ‹cat_Set α› 𝔎 by (rule assms(1))
note ua = 𝔎.universal_arrow_ofD[OF assms(3)]
from ua(2) have u𝔞: "u⦇ArrVal⦈⦇𝔞⦈ ∈⇩∘ 𝔎⦇ObjMap⦈⦇r⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros
)
have [cat_cs_simps]: "Yoneda_arrow α 𝔎 r (u⦇ArrVal⦈⦇𝔞⦈)⦇NTMap⦈⦇c⦈ = ?Y c"
if "c ∈⇩∘ ℭ⦇Obj⦈" for c
using that
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from ua(1) have [cat_cs_simps]: "Hom⇩O⇩.⇩C⇘α⇙ℭ(r,-)⦇ObjMap⦈⦇c⦈ = Hom ℭ r c"
if "c ∈⇩∘ ℭ⦇Obj⦈" for c
using that
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_op_intros)
show ?thesis
proof
(
intro cat_representationI is_iso_ntcfI,
rule assms(1),
rule ua(1),
rule 𝔎.HomDom.cat_Yoneda_arrow_is_ntcf[OF assms(1) ua(1) u𝔞],
rule cat_Set_is_iso_arrI,
simp_all only: cat_cs_simps
)
fix c assume prems: "c ∈⇩∘ ℭ⦇Obj⦈"
with ua(1,2) show Yc: "?Y c : Hom ℭ r c ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇c⦈"
by
(
cs_concl cs_shallow
cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros
)
note YcD = cat_Set_is_arrD[OF Yc]
interpret Yc: arr_Set α ‹?Y c› by (rule YcD(1))
show dom_Yc: "𝒟⇩∘ (?Y c⦇ArrVal⦈) = Hom ℭ r c"
by (simp add: 𝔎.Yoneda_component_ArrVal_vdomain)
show "v11 (?Y c⦇ArrVal⦈)"
proof(intro Yc.ArrVal.vsv_valeq_v11I, unfold dom_Yc in_Hom_iff)
fix g f assume prems':
"g : r ↦⇘ℭ⇙ c" "f : r ↦⇘ℭ⇙ c" "?Y c⦇ArrVal⦈⦇g⦈ = ?Y c⦇ArrVal⦈⦇f⦈"
from prems have c: "c ∈⇩∘ ℭ⦇Obj⦈" by auto
from prems'(3,1,2) have 𝔎gu𝔞_𝔎fu𝔞:
"𝔎⦇ArrMap⦈⦇g⦈⦇ArrVal⦈⦇u⦇ArrVal⦈⦇𝔞⦈⦈ = 𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦇ArrVal⦈⦇𝔞⦈⦈"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from prems'(1,2) ua(1,2) have 𝔎g_u:
"𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u : set {𝔞} ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇c⦈"
and 𝔎f_u:
"𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u : set {𝔞} ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇c⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
then have dom_lhs: "𝒟⇩∘ ((𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈) = set {𝔞}"
and dom_rhs: "𝒟⇩∘ ((𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈) = set {𝔞}"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
have 𝔎g_𝔎f: "𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u = 𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u"
proof(rule arr_Set_eqI)
from 𝔎g_u show arr_Set_𝔎g_u: "arr_Set α (𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u)"
by (auto dest: cat_Set_is_arrD)
from 𝔎f_u show arr_Set_𝔎f_u: "arr_Set α (𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u)"
by (auto dest: cat_Set_is_arrD)
show
"(𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈ =
(𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs vsingleton_iff; (simp only:)?)
from prems'(1,2) ua(2) show
"(𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈⦇𝔞⦈ =
(𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈⦇𝔞⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps 𝔎gu𝔞_𝔎fu𝔞
cs_intro: V_cs_intros cat_cs_intros
)
qed (use arr_Set_𝔎g_u arr_Set_𝔎f_u in auto)
qed (use 𝔎g_u 𝔎f_u in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
from prems'(1) ua(2) have
"𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u : set {𝔞} ↦⇘cat_Set α⇙ 𝔎⦇ObjMap⦈⦇c⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from ua(3)[OF c this] obtain h where h: "h : r ↦⇘ℭ⇙ c"
and 𝔎g_u_def:
"𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇h⦈"
and h_unique: "⋀h'.
⟦
h' : r ↦⇘ℭ⇙ c;
𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇h'⦈
⟧ ⟹ h' = h"
by metis
from prems'(1,2) ua(2) have
"𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇g⦈"
"𝔎⦇ArrMap⦈⦇g⦈ ∘⇩A⇘cat_Set α⇙ u = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇f⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps 𝔎g_𝔎f cs_intro: cat_cs_intros
)+
from h_unique[OF prems'(1) this(1)] h_unique[OF prems'(2) this(2)] show
"g = f"
by simp
qed
show "ℛ⇩∘ (?Y c⦇ArrVal⦈) = 𝔎⦇ObjMap⦈⦇c⦈"
proof
(
intro
vsubset_antisym Yc.arr_Par_ArrVal_vrange[unfolded YcD]
vsubsetI
)
fix y assume prems': "y ∈⇩∘ 𝔎⦇ObjMap⦈⦇c⦈"
from prems have 𝔎c: "𝔎⦇ObjMap⦈⦇c⦈ ∈⇩∘ cat_Set α⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from ua(3)[OF prems 𝔎.ntcf_paa_is_arr[OF assms(2) 𝔎c prems']] obtain f
where f: "f : r ↦⇘ℭ⇙ c"
and ntcf_paa_y:
"ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇c⦈) y = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇f⦈"
and f_unique: "⋀f'.
⟦
f' : r ↦⇘ℭ⇙ c;
ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇c⦈) y = umap_of 𝔎 (set {𝔞}) r u c⦇ArrVal⦈⦇f'⦈
⟧ ⟹ f' = f"
by metis
from ntcf_paa_y f ua(2) have
"ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇c⦈) y = 𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
then have
"ntcf_paa 𝔞 (𝔎⦇ObjMap⦈⦇c⦈) y⦇ArrVal⦈⦇𝔞⦈ =
(𝔎⦇ArrMap⦈⦇f⦈ ∘⇩A⇘cat_Set α⇙ u)⦇ArrVal⦈⦇𝔞⦈"
by simp
from this f ua(2) have [symmetric, cat_cs_simps]:
"y = 𝔎⦇ArrMap⦈⦇f⦈⦇ArrVal⦈⦇u⦇ArrVal⦈⦇𝔞⦈⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: V_cs_intros cat_cs_intros
)
show "y ∈⇩∘ ℛ⇩∘ (?Y c⦇ArrVal⦈)"
by (intro Yc.ArrVal.vsv_vimageI2')
(
use f in
‹
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
›
)+
qed
qed
qed
lemma cat_corepresentation_if_universal_arrow_of:
assumes "category α ℭ"
and "𝔎 : op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
and "𝔞 ∈⇩∘ cat_Set α⦇Obj⦈"
and "universal_arrow_of 𝔎 (set {𝔞}) r u"
shows "cat_corepresentation α 𝔎 r (Yoneda_arrow α 𝔎 r (u⦇ArrVal⦈⦇𝔞⦈))"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔎: is_functor α ‹op_cat ℭ› ‹cat_Set α› 𝔎 by (rule assms(2))
note ua = 𝔎.universal_arrow_ofD[OF assms(4), unfolded cat_op_simps]
note [cat_op_simps] = ℭ.cat_op_cat_cf_Hom_snd[OF ua(1)]
show ?thesis
by
(
intro cat_corepresentationI,
rule assms(1),
rule assms(2),
rule ua(1),
rule cat_representationD(2)
[
OF
cat_representation_if_universal_arrow_of[OF assms(2,3,4)]
assms(2),
unfolded cat_op_simps
]
)
qed
subsection‹Limits and colimits as universal cones›
lemma is_tm_cat_limit_if_cat_corepresentation:
assumes "𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
and "cat_corepresentation α (tm_cf_Cone α 𝔉) r ψ"
(is ‹cat_corepresentation α ?Cone r ψ›)
shows "ntcf_of_ntcf_arrow 𝔍 ℭ (ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈) :
r <⇩C⇩F⇩.⇩t⇩m⇩.⇩l⇩i⇩m 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
(is ‹ntcf_of_ntcf_arrow 𝔍 ℭ ?ψr1r : r <⇩C⇩F⇩.⇩t⇩m⇩.⇩l⇩i⇩m 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ›)
proof-
let ?P = ‹ntcf_paa 0› and ?Funct = ‹cat_Funct α 𝔍 ℭ›
interpret 𝔉: is_tm_functor α 𝔍 ℭ 𝔉 by (rule assms(1))
interpret Funct: category α ?Funct
by
(
cs_concl cs_shallow cs_intro:
cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
note rψ = cat_corepresentationD[
OF assms(2) 𝔉.HomCod.category_axioms 𝔉.tm_cf_cf_Cone_is_functor
]
interpret ψ: is_iso_ntcf α ‹op_cat ℭ› ‹cat_Set α› ‹Hom⇩O⇩.⇩C⇘α⇙ℭ(-,r)› ?Cone ψ
by (rule rψ(2))
have 0: "0 ∈⇩∘ cat_Set α⦇Obj⦈" unfolding cat_Set_components by auto
note ua = universal_arrow_of_if_cat_corepresentation[
OF 𝔉.HomCod.category_axioms 𝔉.tm_cf_cf_Cone_is_functor assms(2) 0
]
show ?thesis
proof(rule is_tm_cat_limitI')
from rψ(1) have [cat_FUNCT_cs_simps]:
"cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r)) = cf_const 𝔍 ℭ r"
by
(
cs_concl
cs_simp: cat_FUNCT_cs_simps
cs_intro: cat_cs_intros cat_FUNCT_cs_intros
)
from ψ.ntcf_NTMap_is_arr[unfolded cat_op_simps, OF rψ(1)] rψ(1) have
"ψ⦇NTMap⦈⦇r⦈ :
Hom ℭ r r ↦⇘cat_Set α⇙ Hom ?Funct (cf_map (cf_const 𝔍 ℭ r)) (cf_map 𝔉)"
by
(
cs_prems
cs_simp: cat_small_cs_simps cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros
)
with rψ(1) have ψr_r:
"?ψr1r : cf_map (cf_const 𝔍 ℭ r) ↦⇘?Funct⇙ cf_map 𝔉"
by
(
cs_concl cs_shallow cs_intro:
cat_Set_cs_intros cat_cs_intros in_Hom_iff[symmetric]
)
from rψ(1) cat_Funct_is_arrD(1)[OF ψr_r, unfolded cat_FUNCT_cs_simps]
show "ntcf_of_ntcf_arrow 𝔍 ℭ ?ψr1r : r <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
by (intro is_tm_cat_coneI)
(cs_concl cs_shallow cs_intro: cat_cs_intros cat_small_cs_intros)
fix r' u' assume "u' : r' <⇩C⇩F⇩.⇩t⇩m⇩.⇩c⇩o⇩n⇩e 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
then interpret u': is_tm_cat_cone α r' 𝔍 ℭ 𝔉 u' .
have Cone_r': "tm_cf_Cone α 𝔉⦇ObjMap⦈⦇r'⦈ ∈⇩∘ cat_Set α⦇Obj⦈"
by (cs_concl cs_intro: cat_lim_cs_intros cat_cs_intros cat_op_intros)
from rψ(1) have Cone_r: "tm_cf_Cone α 𝔉⦇ObjMap⦈⦇r⦈ ∈⇩∘ cat_Set α⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
from rψ(1) have ψr1r:
"ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ ∈⇩∘ tm_cf_Cone α 𝔉⦇ObjMap⦈⦇r⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_small_cs_simps cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros
)
have u': "ntcf_arrow u' ∈⇩∘ ?Cone⦇ObjMap⦈⦇r'⦈"
by
(
cs_concl
cs_simp: cat_small_cs_simps
cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros cat_cs_intros
)
have [cat_cs_simps]:
"cf_of_cf_map 𝔍 ℭ (cf_map 𝔉) = 𝔉"
"cf_of_cf_map 𝔍 ℭ (cf_map (cf_const 𝔍 ℭ r)) = cf_const 𝔍 ℭ r"
by (cs_concl cs_simp: cat_FUNCT_cs_simps)+
from Cone_r 0 ψr1r rψ(1) have ψr1r_is_arr: "ψ⦇NTMap⦈⦇r⦈⦇ArrVal⦈⦇ℭ⦇CId⦈⦇r⦈⦈ :
cf_map (cf_const 𝔍 ℭ r) ↦⇘?Funct⇙ cf_map 𝔉"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_small_cs_simps
cs_intro: cat_cs_intros cat_op_intros
)
from rψ(1) have [cat_cs_intros]:
"Hom ?Funct (cf_map (cf_const 𝔍 ℭ r)) (cf_map 𝔉) ∈⇩∘ cat_Set α⦇Obj⦈"
unfolding cat_Set_components(1)
by (intro Funct.cat_Hom_in_Vset)
(
cs_concl
cs_simp: cat_FUNCT_cs_simps
cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros cat_cs_intros
)+
note ψr1r_is_arrD = cat_Funct_is_arrD[OF ψr1r_is_arr, unfolded cat_cs_simps]
from is_functor.universal_arrow_ofD(3)
[
OF 𝔉.tm_cf_cf_Cone_is_functor ua,
unfolded cat_op_simps,
OF u'.cat_cone_obj 𝔉.ntcf_paa_is_arr[OF 0 Cone_r' u']
]
obtain f where f: "f : r' ↦⇘ℭ⇙ r"
and Pf: "?P (?Cone⦇ObjMap⦈⦇r'⦈) (ntcf_arrow u') =
umap_of ?Cone (set {0}) r (?P (?Cone⦇ObjMap⦈⦇r⦈) ?ψr1r) r'⦇ArrVal⦈⦇f⦈"
and f_unique: "⋀f'.
⟦
f' : r' ↦⇘ℭ⇙ r;
?P (?Cone⦇ObjMap⦈⦇r'⦈) (ntcf_arrow u') =
umap_of ?Cone (set {0}) r (?P (?Cone⦇ObjMap⦈⦇r⦈) ?ψr1r) r'⦇ArrVal⦈⦇f'⦈
⟧ ⟹ f' = f"
by metis
show "∃!f.
f : r' ↦⇘ℭ⇙ r ∧
u' = ntcf_of_ntcf_arrow 𝔍 ℭ ?ψr1r ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f"
proof(intro ex1I conjI; (elim conjE)?)
show "f : r' ↦⇘ℭ⇙ r" by (rule f)
from Pf Cone_r 0 f ψr1r ψr1r_is_arr ψr1r_is_arrD(1) show
"u' = ntcf_of_ntcf_arrow 𝔍 ℭ ?ψr1r ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f"
by (subst (asm) ψr1r_is_arrD(2))
(
cs_prems
cs_simp: cat_FUNCT_cs_simps cat_small_cs_simps cat_cs_simps
cs_intro:
cat_small_cs_intros
cat_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_op_intros
)
fix f' assume prems:
"f' : r' ↦⇘ℭ⇙ r"
"u' = ntcf_of_ntcf_arrow 𝔍 ℭ ?ψr1r ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f'"
from Pf Cone_r 0 f ψr1r ψr1r_is_arr ψr1r_is_arrD(1) prems(1) have
"?P (?Cone⦇ObjMap⦈⦇r'⦈) (ntcf_arrow u') =
umap_of ?Cone (set {0}) r (?P (?Cone⦇ObjMap⦈⦇r⦈) ?ψr1r) r'⦇ArrVal⦈⦇f'⦈"
by (subst ψr1r_is_arrD(2))
(
cs_concl
cs_simp: cat_FUNCT_cs_simps cat_small_cs_simps cat_cs_simps prems(2)
cs_intro:
cat_small_cs_intros
cat_FUNCT_cs_intros
cat_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from f_unique[OF prems(1) this] show "f' = f" .
qed
qed
qed
lemma cat_corepresentation_if_is_tm_cat_limit:
assumes "ψ : r <⇩C⇩F⇩.⇩t⇩m⇩.⇩l⇩i⇩m 𝔉 : 𝔍 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
shows "cat_corepresentation
α (tm_cf_Cone α 𝔉) r (Yoneda_arrow α (tm_cf_Cone α 𝔉) r (ntcf_arrow ψ))"
(is ‹cat_corepresentation α ?Cone r ?Yψ›)
proof-
let ?Funct = ‹cat_Funct α 𝔍 ℭ›
and ?P_ψ = ‹ntcf_paa 0 (?Cone⦇ObjMap⦈⦇r⦈) (ntcf_arrow ψ)›
and ?ntcf_of = ‹ntcf_of_ntcf_arrow 𝔍 ℭ›
interpret ψ: is_tm_cat_limit α 𝔍 ℭ 𝔉 r ψ by (rule assms(1))
interpret Funct: category α ?Funct
by
(
cs_concl cs_shallow cs_intro:
cat_small_cs_intros cat_cs_intros cat_FUNCT_cs_intros
)
interpret Cone: is_functor α ‹op_cat ℭ› ‹cat_Set α› ‹?Cone›
by (rule ψ.NTCod.tm_cf_cf_Cone_is_functor)
have 0: "0 ∈⇩∘ cat_Set α⦇Obj⦈" unfolding cat_Set_components by auto
have ntcf_arrow_ψ:
"ntcf_arrow ψ : cf_map (cf_const 𝔍 ℭ r) ↦⇘?Funct⇙ cf_map 𝔉"
by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros)
from ψ.cat_cone_obj 0 ntcf_arrow_ψ have P_ψ:
"?P_ψ : set {0} ↦⇘cat_Set α⇙ ?Cone⦇ObjMap⦈⦇r⦈"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros cat_op_intros
cs_simp: cat_small_cs_simps cat_FUNCT_cs_simps
)
have "universal_arrow_of ?Cone (set {0}) r ?P_ψ"
proof(rule Cone.universal_arrow_ofI, unfold cat_op_simps, rule ψ.cat_cone_obj)
from 0 ψ.cat_cone_obj show "?P_ψ : set {0} ↦⇘cat_Set α⇙ ?Cone⦇ObjMap⦈⦇r⦈"
by
(
cs_concl
cs_intro:
cat_small_cs_intros
cat_cs_intros
cat_FUNCT_cs_intros
cat_op_intros
cs_simp: cat_small_cs_simps
)
fix r' u' assume prems:
"r' ∈⇩∘ ℭ⦇Obj⦈" "u' : set {0} ↦⇘cat_Set α⇙ ?Cone⦇ObjMap⦈⦇r'⦈"
let ?const_r' = ‹cf_map (cf_const 𝔍 ℭ r')›
let ?Hom_r𝔉 = ‹Hom ?Funct ?const_r' (cf_map 𝔉)›
from prems(2,1) have u': "u' : set {0} ↦⇘cat_Set α⇙ ?Hom_r𝔉"
by
(
cs_prems cs_shallow
cs_simp: cat_small_cs_simps cat_cs_simps cs_intro: cat_cs_intros
)
from prems(1) have [cat_FUNCT_cs_simps]:
"cf_of_cf_map 𝔍 ℭ ?const_r' = cf_const 𝔍 ℭ r'"
by
(
cs_concl
cs_simp: cat_cs_simps cat_FUNCT_cs_simps cs_intro: cat_cs_intros
)
from
cat_Set_ArrVal_app_vrange[OF prems(2) vintersection_vsingleton]
prems(1)
have "u'⦇ArrVal⦈⦇0⦈ : ?const_r' ↦⇘?Funct⇙ cf_map 𝔉"
by (cs_prems cs_shallow cs_simp: cat_small_cs_simps cat_cs_simps)
note u'0 = cat_Funct_is_arrD[OF this, unfolded cat_FUNCT_cs_simps]
interpret u'0: is_tm_cat_cone α r' 𝔍 ℭ 𝔉 ‹?ntcf_of (u'⦇ArrVal⦈⦇0⦈)›
by
(
rule is_tm_cat_coneI[
OF is_tm_ntcfD(1)[OF u'0(1)] ψ.NTCod.is_tm_functor_axioms prems(1)
]
)
from ψ.tm_cat_lim_ua_fo[OF u'0.is_cat_cone_axioms] obtain f
where f: "f : r' ↦⇘ℭ⇙ r"
and u'0_def: "?ntcf_of (u'⦇ArrVal⦈⦇0⦈) = ψ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f"
and f_unique: "⋀f'.
⟦
f' : r' ↦⇘ℭ⇙ r;
?ntcf_of (u'⦇ArrVal⦈⦇0⦈) = ψ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 ℭ f'
⟧ ⟹ f' = f"
by metis
note [cat_FUNCT_cs_simps] =
ψ.ntcf_paa_ArrVal u'0(2)[symmetric] u'0_def[symmetric]
show "∃!f'.
f' : r' ↦⇘ℭ⇙ r ∧ u' = umap_of ?Cone (set {0}) r ?P_ψ r'⦇ArrVal⦈⦇f'⦈"
proof(intro ex1I conjI; (elim conjE)?; (rule f)?)
from f 0 u' ntcf_arrow_ψ show
"u' = umap_of ?Cone (set {0}) r ?P_ψ r'⦇ArrVal⦈⦇f⦈"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro:
cat_small_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_cs_intros
cat_op_intros
cs_simp: cat_FUNCT_cs_simps cat_small_cs_simps
)
fix f' assume prems':
"f' : r' ↦⇘ℭ⇙ r"
"u' = umap_of ?Cone (set {0}) r ?P_ψ r'⦇ArrVal⦈⦇f'⦈"
let ?f' = ‹ntcf_const 𝔍 ℭ f'›
from prems'(2,1) 0 ntcf_arrow_ψ P_ψ have
"u' = ntcf_paa 0 ?Hom_r𝔉 (ntcf_arrow (ψ ∙⇩N⇩T⇩C⇩F ?f'))"
unfolding
Cone.umap_of_ArrVal_app[unfolded cat_op_simps, OF prems'(1) P_ψ]
by
(
cs_prems
cs_simp: cat_FUNCT_cs_simps cat_small_cs_simps cat_cs_simps
cs_intro:
cat_small_cs_intros
cat_FUNCT_cs_intros
cat_prod_cs_intros
cat_cs_intros
cat_op_intros
)
then have
"?ntcf_of (u'⦇ArrVal⦈⦇0⦈) =
?ntcf_of ((ntcf_paa 0 ?Hom_r𝔉 (ntcf_arrow (ψ ∙⇩N⇩T⇩C⇩F ?f')))⦇ArrVal⦈⦇0⦈)"
by simp
from this prems'(1) have "?ntcf_of (u'⦇ArrVal⦈⦇0⦈) = ψ ∙⇩N⇩T⇩C⇩F ?f'"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cat_FUNCT_cs_simps cs_intro: cat_cs_intros
)
from f_unique[OF prems'(1) this] show "f' = f" .
qed
qed
from
cat_corepresentation_if_universal_arrow_of[
OF ψ.NTDom.HomCod.category_axioms Cone.is_functor_axioms 0 this
]
show "cat_corepresentation α ?Cone r ?Yψ"
by (cs_prems cs_shallow cs_simp: cat_cs_simps)
qed
text‹\newpage›
end