Theory Initial
section ‹Empty Set and Initial Objects›
theory Initial
imports Coproduct
begin
text ‹The axiomatization below corresponds to Axiom 8 (Empty Set) in Halvorson.›
axiomatization
initial_func :: "cset ⇒ cfunc" ("α⇘_⇙" 100) and
emptyset :: "cset" ("∅")
where
initial_func_type[type_rule]: "initial_func X : ∅ → X" and
initial_func_unique: "h : ∅ → X ⟹ h = initial_func X" and
emptyset_is_empty: "¬(x ∈⇩c ∅)"
definition initial_object :: "cset ⇒ bool" where
"initial_object(X) ⟷ (∀ Y. ∃! f. f : X → Y)"
lemma emptyset_is_initial:
"initial_object(∅)"
using initial_func_type initial_func_unique initial_object_def by blast
lemma initial_iso_empty:
assumes "initial_object(X)"
shows "X ≅ ∅"
by (metis assms cfunc_type_def comp_type emptyset_is_empty epi_mon_is_iso initial_object_def injective_def injective_imp_monomorphism is_isomorphic_def surjective_def surjective_is_epimorphism)
text ‹The lemma below corresponds to Exercise 2.4.6 in Halvorson.›
lemma coproduct_with_empty:
shows "X ∐ ∅ ≅ X"
proof -
have comp1: "(left_coproj X ∅ ∘⇩c (id X ⨿ α⇘X⇙)) ∘⇩c left_coproj X ∅ = left_coproj X ∅"
proof -
have "(left_coproj X ∅ ∘⇩c (id X ⨿ α⇘X⇙)) ∘⇩c left_coproj X ∅ =
left_coproj X ∅ ∘⇩c (id X ⨿ α⇘X⇙ ∘⇩c left_coproj X ∅)"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = left_coproj X ∅ ∘⇩c id(X)"
by (typecheck_cfuncs, metis left_coproj_cfunc_coprod)
also have "... = left_coproj X ∅"
by (typecheck_cfuncs, metis id_right_unit2)
finally show ?thesis.
qed
have comp2: "(left_coproj X ∅ ∘⇩c (id(X) ⨿ α⇘X⇙)) ∘⇩c right_coproj X ∅ = right_coproj X ∅"
proof -
have "((left_coproj X ∅) ∘⇩c (id(X) ⨿ α⇘X⇙)) ∘⇩c (right_coproj X ∅) =
(left_coproj X ∅) ∘⇩c ((id(X) ⨿ α⇘X⇙) ∘⇩c (right_coproj X ∅))"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (left_coproj X ∅) ∘⇩c α⇘X⇙"
by (typecheck_cfuncs, metis right_coproj_cfunc_coprod)
also have "... = right_coproj X ∅"
by (typecheck_cfuncs, metis initial_func_unique)
finally show ?thesis.
qed
then have fact1: "(left_coproj X ∅)⨿(right_coproj X ∅) ∘⇩c left_coproj X ∅ = left_coproj X ∅"
using left_coproj_cfunc_coprod by (typecheck_cfuncs, blast)
then have fact2: "((left_coproj X ∅)⨿(right_coproj X ∅)) ∘⇩c (right_coproj X ∅) = right_coproj X ∅"
using right_coproj_cfunc_coprod by (typecheck_cfuncs, blast)
then have concl: "(left_coproj X ∅) ∘⇩c (id(X) ⨿ α⇘X⇙) = ((left_coproj X ∅)⨿(right_coproj X ∅))"
using cfunc_coprod_unique comp1 comp2 by (typecheck_cfuncs, blast)
also have "... = id(X∐∅)"
using cfunc_coprod_unique id_left_unit2 by (typecheck_cfuncs, auto)
then have "isomorphism(id(X) ⨿ α⇘X⇙)"
unfolding isomorphism_def
by (intro exI[where x="left_coproj X ∅"], typecheck_cfuncs, simp add: cfunc_type_def concl left_coproj_cfunc_coprod)
then show "X∐∅ ≅ X"
using cfunc_coprod_type id_type initial_func_type is_isomorphic_def by blast
qed
text ‹The lemma below corresponds to Proposition 2.4.7 in Halvorson.›
lemma function_to_empty_is_iso:
assumes "f: X → ∅"
shows "isomorphism(f)"
by (metis assms cfunc_type_def comp_type emptyset_is_empty epi_mon_is_iso injective_def injective_imp_monomorphism surjective_def surjective_is_epimorphism)
lemma empty_prod_X:
"∅ ×⇩c X ≅ ∅"
using cfunc_type_def function_to_empty_is_iso is_isomorphic_def left_cart_proj_type by blast
lemma X_prod_empty:
"X ×⇩c ∅ ≅ ∅"
using cfunc_type_def function_to_empty_is_iso is_isomorphic_def right_cart_proj_type by blast
text ‹The lemma below corresponds to Proposition 2.4.8 in Halvorson.›
lemma no_el_iff_iso_empty:
"is_empty X ⟷ X ≅ ∅"
proof safe
show "X ≅ ∅ ⟹ is_empty X"
by (meson is_empty_def comp_type emptyset_is_empty is_isomorphic_def)
next
assume "is_empty X"
obtain f where f_type: "f: ∅ → X"
using initial_func_type by blast
have f_inj: "injective(f)"
using cfunc_type_def emptyset_is_empty f_type injective_def by auto
then have f_mono: "monomorphism(f)"
using cfunc_type_def f_type injective_imp_monomorphism by blast
have f_surj: "surjective(f)"
using is_empty_def ‹is_empty X› f_type surjective_def2 by presburger
then have epi_f: "epimorphism(f)"
using surjective_is_epimorphism by blast
then have iso_f: "isomorphism(f)"
using cfunc_type_def epi_mon_is_iso f_mono f_type by blast
then show "X ≅ ∅"
using f_type is_isomorphic_def isomorphic_is_symmetric by blast
qed
lemma initial_maps_mono:
assumes "initial_object(X)"
assumes "f : X → Y"
shows "monomorphism(f)"
by (metis assms cfunc_type_def initial_iso_empty injective_def injective_imp_monomorphism no_el_iff_iso_empty is_empty_def)
lemma iso_empty_initial:
assumes "X ≅ ∅"
shows "initial_object X"
unfolding initial_object_def
by (meson assms comp_type is_isomorphic_def isomorphic_is_symmetric isomorphic_is_transitive no_el_iff_iso_empty is_empty_def one_separator terminal_func_type)
lemma function_to_empty_set_is_iso:
assumes "f: X → Y"
assumes "is_empty Y"
shows "isomorphism f"
by (metis assms cfunc_type_def comp_type epi_mon_is_iso injective_def injective_imp_monomorphism is_empty_def surjective_def surjective_is_epimorphism)
lemma prod_iso_to_empty_right:
assumes "nonempty X"
assumes "X ×⇩c Y ≅ ∅"
shows "is_empty Y"
by (metis emptyset_is_empty is_empty_def cfunc_prod_type epi_is_surj is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric nonempty_def surjective_def2 assms)
lemma prod_iso_to_empty_left:
assumes "nonempty Y"
assumes "X ×⇩c Y ≅ ∅"
shows "is_empty X"
by (meson is_empty_def nonempty_def prod_iso_to_empty_right assms)
lemma empty_subset: "(∅, α⇘X⇙) ⊆⇩c X"
by (metis cfunc_type_def emptyset_is_empty initial_func_type injective_def injective_imp_monomorphism subobject_of_def2)
text ‹The lemma below corresponds to Proposition 2.2.1 in Halvorson.›
lemma one_has_two_subsets:
"card ({(X,m). (X,m) ⊆⇩c 𝟭}//{((X1,m1),(X2,m2)). X1 ≅ X2}) = 2"
proof -
have one_subobject: "(𝟭, id 𝟭) ⊆⇩c 𝟭"
using element_monomorphism id_type subobject_of_def2 by blast
have empty_subobject: "(∅, α⇘𝟭⇙) ⊆⇩c 𝟭"
by (simp add: empty_subset)
have subobject_one_or_empty: "⋀X m. (X,m) ⊆⇩c 𝟭 ⟹ X ≅ 𝟭 ∨ X ≅ ∅"
proof -
fix X m
assume X_m_subobject: "(X, m) ⊆⇩c 𝟭"
obtain χ where χ_pullback: "is_pullback X 𝟭 𝟭 Ω (β⇘X⇙) 𝗍 m χ"
using X_m_subobject characteristic_function_exists subobject_of_def2 by blast
then have χ_true_or_false: "χ = 𝗍 ∨ χ = 𝖿"
unfolding is_pullback_def using true_false_only_truth_values by auto
have true_iso_one: "χ = 𝗍 ⟹ X ≅ 𝟭"
proof -
assume χ_true: "χ = 𝗍"
then have "∃!j. j ∈⇩c X ∧ β⇘X⇙ ∘⇩c j = id⇩c 𝟭 ∧ m ∘⇩c j = id⇩c 𝟭"
using χ_pullback χ_true is_pullback_def by (typecheck_cfuncs, auto)
then show "X ≅ 𝟭"
using single_elem_iso_one
by (metis X_m_subobject subobject_of_def2 terminal_func_comp_elem terminal_func_unique)
qed
have false_iso_one: "χ = 𝖿 ⟹ X ≅ ∅"
proof -
assume χ_false: "χ = 𝖿"
have "∄ x. x ∈⇩c X"
proof clarify
fix x
assume x_in_X: "x ∈⇩c X"
have "𝗍 ∘⇩c β⇘X⇙ = 𝖿 ∘⇩c m"
using χ_false χ_pullback is_pullback_def by auto
then have "𝗍 ∘⇩c (β⇘X⇙ ∘⇩c x) = 𝖿 ∘⇩c (m ∘⇩c x)"
by (smt X_m_subobject comp_associative2 false_func_type subobject_of_def2
terminal_func_type true_func_type x_in_X)
then have "𝗍 = 𝖿"
by (smt X_m_subobject cfunc_type_def comp_type false_func_type id_right_unit id_type
subobject_of_def2 terminal_func_unique true_func_type x_in_X)
then show False
using true_false_distinct by auto
qed
then show "X ≅ ∅"
using is_empty_def ‹∄x. x ∈⇩c X› no_el_iff_iso_empty by blast
qed
show "X ≅ 𝟭 ∨ X ≅ ∅"
using χ_true_or_false false_iso_one true_iso_one by blast
qed
have classes_distinct: "{(X, m). X ≅ ∅} ≠ {(X, m). X ≅ 𝟭}"
by (metis case_prod_eta curry_case_prod emptyset_is_empty id_isomorphism id_type is_isomorphic_def mem_Collect_eq)
have "{(X, m). (X, m) ⊆⇩c 𝟭} // {((X1, m1), (X2, m2)). X1 ≅ X2} = {{(X, m). X ≅ ∅}, {(X, m). X ≅ 𝟭}}"
proof
show "{(X, m). (X, m) ⊆⇩c 𝟭} // {((X1, m1), (X2, m2)). X1 ≅ X2} ⊆ {{(X, m). X ≅ ∅}, {(X, m). X ≅ 𝟭}}"
unfolding quotient_def by (auto, insert isomorphic_is_symmetric isomorphic_is_transitive subobject_one_or_empty, blast+)
next
show "{{(X, m). X ≅ ∅}, {(X, m). X ≅ 𝟭}} ⊆ {(X, m). (X, m) ⊆⇩c 𝟭} // {((X1, m1), X2, m2). X1 ≅ X2}"
unfolding quotient_def by (insert empty_subobject one_subobject, auto simp add: isomorphic_is_symmetric)
qed
then show "card ({(X, m). (X, m) ⊆⇩c 𝟭} // {((X, m1), (Y, m2)). X ≅ Y}) = 2"
by (simp add: classes_distinct)
qed
lemma coprod_with_init_obj1:
assumes "initial_object Y"
shows "X ∐ Y ≅ X"
by (meson assms coprod_pres_iso coproduct_with_empty initial_iso_empty isomorphic_is_reflexive isomorphic_is_transitive)
lemma coprod_with_init_obj2:
assumes "initial_object X"
shows "X ∐ Y ≅ Y"
using assms coprod_with_init_obj1 coproduct_commutes isomorphic_is_transitive by blast
lemma prod_with_term_obj1:
assumes "terminal_object(X)"
shows "X ×⇩c Y ≅ Y"
by (meson assms isomorphic_is_reflexive isomorphic_is_transitive one_terminal_object one_x_A_iso_A prod_pres_iso terminal_objects_isomorphic)
lemma prod_with_term_obj2:
assumes "terminal_object(Y)"
shows "X ×⇩c Y ≅ X"
by (meson assms isomorphic_is_transitive prod_with_term_obj1 product_commutes)
end