Theory CZH_UCAT_Adjoints
section‹Adjoints›
theory CZH_UCAT_Adjoints
imports
CZH_UCAT_Limit
CZH_Elementary_Categories.CZH_ECAT_Yoneda
begin
subsection‹Background›
named_theorems adj_cs_simps
named_theorems adj_cs_intros
named_theorems adj_field_simps
definition AdjLeft :: V where [adj_field_simps]: "AdjLeft = 0"
definition AdjRight :: V where [adj_field_simps]: "AdjRight = 1⇩ℕ"
definition AdjNT :: V where [adj_field_simps]: "AdjNT = 2⇩ℕ"
subsection‹Definition and elementary properties›
text‹
See subsection 2.1 in \<^cite>‹"bodo_categories_1970"› or Chapter IV-1 in
\<^cite>‹"mac_lane_categories_2010"›.
›
locale is_cf_adjunction =
𝒵 α +
vfsequence Φ +
L: category α ℭ +
R: category α 𝔇 +
LR: is_functor α ℭ 𝔇 𝔉 +
RL: is_functor α 𝔇 ℭ 𝔊 +
NT: is_iso_ntcf
α
‹op_cat ℭ ×⇩C 𝔇›
‹cat_Set α›
‹Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)›
‹Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)›
‹Φ⦇AdjNT⦈›
for α ℭ 𝔇 𝔉 𝔊 Φ +
assumes cf_adj_length[adj_cs_simps]: "vcard Φ = 3⇩ℕ"
and cf_adj_AdjLeft[adj_cs_simps]: "Φ⦇AdjLeft⦈ = 𝔉"
and cf_adj_AdjRight[adj_cs_simps]: "Φ⦇AdjRight⦈ = 𝔊"
syntax "_is_cf_adjunction" :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ : _ ⇌⇩C⇩F _ : _ ⇌⇌⇩Cı _)› [51, 51, 51, 51, 51] 51)
syntax_consts "_is_cf_adjunction" ⇌ is_cf_adjunction
translations "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇" ⇌
"CONST is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ"
lemmas [adj_cs_simps] =
is_cf_adjunction.cf_adj_length
is_cf_adjunction.cf_adj_AdjLeft
is_cf_adjunction.cf_adj_AdjRight
text‹Components.›
lemma cf_adjunction_components[adj_cs_simps]:
"[𝔉, 𝔊, φ]⇩∘⦇AdjLeft⦈ = 𝔉"
"[𝔉, 𝔊, φ]⇩∘⦇AdjRight⦈ = 𝔊"
"[𝔉, 𝔊, φ]⇩∘⦇AdjNT⦈ = φ"
unfolding AdjLeft_def AdjRight_def AdjNT_def
by (simp_all add: nat_omega_simps)
text‹Rules.›
lemma (in is_cf_adjunction) is_cf_adjunction_axioms'[adj_cs_intros]:
assumes "α' = α" and "ℭ' = ℭ" and "𝔇' = 𝔇" and "𝔉' = 𝔉" and "𝔊' = 𝔊"
shows "Φ : 𝔉' ⇌⇩C⇩F 𝔊' : ℭ' ⇌⇌⇩C⇘α'⇙ 𝔇'"
unfolding assms by (rule is_cf_adjunction_axioms)
lemmas (in is_cf_adjunction) [adj_cs_intros] = is_cf_adjunction_axioms
mk_ide rf is_cf_adjunction_def[unfolded is_cf_adjunction_axioms_def]
|intro is_cf_adjunctionI|
|dest is_cf_adjunctionD[dest]|
|elim is_cf_adjunctionE[elim]|
lemmas [adj_cs_intros] = is_cf_adjunctionD(3-6)
lemma (in is_cf_adjunction) cf_adj_is_iso_ntcf':
assumes "𝔉' = Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)"
and "𝔊' = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)"
and "𝔄' = op_cat ℭ ×⇩C 𝔇"
and "𝔅' = cat_Set α"
shows "Φ⦇AdjNT⦈ : 𝔉' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊' : 𝔄' ↦↦⇩C⇘α⇙ 𝔅'"
unfolding assms by (auto intro: cat_cs_intros)
lemmas [adj_cs_intros] = is_cf_adjunction.cf_adj_is_iso_ntcf'
lemma cf_adj_eqI:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "Φ' : 𝔉' ⇌⇩C⇩F 𝔊' : ℭ' ⇌⇌⇩C⇘α⇙ 𝔇'"
and "ℭ = ℭ'"
and "𝔇 = 𝔇'"
and "𝔉 = 𝔉'"
and "𝔊 = 𝔊'"
and "Φ⦇AdjNT⦈ = Φ'⦇AdjNT⦈"
shows "Φ = Φ'"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Φ': is_cf_adjunction α ℭ' 𝔇' 𝔉' 𝔊' Φ' by (rule assms(2))
show ?thesis
proof(rule vsv_eqI)
have dom: "𝒟⇩∘ Φ = 3⇩ℕ"
by (cs_concl cs_shallow cs_simp: V_cs_simps adj_cs_simps)
show "𝒟⇩∘ Φ = 𝒟⇩∘ Φ'"
by (cs_concl cs_shallow cs_simp: V_cs_simps adj_cs_simps dom)
from assms(4-7) have sup:
"Φ⦇AdjLeft⦈ = Φ'⦇AdjLeft⦈"
"Φ⦇AdjRight⦈ = Φ'⦇AdjRight⦈"
"Φ⦇AdjNT⦈ = Φ'⦇AdjNT⦈"
by (simp_all add: adj_cs_simps)
show "a ∈⇩∘ 𝒟⇩∘ Φ ⟹ Φ⦇a⦈ = Φ'⦇a⦈" for a
by (unfold dom, elim_in_numeral, insert sup)
(auto simp: adj_field_simps)
qed (auto simp: Φ.L.vsv_axioms Φ'.vsv_axioms)
qed
subsection‹Opposite adjunction›
subsubsection‹Definition and elementary properties›
text‹See \<^cite>‹"kan_adjoint_1958"› for further information.›
abbreviation op_cf_adj_nt :: "V ⇒ V ⇒ V ⇒ V"
where "op_cf_adj_nt ℭ 𝔇 φ ≡ inv_ntcf (bnt_flip (op_cat ℭ) 𝔇 φ)"
definition op_cf_adj :: "V ⇒ V"
where "op_cf_adj Φ =
[
op_cf (Φ⦇AdjRight⦈),
op_cf (Φ⦇AdjLeft⦈),
op_cf_adj_nt (Φ⦇AdjLeft⦈⦇HomDom⦈) (Φ⦇AdjLeft⦈⦇HomCod⦈) (Φ⦇AdjNT⦈)
]⇩∘"
lemma op_cf_adj_components:
shows "op_cf_adj Φ⦇AdjLeft⦈ = op_cf (Φ⦇AdjRight⦈)"
and "op_cf_adj Φ⦇AdjRight⦈ = op_cf (Φ⦇AdjLeft⦈)"
and "op_cf_adj Φ⦇AdjNT⦈ =
op_cf_adj_nt (Φ⦇AdjLeft⦈⦇HomDom⦈) (Φ⦇AdjLeft⦈⦇HomCod⦈) (Φ⦇AdjNT⦈)"
unfolding op_cf_adj_def adj_field_simps by (simp_all add: nat_omega_simps)
lemma (in is_cf_adjunction) op_cf_adj_components:
shows "op_cf_adj Φ⦇AdjLeft⦈ = op_cf 𝔊"
and "op_cf_adj Φ⦇AdjRight⦈ = op_cf 𝔉"
and "op_cf_adj Φ⦇AdjNT⦈ = inv_ntcf (bnt_flip (op_cat ℭ) 𝔇 (Φ⦇AdjNT⦈))"
unfolding op_cf_adj_components by (simp_all add: cat_cs_simps adj_cs_simps)
lemmas [cat_op_simps] = is_cf_adjunction.op_cf_adj_components
text‹The opposite adjunction is an adjunction.›
lemma (in is_cf_adjunction) is_cf_adjunction_op:
"op_cf_adj Φ : op_cf 𝔊 ⇌⇩C⇩F op_cf 𝔉 : op_cat 𝔇 ⇌⇌⇩C⇘α⇙ op_cat ℭ"
proof(intro is_cf_adjunctionI, unfold cat_op_simps, unfold op_cf_adj_components)
show "vfsequence (op_cf_adj Φ)" unfolding op_cf_adj_def by simp
show "vcard (op_cf_adj Φ) = 3⇩ℕ"
unfolding op_cf_adj_def by (simp add: nat_omega_simps)
note adj = is_cf_adjunctionD[OF is_cf_adjunction_axioms]
from adj have f_φ: "bnt_flip (op_cat ℭ) 𝔇 (Φ⦇AdjNT⦈) :
Hom⇩O⇩.⇩C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-) :
𝔇 ×⇩C op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_op_intros
)
show "op_cf_adj_nt ℭ 𝔇 (Φ⦇AdjNT⦈) :
Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-) :
𝔇 ×⇩C op_cat ℭ ↦↦⇩C⇘α⇙ cat_Set α"
by (rule CZH_ECAT_NTCF.iso_ntcf_is_iso_arr(1)[OF f_φ])
qed (auto intro: cat_cs_intros cat_op_intros)
lemmas is_cf_adjunction_op =
is_cf_adjunction.is_cf_adjunction_op
lemma (in is_cf_adjunction) is_cf_adjunction_op'[cat_op_intros]:
assumes "𝔊' = op_cf 𝔊"
and "𝔉' = op_cf 𝔉"
and "𝔇' = op_cat 𝔇"
and "ℭ' = op_cat ℭ"
shows "op_cf_adj Φ : 𝔊' ⇌⇩C⇩F 𝔉' : 𝔇' ⇌⇌⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cf_adjunction_op)
lemmas [cat_op_intros] = is_cf_adjunction.is_cf_adjunction_op'
text‹The operation of taking the opposite adjunction is an involution.›
lemma (in is_cf_adjunction) cf_adjunction_op_cf_adj_op_cf_adj[cat_op_simps]:
"op_cf_adj (op_cf_adj Φ) = Φ"
proof(rule cf_adj_eqI)
show Φ': "op_cf_adj (op_cf_adj Φ) : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
proof(intro is_cf_adjunctionI)
show "vfsequence (op_cf_adj (op_cf_adj Φ))" unfolding op_cf_adj_def by simp
from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros
cs_simp: cat_cs_simps cat_op_simps
)
show "vcard (op_cf_adj (op_cf_adj Φ)) = 3⇩ℕ"
unfolding op_cf_adj_def by (simp add: nat_omega_simps)
from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjLeft⦈ = 𝔉"
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
from is_cf_adjunction_axioms show "op_cf_adj (op_cf_adj Φ)⦇AdjRight⦈ = 𝔊"
by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
qed (auto intro: cat_cs_intros)
interpret Φ': is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹op_cf_adj (op_cf_adj Φ)›
by (rule Φ')
show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ = Φ⦇AdjNT⦈"
proof(rule ntcf_eqI)
show op_op_Φ:
"op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (rule Φ'.NT.is_ntcf_axioms)
show Φ: "Φ⦇AdjNT⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (rule NT.is_ntcf_axioms)
from op_op_Φ have dom_lhs:
"𝒟⇩∘ (op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈) = (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈ = Φ⦇AdjNT⦈⦇NTMap⦈"
proof(rule vsv_eqI, unfold NT.ntcf_NTMap_vdomain dom_lhs)
fix cd assume prems: "cd ∈⇩∘ (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
then obtain c d
where cd_def: "cd = [c, d]⇩∘"
and c: "c ∈⇩∘ op_cat ℭ⦇Obj⦈"
and d: "d ∈⇩∘ 𝔇⦇Obj⦈"
by (elim cat_prod_2_ObjE[OF L.category_op R.category_axioms prems])
from is_cf_adjunction_axioms c d L.category_axioms R.category_axioms Φ
show "op_cf_adj (op_cf_adj Φ)⦇AdjNT⦈⦇NTMap⦈⦇cd⦈ = Φ⦇AdjNT⦈⦇NTMap⦈⦇cd⦈"
unfolding cd_def cat_op_simps
by
(
cs_concl
cs_intro:
cat_arrow_cs_intros
ntcf_cs_intros
adj_cs_intros
cat_op_intros
cat_cs_intros
cat_prod_cs_intros
cs_simp: cat_cs_simps cat_op_simps
)
qed (auto intro: inv_ntcf_NTMap_vsv)
qed simp_all
qed (auto intro: adj_cs_intros)
lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_op_cf_adj_op_cf_adj
subsubsection‹Alternative form of the naturality condition›
text‹
The lemmas in this subsection are based on the comments on page 81 in
\<^cite>‹"mac_lane_categories_2010"›.
›
lemma (in is_cf_adjunction) cf_adj_Comp_commute_RL:
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
and "k : a ↦⇘𝔇⇙ a'"
shows
"𝔊⦇ArrMap⦈⦇k⦈ ∘⇩A⇘ℭ⇙ (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈ =
(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈⇩∙)⦇ArrVal⦈⦇k ∘⇩A⇘𝔇⇙ f⦈"
proof-
from
assms
is_cf_adjunction_axioms
L.category_axioms R.category_axioms
L.category_op R.category_op
have φ_x_a: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
note φ_x_a_f =
cat_Set_ArrVal_app_vrange[OF φ_x_a, unfolded in_Hom_iff, OF assms(2)]
from
is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have φ_x_a':
"Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈⇩∙ :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a' ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a'⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
from is_cf_adjunction_axioms this assms have x_k:
"[ℭ⦇CId⦈⦇x⦈, k]⇩∘ : [x, a]⇩∘ ↦⇘op_cat ℭ ×⇩C 𝔇⇙ [x, a']⇩∘"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
from
NT.ntcf_Comp_commute[OF this] is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have
"Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈⇩∙ ∘⇩A⇘cat_Set α⇙ cf_hom 𝔇 [𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈, k]⇩∘ =
cf_hom ℭ [ℭ⦇CId⦈⦇x⦈, 𝔊⦇ArrMap⦈⦇k⦈]⇩∘ ∘⇩A⇘cat_Set α⇙ Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙"
(is ‹?lhs = ?rhs›)
by
(
cs_prems cs_ist_simple
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
moreover from
is_cf_adjunction_axioms assms φ_x_a'
L.category_axioms R.category_axioms
L.category_op R.category_op
have "?lhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a'⦈⇩∙)⦇ArrVal⦈⦇k ∘⇩A⇘𝔇⇙ f⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
moreover from
is_cf_adjunction_axioms assms φ_x_a_f
L.category_axioms R.category_axioms
L.category_op R.category_op
have
"?rhs⦇ArrVal⦈⦇f⦈ = 𝔊⦇ArrMap⦈⦇k⦈ ∘⇩A⇘ℭ⇙ (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
ultimately show ?thesis by simp
qed
lemma (in is_cf_adjunction) cf_adj_Comp_commute_LR:
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
and "h : x' ↦⇘ℭ⇙ x"
shows
"(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈ ∘⇩A⇘ℭ⇙ h =
(Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈⇩∙)⦇ArrVal⦈⦇f ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇h⦈⦈"
proof-
from
is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have φ_x_a: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
note φ_x_a_f =
cat_Set_ArrVal_app_vrange[OF φ_x_a, unfolded in_Hom_iff, OF assms(2)]
from is_cf_adjunction_axioms assms have
"[h, 𝔇⦇CId⦈⦇a⦈]⇩∘ : [x, a]⇩∘ ↦⇘op_cat ℭ ×⇩C 𝔇⇙ [x', a]⇩∘"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
from
NT.ntcf_Comp_commute[OF this] is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have
"Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈⇩∙ ∘⇩A⇘cat_Set α⇙ cf_hom 𝔇 [𝔉⦇ArrMap⦈⦇h⦈, 𝔇⦇CId⦈⦇a⦈]⇩∘ =
cf_hom ℭ [h, ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈]⇩∘ ∘⇩A⇘cat_Set α⇙ Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙"
(is ‹?lhs = ?rhs›)
by
(
cs_prems
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
moreover from
is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have "?lhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x', a⦈⇩∙)⦇ArrVal⦈⦇f ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇h⦈⦈"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
moreover from
is_cf_adjunction_axioms assms φ_x_a_f
L.category_axioms R.category_axioms
L.category_op R.category_op
have "?rhs⦇ArrVal⦈⦇f⦈ = (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈ ∘⇩A⇘ℭ⇙ h"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
ultimately show ?thesis by simp
qed
subsection‹Unit›
subsubsection‹Definition and elementary properties›
text‹See Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.›
definition cf_adjunction_unit :: "V ⇒ V" (‹η⇩C›)
where "η⇩C Φ =
[
(
λx∈⇩∘Φ⦇AdjLeft⦈⦇HomDom⦈⦇Obj⦈.
(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈⇩∙)⦇ArrVal⦈⦇
Φ⦇AdjLeft⦈⦇HomCod⦈⦇CId⦈⦇Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈
⦈
),
cf_id (Φ⦇AdjLeft⦈⦇HomDom⦈),
(Φ⦇AdjRight⦈) ∘⇩C⇩F (Φ⦇AdjLeft⦈),
Φ⦇AdjLeft⦈⦇HomDom⦈,
Φ⦇AdjLeft⦈⦇HomDom⦈
]⇩∘"
text‹Components.›
lemma cf_adjunction_unit_components:
shows "η⇩C Φ⦇NTMap⦈ =
(
λx∈⇩∘Φ⦇AdjLeft⦈⦇HomDom⦈⦇Obj⦈.
(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈⇩∙)⦇ArrVal⦈⦇
Φ⦇AdjLeft⦈⦇HomCod⦈⦇CId⦈⦇Φ⦇AdjLeft⦈⦇ObjMap⦈⦇x⦈⦈
⦈
)"
and "η⇩C Φ⦇NTDom⦈ = cf_id (Φ⦇AdjLeft⦈⦇HomDom⦈)"
and "η⇩C Φ⦇NTCod⦈ = (Φ⦇AdjRight⦈) ∘⇩C⇩F (Φ⦇AdjLeft⦈)"
and "η⇩C Φ⦇NTDGDom⦈ = Φ⦇AdjLeft⦈⦇HomDom⦈"
and "η⇩C Φ⦇NTDGCod⦈ = Φ⦇AdjLeft⦈⦇HomDom⦈"
unfolding cf_adjunction_unit_def nt_field_simps
by (simp_all add: nat_omega_simps)
context is_cf_adjunction
begin
lemma cf_adjunction_unit_components':
shows "η⇩C Φ⦇NTMap⦈ =
(λx∈⇩∘ℭ⦇Obj⦈. (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, 𝔉⦇ObjMap⦈⦇x⦈⦈⇩∙)⦇ArrVal⦈⦇𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈⦈)"
and "η⇩C Φ⦇NTDom⦈ = cf_id ℭ"
and "η⇩C Φ⦇NTCod⦈ = 𝔊 ∘⇩C⇩F 𝔉"
and "η⇩C Φ⦇NTDGDom⦈ = ℭ"
and "η⇩C Φ⦇NTDGCod⦈ = ℭ"
unfolding cf_adjunction_unit_components
by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)+
mk_VLambda cf_adjunction_unit_components'(1)
|vdomain cf_adjunction_unit_NTMap_vdomain[adj_cs_simps]|
|app cf_adjunction_unit_NTMap_app[adj_cs_simps]|
end
mk_VLambda cf_adjunction_unit_components(1)
|vsv cf_adjunction_unit_NTMap_vsv[adj_cs_intros]|
lemmas [adj_cs_simps] =
is_cf_adjunction.cf_adjunction_unit_NTMap_vdomain
is_cf_adjunction.cf_adjunction_unit_NTMap_app
subsubsection‹Natural transformation map›
lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_is_arr:
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
shows "η⇩C Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
proof-
from
is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have φ_x_𝔉x:
"Φ⦇AdjNT⦈⦇NTMap⦈⦇x, 𝔉⦇ObjMap⦈⦇x⦈⦈⇩∙ :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) (𝔉⦇ObjMap⦈⦇x⦈) ↦⇘cat_Set α⇙
Hom ℭ x (𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
from is_cf_adjunction_axioms assms have CId_𝔉x:
"𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇x⦈"
by (cs_concl cs_intro: cat_cs_intros adj_cs_intros)
from
is_cf_adjunction_axioms
assms
cat_Set_ArrVal_app_vrange[OF φ_x_𝔉x, unfolded in_Hom_iff, OF CId_𝔉x]
show "η⇩C Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
qed
lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_is_arr':
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
and "a = x"
and "b = 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
and "ℭ' = ℭ"
shows "η⇩C Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ'⇙ b"
using assms(1) unfolding assms(2-4) by (rule cf_adjunction_unit_NTMap_is_arr)
lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_unit_NTMap_is_arr'
lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_vrange:
"ℛ⇩∘ (η⇩C Φ⦇NTMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cf_adjunction_unit_NTMap_vdomain)
fix x assume prems: "x ∈⇩∘ ℭ⦇Obj⦈"
from cf_adjunction_unit_NTMap_is_arr[OF prems] show "η⇩C Φ⦇NTMap⦈⦇x⦈ ∈⇩∘ ℭ⦇Arr⦈"
by auto
qed (auto intro: adj_cs_intros)
subsubsection‹Unit is a natural transformation›
lemma (in is_cf_adjunction) cf_adjunction_unit_is_ntcf:
"η⇩C Φ : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_ntcfI')
show "vfsequence (η⇩C Φ)" unfolding cf_adjunction_unit_def by simp
show "vcard (η⇩C Φ) = 5⇩ℕ"
unfolding cf_adjunction_unit_def by (simp add: nat_omega_simps)
from is_cf_adjunction_axioms show "cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
from is_cf_adjunction_axioms show "𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
from is_cf_adjunction_axioms show "𝒟⇩∘ (η⇩C Φ⦇NTMap⦈) = ℭ⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
show "η⇩C Φ⦇NTMap⦈⦇a⦈ : cf_id ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ ℭ⦇Obj⦈" for a
using is_cf_adjunction_axioms that
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
show
"η⇩C Φ⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ cf_id ℭ⦇ArrMap⦈⦇f⦈ =
(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘ℭ⇙ b" for a b f
using is_cf_adjunction_axioms that
by
(
cs_concl
cs_simp:
cf_adj_Comp_commute_RL cf_adj_Comp_commute_LR
cat_cs_simps
adj_cs_simps
cs_intro: cat_cs_intros adj_cs_intros
)
qed (auto simp: cf_adjunction_unit_components')
lemma (in is_cf_adjunction) cf_adjunction_unit_is_ntcf':
assumes "𝔖 = cf_id ℭ"
and "𝔖' = 𝔊 ∘⇩C⇩F 𝔉"
and "𝔄 = ℭ"
and "𝔅 = ℭ"
shows "η⇩C Φ : 𝔖 ↦⇩C⇩F 𝔖' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
unfolding assms by (rule cf_adjunction_unit_is_ntcf)
lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_unit_is_ntcf'
subsubsection‹Every component of a unit is a universal arrow›
text‹
The lemmas in this subsection are based on elements of the statement of
Theorem 1 in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
lemma (in is_cf_adjunction) cf_adj_umap_of_unit:
assumes "x ∈⇩∘ ℭ⦇Obj⦈" and "a ∈⇩∘ 𝔇⦇Obj⦈"
shows "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⇩C Φ⦇NTMap⦈⦇x⦈) a"
(is ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ = ?uof_a›)
proof-
from
is_cf_adjunction_axioms assms
L.category_axioms R.category_axioms
L.category_op R.category_op
have φ_xa: "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ :
Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
then have dom_lhs:
"𝒟⇩∘ ((Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from is_cf_adjunction_axioms assms have uof_a:
"?uof_a : Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
by (cs_concl cs_intro: cat_cs_intros adj_cs_intros)
then have dom_rhs: "𝒟⇩∘ (?uof_a⦇ArrVal⦈) = Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a"
by (cs_concl cs_simp: cat_cs_simps)
show ?thesis
proof(rule arr_Set_eqI[of α])
from φ_xa show arr_Set_φ_xa: "arr_Set α (Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)"
by (auto dest: cat_Set_is_arrD(1))
from uof_a show arr_Set_uof_a: "arr_Set α ?uof_a"
by (auto dest: cat_Set_is_arrD(1))
show "(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈ = ?uof_a⦇ArrVal⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs in_Hom_iff)
fix g assume prems: "g : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
from is_cf_adjunction_axioms assms prems show
"(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇g⦈ = ?uof_a⦇ArrVal⦈⦇g⦈"
by
(
cs_concl cs_shallow
cs_simp:
cf_adj_Comp_commute_RL
adj_cs_simps
cat_cs_simps
cat_op_simps
cat_prod_cs_simps
cs_intro:
adj_cs_intros
ntcf_cs_intros
cat_cs_intros
cat_op_intros
cat_prod_cs_intros
)
qed (use arr_Set_φ_xa arr_Set_uof_a in auto)
qed (use φ_xa uof_a in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+
qed
lemma (in is_cf_adjunction) cf_adj_umap_of_unit':
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
and "a ∈⇩∘ 𝔇⦇Obj⦈"
and "η = η⇩C Φ⦇NTMap⦈⦇x⦈"
and "𝔉x = 𝔉⦇ObjMap⦈⦇x⦈"
shows "Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ = umap_of 𝔊 x 𝔉x η a"
using assms(1,2) unfolding assms(3,4) by (rule cf_adj_umap_of_unit)
lemma (in is_cf_adjunction) cf_adjunction_unit_component_is_ua_of:
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
shows "universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⇩C Φ⦇NTMap⦈⦇x⦈)"
(is ‹universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) ?ηx›)
proof(rule RL.cf_ua_of_if_ntcf_ua_of_is_iso_ntcf)
from is_cf_adjunction_axioms assms show "𝔉⦇ObjMap⦈⦇x⦈ ∈⇩∘ 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)
from is_cf_adjunction_axioms assms show
"η⇩C Φ⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)
show
"ntcf_ua_of α 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⇩C Φ⦇NTMap⦈⦇x⦈) :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇x⦈,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙ℭ(x,-) ∘⇩C⇩F 𝔊 :
𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
(is ‹?ntcf_ua_of : ?H𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o ?H𝔊 : 𝔇 ↦↦⇩C⇘α⇙ cat_Set α›)
proof(rule is_iso_ntcfI)
from is_cf_adjunction_axioms assms show
"?ntcf_ua_of : ?H𝔉 ↦⇩C⇩F ?H𝔊 : 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (intro RL.cf_ntcf_ua_of_is_ntcf)
(cs_concl cs_shallow cs_intro: cat_cs_intros adj_cs_intros)+
fix a assume prems: "a ∈⇩∘ 𝔇⦇Obj⦈"
from assms prems have
"Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) ?ηx a"
(is ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ = ?uof_a›)
by (rule cf_adj_umap_of_unit)
from assms prems L.category_axioms R.category_axioms have
"[x, a]⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_op_intros cat_prod_cs_intros)
from
NT.iso_ntcf_is_iso_arr[
OF this, unfolded cf_adj_umap_of_unit[OF assms prems]
]
is_cf_adjunction_axioms assms prems
L.category_axioms R.category_axioms
have "?uof_a : Hom 𝔇 (𝔉⦇ObjMap⦈⦇x⦈) a ↦⇩i⇩s⇩o⇘cat_Set α⇙ Hom ℭ x (𝔊⦇ObjMap⦈⦇a⦈)"
by
(
cs_prems
cs_simp: cat_cs_simps
cs_intro:
cat_cs_intros cat_op_intros adj_cs_intros cat_prod_cs_intros
)
with is_cf_adjunction_axioms assms prems show
"?ntcf_ua_of⦇NTMap⦈⦇a⦈ : ?H𝔉⦇ObjMap⦈⦇a⦈ ↦⇩i⇩s⇩o⇘cat_Set α⇙ ?H𝔊⦇ObjMap⦈⦇a⦈"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros adj_cs_intros
)
qed
qed
subsection‹Counit›
subsubsection‹Definition and elementary properties›
definition cf_adjunction_counit :: "V ⇒ V" (‹ε⇩C›)
where "ε⇩C Φ =
[
(
λx∈⇩∘Φ⦇AdjLeft⦈⦇HomCod⦈⦇Obj⦈.
(Φ⦇AdjNT⦈⦇NTMap⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈, x⦈⇩∙)¯⇩S⇩e⇩t⦇ArrVal⦈⦇
Φ⦇AdjLeft⦈⦇HomDom⦈⦇CId⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈⦈
⦈
),
(Φ⦇AdjLeft⦈) ∘⇩C⇩F (Φ⦇AdjRight⦈),
cf_id (Φ⦇AdjLeft⦈⦇HomCod⦈),
Φ⦇AdjLeft⦈⦇HomCod⦈,
Φ⦇AdjLeft⦈⦇HomCod⦈
]⇩∘"
text‹Components.›
lemma cf_adjunction_counit_components:
shows "ε⇩C Φ⦇NTMap⦈ =
(
λx∈⇩∘Φ⦇AdjLeft⦈⦇HomCod⦈⦇Obj⦈.
(Φ⦇AdjNT⦈⦇NTMap⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈, x⦈⇩∙)¯⇩S⇩e⇩t⦇ArrVal⦈⦇
Φ⦇AdjLeft⦈⦇HomDom⦈⦇CId⦈⦇Φ⦇AdjRight⦈⦇ObjMap⦈⦇x⦈⦈
⦈
)"
and "ε⇩C Φ⦇NTDom⦈ = (Φ⦇AdjLeft⦈) ∘⇩C⇩F (Φ⦇AdjRight⦈)"
and "ε⇩C Φ⦇NTCod⦈ = cf_id (Φ⦇AdjLeft⦈⦇HomCod⦈)"
and "ε⇩C Φ⦇NTDGDom⦈ = Φ⦇AdjLeft⦈⦇HomCod⦈"
and "ε⇩C Φ⦇NTDGCod⦈ = Φ⦇AdjLeft⦈⦇HomCod⦈"
unfolding cf_adjunction_counit_def nt_field_simps
by (simp_all add: nat_omega_simps)
context is_cf_adjunction
begin
lemma cf_adjunction_counit_components':
shows "ε⇩C Φ⦇NTMap⦈ =
(
λx∈⇩∘𝔇⦇Obj⦈.
(Φ⦇AdjNT⦈⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈, x⦈⇩∙)¯⇩S⇩e⇩t⦇ArrVal⦈⦇ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈⦈
)"
and "ε⇩C Φ⦇NTDom⦈ = 𝔉 ∘⇩C⇩F 𝔊"
and "ε⇩C Φ⦇NTCod⦈ = cf_id 𝔇"
and "ε⇩C Φ⦇NTDGDom⦈ = 𝔇"
and "ε⇩C Φ⦇NTDGCod⦈ = 𝔇"
unfolding cf_adjunction_counit_components
by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)+
mk_VLambda cf_adjunction_counit_components'(1)
|vdomain cf_adjunction_counit_NTMap_vdomain[adj_cs_simps]|
|app cf_adjunction_counit_NTMap_app[adj_cs_simps]|
end
mk_VLambda cf_adjunction_counit_components(1)
|vsv cf_adjunction_counit_NTMap_vsv[adj_cs_intros]|
lemmas [adj_cs_simps] =
is_cf_adjunction.cf_adjunction_counit_NTMap_vdomain
is_cf_adjunction.cf_adjunction_counit_NTMap_app
subsubsection‹Duality for the unit and counit›
lemma (in is_cf_adjunction) cf_adjunction_unit_NTMap_op:
"η⇩C (op_cf_adj Φ)⦇NTMap⦈ = ε⇩C Φ⦇NTMap⦈"
proof-
interpret op_Φ:
is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
by (rule is_cf_adjunction_op)
show ?thesis
proof
(
rule vsv_eqI,
unfold
cf_adjunction_counit_NTMap_vdomain
op_Φ.cf_adjunction_unit_NTMap_vdomain
)
fix a assume prems: "a ∈⇩∘ op_cat 𝔇⦇Obj⦈"
then have a: "a ∈⇩∘ 𝔇⦇Obj⦈" unfolding cat_op_simps by simp
from is_cf_adjunction_axioms a show
"η⇩C (op_cf_adj Φ)⦇NTMap⦈⦇a⦈ = ε⇩C Φ⦇NTMap⦈⦇a⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_Set_cs_simps cat_cs_simps cat_op_simps adj_cs_simps
cs_intro:
cat_arrow_cs_intros cat_cs_intros cat_op_intros cat_prod_cs_intros
)
qed
(
simp_all add:
cat_op_simps cf_adjunction_counit_NTMap_vsv cf_adjunction_unit_NTMap_vsv
)
qed
lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_unit_NTMap_op
lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_op:
"ε⇩C (op_cf_adj Φ)⦇NTMap⦈ = η⇩C Φ⦇NTMap⦈"
by
(
rule is_cf_adjunction.cf_adjunction_unit_NTMap_op[
OF is_cf_adjunction_op,
unfolded is_cf_adjunction.cf_adjunction_op_cf_adj_op_cf_adj[
OF is_cf_adjunction_axioms
],
unfolded cat_op_simps,
symmetric
]
)
lemmas [cat_op_simps] = is_cf_adjunction.cf_adjunction_counit_NTMap_op
lemma (in is_cf_adjunction) op_ntcf_cf_adjunction_counit:
"op_ntcf (ε⇩C Φ) = η⇩C (op_cf_adj Φ)"
(is ‹?ε = ?η›)
proof(rule vsv_eqI)
interpret op_Φ:
is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
by (rule is_cf_adjunction_op)
have dom_lhs: "𝒟⇩∘ ?ε = 5⇩ℕ" unfolding op_ntcf_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ ?η = 5⇩ℕ"
unfolding cf_adjunction_unit_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ ?ε = 𝒟⇩∘ ?η" unfolding dom_lhs dom_rhs by simp
show "a ∈⇩∘ 𝒟⇩∘ ?ε ⟹ ?ε⦇a⦈ = ?η⦇a⦈" for a
by
(
unfold dom_lhs,
elim_in_numeral,
fold nt_field_simps,
unfold cf_adjunction_unit_NTMap_op,
unfold
cf_adjunction_counit_components'
cf_adjunction_unit_components'
op_Φ.cf_adjunction_counit_components'
op_Φ.cf_adjunction_unit_components'
cat_op_simps
)
simp_all
qed (auto simp: op_ntcf_def cf_adjunction_unit_def)
lemmas [cat_op_simps] = is_cf_adjunction.op_ntcf_cf_adjunction_counit
lemma (in is_cf_adjunction) op_ntcf_cf_adjunction_unit:
"op_ntcf (η⇩C Φ) = ε⇩C (op_cf_adj Φ)"
(is ‹?η = ?ε›)
proof(rule vsv_eqI)
interpret op_Φ:
is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ‹op_cf_adj Φ›
by (rule is_cf_adjunction_op)
have dom_lhs: "𝒟⇩∘ ?η = 5⇩ℕ"
unfolding op_ntcf_def by (simp add: nat_omega_simps)
have dom_rhs: "𝒟⇩∘ ?ε = 5⇩ℕ"
unfolding cf_adjunction_counit_def by (simp add: nat_omega_simps)
show "𝒟⇩∘ ?η = 𝒟⇩∘ ?ε" unfolding dom_lhs dom_rhs by simp
show "a ∈⇩∘ 𝒟⇩∘ ?η ⟹ ?η⦇a⦈ = ?ε⦇a⦈" for a
by
(
unfold dom_lhs,
elim_in_numeral,
fold nt_field_simps,
unfold cf_adjunction_counit_NTMap_op,
unfold
cf_adjunction_counit_components'
cf_adjunction_unit_components'
op_Φ.cf_adjunction_counit_components'
op_Φ.cf_adjunction_unit_components'
cat_op_simps
)
simp_all
qed (auto simp: op_ntcf_def cf_adjunction_counit_def)
lemmas [cat_op_simps] = is_cf_adjunction.op_ntcf_cf_adjunction_unit
subsubsection‹Natural transformation map›
lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_is_arr:
assumes "x ∈⇩∘ 𝔇⦇Obj⦈"
shows "ε⇩C Φ⦇NTMap⦈⦇x⦈ : 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ↦⇘𝔇⇙ x"
proof-
from assms have x: "x ∈⇩∘ op_cat 𝔇⦇Obj⦈" unfolding cat_op_simps by simp
show ?thesis
by
(
rule is_cf_adjunction.cf_adjunction_unit_NTMap_is_arr[
OF is_cf_adjunction_op x,
unfolded cf_adjunction_unit_NTMap_op cat_op_simps
]
)
qed
lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_is_arr':
assumes "x ∈⇩∘ 𝔇⦇Obj⦈"
and "a = 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
and "b = x"
and "𝔇' = 𝔇"
shows "ε⇩C Φ⦇NTMap⦈⦇x⦈ : a ↦⇘𝔇'⇙ b"
using assms(1) unfolding assms(2-4) by (rule cf_adjunction_counit_NTMap_is_arr)
lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_counit_NTMap_is_arr'
lemma (in is_cf_adjunction) cf_adjunction_counit_NTMap_vrange:
"ℛ⇩∘ (ε⇩C Φ⦇NTMap⦈) ⊆⇩∘ 𝔇⦇Arr⦈"
by
(
rule is_cf_adjunction.cf_adjunction_unit_NTMap_vrange[
OF is_cf_adjunction_op,
unfolded cf_adjunction_unit_NTMap_op cat_op_simps
]
)
subsubsection‹Counit is a natural transformation›
lemma (in is_cf_adjunction) cf_adjunction_counit_is_ntcf:
"ε⇩C Φ : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
proof-
from is_cf_adjunction.cf_adjunction_unit_is_ntcf[OF is_cf_adjunction_op] have
"ε⇩C Φ :
op_cf (op_cf 𝔉 ∘⇩C⇩F op_cf 𝔊) ↦⇩C⇩F op_cf (cf_id (op_cat 𝔇)) :
op_cat (op_cat 𝔇) ↦↦⇩C⇘α⇙ op_cat (op_cat 𝔇)"
unfolding
is_cf_adjunction.op_ntcf_cf_adjunction_unit[
OF is_cf_adjunction_op, unfolded cat_op_simps, symmetric
]
by (rule is_ntcf.is_ntcf_op)
then show ?thesis unfolding cat_op_simps .
qed
lemma (in is_cf_adjunction) cf_adjunction_counit_is_ntcf':
assumes "𝔖 = 𝔉 ∘⇩C⇩F 𝔊"
and "𝔖' = cf_id 𝔇"
and "𝔄 = 𝔇"
and "𝔅 = 𝔇"
shows "ε⇩C Φ : 𝔖 ↦⇩C⇩F 𝔖' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
unfolding assms by (rule cf_adjunction_counit_is_ntcf)
lemmas [adj_cs_intros] = is_cf_adjunction.cf_adjunction_counit_is_ntcf'
subsubsection‹Every component of a counit is a universal arrow›
text‹
The lemmas in this subsection are based on elements of the statement of
Theorem 1 in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
lemma (in is_cf_adjunction) cf_adj_umap_fo_counit:
assumes "x ∈⇩∘ 𝔇⦇Obj⦈" and "a ∈⇩∘ ℭ⦇Obj⦈"
shows "op_cf_adj Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙ =
umap_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (ε⇩C Φ⦇NTMap⦈⦇x⦈) a"
by
(
rule is_cf_adjunction.cf_adj_umap_of_unit[
OF is_cf_adjunction_op,
unfolded cat_op_simps,
OF assms,
unfolded cf_adjunction_unit_NTMap_op
]
)
lemma (in is_cf_adjunction) cf_adjunction_counit_component_is_ua_fo:
assumes "x ∈⇩∘ 𝔇⦇Obj⦈"
shows "universal_arrow_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (ε⇩C Φ⦇NTMap⦈⦇x⦈)"
by
(
rule is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
OF is_cf_adjunction_op,
unfolded cat_op_simps,
OF assms,
unfolded cf_adjunction_unit_NTMap_op
]
)
subsubsection‹Further properties›
lemma (in is_cf_adjunction) cf_adj_AdjNT_cf_adjunction_unit:
assumes "x ∈⇩∘ ℭ⦇Obj⦈" and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
shows
"𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇x⦈ =
(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈"
proof-
from assms(1) have "𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇x⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from cf_adj_Comp_commute_RL[OF assms(1) this assms(2)] assms show ?thesis
by
(
cs_prems cs_shallow
cs_simp:
cat_cs_simps
is_cf_adjunction.cf_adjunction_unit_NTMap_app[symmetric]
cs_intro: adj_cs_intros
)
qed
lemma (in is_cf_adjunction) cf_adj_AdjNT_cf_adjunction_counit:
assumes "x ∈⇩∘ 𝔇⦇Obj⦈" and "g : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈"
shows
"ε⇩C Φ⦇NTMap⦈⦇x⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇g⦈ =
(Φ⦇AdjNT⦈⦇NTMap⦈⦇a, x⦈⇩∙)¯⇩C⇘cat_Set α⇙⦇ArrVal⦈⦇g⦈"
using
is_cf_adjunction.cf_adj_AdjNT_cf_adjunction_unit
[
OF is_cf_adjunction_op,
unfolded cat_op_simps cf_adjunction_unit_NTMap_op,
OF assms
]
assms
by
(
cs_prems
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_cs_intros
adj_cs_intros
cat_op_intros
cat_prod_cs_intros
)
lemma (in is_cf_adjunction) cf_adj_counit_unit_app[adj_cs_simps]:
assumes "x ∈⇩∘ 𝔇⦇Obj⦈" and "g : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈"
shows "𝔊⦇ArrMap⦈⦇ε⇩C Φ⦇NTMap⦈⦇x⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇g⦈⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇a⦈ = g"
proof-
from assms(2) have a: "a ∈⇩∘ ℭ⦇Obj⦈" by auto
from assms have inv_Φ_g:
"(Φ⦇AdjNT⦈⦇NTMap⦈⦇a, x⦈⇩∙)¯⇩C⇘cat_Set α⇙⦇ArrVal⦈⦇g⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ x"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
adj_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from assms show ?thesis
unfolding
cf_adj_AdjNT_cf_adjunction_counit[OF assms]
cf_adj_AdjNT_cf_adjunction_unit[OF a inv_Φ_g]
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
adj_cs_intros
cat_prod_cs_intros
cat_op_intros
)
qed
lemmas [cat_cs_simps] = is_cf_adjunction.cf_adj_counit_unit_app
lemma (in is_cf_adjunction) cf_adj_unit_counit_app[adj_cs_simps]:
assumes "x ∈⇩∘ ℭ⦇Obj⦈" and "f : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ a"
shows "ε⇩C Φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇x⦈⦈ = f"
proof-
from assms(2) have a: "a ∈⇩∘ 𝔇⦇Obj⦈" by auto
from assms have Φ_f:
"(Φ⦇AdjNT⦈⦇NTMap⦈⦇x, a⦈⇩∙)⦇ArrVal⦈⦇f⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇a⦈"
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
adj_cs_intros
cat_prod_cs_intros
cat_op_intros
)
from assms show ?thesis
unfolding
cf_adj_AdjNT_cf_adjunction_unit[OF assms]
cf_adj_AdjNT_cf_adjunction_counit[OF a Φ_f]
by
(
cs_concl
cs_simp: cat_cs_simps cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
adj_cs_intros
cat_prod_cs_intros
cat_op_intros
)
qed
lemmas [cat_cs_simps] = is_cf_adjunction.cf_adj_unit_counit_app
subsection‹Counit-unit equations›
text‹
The following equations appear as part of the statement of
Theorem 1 in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
These equations also appear in \<^cite>‹"noauthor_wikipedia_2001"›,
where they are named ‹counit-unit equations›.
›
lemma (in is_cf_adjunction) cf_adjunction_counit_unit:
"(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ε⇩C Φ) ∙⇩N⇩T⇩C⇩F (η⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) = ntcf_id 𝔊"
(is ‹(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ε) ∙⇩N⇩T⇩C⇩F (?η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) = ntcf_id 𝔊›)
proof(rule ntcf_eqI)
from is_cf_adjunction_axioms show
"(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ε) ∙⇩N⇩T⇩C⇩F (?η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) : 𝔊 ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
show "ntcf_id 𝔊 : 𝔊 ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
by (rule is_functor.cf_ntcf_id_is_ntcf[OF RL.is_functor_axioms])
from is_cf_adjunction_axioms have dom_lhs:
"𝒟⇩∘ (((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ε) ∙⇩N⇩T⇩C⇩F (?η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊))⦇NTMap⦈) = 𝔇⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros
)
from is_cf_adjunction_axioms have dom_rhs: "𝒟⇩∘ (ntcf_id 𝔊⦇NTMap⦈) = 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: adj_cs_intros)
show "((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ε) ∙⇩N⇩T⇩C⇩F (?η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊))⦇NTMap⦈ = ntcf_id 𝔊⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ 𝔇⦇Obj⦈"
let ?φ_aa = ‹Φ⦇AdjNT⦈⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇a⦈, a⦈⇩∙›
have "category α (cat_Set α)"
by (rule category_cat_Set)
from is_cf_adjunction_axioms prems
L.category_axioms R.category_axioms
L.category_op R.category_op
LR.is_functor_axioms RL.is_functor_axioms
category_cat_Set
have
"?φ_aa⦇ArrVal⦈⦇?ε⦇NTMap⦈⦇a⦈⦈ =
(?φ_aa ∘⇩A⇘cat_Set α⇙ ?φ_aa¯⇩C⇘cat_Set α⇙)⦇ArrVal⦈⦇ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈⦈"
by
(
cs_concl cs_shallow
cs_simp:
𝒵.cat_Set_Comp_ArrVal
cat_Set_the_inverse[symmetric]
cat_cs_simps adj_cs_simps cat_prod_cs_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
cat_op_intros
adj_cs_intros
cat_prod_cs_intros
)
also from
is_cf_adjunction_axioms prems
L.category_axioms R.category_axioms
L.category_op R.category_op
LR.is_functor_axioms RL.is_functor_axioms
category_cat_Set
have "… = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp:
cat_cs_simps
cat_Set_components(1)
category.cat_the_inverse_Comp_CId
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
cat_op_intros
cat_prod_cs_intros
)
finally have [cat_cs_simps]:
"?φ_aa⦇ArrVal⦈⦇?ε⦇NTMap⦈⦇a⦈⦈ = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇a⦈⦈"
by simp
from
prems is_cf_adjunction_axioms
L.category_axioms R.category_axioms
show "((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ε) ∙⇩N⇩T⇩C⇩F (?η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊))⦇NTMap⦈⦇a⦈ = ntcf_id 𝔊⦇NTMap⦈⦇a⦈"
by
(
cs_concl
cs_simp:
cat_Set_the_inverse[symmetric]
cf_adj_Comp_commute_RL
cat_cs_simps
adj_cs_simps
cat_prod_cs_simps
cat_op_simps
cs_intro:
cat_arrow_cs_intros
cat_cs_intros
adj_cs_intros
cat_prod_cs_intros
cat_op_intros
)
qed (auto intro: cat_cs_intros)
qed simp_all
lemmas [adj_cs_simps] = is_cf_adjunction.cf_adjunction_counit_unit
lemma (in is_cf_adjunction) cf_adjunction_unit_counit:
"(ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F η⇩C Φ) = ntcf_id 𝔉"
(is ‹(?ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?η) = ntcf_id 𝔉›)
proof-
from is_cf_adjunction_axioms have 𝔉η:
"𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?η : 𝔉 ↦⇩C⇩F 𝔉 ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
from is_cf_adjunction_axioms have ε𝔉:
"?ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉 : 𝔉 ∘⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 ↦⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
from 𝔉η ε𝔉 have ε𝔉_𝔉η:
"(?ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?η) : 𝔉 ↦⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from
is_cf_adjunction.cf_adjunction_counit_unit[
OF is_cf_adjunction_op,
unfolded
op_ntcf_cf_adjunction_unit[symmetric]
op_ntcf_cf_adjunction_counit[symmetric]
op_ntcf_cf_ntcf_comp[symmetric]
op_ntcf_ntcf_cf_comp[symmetric]
op_ntcf_ntcf_vcomp[symmetric]
op_ntcf_ntcf_vcomp[symmetric, OF ε𝔉 𝔉η]
LR.cf_ntcf_id_op_cf
]
have
"op_ntcf (op_ntcf ((?ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?η))) =
op_ntcf (op_ntcf (ntcf_id 𝔉))"
by simp
from this is_cf_adjunction_axioms ε𝔉_𝔉η show ?thesis
by
(
cs_prems cs_shallow
cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)
qed
lemmas [adj_cs_simps] = is_cf_adjunction.cf_adjunction_unit_counit
subsection‹
Construction of an adjunction from universal morphisms
from objects to functors
›
text‹
The subsection presents the construction of an adjunction given
a structured collection of universal morphisms from objects to functors.
The content of this subsection follows the statement and the proof
of Theorem 2-i in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
subsubsection‹
The natural transformation associated with the adjunction
constructed from universal morphisms from objects to functors
›
definition cf_adjunction_AdjNT_of_unit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η =
[
(λcd∈⇩∘(op_cat (𝔉⦇HomDom⦈) ×⇩C 𝔉⦇HomCod⦈)⦇Obj⦈.
umap_of 𝔊 (cd⦇0⦈) (𝔉⦇ObjMap⦈⦇cd⦇0⦈⦈) (η⦇NTMap⦈⦇cd⦇0⦈⦈) (cd⦇1⇩ℕ⦈)),
Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomCod⦈(𝔉-,-),
Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomDom⦈(-,𝔊-),
op_cat (𝔉⦇HomDom⦈) ×⇩C (𝔉⦇HomCod⦈),
cat_Set α
]⇩∘"
text‹Components.›
lemma cf_adjunction_AdjNT_of_unit_components:
shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈ =
(
λcd∈⇩∘(op_cat (𝔉⦇HomDom⦈) ×⇩C 𝔉⦇HomCod⦈)⦇Obj⦈.
umap_of 𝔊 (cd⦇0⦈) (𝔉⦇ObjMap⦈⦇cd⦇0⦈⦈) (η⦇NTMap⦈⦇cd⦇0⦈⦈) (cd⦇1⇩ℕ⦈)
)"
and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDom⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomCod⦈(𝔉-,-)"
and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTCod⦈ = Hom⇩O⇩.⇩C⇘α⇙𝔉⦇HomDom⦈(-,𝔊-)"
and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDGDom⦈ =
op_cat (𝔉⦇HomDom⦈) ×⇩C (𝔉⦇HomCod⦈)"
and "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTDGCod⦈ = cat_Set α"
unfolding cf_adjunction_AdjNT_of_unit_def nt_field_simps
by (simp_all add: nat_omega_simps)
subsubsection‹Natural transformation map›
lemma cf_adjunction_AdjNT_of_unit_NTMap_vsv[adj_cs_intros]:
"vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)"
unfolding cf_adjunction_AdjNT_of_unit_components by simp
lemma cf_adjunction_AdjNT_of_unit_NTMap_vdomain[adj_cs_simps]:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
shows "𝒟⇩∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) = (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
proof-
interpret is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
show ?thesis
unfolding cf_adjunction_AdjNT_of_unit_components
by (simp add: cat_cs_simps)
qed
lemma cf_adjunction_AdjNT_of_unit_NTMap_app[adj_cs_simps]:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇" and "c ∈⇩∘ ℭ⦇Obj⦈" and "d ∈⇩∘ 𝔇⦇Obj⦈"
shows
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇c, d⦈⇩∙ =
umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
from assms have "[c, d]⇩∘ ∈⇩∘ (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)
then show "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈ ⦇c, d⦈⇩∙ =
umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
unfolding cf_adjunction_AdjNT_of_unit_components
by (simp add: nat_omega_simps cat_cs_simps)
qed
lemma cf_adjunction_AdjNT_of_unit_NTMap_vrange:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
shows "ℛ⇩∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) ⊆⇩∘ cat_Set α⦇Arr⦈"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
show ?thesis
proof
(
rule vsv.vsv_vrange_vsubset,
unfold cf_adjunction_AdjNT_of_unit_NTMap_vdomain[OF assms(3)]
)
show "vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)"
by (intro adj_cs_intros)
fix cd assume prems: "cd ∈⇩∘ (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
then obtain c d where cd_def: "cd = [c, d]⇩∘"
and c: "c ∈⇩∘ ℭ⦇Obj⦈"
and d: "d ∈⇩∘ 𝔇⦇Obj⦈"
by
(
auto
simp: cat_op_simps
elim:
cat_prod_2_ObjE[OF 𝔉.HomDom.category_op 𝔉.HomCod.category_axioms]
)
from assms c d show
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈ ∈⇩∘ cat_Set α⦇Arr⦈"
unfolding cd_def
by
(
cs_concl
cs_simp: cat_cs_simps adj_cs_simps cs_intro: cat_cs_intros
)
qed
qed
subsubsection‹
Adjunction constructed from universal morphisms
from objects to functors is an adjunction
›
lemma cf_adjunction_AdjNT_of_unit_is_ntcf:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› η by (rule assms(5))
show ?thesis
proof(intro is_ntcfI')
show "vfsequence (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η)"
unfolding cf_adjunction_AdjNT_of_unit_def by simp
show "vcard (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η) = 5⇩ℕ"
unfolding cf_adjunction_AdjNT_of_unit_def by (simp add: nat_omega_simps)
from assms(2,3) show
"Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) : op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms show "Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) : op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
show "vsv (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈)"
by (intro adj_cs_intros)
from assms show
"𝒟⇩∘ (cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈) = (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps adj_cs_simps)
show "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈ :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)⦇ObjMap⦈⦇cd⦈ ↦⇘cat_Set α⇙
Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ObjMap⦈⦇cd⦈"
if "cd ∈⇩∘ (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈" for cd
proof-
from that obtain c d
where cd_def: "cd = [c, d]⇩∘" and c: "c ∈⇩∘ ℭ⦇Obj⦈" and d: "d ∈⇩∘ 𝔇⦇Obj⦈"
by
(
auto
simp: cat_op_simps
elim: cat_prod_2_ObjE[OF ℭ.category_op 𝔇.category_axioms]
)
from assms c d show ?thesis
unfolding cd_def
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
qed
show
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇c'd'⦈ ∘⇩A⇘cat_Set α⇙
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)⦇ArrMap⦈⦇gf⦈ =
Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⦇ArrMap⦈⦇gf⦈ ∘⇩A⇘cat_Set α⇙
cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⦇NTMap⦈⦇cd⦈"
if "gf : cd ↦⇘op_cat ℭ ×⇩C 𝔇⇙ c'd'" for cd c'd' gf
proof-
from that obtain g f c c' d d'
where gf_def: "gf = [g, f]⇩∘"
and cd_def: "cd = [c, d]⇩∘"
and c'd'_def: "c'd' = [c', d']⇩∘"
and g: "g : c' ↦⇘ℭ⇙ c"
and f: "f : d ↦⇘𝔇⇙ d'"
by
(
auto
simp: cat_op_simps
elim: cat_prod_2_is_arrE[OF ℭ.category_op 𝔇.category_axioms]
)
from assms g f that show ?thesis
unfolding gf_def cd_def c'd'_def
by
(
cs_concl
cs_simp: cf_umap_of_cf_hom_unit_commute adj_cs_simps cat_cs_simps
cs_intro: cat_cs_intros cat_op_intros cat_prod_cs_intros
)
qed
qed (auto simp: cf_adjunction_AdjNT_of_unit_components cat_cs_simps)
qed
lemma cf_adjunction_AdjNT_of_unit_is_ntcf'[adj_cs_intros]:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
and "𝔖 = Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)"
and "𝔖' = Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)"
and "𝔄 = op_cat ℭ ×⇩C 𝔇"
and "𝔅 = cat_Set α"
shows "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η : 𝔖 ↦⇩C⇩F 𝔖' : 𝔄 ↦↦⇩C⇘α⇙ 𝔅"
using assms(1-5) unfolding assms(6-9)
by (rule cf_adjunction_AdjNT_of_unit_is_ntcf)
subsubsection‹
Adjunction constructed from universal morphisms from objects to functors
›
definition cf_adjunction_of_unit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "cf_adjunction_of_unit α 𝔉 𝔊 η =
[𝔉, 𝔊, cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η]⇩∘"
text‹Components.›
lemma cf_adjunction_of_unit_components:
shows [adj_cs_simps]: "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjLeft⦈ = 𝔉"
and [adj_cs_simps]: "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjRight⦈ = 𝔊"
and "cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈ =
cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η"
unfolding cf_adjunction_of_unit_def adj_field_simps
by (simp_all add: nat_omega_simps)
text‹Natural transformation map.›
lemma cf_adjunction_of_unit_AdjNT_NTMap_vdomain[adj_cs_simps]:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
shows "𝒟⇩∘ (cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈⦇NTMap⦈) =
(op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
using assms
unfolding cf_adjunction_of_unit_components(3)
by (rule cf_adjunction_AdjNT_of_unit_NTMap_vdomain)
lemma cf_adjunction_of_unit_AdjNT_NTMap_app[adj_cs_simps]:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇" and "c ∈⇩∘ ℭ⦇Obj⦈" and "d ∈⇩∘ 𝔇⦇Obj⦈"
shows
"cf_adjunction_of_unit α 𝔉 𝔊 η⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈⇩∙ =
umap_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈) d"
using assms
unfolding cf_adjunction_of_unit_components(3)
by (rule cf_adjunction_AdjNT_of_unit_NTMap_app)
text‹
The adjunction constructed from universal morphisms from objects to
functors is an adjunction.
›
lemma cf_adjunction_of_unit_is_cf_adjunction:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
and "⋀x. x ∈⇩∘ ℭ⦇Obj⦈ ⟹ universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈)"
shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› η by (rule assms(5))
show caou_η: "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
proof
(
intro
is_cf_adjunctionI[OF _ _ assms(1-4)]
is_iso_ntcf_if_bnt_proj_snd_is_iso_ntcf[
OF ℭ.category_op 𝔇.category_axioms
],
unfold cat_op_simps cf_adjunction_of_unit_components
)
show caou_η: "cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-) :
op_cat ℭ ×⇩C 𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
unfolding cf_adjunction_of_unit_components
by (rule cf_adjunction_AdjNT_of_unit_is_ntcf[OF assms(1-5)])
fix a assume prems: "a ∈⇩∘ ℭ⦇Obj⦈"
have ua_of_ηa:
"ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈) :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦⇩C⇩F⇩.⇩i⇩s⇩o Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) ∘⇩C⇩F 𝔊 :
𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
rule is_functor.cf_ntcf_ua_of_is_iso_ntcf[
OF assms(4) assms(6)[OF prems]
]
)
have [adj_cs_simps]:
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F =
ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)"
proof(rule ntcf_eqI)
from assms(1-5) caou_η prems show lhs:
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) ∘⇩C⇩F 𝔊 :
𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cat_op_simps
cs_intro: cat_cs_intros cat_op_intros
)
from ua_of_ηa show rhs:
"ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈) :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉⦇ObjMap⦈⦇a⦈,-) ↦⇩C⇩F Hom⇩O⇩.⇩C⇘α⇙ℭ(a,-) ∘⇩C⇩F 𝔊 :
𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by (cs_concl cs_shallow cs_intro: ntcf_cs_intros)
from lhs have dom_lhs:
"𝒟⇩∘ ((cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F)⦇NTMap⦈) =
𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from lhs assms(4) have dom_rhs:
"𝒟⇩∘ (ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈) = 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show
"(cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F)⦇NTMap⦈ =
ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix d assume prems': "d ∈⇩∘ 𝔇⦇Obj⦈"
from assms(3,4) prems prems' show
"(cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F)⦇NTMap⦈⦇d⦈ =
ntcf_ua_of α 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (η⦇NTMap⦈⦇a⦈)⦇NTMap⦈⦇d⦈"
by (cs_concl cs_shallow cs_simp: adj_cs_simps cat_cs_simps)
qed (simp_all add: bnt_proj_snd_NTMap_vsv 𝔊.ntcf_ua_of_NTMap_vsv)
qed simp_all
from assms(1-5) assms(6)[OF prems] prems show
"cf_adjunction_AdjNT_of_unit α 𝔉 𝔊 η⇘op_cat ℭ,𝔇⇙(a,-)⇩N⇩T⇩C⇩F :
Hom⇩O⇩.⇩C⇘α⇙𝔇(𝔉-,-)⇘op_cat ℭ,𝔇⇙(a,-)⇩C⇩F ↦⇩C⇩F⇩.⇩i⇩s⇩o
Hom⇩O⇩.⇩C⇘α⇙ℭ(-,𝔊-)⇘op_cat ℭ,𝔇⇙(a,-)⇩C⇩F :
𝔇 ↦↦⇩C⇘α⇙ cat_Set α"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps cs_intro: cat_cs_intros
)
qed (auto simp: cf_adjunction_of_unit_def nat_omega_simps)
show "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
proof(rule ntcf_eqI)
from caou_η show lhs:
"η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) :
cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_shallow cs_intro: adj_cs_intros)
show rhs: "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (auto intro: cat_cs_intros)
from lhs have dom_lhs:
"𝒟⇩∘ (η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈) = ℭ⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
have dom_rhs: "𝒟⇩∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈" by (auto simp: cat_cs_simps)
show "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈ = η⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ ℭ⦇Obj⦈"
from assms(1-5) prems caou_η show
"η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈⦇a⦈ = η⦇NTMap⦈⦇a⦈"
by
(
cs_concl cs_shallow
cs_simp:
adj_cs_simps cat_cs_simps cf_adjunction_of_unit_components(3)
cs_intro: cat_cs_intros
)
qed (auto intro: adj_cs_intros)
qed simp_all
qed
subsection‹
Construction of an adjunction from a functor and universal morphisms
from objects to functors
›
text‹
The subsection presents the construction of an adjunction given
a functor and a structured collection of universal morphisms
from objects to functors.
The content of this subsection follows the statement and the proof
of Theorem 2-ii in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
subsubsection‹Left adjoint›
definition cf_la_of_ra :: "(V ⇒ V) ⇒ V ⇒ V ⇒ V"
where "cf_la_of_ra F 𝔊 η =
[
(λx∈⇩∘𝔊⦇HomCod⦈⦇Obj⦈. F x),
(
λh∈⇩∘𝔊⦇HomCod⦈⦇Arr⦈. THE f'.
f' : F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈) ↦⇘𝔊⦇HomDom⦈⇙ F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈) ∧
η⦇𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈⦈ ∘⇩A⇘𝔊⦇HomCod⦈⇙ h =
(
umap_of
𝔊
(𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈)
(F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈))
(η⦇𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈⦈)
(F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈))
)⦇ArrVal⦈⦇f'⦈
),
𝔊⦇HomCod⦈,
𝔊⦇HomDom⦈
]⇩∘"
text‹Components.›
lemma cf_la_of_ra_components:
shows "cf_la_of_ra F 𝔊 η⦇ObjMap⦈ = (λx∈⇩∘𝔊⦇HomCod⦈⦇Obj⦈. F x)"
and "cf_la_of_ra F 𝔊 η⦇ArrMap⦈ =
(
λh∈⇩∘𝔊⦇HomCod⦈⦇Arr⦈. THE f'.
f' : F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈) ↦⇘𝔊⦇HomDom⦈⇙ F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈) ∧
η⦇𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈⦈ ∘⇩A⇘𝔊⦇HomCod⦈⇙ h =
(
umap_of
𝔊
(𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈)
(F (𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈))
(η⦇𝔊⦇HomCod⦈⦇Dom⦈⦇h⦈⦈)
(F (𝔊⦇HomCod⦈⦇Cod⦈⦇h⦈))
)⦇ArrVal⦈⦇f'⦈
)"
and "cf_la_of_ra F 𝔊 η⦇HomDom⦈ = 𝔊⦇HomCod⦈"
and "cf_la_of_ra F 𝔊 η⦇HomCod⦈ = 𝔊⦇HomDom⦈"
unfolding cf_la_of_ra_def dghm_field_simps by (simp_all add: nat_omega_simps)
subsubsection‹Object map›
mk_VLambda cf_la_of_ra_components(1)
|vsv cf_la_of_ra_ObjMap_vsv[adj_cs_intros]|
mk_VLambda (in is_functor)
cf_la_of_ra_components(1)[where ?𝔊=𝔉, unfolded cf_HomCod]
|vdomain cf_la_of_ra_ObjMap_vdomain[adj_cs_simps]|
|app cf_la_of_ra_ObjMap_app[adj_cs_simps]|
lemmas [adj_cs_simps] =
is_functor.cf_la_of_ra_ObjMap_vdomain
is_functor.cf_la_of_ra_ObjMap_app
subsubsection‹Arrow map›
mk_VLambda cf_la_of_ra_components(2)
|vsv cf_la_of_ra_ArrMap_vsv[adj_cs_intros]|
mk_VLambda (in is_functor)
cf_la_of_ra_components(2)[where ?𝔊=𝔉, unfolded cf_HomCod cf_HomDom]
|vdomain cf_la_of_ra_ArrMap_vdomain[adj_cs_simps]|
|app cf_la_of_ra_ArrMap_app|
lemmas [adj_cs_simps] = is_functor.cf_la_of_ra_ArrMap_vdomain
lemma (in is_functor) cf_la_of_ra_ArrMap_app':
assumes "h : a ↦⇘𝔅⇙ b"
shows
"cf_la_of_ra F 𝔉 η⦇ArrMap⦈⦇h⦈ =
(
THE f'.
f' : F a ↦⇘𝔄⇙ F b ∧
η⦇b⦈ ∘⇩A⇘𝔅⇙ h = umap_of 𝔉 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
)"
proof-
from assms have h: "h ∈⇩∘ 𝔅⦇Arr⦈" by (simp add: cat_cs_intros)
from assms have h_Dom: "𝔅⦇Dom⦈⦇h⦈ = a" and h_Cod: "𝔅⦇Cod⦈⦇h⦈ = b"
by (simp_all add: cat_cs_simps)
show ?thesis by (rule cf_la_of_ra_ArrMap_app[OF h, unfolded h_Dom h_Cod])
qed
lemma cf_la_of_ra_ArrMap_app_unique:
assumes "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "f : a ↦⇘ℭ⇙ b"
and "universal_arrow_of 𝔊 a (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
and "universal_arrow_of 𝔊 b (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
shows "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F b"
and "η⦇b⦈ ∘⇩A⇘ℭ⇙ f =
umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈⦈"
and "⋀f'.
⟦
f' : F a ↦⇘𝔇⇙ F b;
η⦇b⦈ ∘⇩A⇘ℭ⇙ f = umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
⟧ ⟹ cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ = f'"
proof-
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(1))
from assms(2) have a: "a ∈⇩∘ ℭ⦇Obj⦈" and b: "b ∈⇩∘ ℭ⦇Obj⦈"
by (simp_all add: cat_cs_intros)
note ua_η_a = 𝔊.universal_arrow_ofD[OF assms(3)]
note ua_η_b = 𝔊.universal_arrow_ofD[OF assms(4)]
from ua_η_b(2) have [cat_cs_intros]:
"⟦ c = b; c' = 𝔊⦇ObjMap⦈⦇cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈⦈ ⟧ ⟹ η⦇b⦈ : c ↦⇘ℭ⇙ c'"
for c c'
by auto
from assms(1,2) ua_η_a(2) have ηa_f:
"η⦇b⦈ ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(1,2) have lara_a: "cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈ = F a"
and lara_b: "cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈ = F b"
by (cs_concl cs_simp: adj_cs_simps cs_intro: cat_cs_intros)+
from theD
[
OF
ua_η_a(3)[OF ua_η_b(1) ηa_f, unfolded lara_a lara_b]
𝔊.cf_la_of_ra_ArrMap_app'[OF assms(2), of F η]
]
show "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F b"
and "η⦇b⦈ ∘⇩A⇘ℭ⇙ f = umap_of
𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈⦈"
and "⋀f'.
⟦
f' : F a ↦⇘𝔇⇙ F b;
η⦇b⦈ ∘⇩A⇘ℭ⇙ f = umap_of 𝔊 a (F a) (η⦇a⦈) (F b)⦇ArrVal⦈⦇f'⦈
⟧ ⟹ cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ = f'"
by blast+
qed
lemma cf_la_of_ra_ArrMap_app_is_arr[adj_cs_intros]:
assumes "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "f : a ↦⇘ℭ⇙ b"
and "universal_arrow_of 𝔊 a (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
and "universal_arrow_of 𝔊 b (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
and "Fa = F a"
and "Fb = F b"
shows "cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇f⦈ : Fa ↦⇘𝔇⇙ Fb"
using assms(1-4) unfolding assms(5,6) by (rule cf_la_of_ra_ArrMap_app_unique)
subsubsection‹
An adjunction constructed from a functor and universal morphisms
from objects to functors is an adjunction
›
lemma cf_la_of_ra_is_functor:
assumes "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹ F c ∈⇩∘ 𝔇⦇Obj⦈"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹
universal_arrow_of 𝔊 c (cf_la_of_ra F 𝔊 η⦇ObjMap⦈⦇c⦈) (η⦇c⦈)"
and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
𝔊⦇ArrMap⦈⦇cf_la_of_ra F 𝔊 η⦇ArrMap⦈⦇h⦈⦈ ∘⇩A⇘ℭ⇙ η⦇c⦈ = η⦇c'⦈ ∘⇩A⇘ℭ⇙ h"
shows "cf_la_of_ra F 𝔊 η : ℭ ↦↦⇩C⇘α⇙ 𝔇" (is ‹?𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇›)
proof-
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(1))
show "cf_la_of_ra F 𝔊 η : ℭ ↦↦⇩C⇘α⇙ 𝔇"
proof(rule is_functorI')
show "vfsequence ?𝔉" unfolding cf_la_of_ra_def by auto
show "vcard ?𝔉 = 4⇩ℕ"
unfolding cf_la_of_ra_def by (simp add: nat_omega_simps)
show "ℛ⇩∘ (?𝔉⦇ObjMap⦈) ⊆⇩∘ 𝔇⦇Obj⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold 𝔊.cf_la_of_ra_ObjMap_vdomain)
fix x assume "x ∈⇩∘ ℭ⦇Obj⦈"
with assms(1) show "?𝔉⦇ObjMap⦈⦇x⦈ ∈⇩∘ 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: adj_cs_simps cs_intro: assms(2))
qed (auto intro: adj_cs_intros)
show "?𝔉⦇ArrMap⦈⦇f⦈ : ?𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ ?𝔉⦇ObjMap⦈⦇b⦈"
if "f : a ↦⇘ℭ⇙ b" for a b f
proof-
from that have a: "a ∈⇩∘ ℭ⦇Obj⦈" and b: "b ∈⇩∘ ℭ⦇Obj⦈"
by (simp_all add: cat_cs_intros)
have ua_η_a: "universal_arrow_of 𝔊 a (?𝔉⦇ObjMap⦈⦇a⦈) (η⦇a⦈)"
and ua_η_b: "universal_arrow_of 𝔊 b (?𝔉⦇ObjMap⦈⦇b⦈) (η⦇b⦈)"
by (intro assms(3)[OF a] assms(3)[OF b])+
from a b cf_la_of_ra_ArrMap_app_unique(1)[OF assms(1) that ua_η_a ua_η_b]
show ?thesis
by (cs_concl cs_shallow cs_simp: adj_cs_simps)
qed
show "?𝔉⦇ArrMap⦈⦇g ∘⇩A⇘ℭ⇙ f⦈ = ?𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔇⇙ ?𝔉⦇ArrMap⦈⦇f⦈"
if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for b c g a f
proof-
from that have a: "a ∈⇩∘ ℭ⦇Obj⦈" and b: "b ∈⇩∘ ℭ⦇Obj⦈" and c: "c ∈⇩∘ ℭ⦇Obj⦈"
by (simp_all add: cat_cs_intros)
from assms(1) that have gf: "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
note ua_η_a = assms(3)[OF a]
and ua_η_b = assms(3)[OF b]
and ua_η_c = assms(3)[OF c]
note lara_f =
cf_la_of_ra_ArrMap_app_unique[OF assms(1) that(2) ua_η_a ua_η_b]
note lara_g =
cf_la_of_ra_ArrMap_app_unique[OF assms(1) that(1) ua_η_b ua_η_c]
note lara_gf =
cf_la_of_ra_ArrMap_app_unique[OF assms(1) gf ua_η_a ua_η_c]
note ua_η_a = 𝔊.universal_arrow_ofD[OF ua_η_a]
and ua_η_b = 𝔊.universal_arrow_ofD[OF ua_η_b]
and ua_η_c = 𝔊.universal_arrow_ofD[OF ua_η_c]
from ua_η_a(2) assms(1) that have ηa:
"η⦇a⦈ : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F a⦈"
by (cs_prems cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
from ua_η_b(2) assms(1) that have ηb:
"η⦇b⦈ : b ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F b⦈"
by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
from ua_η_c(2) assms(1) that have ηc:
"η⦇c⦈ : c ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F c⦈"
by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
from assms(1) that ηc have
"η⦇c⦈ ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f) = (η⦇c⦈ ∘⇩A⇘ℭ⇙ g) ∘⇩A⇘ℭ⇙ f"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
also from assms(1) lara_g(1) that(2) ηb have
"… = 𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇g⦈⦈ ∘⇩A⇘ℭ⇙ (η⦇b⦈ ∘⇩A⇘ℭ⇙ f)"
by
(
cs_concl
cs_simp: lara_g(2) cat_cs_simps
cs_intro: cat_cs_intros cat_prod_cs_intros
)
also from assms(1) lara_f(1) ηa have "… =
𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇g⦈⦈ ∘⇩A⇘ℭ⇙
(𝔊⦇ArrMap⦈⦇?𝔉⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ η⦇a⦈)"
by (cs_concl cs_shallow cs_simp: lara_f(2) cat_cs_simps)
finally have [symmetric, cat_cs_simps]:
"η⦇c⦈ ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f) = …".
from assms(1) this ηa ηb ηc lara_g(1) lara_f(1) have
"η⦇c⦈ ∘⇩A⇘ℭ⇙ (g ∘⇩A⇘ℭ⇙ f) =
umap_of 𝔊 a (F a) (η⦇a⦈) (F c)⦇ArrVal⦈⦇?𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔇⇙
?𝔉⦇ArrMap⦈⦇f⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
moreover from assms(1) lara_g(1) lara_f(1) have
"?𝔉⦇ArrMap⦈⦇g⦈ ∘⇩A⇘𝔇⇙ ?𝔉⦇ArrMap⦈⦇f⦈ : F a ↦⇘𝔇⇙ F c"
by (cs_concl cs_shallow cs_intro: adj_cs_intros cat_cs_intros)
ultimately show ?thesis by (intro lara_gf(3))
qed
show "?𝔉⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 𝔇⦇CId⦈⦇?𝔉⦇ObjMap⦈⦇c⦈⦈" if "c ∈⇩∘ ℭ⦇Obj⦈" for c
proof-
note lara_c = cf_la_of_ra_ArrMap_app_unique[
OF
assms(1)
𝔊.HomCod.cat_CId_is_arr[OF that]
assms(3)[OF that]
assms(3)[OF that]
]
from assms(1) that have 𝔇c: "𝔇⦇CId⦈⦇F c⦈ : F c ↦⇘𝔇⇙ F c "
by (cs_concl cs_simp: cat_cs_simps cs_intro: assms(2) cat_cs_intros)
from 𝔊.universal_arrow_ofD(2)[OF assms(3)[OF that]] assms(1) that have ηc:
"η⦇c⦈ : c ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇F c⦈"
by (cs_prems cs_shallow cs_simp: adj_cs_simps cs_intro: cat_cs_intros)
from assms(1) that ηc have
"η⦇c⦈ ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇c⦈ =
umap_of 𝔊 c (F c) (η⦇c⦈) (F c)⦇ArrVal⦈⦇𝔇⦇CId⦈⦇F c⦈⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: assms(2) cat_cs_intros)
note [cat_cs_simps] = lara_c(3)[OF 𝔇c this]
from assms(1) that 𝔇c show ?thesis
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps cs_intro: cat_cs_intros
)
qed
qed (auto simp: cf_la_of_ra_components cat_cs_intros cat_cs_simps)
qed
lemma cf_la_of_ra_is_ntcf:
fixes F ℭ 𝔉 𝔊 η⇩m η
defines "𝔉 ≡ cf_la_of_ra F 𝔊 η⇩m"
and "η ≡ [η⇩m, cf_id ℭ, 𝔊 ∘⇩C⇩F 𝔉, ℭ, ℭ]⇩∘"
assumes "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹ F c ∈⇩∘ 𝔇⦇Obj⦈"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹ universal_arrow_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈)"
and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇h⦈⦈ ∘⇩A⇘ℭ⇙ (η⦇NTMap⦈⦇c⦈) = (η⦇NTMap⦈⦇c'⦈) ∘⇩A⇘ℭ⇙ h"
and "vsv (η⦇NTMap⦈)"
and "𝒟⇩∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈"
shows "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
proof-
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(3))
have η_components:
"η⦇NTMap⦈ = η⇩m"
"η⦇NTDom⦈ = cf_id ℭ"
"η⦇NTCod⦈ = 𝔊 ∘⇩C⇩F 𝔉"
"η⦇NTDGDom⦈ = ℭ"
"η⦇NTDGCod⦈ = ℭ"
unfolding η_def nt_field_simps by (simp_all add: nat_omega_simps)
note 𝔉_def = 𝔉_def[folded η_components(1)]
have 𝔉: "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
unfolding 𝔉_def
by (auto intro: cf_la_of_ra_is_functor[OF assms(3-6)[unfolded 𝔉_def]])
show "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
proof(rule is_ntcfI')
show "vfsequence η" unfolding η_def by simp
show "vcard η = 5⇩ℕ" unfolding η_def by (simp_all add: nat_omega_simps)
from assms(2) show "cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(2) 𝔉 show "𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "η⦇NTMap⦈⦇a⦈ : cf_id ℭ⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ (𝔊 ∘⇩C⇩F 𝔉)⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ ℭ⦇Obj⦈" for a
using assms(2) 𝔉 that 𝔊.universal_arrow_ofD(2)[OF assms(5)[OF that]]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show
"η⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ cf_id ℭ⦇ArrMap⦈⦇f⦈ =
(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ η⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘ℭ⇙ b" for a b f
using assms(3) 𝔉 that
by
(
cs_concl cs_shallow
cs_simp: assms(6) cat_cs_simps cs_intro: cat_cs_intros
)
qed (auto simp: η_components(2-5) assms(7-8))
qed
lemma cf_la_of_ra_is_unit:
fixes F ℭ 𝔉 𝔊 η⇩m η
defines "𝔉 ≡ cf_la_of_ra F 𝔊 η⇩m"
and "η ≡ [η⇩m, cf_id ℭ, 𝔊 ∘⇩C⇩F 𝔉, ℭ, ℭ]⇩∘"
assumes "category α ℭ"
and "category α 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹ F c ∈⇩∘ 𝔇⦇Obj⦈"
and "⋀c. c ∈⇩∘ ℭ⦇Obj⦈ ⟹
universal_arrow_of 𝔊 c (𝔉⦇ObjMap⦈⦇c⦈) (η⦇NTMap⦈⦇c⦈)"
and "⋀c c' h. h : c ↦⇘ℭ⇙ c' ⟹
𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇h⦈⦈ ∘⇩A⇘ℭ⇙ (η⦇NTMap⦈⦇c⦈) = (η⦇NTMap⦈⦇c'⦈) ∘⇩A⇘ℭ⇙ h"
and "vsv (η⦇NTMap⦈)"
and "𝒟⇩∘ (η⦇NTMap⦈) = ℭ⦇Obj⦈"
shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
proof-
have η_components:
"η⦇NTMap⦈ = η⇩m"
"η⦇NTDom⦈ = cf_id ℭ"
"η⦇NTCod⦈ = 𝔊 ∘⇩C⇩F 𝔉"
"η⦇NTDGDom⦈ = ℭ"
"η⦇NTDGCod⦈ = ℭ"
unfolding η_def nt_field_simps by (simp_all add: nat_omega_simps)
note 𝔉_def = 𝔉_def[folded η_components(1)]
note 𝔉 = cf_la_of_ra_is_functor
[
where F=F and ℭ=ℭ and 𝔊=𝔊 and η=η⇩m,
folded 𝔉_def[unfolded η_components(1)],
folded η_components(1),
OF assms(5-8),
simplified
]
note η = cf_la_of_ra_is_ntcf
[
where F=F and ℭ=ℭ and 𝔊=𝔊 and η⇩m=η⇩m,
folded 𝔉_def[unfolded η_components(1)],
folded η_def,
OF assms(5-10),
simplified
]
show "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
by
(
intro cf_adjunction_of_unit_is_cf_adjunction[
OF assms(3,4) 𝔉 assms(5) η assms(7), simplified, folded 𝔉_def
]
)+
qed
subsection‹
Construction of an adjunction from universal morphisms
from functors to objects
›
subsubsection‹Definition and elementary properties›
text‹
The subsection presents the construction of an adjunction given
a structured collection of universal morphisms from functors to objects.
The content of this subsection follows the statement and the proof
of Theorem 2-iii in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
definition cf_adjunction_of_counit :: "V ⇒ V ⇒ V ⇒ V ⇒ V"
where "cf_adjunction_of_counit α 𝔉 𝔊 ε =
op_cf_adj (cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε))"
text‹Components.›
lemma cf_adjunction_of_counit_components:
shows "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjLeft⦈ = op_cf (op_cf 𝔉)"
and "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjRight⦈ = op_cf (op_cf 𝔊)"
and "cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈ = op_cf_adj_nt
(op_cf 𝔊⦇HomDom⦈)
(op_cf 𝔊⦇HomCod⦈)
(cf_adjunction_AdjNT_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε))"
unfolding
cf_adjunction_of_counit_def
op_cf_adj_components
cf_adjunction_of_unit_components
by (simp_all add: cat_op_simps)
subsubsection‹Natural transformation map›
lemma cf_adjunction_of_counit_NTMap_vsv:
"vsv (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈)"
unfolding cf_adjunction_of_counit_components by (rule inv_ntcf_NTMap_vsv)
subsubsection‹
An adjunction constructed from universal morphisms
from functors to objects is an adjunction
›
lemma cf_adjunction_of_counit_is_cf_adjunction:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "ε : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
and "⋀x. x ∈⇩∘ 𝔇⦇Obj⦈ ⟹ universal_arrow_fo 𝔉 x (𝔊⦇ObjMap⦈⦇x⦈) (ε⦇NTMap⦈⦇x⦈)"
shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
and "𝒟⇩∘ (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈) =
(op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
and "⋀c d. ⟦ c ∈⇩∘ ℭ⦇Obj⦈; d ∈⇩∘ 𝔇⦇Obj⦈ ⟧ ⟹
cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈⇩∙ =
(umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯⇩S⇩e⇩t"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ε by (rule assms(5))
note cf_adjunction_of_counit_def' =
cf_adjunction_of_counit_def[where 𝔉=𝔉, unfolded 𝔉.cf_HomDom 𝔉.cf_HomCod]
have ua:
"universal_arrow_of (op_cf 𝔉) x (op_cf 𝔊⦇ObjMap⦈⦇x⦈) (op_ntcf ε⦇NTMap⦈⦇x⦈)"
if "x ∈⇩∘ op_cat 𝔇⦇Obj⦈" for x
using that unfolding cat_op_simps by (rule assms(6))
let ?aou = ‹cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε)›
from
cf_adjunction_of_unit_is_cf_adjunction
[
OF
𝔇.category_op
ℭ.category_op
𝔊.is_functor_op
𝔉.is_functor_op
ε.is_ntcf_op[unfolded cat_op_simps]
ua,
simplified cf_adjunction_of_counit_def[symmetric]
]
have aou: "?aou : op_cf 𝔊 ⇌⇩C⇩F op_cf 𝔉 : op_cat 𝔇 ⇌⇌⇩C⇘α⇙ op_cat ℭ"
and η_aou: "η⇩C ?aou = op_ntcf ε"
by auto
interpret aou:
is_cf_adjunction α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔉› ?aou
by (rule aou)
from η_aou have
"op_ntcf (η⇩C ?aou) = op_ntcf (op_ntcf ε)"
by simp
then show "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
unfolding
ε.ntcf_op_ntcf_op_ntcf
is_cf_adjunction.op_ntcf_cf_adjunction_unit[OF aou]
cf_adjunction_of_counit_def'[symmetric]
by (simp add: cat_op_simps)
show aoc_ε: "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
by
(
rule
is_cf_adjunction_op[
OF aou, folded cf_adjunction_of_counit_def', unfolded cat_op_simps
]
)
interpret aoc_ε: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_counit α 𝔉 𝔊 ε›
by (rule aoc_ε)
from aoc_ε.NT.is_ntcf_axioms show
"𝒟⇩∘ (cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈) = (op_cat ℭ ×⇩C 𝔇)⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "⋀c d. ⟦ c ∈⇩∘ ℭ⦇Obj⦈; d ∈⇩∘ 𝔇⦇Obj⦈ ⟧ ⟹
cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈⇩∙ =
(umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯⇩S⇩e⇩t"
proof-
fix c d assume prems: "c ∈⇩∘ ℭ⦇Obj⦈" "d ∈⇩∘ 𝔇⦇Obj⦈"
from assms(1-4) prems have aou_dc:
"cf_adjunction_AdjNT_of_unit
α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε)⦇NTMap⦈⦇d, c⦈⇩∙ =
umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c"
by
(
cs_concl cs_shallow
cs_simp: cat_op_simps adj_cs_simps cs_intro: cat_op_intros
)
from assms(1-4) aou prems have ufo_ε_dc:
"umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c :
Hom⇩O⇩.⇩C⇘α⇙op_cat ℭ(op_cf 𝔊-,-)⦇ObjMap⦈⦇d, c⦈⇩∙ ↦⇩i⇩s⇩o⇘cat_Set α⇙
Hom⇩O⇩.⇩C⇘α⇙op_cat 𝔇(-,op_cf 𝔉-)⦇ObjMap⦈⦇d, c⦈⇩∙"
by
(
cs_concl cs_shallow
cs_simp:
aou_dc[symmetric] cf_adjunction_of_unit_components(3)[symmetric]
cs_intro:
is_iso_ntcf.iso_ntcf_is_iso_arr'
adj_cs_intros
cat_cs_intros
cat_op_intros
cat_prod_cs_intros
)
from
assms(1-4)
aoc_ε[unfolded cf_adjunction_of_counit_def']
aou
prems
ufo_ε_dc
show
"cf_adjunction_of_counit α 𝔉 𝔊 ε⦇AdjNT⦈⦇NTMap⦈⦇c, d⦈⇩∙ =
(umap_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈) c)¯⇩S⇩e⇩t"
unfolding cf_adjunction_of_counit_def'
by
(
cs_concl
cs_simp: cat_op_simps adj_cs_simps cat_cs_simps cat_Set_cs_simps
cs_intro: adj_cs_intros cat_cs_intros cat_prod_cs_intros
)
qed
qed
subsection‹
Construction of an adjunction from a functor and universal morphisms
from functors to objects
›
text‹
The subsection presents the construction of an adjunction given
a functor and a structured collection of universal morphisms
from functors to objects.
The content of this subsection follows the statement and the proof
of Theorem 2-iv in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
subsubsection‹Definition and elementary properties›
definition cf_ra_of_la :: "(V ⇒ V) ⇒ V ⇒ V ⇒ V"
where "cf_ra_of_la F 𝔉 ε = op_cf (cf_la_of_ra F (op_cf 𝔉) ε)"
subsubsection‹Object map›
lemma cf_ra_of_la_ObjMap_vsv[adj_cs_intros]: "vsv (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈)"
unfolding cf_ra_of_la_def op_cf_components by (auto intro: adj_cs_intros)
lemma (in is_functor) cf_ra_of_la_ObjMap_vdomain:
"𝒟⇩∘ (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈) = 𝔅⦇Obj⦈"
unfolding cf_ra_of_la_def cf_la_of_ra_components cat_op_simps
by (simp add: cat_cs_simps)
lemmas [adj_cs_simps] = is_functor.cf_ra_of_la_ObjMap_vdomain
lemma (in is_functor) cf_ra_of_la_ObjMap_app:
assumes "d ∈⇩∘ 𝔅⦇Obj⦈"
shows "cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈ = F d"
using assms
unfolding cf_ra_of_la_def cf_la_of_ra_components cat_op_simps
by (simp add: cat_cs_simps)
lemmas [adj_cs_simps] = is_functor.cf_ra_of_la_ObjMap_app
subsubsection‹Arrow map›
lemma cf_ra_of_la_ArrMap_app_unique:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "f : a ↦⇘𝔇⇙ b"
and "universal_arrow_fo 𝔉 a (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇a⦈) (ε⦇a⦈)"
and "universal_arrow_fo 𝔉 b (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇b⦈) (ε⦇b⦈)"
shows "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : F a ↦⇘ℭ⇙ F b"
and "f ∘⇩A⇘𝔇⇙ ε⦇a⦈ =
umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈⦈"
and "⋀f'.
⟦
f' : F a ↦⇘ℭ⇙ F b;
f ∘⇩A⇘𝔇⇙ ε⦇a⦈ = umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇f'⦈
⟧ ⟹ cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ = f'"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
from assms(2) have op_f: "f : b ↦⇘op_cat 𝔇⇙ a" unfolding cat_op_simps by simp
let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) ε›
have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
unfolding cat_op_simps by simp_all
note ua_η_a = 𝔉.universal_arrow_foD[OF assms(3)]
and ua_η_b = 𝔉.universal_arrow_foD[OF assms(4)]
from assms(1,2) ua_η_a(2) have [cat_op_simps]:
"ε⦇a⦈ ∘⇩A⇘op_cat 𝔇⇙ f = f ∘⇩A⇘𝔇⇙ ε⦇a⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_op_simps)
show "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : F a ↦⇘ℭ⇙ F b"
and "f ∘⇩A⇘𝔇⇙ ε⦇a⦈ =
umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈⦈"
and "⋀f'.
⟦
f' : F a ↦⇘ℭ⇙ F b;
f ∘⇩A⇘𝔇⇙ ε⦇a⦈ = umap_fo 𝔉 b (F b) (ε⦇b⦈) (F a)⦇ArrVal⦈⦇f'⦈
⟧ ⟹ cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ = f'"
by
(
intro
cf_la_of_ra_ArrMap_app_unique
[
where η=ε and F=F,
OF 𝔉.is_functor_op op_f,
unfolded
𝔉.op_cf_universal_arrow_of
lara_ObjMap_eq_op
lara_ArrMap_eq_op,
folded cf_ra_of_la_def,
unfolded cat_op_simps, OF assms(4,3)
]
)+
qed
lemma cf_ra_of_la_ArrMap_app_is_arr[adj_cs_intros]:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "f : a ↦⇘𝔇⇙ b"
and "universal_arrow_fo 𝔉 a (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇a⦈) (ε⦇a⦈)"
and "universal_arrow_fo 𝔉 b (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇b⦈) (ε⦇b⦈)"
and "Fa = F a"
and "Fb = F b"
shows "cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇f⦈ : Fa ↦⇘ℭ⇙ Fb"
using assms(1-4) unfolding assms(5,6) by (rule cf_ra_of_la_ArrMap_app_unique)
subsubsection‹
An adjunction constructed from a functor and universal morphisms
from functors to objects is an adjunction
›
lemma op_cf_cf_la_of_ra_op[cat_op_simps]:
"op_cf (cf_la_of_ra F (op_cf 𝔉) ε) = cf_ra_of_la F 𝔉 ε"
unfolding cf_ra_of_la_def by simp
lemma cf_ra_of_la_commute_op:
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹
universal_arrow_fo 𝔉 d (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈) (ε⦇d⦈)"
and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
ε⦇d'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ =
h ∘⇩A⇘𝔇⇙ ε⦇d⦈"
and "h : c' ↦⇘𝔇⇙ c"
shows "𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ ∘⇩A⇘op_cat 𝔇⇙ ε⦇c⦈ =
ε⦇c'⦈ ∘⇩A⇘op_cat 𝔇⇙ h"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
from assms(4) have c': "c' ∈⇩∘ 𝔇⦇Obj⦈" and c: "c ∈⇩∘ 𝔇⦇Obj⦈" by auto
note ua_η_c' = 𝔉.universal_arrow_foD[OF assms(2)[OF c']]
and ua_η_c = 𝔉.universal_arrow_foD[OF assms(2)[OF c]]
note rala_f = cf_ra_of_la_ArrMap_app_unique[
OF assms(1) assms(4) assms(2)[OF c'] assms(2)[OF c]
]
from assms(1) assms(4) ua_η_c'(2) ua_η_c(2) rala_f(1) show ?thesis
by
(
cs_concl cs_shallow
cs_simp: assms(3) cat_op_simps adj_cs_simps cat_cs_simps
cs_intro: cat_cs_intros
)
qed
lemma
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹ F d ∈⇩∘ ℭ⦇Obj⦈"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹
universal_arrow_fo 𝔉 d (cf_ra_of_la F 𝔉 ε⦇ObjMap⦈⦇d⦈) (ε⦇d⦈)"
and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
ε⦇d'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ =
h ∘⇩A⇘𝔇⇙ ε⦇d⦈"
shows cf_ra_of_la_is_functor: "cf_ra_of_la F 𝔉 ε : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and cf_la_of_ra_op_is_functor:
"cf_la_of_ra F (op_cf 𝔉) ε : op_cat 𝔇 ↦↦⇩C⇘α⇙ op_cat ℭ"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(1))
have 𝔉h_εc:
"𝔉⦇ArrMap⦈⦇cf_ra_of_la F 𝔉 ε⦇ArrMap⦈⦇h⦈⦈ ∘⇩A⇘op_cat 𝔇⇙ ε⦇c⦈ =
ε⦇c'⦈ ∘⇩A⇘op_cat 𝔇⇙ h"
if "h : c' ↦⇘𝔇⇙ c" for c c' h
proof-
from that have c': "c' ∈⇩∘ 𝔇⦇Obj⦈" and c: "c ∈⇩∘ 𝔇⦇Obj⦈" by auto
note ua_η_c' = 𝔉.universal_arrow_foD[OF assms(3)[OF c']]
and ua_η_c = 𝔉.universal_arrow_foD[OF assms(3)[OF c]]
note rala_f = cf_ra_of_la_ArrMap_app_unique[
OF assms(1) that assms(3)[OF c'] assms(3)[OF c]
]
from assms(1) that ua_η_c'(2) ua_η_c(2) rala_f(1) show ?thesis
by
(
cs_concl cs_shallow
cs_simp: assms(4) cat_op_simps adj_cs_simps cat_cs_simps
cs_intro: cat_cs_intros
)
qed
let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) ε›
have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
by (simp_all add: cat_op_simps del: op_cf_cf_la_of_ra_op)
show "cf_la_of_ra F (op_cf 𝔉) ε : op_cat 𝔇 ↦↦⇩C⇘α⇙ op_cat ℭ"
by
(
intro cf_la_of_ra_is_functor
[
where F=F and η=ε,
OF 𝔉.is_functor_op,
unfolded cat_op_simps,
OF assms(2),
simplified,
unfolded lara_ObjMap_eq_op lara_ArrMap_eq_op,
folded cf_ra_of_la_def,
OF assms(3) 𝔉h_εc,
simplified
]
)
from
is_functor.is_functor_op[
OF this, unfolded cat_op_simps, folded cf_ra_of_la_def
]
show "cf_ra_of_la F 𝔉 ε : 𝔇 ↦↦⇩C⇘α⇙ ℭ".
qed
lemma cf_ra_of_la_is_ntcf:
fixes F 𝔇 𝔉 𝔊 ε⇩m ε
defines "𝔊 ≡ cf_ra_of_la F 𝔉 ε⇩m"
and "ε ≡ [ε⇩m, 𝔉 ∘⇩C⇩F 𝔊, cf_id 𝔇, 𝔇, 𝔇]⇩∘"
assumes "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹ F d ∈⇩∘ ℭ⦇Obj⦈"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹
universal_arrow_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈)"
and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
ε⦇NTMap⦈⦇d'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇h⦈⦈ = h ∘⇩A⇘𝔇⇙ ε⦇NTMap⦈⦇d⦈"
and "vsv (ε⦇NTMap⦈)"
and "𝒟⇩∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
shows "ε : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
proof-
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
have ε_components:
"ε⦇NTMap⦈ = ε⇩m"
"ε⦇NTDom⦈ = 𝔉 ∘⇩C⇩F 𝔊"
"ε⦇NTCod⦈ = cf_id 𝔇"
"ε⦇NTDGDom⦈ = 𝔇"
"ε⦇NTDGCod⦈ = 𝔇"
unfolding ε_def nt_field_simps by (simp_all add: nat_omega_simps)
note 𝔊_def = 𝔊_def[folded ε_components(1)]
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊
unfolding 𝔊_def
by (auto intro: cf_ra_of_la_is_functor[OF assms(3-6)[unfolded 𝔊_def]])
interpret op_ε: is_functor
α ‹op_cat 𝔇› ‹op_cat ℭ› ‹cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)›
by
(
intro cf_la_of_ra_op_is_functor[
where F=F and ε=‹ε⦇NTMap⦈›, OF assms(3-6)[unfolded 𝔊_def], simplified
]
)
interpret ε: vfsequence ε unfolding ε_def by simp
have [cat_op_simps]: "op_ntcf (op_ntcf ε) = ε"
proof(rule vsv_eqI)
have dom_lhs: "𝒟⇩∘ (op_ntcf (op_ntcf ε)) = 5⇩ℕ"
unfolding op_ntcf_def by (simp add: nat_omega_simps)
from assms(7) show "𝒟⇩∘ (op_ntcf (op_ntcf ε)) = 𝒟⇩∘ ε"
unfolding dom_lhs by (simp add: ε_def ε.vfsequence_vdomain nat_omega_simps)
have sup:
"op_ntcf (op_ntcf ε)⦇NTDom⦈ = ε⦇NTDom⦈"
"op_ntcf (op_ntcf ε)⦇NTCod⦈ = ε⦇NTCod⦈"
"op_ntcf (op_ntcf ε)⦇NTDGDom⦈ = ε⦇NTDGDom⦈"
"op_ntcf (op_ntcf ε)⦇NTDGCod⦈ = ε⦇NTDGCod⦈"
unfolding op_ntcf_components cat_op_simps ε_components
by simp_all
show "a ∈⇩∘ 𝒟⇩∘ (op_ntcf (op_ntcf ε)) ⟹ op_ntcf (op_ntcf ε)⦇a⦈ = ε⦇a⦈" for a
by (unfold dom_lhs, elim_in_numeral, fold nt_field_simps, unfold sup)
(simp_all add: cat_op_simps)
qed (auto simp: op_ntcf_def)
let ?lara = ‹cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)›
have lara_ObjMap_eq_op: "?lara⦇ObjMap⦈ = (op_cf ?lara⦇ObjMap⦈)"
and lara_ArrMap_eq_op: "?lara⦇ArrMap⦈ = (op_cf ?lara⦇ArrMap⦈)"
by (simp_all add: cat_op_simps del: op_cf_cf_la_of_ra_op)
have seq: "vfsequence (op_ntcf ε)" unfolding op_ntcf_def by auto
have card: "vcard (op_ntcf ε) = 5⇩ℕ"
unfolding op_ntcf_def by (simp add: nat_omega_simps)
have op_cf_NTCod: "op_cf (ε⦇NTCod⦈) = cf_id (op_cat 𝔇)"
unfolding ε_components cat_op_simps by simp
from assms(3) have op_cf_NTDom:
"op_cf (ε⦇NTDom⦈) = op_cf 𝔉 ∘⇩C⇩F cf_la_of_ra F (op_cf 𝔉) (ε⦇NTMap⦈)"
unfolding ε_components
by
(
simp
add: cat_op_simps 𝔊_def cf_ra_of_la_def ε_components(1)[symmetric]
del: op_cf_cf_la_of_ra_op
)
note cf_la_of_ra_is_ntcf
[
where F=F and η⇩m=‹ε⦇NTMap⦈›,
OF is_functor.is_functor_op[OF assms(3)],
unfolded cat_op_simps,
OF assms(4),
unfolded ε_components(1),
folded op_cf_NTCod op_cf_NTDom[unfolded ε_components(1)] ε_components(1),
folded op_ntcf_def[of ε, unfolded ε_components(4,5)],
unfolded
cat_op_simps
lara_ObjMap_eq_op lara_ArrMap_eq_op cf_ra_of_la_def[symmetric],
folded 𝔊_def,
simplified,
OF
assms(5)
cf_ra_of_la_commute_op[
OF assms(3,5,6)[unfolded 𝔊_def], folded 𝔊_def
]
assms(7,8),
unfolded ε_components,
simplified
]
from is_ntcf.is_ntcf_op[OF this, unfolded cat_op_simps 𝔊_def[symmetric]] show
"ε : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇".
qed
lemma cf_ra_of_la_is_counit:
fixes F 𝔇 𝔉 𝔊 ε⇩m ε
defines "𝔊 ≡ cf_ra_of_la F 𝔉 ε⇩m"
and "ε ≡ [ε⇩m, 𝔉 ∘⇩C⇩F 𝔊, cf_id 𝔇, 𝔇, 𝔇]⇩∘"
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹ F d ∈⇩∘ ℭ⦇Obj⦈"
and "⋀d. d ∈⇩∘ 𝔇⦇Obj⦈ ⟹
universal_arrow_fo 𝔉 d (𝔊⦇ObjMap⦈⦇d⦈) (ε⦇NTMap⦈⦇d⦈)"
and "⋀d d' h. h : d ↦⇘𝔇⇙ d' ⟹
ε⦇NTMap⦈⦇d'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇h⦈⦈ = h ∘⇩A⇘𝔇⇙ ε⦇NTMap⦈⦇d⦈"
and "vfsequence ε"
and "vsv (ε⦇NTMap⦈)"
and "𝒟⇩∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
proof-
have ε_components:
"ε⦇NTMap⦈ = ε⇩m"
"ε⦇NTDom⦈ = 𝔉 ∘⇩C⇩F 𝔊"
"ε⦇NTCod⦈ = cf_id 𝔇"
"ε⦇NTDGDom⦈ = 𝔇"
"ε⦇NTDGCod⦈ = 𝔇"
unfolding ε_def nt_field_simps by (simp_all add: nat_omega_simps)
note 𝔊_def = 𝔊_def[folded ε_components(1)]
note 𝔉 = cf_ra_of_la_is_functor[
where F=F and ε=‹ε⦇NTMap⦈›, OF assms(5-8)[unfolded 𝔊_def], simplified
]
note ε = cf_ra_of_la_is_ntcf
[
where F=F and ε⇩m=‹ε⇩m› and 𝔇=𝔇 and 𝔉=𝔉,
folded 𝔊_def[unfolded ε_components(1)],
folded ε_def,
OF assms(5-8) assms(10,11),
simplified
]
show "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
by
(
intro cf_adjunction_of_counit_is_cf_adjunction
[
OF assms(3-5) 𝔉,
folded 𝔊_def,
OF ε assms(7)[folded 𝔊_def],
simplified
]
)+
qed
subsection‹Construction of an adjunction from the counit-unit equations›
text‹
The subsection presents the construction of an adjunction given
two natural transformations satisfying counit-unit equations.
The content of this subsection follows the statement and the proof
of Theorem 2-v in Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
lemma counit_unit_is_cf_adjunction:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
and "ε : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
and "(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ε) ∙⇩N⇩T⇩C⇩F (η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) = ntcf_id 𝔊"
and "(ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F η) = ntcf_id 𝔉"
shows "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
and "ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = ε"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› η by (rule assms(5))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ε by (rule assms(6))
have 𝔊εx_η𝔊x[cat_cs_simps]:
"𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘⇩A⇘ℭ⇙ η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ = ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
if "x ∈⇩∘ 𝔇⦇Obj⦈" for x
proof-
from assms(7) have
"((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ε) ∙⇩N⇩T⇩C⇩F (η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊))⦇NTMap⦈⦇x⦈ = ntcf_id 𝔊⦇NTMap⦈⦇x⦈"
by simp
from this assms(1-6) that show
"𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘⇩A⇘ℭ⇙ η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ =
ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
have [cat_cs_simps]:
"𝔊⦇ArrMap⦈⦇ε⦇NTMap⦈⦇x⦈⦈ ∘⇩A⇘ℭ⇙ (η⦇NTMap⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ∘⇩A⇘ℭ⇙ f) =
ℭ⦇CId⦈⦇𝔊⦇ObjMap⦈⦇x⦈⦈ ∘⇩A⇘ℭ⇙ f"
if "x ∈⇩∘ 𝔇⦇Obj⦈" and "f : a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇x⦈" for x f a
using assms(1-6) that
by (intro ℭ.cat_assoc_helper)
(cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+
have [cat_cs_simps]:
"ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇η⦇NTMap⦈⦇x⦈⦈ = 𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
if "x ∈⇩∘ ℭ⦇Obj⦈" for x
proof-
from assms(8) have
"((ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F η))⦇NTMap⦈⦇x⦈ = ntcf_id 𝔉⦇NTMap⦈⦇x⦈"
by simp
from this assms(1-6) that show
"ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇η⦇NTMap⦈⦇x⦈⦈ = 𝔇⦇CId⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
have ua_𝔉x_ηx: "universal_arrow_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈)"
if "x ∈⇩∘ ℭ⦇Obj⦈" for x
proof(intro is_functor.universal_arrow_ofI)
from assms(3) that show "𝔉⦇ObjMap⦈⦇x⦈ ∈⇩∘ 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from assms(3-6) that show "η⦇NTMap⦈⦇x⦈ : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
fix r' u' assume prems': "r' ∈⇩∘ 𝔇⦇Obj⦈" "u' : x ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇r'⦈"
show "∃!f'.
f' : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r' ∧
u' = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇f'⦈"
proof(intro ex1I conjI; (elim conjE)?)
from assms(3-6) that prems' show
"ε⦇NTMap⦈⦇r'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇u'⦈ : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r'"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from assms(3-6) prems' have 𝔊𝔉u':
"(𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇u'⦈ = 𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇u'⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
note [cat_cs_simps] =
η.ntcf_Comp_commute[symmetric, OF prems'(2), unfolded 𝔊𝔉u']
from assms(3-6) that prems' show
"u' =
umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇ε⦇NTMap⦈⦇r'⦈ ∘⇩A⇘𝔇⇙
𝔉⦇ArrMap⦈⦇u'⦈⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)
fix f' assume prems'':
"f' : 𝔉⦇ObjMap⦈⦇x⦈ ↦⇘𝔇⇙ r'"
"u' = umap_of 𝔊 x (𝔉⦇ObjMap⦈⦇x⦈) (η⦇NTMap⦈⦇x⦈) r'⦇ArrVal⦈⦇f'⦈"
from prems''(2,1) assms(3-6) that have u'_def:
"u' = 𝔊⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘ℭ⇙ η⦇NTMap⦈⦇x⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)
from
ε.ntcf_Comp_commute[OF prems''(1)]
assms(3-6)
prems''(1)
have [cat_cs_simps]:
"ε⦇NTMap⦈⦇r'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f'⦈⦈ =
f' ∘⇩A⇘𝔇⇙ ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have [cat_cs_simps]:
"ε⦇NTMap⦈⦇r'⦈ ∘⇩A⇘𝔇⇙ (𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇f'⦈⦈ ∘⇩A⇘𝔇⇙ f) =
(f' ∘⇩A⇘𝔇⇙ ε⦇NTMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈) ∘⇩A⇘𝔇⇙ f"
if "f : a ↦⇘𝔇⇙ 𝔉⦇ObjMap⦈⦇𝔊⦇ObjMap⦈⦇𝔉⦇ObjMap⦈⦇x⦈⦈⦈" for f a
using assms(1-6) prems''(1) prems' that
by (intro 𝔇.cat_assoc_helper)
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)+
from prems''(2,1) assms(3-6) that show
"f' = ε⦇NTMap⦈⦇r'⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇u'⦈"
unfolding u'_def
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_prod_cs_intros
)
qed
qed (auto intro: cat_cs_intros)
show aou: "cf_adjunction_of_unit α 𝔉 𝔊 η : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
by (intro cf_adjunction_of_unit_is_cf_adjunction ua_𝔉x_ηx assms(1-5))
from ℭ.category_axioms 𝔇.category_axioms show
"η⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = η"
by
(
cs_concl cs_shallow
cs_intro: cf_adjunction_of_unit_is_cf_adjunction assms(1-5) ua_𝔉x_ηx
)
interpret aou: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_unit α 𝔉 𝔊 η›
by (rule aou)
show "ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) = ε"
proof(rule ntcf_eqI)
show ε_η: "ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η) :
𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
by (rule aou.cf_adjunction_counit_is_ntcf)
from assms(1-6) ε_η have dom_lhs:
"𝒟⇩∘ (ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈) = 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from assms(1-6) ε_η have dom_rhs: "𝒟⇩∘ (ε⦇NTMap⦈) = 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈ = ε⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume "a ∈⇩∘ 𝔇⦇Obj⦈"
with aou.is_cf_adjunction_axioms assms(1-6) show
"ε⇩C (cf_adjunction_of_unit α 𝔉 𝔊 η)⦇NTMap⦈⦇a⦈ = ε⦇NTMap⦈⦇a⦈"
by
(
cs_concl
cs_intro:
cat_arrow_cs_intros
cat_op_intros
cat_cs_intros
cat_prod_cs_intros
cs_simp:
aou.cf_adj_umap_of_unit'[symmetric]
cat_Set_the_inverse[symmetric]
adj_cs_simps cat_cs_simps cat_op_simps
)
qed (auto simp: adj_cs_intros)
qed (auto simp: assms)
qed
lemma counit_unit_cf_adjunction_of_counit_is_cf_adjunction:
assumes "category α ℭ"
and "category α 𝔇"
and "𝔉 : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "η : cf_id ℭ ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔉 : ℭ ↦↦⇩C⇘α⇙ ℭ"
and "ε : 𝔉 ∘⇩C⇩F 𝔊 ↦⇩C⇩F cf_id 𝔇 : 𝔇 ↦↦⇩C⇘α⇙ 𝔇"
and "(𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ε) ∙⇩N⇩T⇩C⇩F (η ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔊) = ntcf_id 𝔊"
and "(ε ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔉) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F η) = ntcf_id 𝔉"
shows "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "η⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = η"
and "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
proof-
interpret ℭ: category α ℭ by (rule assms(1))
interpret 𝔇: category α 𝔇 by (rule assms(2))
interpret 𝔉: is_functor α ℭ 𝔇 𝔉 by (rule assms(3))
interpret 𝔊: is_functor α 𝔇 ℭ 𝔊 by (rule assms(4))
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› η by (rule assms(5))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ε by (rule assms(6))
have unit_op: "cf_adjunction_of_unit α (op_cf 𝔊) (op_cf 𝔉) (op_ntcf ε) :
op_cf 𝔊 ⇌⇩C⇩F op_cf 𝔉 : op_cat 𝔇 ⇌⇌⇩C⇘α⇙ op_cat ℭ"
by (rule counit_unit_is_cf_adjunction(1)[where ε=‹op_ntcf η›])
(
cs_concl
cs_simp:
cat_op_simps cat_cs_simps
𝔊.cf_ntcf_id_op_cf
𝔉.cf_ntcf_id_op_cf
op_ntcf_ntcf_vcomp[symmetric]
op_ntcf_ntcf_cf_comp[symmetric]
op_ntcf_cf_ntcf_comp[symmetric]
assms(7,8)
cs_intro: cat_op_intros cat_cs_intros
)+
then show aou: "cf_adjunction_of_counit α 𝔉 𝔊 ε : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
unfolding cf_adjunction_of_counit_def
by
(
subst 𝔉.cf_op_cf_op_cf[symmetric],
subst 𝔊.cf_op_cf_op_cf[symmetric],
subst ℭ.cat_op_cat_op_cat[symmetric],
subst 𝔇.cat_op_cat_op_cat[symmetric],
rule is_cf_adjunction_op
)
interpret aou: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 ‹cf_adjunction_of_counit α 𝔉 𝔊 ε›
by (rule aou)
show "η⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = η"
unfolding cf_adjunction_of_counit_def
by
(
cs_concl_step is_cf_adjunction.op_ntcf_cf_adjunction_counit[symmetric],
rule unit_op,
cs_concl_step counit_unit_is_cf_adjunction(3)[where ε=‹op_ntcf η›],
insert ℭ.category_op 𝔇.category_op,
rule 𝔇.category_op, rule ℭ.category_op
)
(
cs_concl
cs_simp:
cat_op_simps cat_cs_simps
𝔊.cf_ntcf_id_op_cf
𝔉.cf_ntcf_id_op_cf
op_ntcf_ntcf_vcomp[symmetric]
op_ntcf_ntcf_cf_comp[symmetric]
op_ntcf_cf_ntcf_comp[symmetric]
assms(7,8)
cs_intro: cat_op_intros cat_cs_intros
)+
show "ε⇩C (cf_adjunction_of_counit α 𝔉 𝔊 ε) = ε"
unfolding cf_adjunction_of_counit_def
by
(
cs_concl_step is_cf_adjunction.op_ntcf_cf_adjunction_unit[symmetric],
rule unit_op,
cs_concl_step counit_unit_is_cf_adjunction(2)[where ε=‹op_ntcf η›],
insert ℭ.category_op 𝔇.category_op,
rule 𝔇.category_op, rule ℭ.category_op
)
(
cs_concl
cs_simp:
cat_op_simps cat_cs_simps
𝔊.cf_ntcf_id_op_cf
𝔉.cf_ntcf_id_op_cf
op_ntcf_ntcf_vcomp[symmetric]
op_ntcf_ntcf_cf_comp[symmetric]
op_ntcf_cf_ntcf_comp[symmetric]
assms(7,8)
cs_intro: cat_op_intros cat_cs_intros
)+
qed
subsection‹Adjoints are unique up to isomorphism›
text‹
The content of the following subsection is based predominantly on
the statement and the proof of Corollary 1 in
Chapter IV-1 in \<^cite>‹"mac_lane_categories_2010"›. However, similar
results can also be found in section 4 in \<^cite>‹"riehl_category_2016"›
and in subsection 2.1 in \<^cite>‹"bodo_categories_1970"›.
›
subsubsection‹Definitions and elementary properties›
definition cf_adj_LR_iso :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ =
[
(
λx∈⇩∘ℭ⦇Obj⦈. THE f'.
let
η = η⇩C Φ;
η' = η⇩C Ψ;
𝔉x = 𝔉⦇ObjMap⦈⦇x⦈;
𝔉'x = 𝔉'⦇ObjMap⦈⦇x⦈
in
f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x (𝔉x) (η⦇NTMap⦈⦇x⦈) (𝔉'x)⦇ArrVal⦈⦇f'⦈
),
𝔉,
𝔉',
ℭ,
𝔇
]⇩∘"
definition cf_adj_RL_iso :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V"
where "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ =
[
(
λx∈⇩∘𝔇⦇Obj⦈. THE f'.
let
ε = ε⇩C Φ;
ε' = ε⇩C Ψ;
𝔊x = 𝔊⦇ObjMap⦈⦇x⦈;
𝔊'x = 𝔊'⦇ObjMap⦈⦇x⦈
in
f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
),
𝔊',
𝔊,
𝔇,
ℭ
]⇩∘"
text‹Components.›
lemma cf_adj_LR_iso_components:
shows "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈ =
(
λx∈⇩∘ℭ⦇Obj⦈. THE f'.
let
η = η⇩C Φ;
η' = η⇩C Ψ;
𝔉x = 𝔉⦇ObjMap⦈⦇x⦈;
𝔉'x = 𝔉'⦇ObjMap⦈⦇x⦈
in
f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈
)"
and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDom⦈ = 𝔉"
and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTCod⦈ = 𝔉'"
and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDGDom⦈ = ℭ"
and [adj_cs_simps]: "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTDGCod⦈ = 𝔇"
unfolding cf_adj_LR_iso_def nt_field_simps
by (simp_all add: nat_omega_simps)
lemma cf_adj_RL_iso_components:
shows "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈ =
(
λx∈⇩∘𝔇⦇Obj⦈. THE f'.
let
ε = ε⇩C Φ;
ε' = ε⇩C Ψ;
𝔊x = 𝔊⦇ObjMap⦈⦇x⦈;
𝔊'x = 𝔊'⦇ObjMap⦈⦇x⦈
in
f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
)"
and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDom⦈ = 𝔊'"
and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTCod⦈ = 𝔊"
and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDGDom⦈ = 𝔇"
and [adj_cs_simps]: "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTDGCod⦈ = ℭ"
unfolding cf_adj_RL_iso_def nt_field_simps
by (simp_all add: nat_omega_simps)
subsubsection‹Natural transformation map›
lemma cf_adj_LR_iso_vsv[adj_cs_intros]:
"vsv (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈)"
unfolding cf_adj_LR_iso_components by simp
lemma cf_adj_RL_iso_vsv[adj_cs_intros]:
"vsv (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈)"
unfolding cf_adj_RL_iso_components by simp
lemma cf_adj_LR_iso_vdomain[adj_cs_simps]:
"𝒟⇩∘ (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈) = ℭ⦇Obj⦈"
unfolding cf_adj_LR_iso_components by simp
lemma cf_adj_RL_iso_vdomain[adj_cs_simps]:
"𝒟⇩∘ (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈) = 𝔇⦇Obj⦈"
unfolding cf_adj_RL_iso_components by simp
lemma cf_adj_LR_iso_app:
fixes ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ
assumes "x ∈⇩∘ ℭ⦇Obj⦈"
defines "𝔉x ≡ 𝔉⦇ObjMap⦈⦇x⦈"
and "𝔉'x ≡ 𝔉'⦇ObjMap⦈⦇x⦈"
and "η ≡ η⇩C Φ"
and "η' ≡ η⇩C Ψ"
shows "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈⦇x⦈ =
(
THE f'.
f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈
)"
using assms(1) unfolding cf_adj_LR_iso_components assms(2-5) by simp meson
lemma cf_adj_RL_iso_app:
fixes ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ
assumes "x ∈⇩∘ 𝔇⦇Obj⦈"
defines "𝔊x ≡ 𝔊⦇ObjMap⦈⦇x⦈"
and "𝔊'x ≡ 𝔊'⦇ObjMap⦈⦇x⦈"
and "ε ≡ ε⇩C Φ"
and "ε' ≡ ε⇩C Ψ"
shows "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈⦇x⦈ =
(
THE f'.
f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈
)"
using assms(1) unfolding cf_adj_RL_iso_components assms(2-5) Let_def by simp
lemma cf_adj_LR_iso_app_unique:
fixes ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "Ψ : 𝔉' ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "x ∈⇩∘ ℭ⦇Obj⦈"
defines "𝔉x ≡ 𝔉⦇ObjMap⦈⦇x⦈"
and "𝔉'x ≡ 𝔉'⦇ObjMap⦈⦇x⦈"
and "η ≡ η⇩C Φ"
and "η' ≡ η⇩C Ψ"
and "f ≡ cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ⦇NTMap⦈⦇x⦈"
shows
"∃!f'.
f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
"f : 𝔉x ↦⇩i⇩s⇩o⇘𝔇⇙ 𝔉'x"
"η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))
note 𝔉a_η =
is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
OF assms(1) assms(3), folded assms(4-8)
]
note 𝔉'a_η =
is_cf_adjunction.cf_adjunction_unit_component_is_ua_of[
OF assms(2) assms(3), folded assms(4-8)
]
from
is_functor.cf_universal_arrow_of_unique[
OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η, folded assms(4-8)
]
obtain f'
where f': "f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x"
and η'_def:
"η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
and unique_f':
"⟦
f'' : 𝔉x ↦⇘𝔇⇙ 𝔉'x;
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f''⦈
⟧ ⟹ f'' = f'"
for f''
by metis
show unique_f': "∃!f'.
f' : 𝔉x ↦⇘𝔇⇙ 𝔉'x ∧
η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f'⦈"
by
(
rule is_functor.cf_universal_arrow_of_unique[
OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η, folded assms(4-8)
]
)
from
theD
[
OF unique_f' cf_adj_LR_iso_app[
OF assms(3), of 𝔇 𝔊 𝔉 Φ 𝔉' Ψ, folded assms(4-8)
]
]
have f: "f : 𝔉x ↦⇘𝔇⇙ 𝔉'x"
and η': "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈"
by simp_all
show "η'⦇NTMap⦈⦇x⦈ = umap_of 𝔊 x 𝔉x (η⦇NTMap⦈⦇x⦈) 𝔉'x⦇ArrVal⦈⦇f⦈" by (rule η')
show "f : 𝔉x ↦⇩i⇩s⇩o⇘𝔇⇙ 𝔉'x"
by
(
rule
is_functor.cf_universal_arrow_of_is_iso_arr[
OF Φ.RL.is_functor_axioms 𝔉a_η 𝔉'a_η f η'
]
)
qed
subsubsection‹Main results›
lemma cf_adj_LR_iso_is_iso_functor:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇" and "Ψ : 𝔉' ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
shows "∃!θ. θ : 𝔉 ↦⇩C⇩F 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇 ∧ η⇩C Ψ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ) ∙⇩N⇩T⇩C⇩F η⇩C Φ"
and "cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇"
and "η⇩C Ψ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ) ∙⇩N⇩T⇩C⇩F η⇩C Φ"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))
let ?η = ‹η⇩C Φ›
let ?η' = ‹η⇩C Ψ›
let ?ΦΨ = ‹cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ›
show 𝔉'Ψ: "?ΦΨ : 𝔉 ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇"
proof(intro is_iso_ntcfI is_ntcfI')
show "vfsequence ?ΦΨ" unfolding cf_adj_LR_iso_def by auto
show "vcard ?ΦΨ = 5⇩ℕ"
unfolding cf_adj_LR_iso_def by (simp add: nat_omega_simps)
show "?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ ℭ⦇Obj⦈" for a
using cf_adj_LR_iso_app_unique(2)[OF assms that] by auto
show "?ΦΨ⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇f⦈ = 𝔉'⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔇⇙ ?ΦΨ⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘ℭ⇙ b" for a b f
proof-
from that have a: "a ∈⇩∘ ℭ⦇Obj⦈" and b: "b ∈⇩∘ ℭ⦇Obj⦈" by auto
note unique_a = cf_adj_LR_iso_app_unique[OF assms a]
note unique_b = cf_adj_LR_iso_app_unique[OF assms b]
from unique_a(2) have a_is_arr:
"?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
by auto
from unique_b(2) have b_is_arr:
"?ΦΨ⦇NTMap⦈⦇b⦈ : 𝔉⦇ObjMap⦈⦇b⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
by auto
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› ?η
by (rule Φ.cf_adjunction_unit_is_ntcf)
interpret η': is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉'› ?η'
by (rule Ψ.cf_adjunction_unit_is_ntcf)
from unique_a(3) a_is_arr a b have η'_a_def:
"?η'⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
from unique_b(3) b_is_arr a b have η'_b_def:
"?η'⦇NTMap⦈⦇b⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇b⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
from that a b a_is_arr have
"𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙
(𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈) =
𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps η'_a_def cs_intro: cat_cs_intros
)
also from η'.ntcf_Comp_commute[OF that, symmetric] that a b have
"… = ?η'⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
also from that a b b_is_arr have
"… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙
(?η⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ f)"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps η'_b_def cs_intro: cat_cs_intros
)
also from that have
"… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙
((𝔊 ∘⇩C⇩F 𝔉)⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
unfolding η.ntcf_Comp_commute[OF that, symmetric]
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps η'_b_def cs_intro: cat_cs_intros
)
also from that b_is_arr have
"… = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙
(𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
finally have [cat_cs_simps]:
"𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ (𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙
?η⦇NTMap⦈⦇a⦈) =
𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇b⦈⦈ ∘⇩A⇘ℭ⇙
(𝔊⦇ArrMap⦈⦇𝔉⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η⦇NTMap⦈⦇a⦈)"
by simp
note unique_f_a = is_functor.universal_arrow_ofD
[
OF
Φ.RL.is_functor_axioms
Φ.cf_adjunction_unit_component_is_ua_of[OF a]
]
from that a b a_is_arr b_is_arr have 𝔊𝔉f_ηa:
"𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ :
a ↦⇘ℭ⇙ 𝔊⦇ObjMap⦈⦇𝔉'⦇ObjMap⦈⦇b⦈⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from b have 𝔉'b: "𝔉'⦇ObjMap⦈⦇b⦈ ∈⇩∘ 𝔇⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from unique_f_a(3)[OF 𝔉'b 𝔊𝔉f_ηa] obtain f'
where f': "f' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈"
and ηa: "𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ =
umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)⦇ArrVal⦈⦇f'⦈"
and unique_f':
"⟦
f'' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇b⦈;
𝔊⦇ArrMap⦈⦇𝔉'⦇ArrMap⦈⦇f⦈⦈ ∘⇩A⇘ℭ⇙ ?η'⦇NTMap⦈⦇a⦈ =
umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇b⦈)⦇ArrVal⦈⦇f''⦈
⟧ ⟹ f'' = f'"
for f''
by metis
have "?ΦΨ⦇NTMap⦈⦇b⦈ ∘⇩A⇘𝔇⇙ 𝔉⦇ArrMap⦈⦇f⦈ = f'"
by (rule unique_f', insert a b a_is_arr b_is_arr that)
(
cs_concl cs_shallow
cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
)
moreover have "𝔉'⦇ArrMap⦈⦇f⦈ ∘⇩A⇘𝔇⇙ ?ΦΨ⦇NTMap⦈⦇a⦈ = f'"
by (rule unique_f', insert a b a_is_arr b_is_arr that)
(
cs_concl cs_shallow
cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
)
ultimately show ?thesis by simp
qed
qed
(
auto
intro: cat_cs_intros adj_cs_intros
simp: adj_cs_simps cf_adj_LR_iso_app_unique(2)[OF assms]
)
interpret 𝔉'Ψ: is_iso_ntcf α ℭ 𝔇 𝔉 𝔉' ‹?ΦΨ› by (rule 𝔉'Ψ)
show η'_def: "?η' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ΦΨ ∙⇩N⇩T⇩C⇩F η⇩C Φ"
proof(rule ntcf_eqI)
have dom_lhs: "𝒟⇩∘ (?η'⦇NTMap⦈) = ℭ⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: adj_cs_intros)
have dom_rhs: "𝒟⇩∘ ((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ΦΨ ∙⇩N⇩T⇩C⇩F η⇩C Φ)⦇NTMap⦈) = ℭ⦇Obj⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
show "?η'⦇NTMap⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ΦΨ ∙⇩N⇩T⇩C⇩F η⇩C Φ)⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems: "a ∈⇩∘ ℭ⦇Obj⦈"
note unique_a = cf_adj_LR_iso_app_unique[OF assms prems]
from unique_a(2) have a_is_arr:
"?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
by auto
interpret η: is_ntcf α ℭ ℭ ‹cf_id ℭ› ‹𝔊 ∘⇩C⇩F 𝔉› ?η
by (rule Φ.cf_adjunction_unit_is_ntcf)
from unique_a(3) a_is_arr prems have η'_a_def:
"?η'⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇a⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
from prems a_is_arr show
"?η'⦇NTMap⦈⦇a⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ΦΨ ∙⇩N⇩T⇩C⇩F ?η)⦇NTMap⦈⦇a⦈"
by
(
cs_concl cs_shallow
cs_simp: η'_a_def cat_cs_simps cs_intro: cat_cs_intros
)
qed (auto intro: cat_cs_intros adj_cs_intros)
qed
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)+
show "∃!θ. θ : 𝔉 ↦⇩C⇩F 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇 ∧ ?η' = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ) ∙⇩N⇩T⇩C⇩F ?η"
proof(intro ex1I conjI; (elim conjE)?)
from 𝔉'Ψ show "?ΦΨ : 𝔉 ↦⇩C⇩F 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇" by auto
show "?η' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F ?ΦΨ ∙⇩N⇩T⇩C⇩F η⇩C Φ" by (rule η'_def)
fix θ assume prems:
"θ : 𝔉 ↦⇩C⇩F 𝔉' : ℭ ↦↦⇩C⇘α⇙ 𝔇"
"?η' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ ∙⇩N⇩T⇩C⇩F η⇩C Φ"
interpret θ: is_ntcf α ℭ 𝔇 𝔉 𝔉' θ by (rule prems(1))
from prems have η'_a:
"?η'⦇NTMap⦈⦇a⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ ∙⇩N⇩T⇩C⇩F η⇩C Φ)⦇NTMap⦈⦇a⦈"
for a
by simp
have η'a: "η⇩C Ψ⦇NTMap⦈⦇a⦈ =
𝔊⦇ArrMap⦈⦇θ⦇NTMap⦈⦇a⦈⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇a⦈"
if "a ∈⇩∘ ℭ⦇Obj⦈" for a
using η'_a[where a=a] that
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
show "θ = ?ΦΨ"
proof(rule ntcf_eqI)
have dom_lhs: "𝒟⇩∘ (θ⦇NTMap⦈) = ℭ⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
have dom_rhs: "𝒟⇩∘ (?ΦΨ⦇NTMap⦈) = ℭ⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
show "θ⦇NTMap⦈ = ?ΦΨ⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix a assume prems': "a ∈⇩∘ ℭ⦇Obj⦈"
let ?uof = ‹umap_of 𝔊 a (𝔉⦇ObjMap⦈⦇a⦈) (?η⦇NTMap⦈⦇a⦈) (𝔉'⦇ObjMap⦈⦇a⦈)›
from cf_adj_LR_iso_app_unique[OF assms prems'] obtain f'
where f': "f' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
and η_def: "?η'⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇f'⦈"
and unique_f': "⋀f''.
⟦
f'' : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈;
?η'⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇f''⦈
⟧ ⟹ f'' = f'"
by metis
from prems' have θa: "θ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
from η_def f' prems' have
"η⇩C Ψ⦇NTMap⦈⦇a⦈ = 𝔊⦇ArrMap⦈⦇f'⦈ ∘⇩A⇘ℭ⇙ η⇩C Φ⦇NTMap⦈⦇a⦈"
by
(
cs_prems
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
from prems' have "η⇩C Ψ⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇θ⦇NTMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: cat_cs_simps η'a[OF prems']
cs_intro: adj_cs_intros cat_cs_intros
)
from unique_f'[OF θa this] have θa: "θ⦇NTMap⦈⦇a⦈ = f'".
from prems' have Ψa:
"?ΦΨ⦇NTMap⦈⦇a⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔇⇙ 𝔉'⦇ObjMap⦈⦇a⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from prems' have "η⇩C Ψ⦇NTMap⦈⦇a⦈ = ?uof⦇ArrVal⦈⦇?ΦΨ⦇NTMap⦈⦇a⦈⦈"
by
(
cs_concl
cs_simp: cf_adj_LR_iso_app_unique(3)[OF assms] cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
from unique_f'[OF Ψa this] have 𝔉'Ψ_def: "?ΦΨ⦇NTMap⦈⦇a⦈ = f'".
show "θ⦇NTMap⦈⦇a⦈ = ?ΦΨ⦇NTMap⦈⦇a⦈" unfolding θa 𝔉'Ψ_def ..
qed auto
qed (cs_concl cs_shallow cs_intro: cat_cs_intros)+
qed
qed
lemma op_ntcf_cf_adj_RL_iso[cat_op_simps]:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "Ψ : 𝔉 ⇌⇩C⇩F 𝔊' : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
defines "op_𝔇 ≡ op_cat 𝔇"
and "op_ℭ ≡ op_cat ℭ"
and "op_𝔉 ≡ op_cf 𝔉"
and "op_𝔊 ≡ op_cf 𝔊"
and "op_Φ ≡ op_cf_adj Φ"
and "op_𝔊' ≡ op_cf 𝔊'"
and "op_Ψ ≡ op_cf_adj Ψ"
shows
"op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ) =
cf_adj_LR_iso op_𝔇 op_ℭ op_𝔉 op_𝔊 op_Φ op_𝔊' op_Ψ"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ‹ε⇩C Φ›
by (rule Φ.cf_adjunction_counit_is_ntcf)
have dom_lhs: "𝒟⇩∘ (op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)) = 5⇩ℕ"
unfolding op_ntcf_def by (simp add: nat_omega_simps)
show ?thesis
proof(rule vsv_eqI, unfold dom_lhs)
fix a assume prems: "a ∈⇩∘ 5⇩ℕ"
then have "a ∈⇩∘ 5⇩ℕ" unfolding dom_lhs by simp
then show
"op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)⦇a⦈ =
cf_adj_LR_iso op_𝔇 op_ℭ op_𝔉 op_𝔊 op_Φ op_𝔊' op_Ψ⦇a⦈"
by
(
elim_in_numeral,
fold nt_field_simps,
unfold
cf_adj_LR_iso_components
op_ntcf_components
cf_adj_RL_iso_components
Let_def
Φ.cf_adjunction_unit_NTMap_op
Ψ.cf_adjunction_unit_NTMap_op
assms(3-9)
cat_op_simps
)
simp_all
qed (auto simp: op_ntcf_def cf_adj_LR_iso_def nat_omega_simps)
qed
lemma op_ntcf_cf_adj_LR_iso[cat_op_simps]:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇" and "Ψ : 𝔉' ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
defines "op_𝔇 ≡ op_cat 𝔇"
and "op_ℭ ≡ op_cat ℭ"
and "op_𝔉 ≡ op_cf 𝔉"
and "op_𝔊 ≡ op_cf 𝔊"
and "op_Φ ≡ op_cf_adj Φ"
and "op_𝔉' ≡ op_cf 𝔉'"
and "op_Ψ ≡ op_cf_adj Ψ"
shows
"op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ) =
cf_adj_RL_iso op_𝔇 op_ℭ op_𝔊 op_𝔉 op_Φ op_𝔉' op_Ψ"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉' 𝔊 Ψ by (rule assms(2))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ‹ε⇩C Φ›
by (rule Φ.cf_adjunction_counit_is_ntcf)
have dom_lhs: "𝒟⇩∘ (op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ)) = 5⇩ℕ"
unfolding op_ntcf_def by (simp add: nat_omega_simps)
show ?thesis
proof(rule vsv_eqI, unfold dom_lhs)
fix a assume prems: "a ∈⇩∘ 5⇩ℕ"
then show
"op_ntcf (cf_adj_LR_iso ℭ 𝔇 𝔊 𝔉 Φ 𝔉' Ψ)⦇a⦈ =
cf_adj_RL_iso op_𝔇 op_ℭ op_𝔊 op_𝔉 op_Φ op_𝔉' op_Ψ⦇a⦈"
by
(
elim_in_numeral,
use nothing in
‹
fold nt_field_simps,
unfold
cf_adj_LR_iso_components
op_ntcf_components
cf_adj_RL_iso_components
Let_def
Φ.op_ntcf_cf_adjunction_unit[symmetric]
Ψ.op_ntcf_cf_adjunction_unit[symmetric]
assms(3-9)
cat_op_simps
›
)
simp_all
qed (auto simp: op_ntcf_def cf_adj_RL_iso_def nat_omega_simps)
qed
lemma cf_adj_RL_iso_app_unique:
fixes ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "Ψ : 𝔉 ⇌⇩C⇩F 𝔊' : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
and "x ∈⇩∘ 𝔇⦇Obj⦈"
defines "𝔊x ≡ 𝔊⦇ObjMap⦈⦇x⦈"
and "𝔊'x ≡ 𝔊'⦇ObjMap⦈⦇x⦈"
and "ε ≡ ε⇩C Φ"
and "ε' ≡ ε⇩C Ψ"
and "f ≡ cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ⦇NTMap⦈⦇x⦈"
shows
"∃!f'.
f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈"
"f : 𝔊'x ↦⇩i⇩s⇩o⇘ℭ⇙ 𝔊x"
"ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f⦈"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ‹ε⇩C Φ›
by (rule Φ.cf_adjunction_counit_is_ntcf)
show
"∃!f'.
f' : 𝔊'x ↦⇘ℭ⇙ 𝔊x ∧
ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f'⦈"
"f : 𝔊'x ↦⇩i⇩s⇩o⇘ℭ⇙ 𝔊x"
"ε'⦇NTMap⦈⦇x⦈ = umap_fo 𝔉 x 𝔊x (ε⦇NTMap⦈⦇x⦈) 𝔊'x⦇ArrVal⦈⦇f⦈"
by
(
intro cf_adj_LR_iso_app_unique
[
OF Φ.is_cf_adjunction_op Ψ.is_cf_adjunction_op,
unfolded cat_op_simps,
OF assms(3),
unfolded Ψ.cf_adjunction_unit_NTMap_op,
folded Φ.op_ntcf_cf_adjunction_counit,
folded op_ntcf_cf_adj_RL_iso[OF assms(1,2)],
unfolded cat_op_simps,
folded assms(4-8)
]
)+
qed
lemma cf_adj_RL_iso_is_iso_functor:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : ℭ ⇌⇌⇩C⇘α⇙ 𝔇" and "Ψ : 𝔉 ⇌⇩C⇩F 𝔊' : ℭ ⇌⇌⇩C⇘α⇙ 𝔇"
shows "∃!θ.
θ : 𝔊' ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ ∧
ε⇩C Ψ = ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ)"
and "cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ : 𝔊' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
and "ε⇩C Ψ =
ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)"
proof-
interpret Φ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊 Φ by (rule assms(1))
interpret Ψ: is_cf_adjunction α ℭ 𝔇 𝔉 𝔊' Ψ by (rule assms(2))
interpret ε: is_ntcf α 𝔇 𝔇 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔇› ‹ε⇩C Φ›
by (rule Φ.cf_adjunction_counit_is_ntcf)
note cf_adj_LR_iso_is_iso_functor_op = cf_adj_LR_iso_is_iso_functor
[
OF Φ.is_cf_adjunction_op Ψ.is_cf_adjunction_op,
folded
Φ.op_ntcf_cf_adjunction_counit
Ψ.op_ntcf_cf_adjunction_counit
op_ntcf_cf_adj_RL_iso[OF assms]
]
from cf_adj_LR_iso_is_iso_functor_op(1) obtain θ
where θ: "θ : op_cf 𝔊 ↦⇩C⇩F op_cf 𝔊' : op_cat 𝔇 ↦↦⇩C⇘α⇙ op_cat ℭ"
and op_ntcf_ε_def: "op_ntcf (ε⇩C Ψ) =
op_cf 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ ∙⇩N⇩T⇩C⇩F op_ntcf (ε⇩C Φ)"
and unique_θ':
"⟦
θ' : op_cf 𝔊 ↦⇩C⇩F op_cf 𝔊' : op_cat 𝔇 ↦↦⇩C⇘α⇙ op_cat ℭ;
op_ntcf (ε⇩C Ψ) = op_cf 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ' ∙⇩N⇩T⇩C⇩F op_ntcf (ε⇩C Φ)
⟧ ⟹ θ' = θ"
for θ'
by metis
interpret θ: is_ntcf α ‹op_cat 𝔇› ‹op_cat ℭ› ‹op_cf 𝔊› ‹op_cf 𝔊'› θ
by (rule θ)
show "∃!θ. θ : 𝔊' ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ ∧ ε⇩C Ψ = ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ)"
proof(intro ex1I conjI; (elim conjE)?)
show op_θ: "op_ntcf θ : 𝔊' ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
by (rule θ.is_ntcf_op[unfolded cat_op_simps])
from op_ntcf_ε_def have
"op_ntcf (op_ntcf (ε⇩C Ψ)) =
op_ntcf (op_cf 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ ∙⇩N⇩T⇩C⇩F op_ntcf (ε⇩C Φ))"
by simp
then show ε_def: "ε⇩C Ψ = ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf θ)"
by
(
cs_prems cs_shallow
cs_simp: cat_op_simps
cs_intro: adj_cs_intros cat_cs_intros cat_op_intros
)
fix θ' assume prems:
"θ' : 𝔊' ↦⇩C⇩F 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
"ε⇩C Ψ = ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F θ')"
interpret θ': is_ntcf α 𝔇 ℭ 𝔊' 𝔊 θ' by (rule prems(1))
have "op_ntcf (ε⇩C Ψ) = op_cf 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf θ' ∙⇩N⇩T⇩C⇩F op_ntcf (ε⇩C Φ)"
by
(
cs_concl cs_shallow
cs_simp:
prems(2)
op_ntcf_cf_ntcf_comp[symmetric]
op_ntcf_ntcf_vcomp[symmetric]
cs_intro: cat_cs_intros
)
from unique_θ'[OF θ'.is_ntcf_op this, symmetric] have
"op_ntcf θ = op_ntcf (op_ntcf θ')"
by simp
then show "θ' = op_ntcf θ"
by (cs_prems cs_shallow cs_simp: cat_cs_simps cat_op_simps) simp
qed
from is_iso_ntcf.is_iso_ntcf_op[OF cf_adj_LR_iso_is_iso_functor_op(2)] show
"cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ : 𝔊' ↦⇩C⇩F⇩.⇩i⇩s⇩o 𝔊 : 𝔇 ↦↦⇩C⇘α⇙ ℭ"
by
(
cs_prems cs_shallow
cs_simp: cat_op_simps cs_intro: adj_cs_intros cat_op_intros
)
from cf_adj_LR_iso_is_iso_functor_op(3) have
"op_ntcf (op_ntcf (ε⇩C Ψ)) =
op_ntcf
(
op_cf 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F op_ntcf (cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ) ∙⇩N⇩T⇩C⇩F
op_ntcf (ε⇩C Φ)
)"
by simp
from
this
cf_adj_LR_iso_is_iso_functor_op(2)[
unfolded op_ntcf_cf_adj_RL_iso[OF assms]
]
show "ε⇩C Ψ = ε⇩C Φ ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F cf_adj_RL_iso ℭ 𝔇 𝔉 𝔊 Φ 𝔊' Ψ)"
by
(
cs_prems cs_shallow
cs_simp: cat_op_simps cat_op_simps
cs_intro: ntcf_cs_intros adj_cs_intros cat_cs_intros cat_op_intros
)
qed
subsection‹Further properties of the adjoint functors›
lemma (in is_cf_adjunction) cf_adj_exp_cf_cat:
assumes "𝒵 β" and "α ∈⇩∘ β" and "category α 𝔍"
shows
"cf_adjunction_of_unit
β
(exp_cf_cat α 𝔉 𝔍)
(exp_cf_cat α 𝔊 𝔍)
(exp_ntcf_cat α (η⇩C Φ) 𝔍) :
exp_cf_cat α 𝔉 𝔍 ⇌⇩C⇩F exp_cf_cat α 𝔊 𝔍 :
cat_FUNCT α 𝔍 ℭ ⇌⇌⇩C⇘β⇙ cat_FUNCT α 𝔍 𝔇"
proof-
interpret β: 𝒵 β by (rule assms(1))
interpret 𝔍: category α 𝔍 by (rule assms(3))
show ?thesis
proof
(
rule counit_unit_is_cf_adjunction(1)[
where ε = ‹exp_ntcf_cat α (ε⇩C Φ) 𝔍›
]
)
from assms show "exp_ntcf_cat α (η⇩C Φ) 𝔍 :
cf_id (cat_FUNCT α 𝔍 ℭ) ↦⇩C⇩F exp_cf_cat α 𝔊 𝔍 ∘⇩C⇩F exp_cf_cat α 𝔉 𝔍 :
cat_FUNCT α 𝔍 ℭ ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔍 ℭ"
by
(
cs_concl
cs_simp:
cat_cs_simps cat_FUNCT_cs_simps
exp_cf_cat_cf_id_cat[symmetric] exp_cf_cat_cf_comp[symmetric]
cs_intro:
cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
)
from assms show
"exp_ntcf_cat α (ε⇩C Φ) 𝔍 :
exp_cf_cat α 𝔉 𝔍 ∘⇩C⇩F exp_cf_cat α 𝔊 𝔍 ↦⇩C⇩F cf_id (cat_FUNCT α 𝔍 𝔇) :
cat_FUNCT α 𝔍 𝔇 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔍 𝔇"
by
(
cs_concl
cs_simp:
cat_cs_simps
cat_FUNCT_cs_simps
exp_cf_cat_cf_id_cat[symmetric]
exp_cf_cat_cf_comp[symmetric]
cs_intro:
cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
)
note [symmetric, cat_cs_simps] =
ntcf_id_exp_cf_cat
exp_ntcf_cat_ntcf_vcomp
exp_ntcf_cat_ntcf_cf_comp
exp_ntcf_cat_cf_ntcf_comp
from assms show
"(exp_cf_cat α 𝔊 𝔍 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α (ε⇩C Φ) 𝔍) ∙⇩N⇩T⇩C⇩F
(exp_ntcf_cat α (η⇩C Φ) 𝔍 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α 𝔊 𝔍) =
ntcf_id (exp_cf_cat α 𝔊 𝔍)"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
from assms show
"exp_ntcf_cat α (ε⇩C Φ) 𝔍 ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cf_cat α 𝔉 𝔍 ∙⇩N⇩T⇩C⇩F
(exp_cf_cat α 𝔉 𝔍 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_ntcf_cat α (η⇩C Φ) 𝔍) =
ntcf_id (exp_cf_cat α 𝔉 𝔍)"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
qed
(
use assms in
‹
cs_concl
cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
›
)+
qed
lemma (in is_cf_adjunction) cf_adj_exp_cf_cat_exp_cf_cat:
assumes "𝒵 β" and "α ∈⇩∘ β" and "category α 𝔄"
shows
"cf_adjunction_of_unit
β
(exp_cat_cf α 𝔄 𝔊)
(exp_cat_cf α 𝔄 𝔉)
(exp_cat_ntcf α 𝔄 (η⇩C Φ)) :
exp_cat_cf α 𝔄 𝔊 ⇌⇩C⇩F exp_cat_cf α 𝔄 𝔉 :
cat_FUNCT α ℭ 𝔄 ⇌⇌⇩C⇘β⇙ cat_FUNCT α 𝔇 𝔄"
proof-
interpret β: 𝒵 β by (rule assms(1))
interpret 𝔄: category α 𝔄 by (rule assms(3))
show ?thesis
proof
(
rule counit_unit_is_cf_adjunction(1)[
where ε = ‹exp_cat_ntcf α 𝔄 (ε⇩C Φ)›
]
)
from assms is_cf_adjunction_axioms show
"exp_cat_ntcf α 𝔄 (η⇩C Φ) :
cf_id (cat_FUNCT α ℭ 𝔄) ↦⇩C⇩F exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔊 :
cat_FUNCT α ℭ 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α ℭ 𝔄"
by
(
cs_concl
cs_simp:
exp_cat_cf_cat_cf_id[symmetric] exp_cat_cf_cf_comp[symmetric]
cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
)
from assms is_cf_adjunction_axioms show
"exp_cat_ntcf α 𝔄 (ε⇩C Φ) :
exp_cat_cf α 𝔄 𝔊 ∘⇩C⇩F exp_cat_cf α 𝔄 𝔉 ↦⇩C⇩F cf_id (cat_FUNCT α 𝔇 𝔄) :
cat_FUNCT α 𝔇 𝔄 ↦↦⇩C⇘β⇙ cat_FUNCT α 𝔇 𝔄"
by
(
cs_concl
cs_simp:
exp_cat_cf_cat_cf_id[symmetric] exp_cat_cf_cf_comp[symmetric]
cs_intro: cat_small_cs_intros cat_FUNCT_cs_intros adj_cs_intros
)
note [symmetric, cat_cs_simps] =
ntcf_id_exp_cat_cf
exp_cat_ntcf_ntcf_vcomp
exp_cat_ntcf_ntcf_cf_comp
exp_cat_ntcf_cf_ntcf_comp
from assms show
"exp_cat_cf α 𝔄 𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 (ε⇩C Φ) ∙⇩N⇩T⇩C⇩F
(exp_cat_ntcf α 𝔄 (η⇩C Φ) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔄 𝔉) =
ntcf_id (exp_cat_cf α 𝔄 𝔉)"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
from assms show
"exp_cat_ntcf α 𝔄 (ε⇩C Φ) ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F exp_cat_cf α 𝔄 𝔊 ∙⇩N⇩T⇩C⇩F
(exp_cat_cf α 𝔄 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F exp_cat_ntcf α 𝔄 (η⇩C Φ)) =
ntcf_id (exp_cat_cf α 𝔄 𝔊)"
by
(
cs_concl cs_shallow
cs_simp: adj_cs_simps cat_cs_simps
cs_intro: adj_cs_intros cat_cs_intros
)
qed
(
use assms in
‹
cs_concl
cs_intro: cat_cs_intros cat_small_cs_intros cat_FUNCT_cs_intros
›
)+
qed
subsection‹Adjoints on limits›
lemma cf_AdjRight_preserves_limits:
assumes "Φ : 𝔉 ⇌⇩C⇩F 𝔊 : 𝔛 ⇌⇌⇩C⇘α⇙ 𝔄"
shows "is_cf_continuous α 𝔊"
proof(intro is_cf_continuousI)
interpret Φ: is_cf_adjunction α 𝔛 𝔄 𝔉 𝔊 Φ by (rule assms(1))
show "𝔊 : 𝔄 ↦↦⇩C⇘α⇙ 𝔛" by (rule Φ.RL.is_functor_axioms)
fix 𝔗 𝔍 assume prems: "𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔄"
show "cf_preserves_limits α 𝔊 𝔗"
proof(intro cf_preserves_limitsI, rule prems, rule Φ.RL.is_functor_axioms)
fix τ a assume "τ : a <⇩C⇩F⇩.⇩l⇩i⇩m 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔄"
then interpret τ: is_cat_limit α 𝔍 𝔄 𝔗 a τ .
show "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ : 𝔊⦇ObjMap⦈⦇a⦈ <⇩C⇩F⇩.⇩l⇩i⇩m 𝔊 ∘⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔛"
proof(intro is_cat_limitI)
show "𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ : 𝔊⦇ObjMap⦈⦇a⦈ <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔊 ∘⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔛"
by
(
intro cf_ntcf_comp_cf_cat_cone prems,
rule τ.is_cat_cone_axioms,
intro Φ.RL.is_functor_axioms
)
fix σ' b' assume "σ' : b' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔊 ∘⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔛"
then interpret σ': is_cat_cone α b' 𝔍 𝔛 ‹𝔊 ∘⇩C⇩F 𝔗› σ' .
have "ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 : 𝔉 ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔗) ↦⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔄"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros adj_cs_intros)
moreover have "𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F σ' :
𝔉⦇ObjMap⦈⦇b'⦈ <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔉 ∘⇩C⇩F (𝔊 ∘⇩C⇩F 𝔗) : 𝔍 ↦↦⇩C⇘α⇙ 𝔄"
by
(
intro cf_ntcf_comp_cf_cat_cone,
rule σ'.is_cat_cone_axioms,
rule Φ.LR.is_functor_axioms
)
ultimately have "(ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F σ') :
𝔉⦇ObjMap⦈⦇b'⦈ <⇩C⇩F⇩.⇩c⇩o⇩n⇩e 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔄"
by (rule ntcf_vcomp_is_cat_cone)
from τ.cat_lim_unique_cone'[OF this] obtain h
where h: "h : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a"
and ε𝔗_𝔉σ': "⋀j. j ∈⇩∘ 𝔍⦇Obj⦈ ⟹
((ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F σ'))⦇NTMap⦈⦇j⦈ = τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ h"
and h_unique:
"⟦
h' : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a;
⋀j. j ∈⇩∘ 𝔍⦇Obj⦈ ⟹
((ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗) ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F σ'))⦇NTMap⦈⦇j⦈ =
τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ h'
⟧ ⟹ h' = h"
for h'
by metis
have ε𝔗_𝔉σ:
"ε⇩C Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈ ∘⇩A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇σ'⦇NTMap⦈⦇j⦈⦈ =
τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ h"
if "j ∈⇩∘ 𝔍⦇Obj⦈" for j
using ε𝔗_𝔉σ'[OF that] that
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: adj_cs_intros cat_cs_intros
)
show "∃!f'.
f' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈ ∧ σ' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 f'"
proof(intro ex1I conjI; (elim conjE)?)
let ?h' = ‹𝔊⦇ArrMap⦈⦇h⦈ ∘⇩A⇘𝔛⇙ η⇩C Φ⦇NTMap⦈⦇b'⦈›
from h show "?h' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈"
by
(
cs_concl cs_shallow
cs_intro: cat_cs_intros cat_lim_cs_intros adj_cs_intros
)
show "σ' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 ?h'"
proof(rule ntcf_eqI)
show "σ' : cf_const 𝔍 𝔛 b' ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔛"
by (rule σ'.is_ntcf_axioms)
then have dom_lhs: "𝒟⇩∘ (σ'⦇NTMap⦈) = 𝔍⦇Obj⦈"
by (cs_concl cs_shallow cs_simp: cat_cs_simps)
from h show
"𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 ?h' :
cf_const 𝔍 𝔛 b' ↦⇩C⇩F 𝔊 ∘⇩C⇩F 𝔗 : 𝔍 ↦↦⇩C⇘α⇙ 𝔛"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_lim_cs_intros adj_cs_intros cat_cs_intros
)
then have dom_rhs:
"𝒟⇩∘ ((𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈) = 𝔍⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps)
show "σ'⦇NTMap⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
fix j assume prems': "j ∈⇩∘ 𝔍⦇Obj⦈"
note [cat_cs_simps] = Φ.L.cat_assoc_helper
[
where h=‹𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈›
and g=‹𝔊⦇ArrMap⦈⦇h⦈›
and f=‹η⇩C Φ⦇NTMap⦈⦇b'⦈›
and q=‹𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ h⦈›
]
from prems' h have [cat_cs_simps]:
"𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ h⦈ ∘⇩A⇘𝔛⇙ η⇩C Φ⦇NTMap⦈⦇b'⦈ = σ'⦇NTMap⦈⦇j⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps ε𝔗_𝔉σ[OF prems', symmetric]
cs_intro: adj_cs_intros cat_cs_intros
)
from prems' h show
"σ'⦇NTMap⦈⦇j⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 ?h')⦇NTMap⦈⦇j⦈"
by
(
cs_concl
cs_simp: cat_cs_simps
cs_intro: cat_lim_cs_intros adj_cs_intros cat_cs_intros
)
qed (cs_concl cs_intro: V_cs_intros cat_cs_intros)+
qed simp_all
fix f' assume prems':
"f' : b' ↦⇘𝔛⇙ 𝔊⦇ObjMap⦈⦇a⦈"
"σ' = 𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 f'"
from prems'(2) have σ'_j_def':
"σ'⦇NTMap⦈⦇j⦈ = (𝔊 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F τ ∙⇩N⇩T⇩C⇩F ntcf_const 𝔍 𝔛 f')⦇NTMap⦈⦇j⦈"
for j
by simp
have σ'_j_def: "σ'⦇NTMap⦈⦇j⦈ = 𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈ ∘⇩A⇘𝔛⇙ f'"
if "j ∈⇩∘ 𝔍⦇Obj⦈" for j
using σ'_j_def'[of j] that prems'(1)
by
(
cs_prems
cs_simp: cat_cs_simps cs_intro: cat_lim_cs_intros cat_cs_intros
)
from prems'(1) have εa_𝔉f':
"ε⇩C Φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈ : 𝔉⦇ObjMap⦈⦇b'⦈ ↦⇘𝔄⇙ a"
by (cs_concl cs_intro: cat_lim_cs_intros cat_cs_intros adj_cs_intros)
interpret ε: is_ntcf α 𝔄 𝔄 ‹𝔉 ∘⇩C⇩F 𝔊› ‹cf_id 𝔄› ‹ε⇩C Φ›
by (rule Φ.cf_adjunction_counit_is_ntcf)
have
"(ε⇩C Φ ∘⇩N⇩T⇩C⇩F⇩-⇩C⇩F 𝔗 ∙⇩N⇩T⇩C⇩F (𝔉 ∘⇩C⇩F⇩-⇩N⇩T⇩C⇩F σ'))⦇NTMap⦈⦇j⦈ =
τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ (ε⇩C Φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈)"
if "j ∈⇩∘ 𝔍⦇Obj⦈" for j
proof-
from that have "τ⦇NTMap⦈⦇j⦈ : a ↦⇘𝔄⇙ 𝔗⦇ObjMap⦈⦇j⦈"
by
(
cs_concl cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
from ε.ntcf_Comp_commute[OF this] that have [cat_cs_simps]:
"ε⇩C Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈ ∘⇩A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈⦈ =
τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ ε⇩C Φ⦇NTMap⦈⦇a⦈"
by
(
cs_prems cs_shallow
cs_simp: cat_cs_simps cs_intro: cat_cs_intros
)
note [cat_cs_simps] = Φ.R.cat_assoc_helper
[
where h=‹ε⇩C Φ⦇NTMap⦈⦇𝔗⦇ObjMap⦈⦇j⦈⦈›
and g=‹𝔉⦇ArrMap⦈⦇𝔊⦇ArrMap⦈⦇τ⦇NTMap⦈⦇j⦈⦈⦈›
and q=‹τ⦇NTMap⦈⦇j⦈ ∘⇩A⇘𝔄⇙ ε⇩C Φ⦇NTMap⦈⦇a⦈›
]
show ?thesis
using that prems'(1)
by
(
cs_concl
cs_simp: cat_cs_simps σ'_j_def
cs_intro: cat_lim_cs_intros cat_cs_intros adj_cs_intros
)
qed
from h_unique[OF εa_𝔉f' this] have
"𝔊⦇ArrMap⦈⦇ε⇩C Φ⦇NTMap⦈⦇a⦈ ∘⇩A⇘𝔄⇙ 𝔉⦇ArrMap⦈⦇f'⦈⦈ ∘⇩A⇘𝔛⇙ η⇩C Φ⦇NTMap⦈⦇b'⦈ = ?h'"
by simp
from this prems'(1) show "f' = 𝔊⦇ArrMap⦈⦇h⦈ ∘⇩A⇘𝔛⇙ η⇩C Φ⦇NTMap⦈⦇b'⦈"
by
(
cs_prems
cs_simp: cat_cs_simps Φ.cf_adj_counit_unit_app
cs_intro: cat_lim_cs_intros cat_cs_intros
)
qed
qed
qed
qed
text‹\newpage›
end