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