Theory CZH_UCAT_Limit_IT
section‹Initial and terminal objects as limits and colimits›
theory CZH_UCAT_Limit_IT
imports
CZH_UCAT_Limit
CZH_Elementary_Categories.CZH_ECAT_Comma
begin
subsection‹Initial and terminal objects as limits/colimits of an empty diagram›
subsubsection‹Definition and elementary properties›
text‹
See
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/initial+object}
}, \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/terminal+object}
} and Chapter X-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
locale is_cat_obj_empty_terminal = is_cat_limit α cat_0 ℭ ‹cf_0 ℭ› z ℨ
for α ℭ z ℨ
syntax "_is_cat_obj_empty_terminal" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ <⇩C⇩F⇩.⇩1 0⇩C⇩F :/ 0⇩C ↦↦⇩Cı _)› [51, 51] 51)
syntax_consts "_is_cat_obj_empty_terminal" ⇌ is_cat_obj_empty_terminal
translations "ℨ : z <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α⇙ ℭ" ⇌
"CONST is_cat_obj_empty_terminal α ℭ z ℨ"
locale is_cat_obj_empty_initial = is_cat_colimit α cat_0 ℭ ‹cf_0 ℭ› z ℨ
for α ℭ z ℨ
syntax "_is_cat_obj_empty_initial" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ 0⇩C⇩F >⇩C⇩F⇩.⇩0 _ :/ 0⇩C ↦↦⇩Cı _)› [51, 51] 51)
syntax_consts "_is_cat_obj_empty_initial" ⇌ is_cat_obj_empty_initial
translations "ℨ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z : 0⇩C ↦↦⇩C⇘α⇙ ℭ" ⇌
"CONST is_cat_obj_empty_initial α ℭ z ℨ"
text‹Rules.›
lemma (in is_cat_obj_empty_terminal)
is_cat_obj_empty_terminal_axioms'[cat_lim_cs_intros]:
assumes "α' = α" and "z' = z" and "ℭ' = ℭ"
shows "ℨ : z' <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α'⇙ ℭ'"
unfolding assms by (rule is_cat_obj_empty_terminal_axioms)
mk_ide rf is_cat_obj_empty_terminal_def
|intro is_cat_obj_empty_terminalI|
|dest is_cat_obj_empty_terminalD[dest]|
|elim is_cat_obj_empty_terminalE[elim]|
lemmas [cat_lim_cs_intros] = is_cat_obj_empty_terminalD
lemma (in is_cat_obj_empty_initial)
is_cat_obj_empty_initial_axioms'[cat_lim_cs_intros]:
assumes "α' = α" and "z' = z" and "ℭ' = ℭ"
shows "ℨ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z' : 0⇩C ↦↦⇩C⇘α'⇙ ℭ'"
unfolding assms by (rule is_cat_obj_empty_initial_axioms)
mk_ide rf is_cat_obj_empty_initial_def
|intro is_cat_obj_empty_initialI|
|dest is_cat_obj_empty_initialD[dest]|
|elim is_cat_obj_empty_initialE[elim]|
lemmas [cat_lim_cs_intros] = is_cat_obj_empty_initialD
text‹Duality.›
lemma (in is_cat_obj_empty_terminal) is_cat_obj_empty_initial_op:
"op_ntcf ℨ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z : 0⇩C ↦↦⇩C⇘α⇙ op_cat ℭ"
by (intro is_cat_obj_empty_initialI)
(
cs_concl cs_shallow
cs_simp: cat_op_simps op_cf_cf_0 cs_intro: cat_cs_intros cat_op_intros
)
lemma (in is_cat_obj_empty_terminal) is_cat_obj_empty_initial_op'[cat_op_intros]:
assumes "ℭ' = op_cat ℭ"
shows "op_ntcf ℨ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z : 0⇩C ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cat_obj_empty_initial_op)
lemmas [cat_op_intros] = is_cat_obj_empty_terminal.is_cat_obj_empty_initial_op'
lemma (in is_cat_obj_empty_initial) is_cat_obj_empty_terminal_op:
"op_ntcf ℨ : z <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α⇙ op_cat ℭ"
by (intro is_cat_obj_empty_terminalI)
(
cs_concl cs_shallow
cs_simp: cat_op_simps op_cf_cf_0 cs_intro: cat_cs_intros cat_op_intros
)
lemma (in is_cat_obj_empty_initial) is_cat_obj_empty_terminal_op'[cat_op_intros]:
assumes "ℭ' = op_cat ℭ"
shows "op_ntcf ℨ : z <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cat_obj_empty_terminal_op)
lemmas [cat_op_intros] = is_cat_obj_empty_initial.is_cat_obj_empty_terminal_op'
text‹Elementary properties.›
lemma (in is_cat_obj_empty_terminal) cat_oet_ntcf_0: "ℨ = ntcf_0 ℭ"
by (rule is_ntcf_is_ntcf_0_if_cat_0)
(cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
lemma (in is_cat_obj_empty_initial) cat_oei_ntcf_0: "ℨ = ntcf_0 ℭ"
by (rule is_ntcf_is_ntcf_0_if_cat_0)
(cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
subsubsection‹
Initial and terminal objects as limits/colimits of an empty diagram
are initial and terminal objects
›
lemma (in category) cat_obj_terminal_is_cat_obj_empty_terminal:
assumes "obj_terminal ℭ z"
shows "ntcf_0 ℭ : z <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α⇙ ℭ"
proof-
from assms have z: "z ∈⇩∘ ℭ⦇Obj⦈" by auto
from z have [cat_cs_simps]: "cf_const cat_0 ℭ z = cf_0 ℭ"
by (intro is_functor_is_cf_0_if_cat_0) (cs_concl cs_intro: cat_cs_intros)
note obj_terminalD = obj_terminalD[OF assms]
show ?thesis
proof
(
intro is_cat_obj_empty_terminalI is_cat_limitI is_cat_coneI,
unfold cat_cs_simps
)
show "∃!f'. f' : r' ↦⇘ℭ⇙ z ∧ u' = ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f'"
if "u' : r' <⇩C⇩F⇩.⇩c⇩o⇩n⇩e cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ" for u' r'
proof-
interpret u': is_cat_cone α r' cat_0 ℭ ‹cf_0 ℭ› u' by (rule that)
from z have [cat_cs_simps]: "cf_const cat_0 ℭ r' = cf_0 ℭ"
by (intro is_functor_is_cf_0_if_cat_0)
(cs_concl cs_shallow cs_intro: cat_cs_intros)
have u'_def: "u' = ntcf_0 ℭ"
by
(
rule is_ntcf_is_ntcf_0_if_cat_0[
OF u'.is_ntcf_axioms, unfolded cat_cs_simps
]
)
from obj_terminalD(2)[OF u'.cat_cone_obj] obtain f'
where f': "f' : r' ↦⇘ℭ⇙ z"
and f'_unique: "f'' : r' ↦⇘ℭ⇙ z ⟹ f'' = f'"
for f''
by auto
from f' have [cat_cs_simps]: "ntcf_const cat_0 ℭ f' = ntcf_0 ℭ"
by (intro is_ntcf_is_ntcf_0_if_cat_0(1))
(cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show ?thesis
proof(intro ex1I conjI; (elim conjE)?)
show "u' = ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f'"
by
(
cs_concl cs_shallow
cs_simp: u'_def cat_cs_simps cs_intro: cat_cs_intros
)
fix f'' assume prems:
"f'' : r' ↦⇘ℭ⇙ z" "u' = ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f''"
show "f'' = f'" by (rule f'_unique[OF prems(1)])
qed (rule f')
qed
qed (cs_concl cs_simp: cat_cs_simps cs_intro: z cat_cs_intros)
qed
lemma (in category) cat_obj_initial_is_cat_obj_empty_initial:
assumes "obj_initial ℭ z"
shows "ntcf_0 ℭ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z : 0⇩C ↦↦⇩C⇘α⇙ ℭ"
proof-
have z: "obj_terminal (op_cat ℭ) z" unfolding cat_op_simps by (rule assms)
show ?thesis
by
(
rule is_cat_obj_empty_terminal.is_cat_obj_empty_initial_op
[
OF category.cat_obj_terminal_is_cat_obj_empty_terminal[
OF category_op z, folded op_ntcf_ntcf_0
],
unfolded cat_op_simps op_ntcf_ntcf_0
]
)
qed
lemma (in is_cat_obj_empty_terminal) cat_oet_obj_terminal: "obj_terminal ℭ z"
proof-
show "obj_terminal ℭ z"
proof(rule obj_terminalI)
fix a assume prems: "a ∈⇩∘ ℭ⦇Obj⦈"
have [cat_cs_simps]: "cf_const cat_0 ℭ a = cf_0 ℭ"
by (rule is_functor_is_cf_0_if_cat_0)
(cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros prems)
from prems have "ntcf_0 ℭ : a <⇩C⇩F⇩.⇩c⇩o⇩n⇩e cf_0 ℭ : cat_0 ↦↦⇩C⇘α⇙ ℭ"
by (intro is_cat_coneI)
(cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from cat_lim_ua_fo[OF this] obtain f'
where f': "f' : a ↦⇘ℭ⇙ z"
and "ntcf_0 ℭ = ℨ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f'"
and f'_unique:
"⟦ f'' : a ↦⇘ℭ⇙ z; ntcf_0 ℭ = ℨ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f'' ⟧ ⟹
f'' = f'"
for f''
by metis
show "∃!f'. f' : a ↦⇘ℭ⇙ z"
proof(intro ex1I)
fix f'' assume prems': "f'' : a ↦⇘ℭ⇙ z"
from prems' have "ntcf_0 ℭ = ntcf_0 ℭ ∙⇩N⇩T⇩C⇩F ntcf_const cat_0 ℭ f''"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from f'_unique[OF prems', unfolded cat_oet_ntcf_0, OF this]
show "f'' = f'".
qed (rule f')
qed (rule cat_cone_obj)
qed
lemma (in is_cat_obj_empty_initial) cat_oei_obj_initial: "obj_initial ℭ z"
by
(
rule is_cat_obj_empty_terminal.cat_oet_obj_terminal[
OF is_cat_obj_empty_initial.is_cat_obj_empty_terminal_op[
OF is_cat_obj_empty_initial_axioms
],
unfolded cat_op_simps
]
)
lemma (in category) cat_is_cat_obj_empty_terminal_obj_terminal_iff:
"(ntcf_0 ℭ : z <⇩C⇩F⇩.⇩1 0⇩C⇩F : 0⇩C ↦↦⇩C⇘α⇙ ℭ) ⟷ obj_terminal ℭ z"
using
cat_obj_terminal_is_cat_obj_empty_terminal
is_cat_obj_empty_terminal.cat_oet_obj_terminal
by auto
lemma (in category) cat_is_cat_obj_empty_initial_obj_initial_iff:
"(ntcf_0 ℭ : 0⇩C⇩F >⇩C⇩F⇩.⇩0 z : 0⇩C ↦↦⇩C⇘α⇙ ℭ) ⟷ obj_initial ℭ z"
using
cat_obj_initial_is_cat_obj_empty_initial
is_cat_obj_empty_initial.cat_oei_obj_initial
by auto
subsection‹Initial cone and terminal cocone›
subsubsection‹Definitions and elementary properties›
definition ntcf_initial :: "V ⇒ V ⇒ V"
where "ntcf_initial ℭ z =
[
(λb∈⇩∘ℭ⦇Obj⦈. THE f. f : z ↦⇘ℭ⇙ b),
cf_const ℭ ℭ z,
cf_id ℭ,
ℭ,
ℭ
]⇩∘"
definition ntcf_terminal :: "V ⇒ V ⇒ V"
where "ntcf_terminal ℭ z =
[
(λb∈⇩∘ℭ⦇Obj⦈. THE f. f : b ↦⇘ℭ⇙ z),
cf_id ℭ,
cf_const ℭ ℭ z,
ℭ,
ℭ
]⇩∘"
text‹Components.›
lemma ntcf_initial_components:
shows "ntcf_initial ℭ z⦇NTMap⦈ = (λc∈⇩∘ℭ⦇Obj⦈. THE f. f : z ↦⇘ℭ⇙ c)"
and "ntcf_initial ℭ z⦇NTDom⦈ = cf_const ℭ ℭ z"
and "ntcf_initial ℭ z⦇NTCod⦈ = cf_id ℭ"
and "ntcf_initial ℭ z⦇NTDGDom⦈ = ℭ"
and "ntcf_initial ℭ z⦇NTDGCod⦈ = ℭ"
unfolding ntcf_initial_def nt_field_simps
by (simp_all add: nat_omega_simps)
lemmas [cat_lim_cs_simps] = ntcf_initial_components(2-5)
lemma ntcf_terminal_components:
shows "ntcf_terminal ℭ z⦇NTMap⦈ = (λc∈⇩∘ℭ⦇Obj⦈. THE f. f : c ↦⇘ℭ⇙ z)"
and "ntcf_terminal ℭ z⦇NTDom⦈ = cf_id ℭ"
and "ntcf_terminal ℭ z⦇NTCod⦈ = cf_const ℭ ℭ z"
and "ntcf_terminal ℭ z⦇NTDGDom⦈ = ℭ"
and "ntcf_terminal ℭ z⦇NTDGCod⦈ = ℭ"
unfolding ntcf_terminal_def nt_field_simps
by (simp_all add: nat_omega_simps)
lemmas [cat_lim_cs_simps] = ntcf_terminal_components(2-5)
text‹Duality.›
lemma ntcf_initial_op[cat_op_simps]:
"op_ntcf (ntcf_initial ℭ z) = ntcf_terminal (op_cat ℭ) z"
unfolding
ntcf_initial_def ntcf_terminal_def op_ntcf_def
nt_field_simps cat_op_simps
by (auto simp: nat_omega_simps cat_op_simps)
lemma ntcf_cone_terminal_op[cat_op_simps]:
"op_ntcf (ntcf_terminal ℭ z) = ntcf_initial (op_cat ℭ) z"
unfolding
ntcf_initial_def ntcf_terminal_def op_ntcf_def
nt_field_simps cat_op_simps
by (auto simp: nat_omega_simps cat_op_simps)
subsubsection‹Natural transformation map›
mk_VLambda ntcf_initial_components(1)
|vsv ntcf_initial_vsv[cat_lim_cs_intros]|
|vdomain ntcf_initial_vdomain[cat_lim_cs_simps]|
|app ntcf_initial_app|
mk_VLambda ntcf_terminal_components(1)
|vsv ntcf_terminal_vsv[cat_lim_cs_intros]|
|vdomain ntcf_terminal_vdomain[cat_lim_cs_simps]|
|app ntcf_terminal_app|
lemma (in category)
assumes "obj_initial ℭ z" and "c ∈⇩∘ ℭ⦇Obj⦈"
shows ntcf_initial_NTMap_app_is_arr:
"ntcf_initial ℭ z⦇NTMap⦈⦇c⦈ : z ↦⇘ℭ⇙ c"
and ntcf_initial_NTMap_app_unique:
"⋀f'. f' : z ↦⇘ℭ⇙ c ⟹ f' = ntcf_initial ℭ z⦇NTMap⦈⦇c⦈"
proof-
from obj_initialD(2)[OF assms(1,2)] obtain f
where f: "f : z ↦⇘ℭ⇙ c"
and f_unique: "f' : z ↦⇘ℭ⇙ c ⟹ f' = f"
for f'
by auto
show is_arr: "ntcf_initial ℭ z⦇NTMap⦈⦇c⦈ : z ↦⇘ℭ⇙ c"
proof(cs_concl_step ntcf_initial_app, rule assms(2), rule theI)
fix f' assume "f' : z ↦⇘ℭ⇙ c"
from f_unique[OF this] show "f' = f".
qed (rule f)
fix f' assume "f' : z ↦⇘ℭ⇙ c"
from f_unique[OF this, folded f_unique[OF is_arr]]
show "f' = ntcf_initial ℭ z⦇NTMap⦈⦇c⦈".
qed
lemma (in category) ntcf_initial_NTMap_app_is_arr'[cat_lim_cs_intros]:
assumes "obj_initial ℭ z"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "ℭ' = ℭ"
and "z' = z"
and "c' = c"
shows "ntcf_initial ℭ z⦇NTMap⦈⦇c⦈ : z' ↦⇘ℭ'⇙ c'"
using assms(1,2)
unfolding assms(3-5)
by (rule ntcf_initial_NTMap_app_is_arr)
lemma (in category)
assumes "obj_terminal ℭ z" and "c ∈⇩∘ ℭ⦇Obj⦈"
shows ntcf_terminal_NTMap_app_is_arr:
"ntcf_terminal ℭ z⦇NTMap⦈⦇c⦈ : c ↦⇘ℭ⇙ z"
and ntcf_terminal_NTMap_app_unique:
"⋀f'. f' : c ↦⇘ℭ⇙ z ⟹ f' = ntcf_terminal ℭ z⦇NTMap⦈⦇c⦈"
proof-
from obj_terminalD(2)[OF assms(1,2)] obtain f
where f: "f : c ↦⇘ℭ⇙ z"
and f_unique: "f' : c ↦⇘ℭ⇙ z ⟹ f' = f"
for f'
by auto
show is_arr: "ntcf_terminal ℭ z⦇NTMap⦈⦇c⦈ : c ↦⇘ℭ⇙ z"
proof(cs_concl_step ntcf_terminal_app, rule assms(2), rule theI)
fix f' assume "f' : c ↦⇘ℭ⇙ z"
from f_unique[OF this] show "f' = f".
qed (rule f)
fix f' assume "f' : c ↦⇘ℭ⇙ z"
from f_unique[OF this, folded f_unique[OF is_arr]]
show "f' = ntcf_terminal ℭ z⦇NTMap⦈⦇c⦈".
qed
lemma (in category) ntcf_terminal_NTMap_app_is_arr'[cat_lim_cs_intros]:
assumes "obj_terminal ℭ z"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "ℭ' = ℭ"
and "z' = z"
and "c' = c"
shows "ntcf_terminal ℭ z⦇NTMap⦈⦇c⦈ : c' ↦⇘ℭ'⇙ z'"
using assms(1,2)
unfolding assms(3-5)
by (rule ntcf_terminal_NTMap_app_is_arr)
subsection‹
Initial and terminal objects as limits/colimits of the identity functor
›
subsubsection‹Definition and elementary properties›
text‹
See
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/initial+object}
}, \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/terminal+object}
} and Chapter X-1 in \<^cite>‹"mac_lane_categories_2010"›.
›
locale is_cat_obj_id_initial = is_cat_limit α ℭ ℭ ‹cf_id ℭ› z ℨ for α ℭ z ℨ
syntax "_is_cat_obj_id_initial" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ <⇩C⇩F⇩.⇩0 id⇩C :/ ↦↦⇩Cı _)› [51, 51, 51] 51)
syntax_consts "_is_cat_obj_id_initial" ⇌ is_cat_obj_id_initial
translations "ℨ : z <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ ℭ" ⇌
"CONST is_cat_obj_id_initial α ℭ z ℨ"
locale is_cat_obj_id_terminal = is_cat_colimit α ℭ ℭ ‹cf_id ℭ› z ℨ for α ℭ z ℨ
syntax "_is_cat_obj_id_terminal" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ id⇩C >⇩C⇩F⇩.⇩1 _ :/ ↦↦⇩Cı _)› [51, 51, 51] 51)
syntax_consts "_is_cat_obj_id_terminal" ⇌ is_cat_obj_id_terminal
translations "ℨ : id⇩C >⇩C⇩F⇩.⇩1 z : ↦↦⇩C⇘α⇙ ℭ" ⇌
"CONST is_cat_obj_id_terminal α ℭ z ℨ"
text‹Rules.›
lemma (in is_cat_obj_id_initial)
is_cat_obj_id_initial_axioms'[cat_lim_cs_intros]:
assumes "α' = α" and "z' = z" and "ℭ' = ℭ"
shows "ℨ : z' <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cat_obj_id_initial_axioms)
mk_ide rf is_cat_obj_id_initial_def
|intro is_cat_obj_id_initialI|
|dest is_cat_obj_id_initialD[dest]|
|elim is_cat_obj_id_initialE[elim]|
lemmas [cat_lim_cs_intros] = is_cat_obj_id_initialD
lemma (in is_cat_obj_id_terminal)
is_cat_obj_id_terminal_axioms'[cat_lim_cs_intros]:
assumes "α' = α" and "z' = z" and "ℭ' = ℭ"
shows "ℨ : id⇩C >⇩C⇩F⇩.⇩1 z' : ↦↦⇩C⇘α'⇙ ℭ'"
unfolding assms by (rule is_cat_obj_id_terminal_axioms)
mk_ide rf is_cat_obj_id_terminal_def
|intro is_cat_obj_id_terminalI|
|dest is_cat_obj_id_terminalD[dest]|
|elim is_cat_obj_id_terminalE[elim]|
lemmas [cat_lim_cs_intros] = is_cat_obj_id_terminalD
text‹Duality.›
lemma (in is_cat_obj_id_initial) is_cat_obj_id_terminal_op:
"op_ntcf ℨ : id⇩C >⇩C⇩F⇩.⇩1 z : ↦↦⇩C⇘α⇙ op_cat ℭ"
by (intro is_cat_obj_id_terminalI)
(cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
lemma (in is_cat_obj_id_initial) is_cat_obj_id_terminal_op'[cat_op_intros]:
assumes "ℭ' = op_cat ℭ"
shows "op_ntcf ℨ : id⇩C >⇩C⇩F⇩.⇩1 z : ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cat_obj_id_terminal_op)
lemmas [cat_op_intros] = is_cat_obj_id_initial.is_cat_obj_id_terminal_op'
lemma (in is_cat_obj_id_terminal) is_cat_obj_id_initial_op:
"op_ntcf ℨ : z <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ op_cat ℭ"
by (intro is_cat_obj_id_initialI)
(cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
lemma (in is_cat_obj_id_terminal) is_cat_obj_id_initial_op'[cat_op_intros]:
assumes "ℭ' = op_cat ℭ"
shows "op_ntcf ℨ : z <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ ℭ'"
unfolding assms by (rule is_cat_obj_id_initial_op)
lemmas [cat_op_intros] = is_cat_obj_id_terminal.is_cat_obj_id_initial_op'
subsubsection‹
Initial and terminal objects as limits/colimits are initial and terminal objects
›
lemma (in category) cat_obj_initial_is_cat_obj_id_initial:
assumes "obj_initial ℭ z"
shows "ntcf_initial ℭ z : z <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_cat_obj_id_initialI is_cat_limitI)
from assms have z: "z ∈⇩∘ ℭ⦇Obj⦈" by auto
note obj_initialD = obj_initialD[OF assms]
show "ntcf_initial ℭ z : z <⇩C⇩F⇩.⇩c⇩o⇩n⇩e cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
proof(intro is_cat_coneI is_ntcfI', unfold cat_lim_cs_simps)
show "vfsequence (ntcf_initial ℭ z)"
unfolding ntcf_initial_def by auto
show "vcard (ntcf_initial ℭ z) = 5⇩ℕ"
unfolding ntcf_initial_def by (simp add: nat_omega_simps)
show "ntcf_initial ℭ z⦇NTMap⦈⦇a⦈ :
cf_const ℭ ℭ z⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙ cf_id ℭ⦇ObjMap⦈⦇a⦈"
if "a ∈⇩∘ ℭ⦇Obj⦈" for a
using that assms(1)
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_lim_cs_intros
)
show
"ntcf_initial ℭ z⦇NTMap⦈⦇b⦈ ∘⇩A⇘ℭ⇙ cf_const ℭ ℭ z⦇ArrMap⦈⦇f⦈ =
cf_id ℭ⦇ArrMap⦈⦇f⦈ ∘⇩A⇘ℭ⇙ ntcf_initial ℭ z⦇NTMap⦈⦇a⦈"
if "f : a ↦⇘ℭ⇙ b" for a b f
proof-
from that assms(1) have
"f ∘⇩A⇘ℭ⇙ ntcf_initial ℭ z⦇NTMap⦈⦇a⦈ : z ↦⇘ℭ⇙ b"
by (cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros)
note [cat_cs_simps] = ntcf_initial_NTMap_app_unique[
OF assms(1) cat_is_arrD(3)[OF that] this
]
from that assms(1) show ?thesis
by
(
cs_concl
cs_simp: cat_cs_simps cs_intro: cat_cs_intros cat_lim_cs_intros
)
qed
qed (use z in ‹cs_concl cs_intro: cat_cs_intros cat_lim_cs_intros›)+
then interpret i: is_cat_cone α z ℭ ℭ ‹cf_id ℭ› ‹ntcf_initial ℭ z› .
fix u r assume "u : r <⇩C⇩F⇩.⇩c⇩o⇩n⇩e cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
then interpret u: is_cat_cone α r ℭ ℭ ‹cf_id ℭ› u .
from obj_initialD(2)[OF u.cat_cone_obj] obtain f
where f: "f : z ↦⇘ℭ⇙ r" and f_unique: "f' : z ↦⇘ℭ⇙ r ⟹ f' = f" for f'
by auto
note u.cat_cone_Comp_commute[cat_cs_simps del]
from u.ntcf_Comp_commute[OF f] f have "u⦇NTMap⦈⦇r⦈ = f ∘⇩A⇘ℭ⇙ u⦇NTMap⦈⦇z⦈"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "∃!f'.
f' : r ↦⇘ℭ⇙ z ∧
u = ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ f'"
proof(intro ex1I conjI; (elim conjE)?)
from f show "u⦇NTMap⦈⦇z⦈ : r ↦⇘ℭ⇙ z"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "u = ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ (u⦇NTMap⦈⦇z⦈)"
proof(rule ntcf_eqI, rule u.is_ntcf_axioms)
show "ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ (u⦇NTMap⦈⦇z⦈) :
cf_const ℭ ℭ r ↦⇩C⇩F cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from z have dom_rhs:
"𝒟⇩∘ ((ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ (u⦇NTMap⦈⦇z⦈))⦇NTMap⦈) =
ℭ⦇Obj⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
show "u⦇NTMap⦈ =
(ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ (u⦇NTMap⦈⦇z⦈))⦇NTMap⦈"
proof(rule vsv_eqI, unfold dom_rhs u.ntcf_NTMap_vdomain)
fix c assume prems: "c ∈⇩∘ ℭ⦇Obj⦈"
then have ic: "ntcf_initial ℭ z⦇NTMap⦈⦇c⦈ : z ↦⇘ℭ⇙ c"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from u.ntcf_Comp_commute[OF ic] ic have [cat_cs_simps]:
"ntcf_initial ℭ z⦇NTMap⦈⦇c⦈ ∘⇩A⇘ℭ⇙ u⦇NTMap⦈⦇z⦈ = u⦇NTMap⦈⦇c⦈"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros) simp
from prems z show "u⦇NTMap⦈⦇c⦈ =
(ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ (u⦇NTMap⦈⦇z⦈))⦇NTMap⦈⦇c⦈"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed (auto intro: cat_cs_intros)
qed simp_all
fix f' assume prems:
"f' : r ↦⇘ℭ⇙ z"
"u = ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ f'"
from z have "ntcf_initial ℭ z⦇NTMap⦈⦇z⦈ : z ↦⇘ℭ⇙ z"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
note [cat_cs_simps] = cat_obj_initial_CId[OF assms this, symmetric]
from prems(2) have
"u⦇NTMap⦈⦇z⦈ = (ntcf_initial ℭ z ∙⇩N⇩T⇩C⇩F ntcf_const ℭ ℭ f')⦇NTMap⦈⦇z⦈"
by simp
from this prems(1) show "f' = u⦇NTMap⦈⦇z⦈"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros) simp
qed
qed
lemma (in category) cat_obj_terminal_is_cat_obj_id_terminal:
assumes "obj_terminal ℭ z"
shows "ntcf_terminal ℭ z : id⇩C >⇩C⇩F⇩.⇩1 z : ↦↦⇩C⇘α⇙ ℭ"
by
(
rule is_cat_obj_id_initial.is_cat_obj_id_terminal_op
[
OF category.cat_obj_initial_is_cat_obj_id_initial[
OF category_op op_cat_obj_initial[THEN iffD2, OF assms(1)]
],
unfolded cat_op_simps
]
)
lemma cat_cone_CId_obj_initial:
assumes "ℨ : z <⇩C⇩F⇩.⇩c⇩o⇩n⇩e cf_id ℭ : ℭ ↦↦⇩C⇘α⇙ ℭ" and "ℨ⦇NTMap⦈⦇z⦈ = ℭ⦇CId⦈⦇z⦈"
shows "obj_initial ℭ z"
proof(intro obj_initialI)
interpret ℨ: is_cat_cone α z ℭ ℭ ‹cf_id ℭ› ℨ by (rule assms(1))
show "z ∈⇩∘ ℭ⦇Obj⦈" by (cs_concl cs_intro: cat_cs_intros)
fix c assume prems: "c ∈⇩∘ ℭ⦇Obj⦈"
show "∃!f. f : z ↦⇘ℭ⇙ c"
proof(intro ex1I)
from prems show ℨc: "ℨ⦇NTMap⦈⦇c⦈ : z ↦⇘ℭ⇙ c"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
fix f assume prems': "f : z ↦⇘ℭ⇙ c"
from ℨ.ntcf_Comp_commute[OF prems'] prems' ℨc show "f = ℨ⦇NTMap⦈⦇c⦈"
by (cs_prems cs_simp: cat_cs_simps assms(2) cs_intro: cat_cs_intros) simp
qed
qed
lemma cat_cocone_CId_obj_terminal:
assumes "ℨ : cf_id ℭ >⇩C⇩F⇩.⇩c⇩o⇩c⇩o⇩n⇩e z : ℭ ↦↦⇩C⇘α⇙ ℭ" and "ℨ⦇NTMap⦈⦇z⦈ = ℭ⦇CId⦈⦇z⦈"
shows "obj_terminal ℭ z"
proof-
interpret ℨ: is_cat_cocone α z ℭ ℭ ‹cf_id ℭ› ℨ by (rule assms(1))
show ?thesis
by
(
rule cat_cone_CId_obj_initial
[
OF ℨ.is_cat_cone_op[unfolded cat_op_simps],
unfolded cat_op_simps,
OF assms(2)
]
)
qed
lemma (in is_cat_obj_id_initial) cat_oii_obj_initial: "obj_initial ℭ z"
proof(rule cat_cone_CId_obj_initial, rule is_cat_cone_axioms)
from cat_lim_unique_cone'[OF is_cat_cone_axioms] obtain f
where f: "f : z ↦⇘ℭ⇙ z"
and ℨ'j: "⋀j. j ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℨ⦇NTMap⦈⦇j⦈ = ℨ⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f"
and f_unique:
"⟦
f' : z ↦⇘ℭ⇙ z;
⋀j. j ∈⇩∘ ℭ⦇Obj⦈ ⟹ ℨ⦇NTMap⦈⦇j⦈ = ℨ⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ f'
⟧ ⟹ f' = f"
for f'
by metis
have CId_z: "ℭ⦇CId⦈⦇z⦈ : z ↦⇘ℭ⇙ z"
by (cs_concl cs_intro: cat_cs_intros)
have "ℨ⦇NTMap⦈⦇j⦈ = ℨ⦇NTMap⦈⦇j⦈ ∘⇩A⇘ℭ⇙ ℭ⦇CId⦈⦇z⦈" if "j ∈⇩∘ ℭ⦇Obj⦈" for j
using that by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
from f_unique[OF CId_z this] have CId_f: "ℭ⦇CId⦈⦇z⦈ = f" .
have ℨz: "ℨ⦇NTMap⦈⦇z⦈ : z ↦⇘ℭ⇙ z"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
have "ℨ⦇NTMap⦈⦇c⦈ = ℨ⦇NTMap⦈⦇c⦈ ∘⇩A⇘ℭ⇙ ℨ⦇NTMap⦈⦇z⦈" if "c ∈⇩∘ ℭ⦇Obj⦈" for c
proof-
from that have ℨc: "ℨ⦇NTMap⦈⦇c⦈ : z ↦⇘ℭ⇙ c"
by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
note cat_cone_Comp_commute[cat_cs_simps del]
from ntcf_Comp_commute[OF ℨc] ℨc show
"ℨ⦇NTMap⦈⦇c⦈ = ℨ⦇NTMap⦈⦇c⦈ ∘⇩A⇘ℭ⇙ ℨ⦇NTMap⦈⦇z⦈"
by (cs_prems cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed
from f_unique[OF ℨz this] have "ℨ⦇NTMap⦈⦇z⦈ = f" .
with CId_f show "ℨ⦇NTMap⦈⦇z⦈ = ℭ⦇CId⦈⦇z⦈" by simp
qed
lemma (in is_cat_obj_id_terminal) cat_oit_obj_terminal: "obj_terminal ℭ z"
by
(
rule is_cat_obj_id_initial.cat_oii_obj_initial[
OF is_cat_obj_id_initial_op, unfolded cat_op_simps
]
)
lemma (in category) cat_is_cat_obj_id_initial_obj_initial_iff:
"(ntcf_initial ℭ z : z <⇩C⇩F⇩.⇩0 id⇩C : ↦↦⇩C⇘α⇙ ℭ) ⟷ obj_initial ℭ z"
using
cat_obj_initial_is_cat_obj_id_initial
is_cat_obj_id_initial.cat_oii_obj_initial
by auto
lemma (in category) cat_is_cat_obj_id_terminal_obj_terminal_iff:
"(ntcf_terminal ℭ z : id⇩C >⇩C⇩F⇩.⇩1 z : ↦↦⇩C⇘α⇙ ℭ) ⟷ obj_terminal ℭ z"
using
cat_obj_terminal_is_cat_obj_id_terminal
is_cat_obj_id_terminal.cat_oit_obj_terminal
by auto
text‹\newpage›
end