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 ⨿ α⇘Xc 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  β⇘Xc j = idc 𝟭  m c j = idc 𝟭"
        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 (β⇘Xc 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