Theory CZH_ECAT_Order
section‹Orders›
theory CZH_ECAT_Order
imports
CZH_ECAT_Functor
begin
subsection‹Background›
named_theorems cat_order_cs_simps
named_theorems cat_order_cs_intros
subsection‹Preorder category›
text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›
locale cat_preorder = category α ℭ for α ℭ +
assumes cat_peo:
"⟦ a ∈⇩∘ ℭ⦇Obj⦈; b ∈⇩∘ ℭ⦇Obj⦈ ⟧ ⟹
(∃f. Hom ℭ a b = set {f}) ∨ (Hom ℭ a b = 0)"
text‹Rules.›
lemma (in cat_preorder) cat_preorder_axioms'[cat_order_cs_intros]:
assumes "α' = α"
shows "cat_preorder α' ℭ"
unfolding assms by (rule cat_preorder_axioms)
mk_ide rf cat_preorder_def[unfolded cat_preorder_axioms_def]
|intro cat_preorderI|
|dest cat_preorderD[dest]|
|elim cat_preorderE[elim]|
lemmas [cat_order_cs_intros] = cat_preorderD(1)
text‹Elementary properties.›
lemma (in cat_preorder) cat_peo_HomE:
assumes "a ∈⇩∘ ℭ⦇Obj⦈" and "b ∈⇩∘ ℭ⦇Obj⦈"
obtains f where ‹Hom ℭ a b = set {f}› | ‹Hom ℭ a b = 0›
using cat_peo[OF assms] by auto
lemma (in cat_preorder) cat_peo_is_thin_category:
assumes "f : a ↦⇘ℭ⇙ b" and "g : a ↦⇘ℭ⇙ b"
shows "f = g"
proof-
note f = cat_is_arrD[OF assms(1)]
from assms have "Hom ℭ a b ≠ 0" by (metis HomI eq0_iff)
with cat_peo_HomE[OF f(2,3)] obtain h where "Hom ℭ a b = set {h}" by auto
moreover from assms have "f ∈⇩∘ Hom ℭ a b" and "g ∈⇩∘ Hom ℭ a b" by auto
ultimately have "h = f" and "h = g" by auto
then show ?thesis by auto
qed
subsection‹Order relation›
subsubsection‹Definition and elementary properties›
definition is_le :: "V ⇒ V ⇒ V ⇒ bool" (infix ‹≤⇩Oı› 50)
where "a ≤⇩O⇘ℭ⇙ b ⟷ Hom ℭ a b ≠ 0"
text‹Rules.›
mk_ide is_le_def
|intro is_leI|
|dest is_leD[dest]|
|elim is_leE[elim]|
text‹Elementary properties.›
lemma (in cat_preorder) cat_peo_is_le[cat_order_cs_intros]:
assumes "f : a ↦⇘ℭ⇙ b"
shows "a ≤⇩O⇘ℭ⇙ b"
using assms by (force intro: is_leI)
lemmas [cat_order_cs_intros] = cat_preorder.cat_peo_is_le
lemma (in cat_preorder) cat_peo_is_le_ex1:
assumes "a ≤⇩O⇘ℭ⇙ b" and "a ∈⇩∘ ℭ⦇Obj⦈" and "b ∈⇩∘ ℭ⦇Obj⦈"
shows "∃!f. f : a ↦⇘ℭ⇙ b"
proof-
from assms have "Hom ℭ a b ≠ 0" by auto
with assms cat_peo obtain f where Hom_ab: "Hom ℭ a b = set {f}" by meson
show "∃!f. f : a ↦⇘ℭ⇙ b"
proof(intro ex1I)
from Hom_ab show "f : a ↦⇘ℭ⇙ b" by auto
fix g assume "g : a ↦⇘ℭ⇙ b"
with Hom_ab show "g = f" by auto
qed
qed
lemma (in cat_preorder) cat_peo_is_le_ex[elim]:
assumes "a ≤⇩O⇘ℭ⇙ b" and "a ∈⇩∘ ℭ⦇Obj⦈" and "b ∈⇩∘ ℭ⦇Obj⦈"
obtains f where "f : a ↦⇘ℭ⇙ b"
using cat_peo_is_le_ex1[OF assms] that by clarsimp
subsubsection‹Order relation on a preorder category is a preorder›
lemma (in cat_preorder) is_le_refl:
assumes "a ∈⇩∘ ℭ⦇Obj⦈"
shows "a ≤⇩O⇘ℭ⇙ a"
proof(intro is_leI)
from assms have "ℭ⦇CId⦈⦇a⦈ ∈⇩∘ Hom ℭ a a"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
then show "Hom ℭ a a ≠ 0" by force
qed
lemma (in cat_preorder) is_le_trans:
assumes "a ∈⇩∘ ℭ⦇Obj⦈"
and "b ∈⇩∘ ℭ⦇Obj⦈"
and "c ∈⇩∘ ℭ⦇Obj⦈"
and "a ≤⇩O⇘ℭ⇙ b"
and "b ≤⇩O⇘ℭ⇙ c"
shows "a ≤⇩O⇘ℭ⇙ c"
proof(intro is_leI)
from assms obtain f where f: "f : a ↦⇘ℭ⇙ b" by auto
from assms obtain g where g: "g : b ↦⇘ℭ⇙ c" by auto
from f g have "g ∘⇩A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c"
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
then show "Hom ℭ a c ≠ 0" by force
qed
subsection‹Partial order category›
text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›
locale cat_partial_order = cat_preorder α ℭ for α ℭ +
assumes cat_po: "⟦ a ∈⇩∘ ℭ⦇Obj⦈; b ∈⇩∘ ℭ⦇Obj⦈; a ≤⇩O⇘ℭ⇙ b; b ≤⇩O⇘ℭ⇙ a ⟧ ⟹ a = b"
text‹Rules.›
lemma (in cat_partial_order) cat_partial_order_axioms'[cat_order_cs_intros]:
assumes "α' = α"
shows "cat_partial_order α' ℭ"
unfolding assms by (rule cat_partial_order_axioms)
mk_ide rf cat_partial_order_def[unfolded cat_partial_order_axioms_def]
|intro cat_partial_orderI|
|dest cat_partial_orderD[dest]|
|elim cat_partial_orderE[elim]|
lemmas [cat_order_cs_intros] = cat_partial_orderD(1)
subsection‹Linear order category›
text‹See Chapter I-2 in \<^cite>‹"mac_lane_categories_2010"›.›
locale cat_linear_order = cat_partial_order α ℭ for α ℭ +
assumes cat_lo: "⟦ a ∈⇩∘ ℭ⦇Obj⦈; b ∈⇩∘ ℭ⦇Obj⦈ ⟧ ⟹ a ≤⇩O⇘ℭ⇙ b ∨ b ≤⇩O⇘ℭ⇙ a"
text‹Rules.›
lemma (in cat_linear_order) cat_linear_order_axioms'[cat_order_cs_intros]:
assumes "α' = α"
shows "cat_linear_order α' ℭ"
unfolding assms by (rule cat_linear_order_axioms)
mk_ide rf cat_linear_order_def[unfolded cat_linear_order_axioms_def]
|intro cat_linear_orderI|
|dest cat_linear_orderD[dest]|
|elim cat_linear_orderE[elim]|
lemmas [cat_order_cs_intros] = cat_linear_orderD(1)
subsection‹Preorder functor›
subsubsection‹Definition and elementary properties›
text‹
See \<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/monotone+function}
}.
›
locale is_preorder_functor =
is_functor α 𝔄 𝔅 𝔉 + HomDom: cat_preorder α 𝔄 + HomCod: cat_preorder α 𝔅
for α 𝔄 𝔅 𝔉
syntax "_is_preorder_functor" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
(‹(_ :/ _ ≤⇩C⇩.⇩P⇩E⇩Oı _)› [51, 51, 51] 51)
translations "𝔉 : 𝔄 ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 𝔅" ⇌ "CONST is_preorder_functor α 𝔄 𝔅 𝔉"
text‹Rules.›
lemma (in is_preorder_functor) is_preorder_functor_axioms'[cat_order_cs_intros]:
assumes "α' = α" and "𝔄' = 𝔄" and "𝔅' = 𝔅"
shows "𝔉 : 𝔄' ≤⇩C⇩.⇩P⇩E⇩O⇘α'⇙ 𝔅'"
unfolding assms by (rule is_preorder_functor_axioms)
mk_ide rf is_preorder_functor_def
|intro is_preorder_functorI|
|dest is_preorder_functorD[dest]|
|elim is_preorder_functorE[elim]|
lemmas [cat_order_cs_intros] = is_preorder_functorD
subsubsection‹A preorder functor is a faithful functor›
sublocale is_preorder_functor ⊆ is_ft_functor
proof(intro is_ft_functorI')
fix a b assume "a ∈⇩∘ 𝔄⦇Obj⦈" "b ∈⇩∘ 𝔄⦇Obj⦈"
show "v11 (𝔉⦇ArrMap⦈ ↾⇧l⇩∘ Hom 𝔄 a b)"
proof
(
intro vsv.vsv_valeq_v11I,
unfold vdomain_vlrestriction cat_cs_simps vintersection_iff;
(elim conjE)?
)
fix g f assume "g : a ↦⇘𝔄⇙ b" "f : a ↦⇘𝔄⇙ b"
then show "g = f" by (auto simp: HomDom.cat_peo_is_thin_category)
qed simp
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
lemmas (in is_preorder_functor) is_preorder_functor_is_ft_functor =
is_ft_functor_axioms
lemmas [cat_order_cs_intros] =
is_preorder_functor.is_preorder_functor_is_ft_functor
subsubsection‹A preorder functor is a monotone function›
lemma (in is_preorder_functor) cat_peo:
assumes "a ∈⇩∘ 𝔄⦇Obj⦈" and "b ∈⇩∘ 𝔄⦇Obj⦈" and "a ≤⇩O⇘𝔄⇙ b"
shows "𝔉⦇ObjMap⦈⦇a⦈ ≤⇩O⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
proof-
from assms obtain f where "f : a ↦⇘𝔄⇙ b" by auto
then have "𝔉⦇ArrMap⦈⦇f⦈ : 𝔉⦇ObjMap⦈⦇a⦈ ↦⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
by (simp add: cf_ArrMap_is_arr)
then show "𝔉⦇ObjMap⦈⦇a⦈ ≤⇩O⇘𝔅⇙ 𝔉⦇ObjMap⦈⦇b⦈"
by (cs_concl cs_shallow cs_intro: cat_order_cs_intros)
qed
subsubsection‹Composition of preorder functors›
lemma cf_comp_is_preorder_functor[cat_order_cs_intros]:
assumes "𝔊 : 𝔅 ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ ℭ" and "𝔉 : 𝔄 ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 𝔅"
shows "𝔊 ∘⇩C⇩F 𝔉 : 𝔄 ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ ℭ"
proof-
interpret 𝔊: is_preorder_functor α 𝔅 ℭ 𝔊 by (rule assms(1))
interpret 𝔉: is_preorder_functor α 𝔄 𝔅 𝔉 by (rule assms(2))
show ?thesis
by (intro is_preorder_functorI)
(cs_concl cs_intro: cat_cs_intros cat_order_cs_intros)+
qed
lemma (in cat_preorder) cat_peo_cf_is_preorder_functor:
"cf_id ℭ : ℭ ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ ℭ"
by (intro is_preorder_functorI)
(cs_concl cs_intro: cat_cs_intros cat_order_cs_intros)+
lemma (in cat_preorder) cat_peo_cf_is_preorder_functor'[cat_order_cs_intros]:
assumes "𝔄' = ℭ" and "𝔅' = ℭ"
shows "cf_id ℭ : 𝔄' ≤⇩C⇩.⇩P⇩E⇩O⇘α⇙ 𝔅'"
unfolding assms by (rule cat_peo_cf_is_preorder_functor)
lemmas [cat_order_cs_intros] = cat_preorder.cat_peo_cf_is_preorder_functor'
end