Theory Truth
section βΉTruth Values and Characteristic FunctionsβΊ
theory Truth
imports Equalizer
begin
text βΉThe axiomatization below corresponds to Axiom 5 (Truth-Value Object) in Halvorson.βΊ
axiomatization
true_func :: "cfunc" ("π") and
false_func :: "cfunc" ("πΏ") and
truth_value_set :: "cset" ("Ξ©")
where
true_func_type[type_rule]: "π ββ©c Ξ©" and
false_func_type[type_rule]: "πΏ ββ©c Ξ©" and
true_false_distinct: "π β πΏ" and
true_false_only_truth_values: "x ββ©c Ξ© βΉ x = πΏ β¨ x = π" and
characteristic_function_exists:
"m : B β X βΉ monomorphism m βΉ β! Ο. is_pullback B π X Ξ© (Ξ²βBβ) π m Ο"
definition characteristic_func :: "cfunc β cfunc" where
"characteristic_func m =
(THE Ο. monomorphism m βΆ is_pullback (domain m) π (codomain m) Ξ© (Ξ²βdomain mβ) π m Ο)"
lemma characteristic_func_is_pullback:
assumes "m : B β X" "monomorphism m"
shows "is_pullback B π X Ξ© (Ξ²βBβ) π m (characteristic_func m)"
proof -
obtain Ο where chi_is_pullback: "is_pullback B π X Ξ© (Ξ²βBβ) π m Ο"
using assms characteristic_function_exists by blast
have "monomorphism m βΆ is_pullback (domain m) π (codomain m) Ξ© (Ξ²βdomain mβ) π m (characteristic_func m)"
unfolding characteristic_func_def
proof (rule theI', rule ex1I[where a= Ο], clarify)
show "is_pullback (domain m) π (codomain m) Ξ© (Ξ²βdomain mβ) π m Ο"
using assms(1) cfunc_type_def chi_is_pullback by auto
show "βx. monomorphism m βΆ is_pullback (domain m) π (codomain m) Ξ© (Ξ²βdomain mβ) π m x βΉ x = Ο"
using assms cfunc_type_def characteristic_function_exists chi_is_pullback by fastforce
qed
then show "is_pullback B π X Ξ© (Ξ²βBβ) π m (characteristic_func m)"
using assms cfunc_type_def by auto
qed
lemma characteristic_func_type[type_rule]:
assumes "m : B β X" "monomorphism m"
shows "characteristic_func m : X β Ξ©"
proof -
have "is_pullback B π X Ξ© (Ξ²βBβ) π m (characteristic_func m)"
using assms by (rule characteristic_func_is_pullback)
then show "characteristic_func m : X β Ξ©"
unfolding is_pullback_def by auto
qed
lemma characteristic_func_eq:
assumes "m : B β X" "monomorphism m"
shows "characteristic_func m ββ©c m = π ββ©c Ξ²βBβ"
using assms characteristic_func_is_pullback unfolding is_pullback_def by auto
lemma monomorphism_equalizes_char_func:
assumes m_type[type_rule]: "m : B β X" and m_mono[type_rule]: "monomorphism m"
shows "equalizer B m (characteristic_func m) (π ββ©c Ξ²βXβ)"
unfolding equalizer_def
proof (rule exI[where x=X], rule exI[where x=Ξ©], safe)
show "characteristic_func m : X β Ξ©"
by typecheck_cfuncs
show "π ββ©c Ξ²βXβ : X β Ξ©"
by typecheck_cfuncs
show "m : B β X"
by typecheck_cfuncs
have comm: "π ββ©c Ξ²βBβ = characteristic_func m ββ©c m"
using characteristic_func_eq m_mono m_type by auto
then have "Ξ²βBβ = Ξ²βXβ ββ©c m"
using m_type terminal_func_comp by auto
then show "characteristic_func m ββ©c m = (π ββ©c Ξ²βXβ) ββ©c m"
using comm comp_associative2 by (typecheck_cfuncs, auto)
next
show "βh F. h : F β X βΉ characteristic_func m ββ©c h = (π ββ©c Ξ²βXβ) ββ©c h βΉ βk. k : F β B β§ m ββ©c k = h"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) cfunc_type_def characteristic_func_is_pullback comp_associative comp_type is_pullback_def m_mono)
next
show "βF k y. characteristic_func m ββ©c m ββ©c k = (π ββ©c Ξ²βXβ) ββ©c m ββ©c k βΉ k : F β B βΉ y : F β B βΉ m ββ©c y = m ββ©c k βΉ k = y"
by (typecheck_cfuncs, smt m_mono monomorphism_def2)
qed
lemma characteristic_func_true_relative_member:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes characteristic_func_true: "characteristic_func m ββ©c x = π"
shows "x ββXβ (B,m)"
unfolding relative_member_def2 factors_through_def
proof (insert assms, clarify)
have "is_pullback B π X Ξ© (Ξ²βBβ) π m (characteristic_func m)"
by (simp add: assms characteristic_func_is_pullback)
then have "βj. j : π β B β§ Ξ²βBβ ββ©c j = id π β§ m ββ©c j = x"
unfolding is_pullback_def using assms by (metis id_right_unit2 id_type true_func_type)
then show "βj. j : domain x β domain m β§ m ββ©c j = x"
using assms(1,3) cfunc_type_def by auto
qed
lemma characteristic_func_false_not_relative_member:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes characteristic_func_true: "characteristic_func m ββ©c x = πΏ"
shows "Β¬ (x ββXβ (B,m))"
unfolding relative_member_def2 factors_through_def
proof (insert assms, clarify)
fix h
assume x_def: "x = m ββ©c h"
assume "h : domain (m ββ©c h) β domain m"
then have h_type: "h ββ©c B"
using assms(1,3) cfunc_type_def x_def by auto
have "is_pullback B π X Ξ© (Ξ²βBβ) π m (characteristic_func m)"
by (simp add: assms characteristic_func_is_pullback)
then have char_m_true: "characteristic_func m ββ©c m = π ββ©c Ξ²βBβ"
unfolding is_pullback_def by auto
then have "characteristic_func m ββ©c m ββ©c h = πΏ"
using x_def characteristic_func_true by auto
then have "(characteristic_func m ββ©c m) ββ©c h = πΏ"
using assms h_type by (typecheck_cfuncs, simp add: comp_associative2)
then have "(π ββ©c Ξ²βBβ) ββ©c h = πΏ"
using char_m_true by auto
then have "π = πΏ"
by (metis cfunc_type_def comp_associative h_type id_right_unit2 id_type one_unique_element
terminal_func_comp terminal_func_type true_func_type)
then show False
using true_false_distinct by auto
qed
lemma rel_mem_char_func_true:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes "x ββXβ (B,m)"
shows "characteristic_func m ββ©c x = π"
by (meson assms(4) characteristic_func_false_not_relative_member characteristic_func_type comp_type relative_member_def2 true_false_only_truth_values)
lemma not_rel_mem_char_func_false:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes "Β¬ (x ββXβ (B,m))"
shows "characteristic_func m ββ©c x = πΏ"
by (meson assms characteristic_func_true_relative_member characteristic_func_type comp_type true_false_only_truth_values)
text βΉThe lemma below corresponds to Proposition 2.2.2 in Halvorson.βΊ
lemma "card {x. x ββ©c Ξ© Γβ©c Ξ©} = 4"
proof -
have "{x. x ββ©c Ξ© Γβ©c Ξ©} = {β¨π,πβ©, β¨π,πΏβ©, β¨πΏ,πβ©, β¨πΏ,πΏβ©}"
by (auto simp add: cfunc_prod_type true_func_type false_func_type,
smt cfunc_prod_unique comp_type left_cart_proj_type right_cart_proj_type true_false_only_truth_values)
then show "card {x. x ββ©c Ξ© Γβ©c Ξ©} = 4"
using element_pair_eq false_func_type true_false_distinct true_func_type by auto
qed
subsection βΉEquality PredicateβΊ
definition eq_pred :: "cset β cfunc" where
"eq_pred X = (THE Ο. is_pullback X π (X Γβ©c X) Ξ© (Ξ²βXβ) π (diagonal X) Ο)"
lemma eq_pred_pullback: "is_pullback X π (X Γβ©c X) Ξ© (Ξ²βXβ) π (diagonal X) (eq_pred X)"
unfolding eq_pred_def
by (rule the1I2, simp_all add: characteristic_function_exists diag_mono diagonal_type)
lemma eq_pred_type[type_rule]:
"eq_pred X : X Γβ©c X β Ξ©"
using eq_pred_pullback unfolding is_pullback_def by auto
lemma eq_pred_square: "eq_pred X ββ©c diagonal X = π ββ©c Ξ²βXβ"
using eq_pred_pullback unfolding is_pullback_def by auto
lemma eq_pred_iff_eq:
assumes "x : π β X" "y : π β X"
shows "(x = y) = (eq_pred X ββ©c β¨x, yβ© = π)"
proof safe
assume x_eq_y: "x = y"
have "(eq_pred X ββ©c β¨idβ©c X,idβ©c Xβ©) ββ©c y = (π ββ©c Ξ²βXβ) ββ©c y"
using eq_pred_square unfolding diagonal_def by auto
then have "eq_pred X ββ©c β¨y, yβ© = (π ββ©c Ξ²βXβ) ββ©c y"
using assms diagonal_type id_type
by (typecheck_cfuncs, smt cfunc_prod_comp comp_associative2 diagonal_def id_left_unit2)
then show "eq_pred X ββ©c β¨y, yβ© = π"
using assms id_type
by (typecheck_cfuncs, smt comp_associative2 terminal_func_comp terminal_func_type terminal_func_unique id_right_unit2)
next
assume "eq_pred X ββ©c β¨x,yβ© = π"
then have "eq_pred X ββ©c β¨x,yβ© = π ββ©c id π"
using id_right_unit2 true_func_type by auto
then obtain j where j_type: "j : π β X" and "diagonal X ββ©c j = β¨x,yβ©"
using eq_pred_pullback assms unfolding is_pullback_def by (metis cfunc_prod_type id_type)
then have "β¨j,jβ© = β¨x,yβ©"
using diag_on_elements by auto
then show "x = y"
using assms element_pair_eq j_type by auto
qed
lemma eq_pred_iff_eq_conv:
assumes "x : π β X" "y : π β X"
shows "(x β y) = (eq_pred X ββ©c β¨x, yβ© = πΏ)"
proof(safe)
assume "x β y"
then show "eq_pred X ββ©c β¨x,yβ© = πΏ"
using assms eq_pred_iff_eq true_false_only_truth_values by (typecheck_cfuncs, blast)
next
show "eq_pred X ββ©c β¨y,yβ© = πΏ βΉ x = y βΉ False"
by (metis assms(1) eq_pred_iff_eq true_false_distinct)
qed
lemma eq_pred_iff_eq_conv2:
assumes "x : π β X" "y : π β X"
shows "(x β y) = (eq_pred X ββ©c β¨x, yβ© β π)"
using assms eq_pred_iff_eq by presburger
lemma eq_pred_of_monomorphism:
assumes m_type[type_rule]: "m : X β Y" and m_mono: "monomorphism m"
shows "eq_pred Y ββ©c (m Γβ©f m) = eq_pred X"
proof (rule one_separator[where X="X Γβ©c X", where Y=Ξ©])
show "eq_pred Y ββ©c m Γβ©f m : X Γβ©c X β Ξ©"
by typecheck_cfuncs
show "eq_pred X : X Γβ©c X β Ξ©"
by typecheck_cfuncs
next
fix x
assume "x ββ©c X Γβ©c X"
then obtain x1 x2 where x_def: "x = β¨x1, x2β©" and x1_type[type_rule]: "x1 ββ©c X" and x2_type[type_rule]: "x2 ββ©c X"
using cart_prod_decomp by blast
show "(eq_pred Y ββ©c m Γβ©f m) ββ©c x = eq_pred X ββ©c x"
unfolding x_def
proof (cases "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© = π")
assume LHS: "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© = π"
then have "eq_pred Y ββ©c (m Γβ©f m) ββ©c β¨x1,x2β© = π"
by (typecheck_cfuncs, simp add: comp_associative2)
then have "eq_pred Y ββ©c β¨m ββ©c x1, m ββ©c x2β© = π"
by (typecheck_cfuncs, auto simp add: cfunc_cross_prod_comp_cfunc_prod)
then have "m ββ©c x1 = m ββ©c x2"
by (typecheck_cfuncs_prems, simp add: eq_pred_iff_eq)
then have "x1 = x2"
using m_mono m_type monomorphism_def3 x1_type x2_type by blast
then have RHS: "eq_pred X ββ©c β¨x1,x2β© = π"
by (typecheck_cfuncs, insert eq_pred_iff_eq, blast)
show "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© = eq_pred X ββ©c β¨x1,x2β©"
using LHS RHS by auto
next
assume "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© β π"
then have LHS: "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© = πΏ"
by (typecheck_cfuncs, meson true_false_only_truth_values)
then have "eq_pred Y ββ©c (m Γβ©f m) ββ©c β¨x1,x2β© = πΏ"
by (typecheck_cfuncs, simp add: comp_associative2)
then have "eq_pred Y ββ©c β¨m ββ©c x1, m ββ©c x2β© = πΏ"
by (typecheck_cfuncs, auto simp add: cfunc_cross_prod_comp_cfunc_prod)
then have "m ββ©c x1 β m ββ©c x2"
using eq_pred_iff_eq_conv by (typecheck_cfuncs_prems, blast)
then have "x1 β x2"
by auto
then have RHS: "eq_pred X ββ©c β¨x1,x2β© = πΏ"
using eq_pred_iff_eq_conv by (typecheck_cfuncs, blast)
show "(eq_pred Y ββ©c m Γβ©f m) ββ©c β¨x1,x2β© = eq_pred X ββ©c β¨x1,x2β©"
using LHS RHS by auto
qed
qed
lemma :
assumes "x ββ©c X"
shows "eq_pred X ββ©c β¨x ββ©c Ξ²βXβ, id Xβ© ββ©c x = π"
using assms cart_prod_extract_right eq_pred_iff_eq by fastforce
lemma :
assumes "x ββ©c X" "y ββ©c X" "x β y"
shows "eq_pred X ββ©c β¨x ββ©c Ξ²βXβ, id Xβ© ββ©c y = πΏ"
using assms cart_prod_extract_right eq_pred_iff_eq true_false_only_truth_values by (typecheck_cfuncs, fastforce)
subsection βΉProperties of Monomorphisms and EpimorphismsβΊ
text βΉThe lemma below corresponds to Exercise 2.2.3 in Halvorson.βΊ
lemma regmono_is_mono: "regular_monomorphism m βΉ monomorphism m"
using equalizer_is_monomorphism regular_monomorphism_def by blast
text βΉThe lemma below corresponds to Proposition 2.2.4 in Halvorson.βΊ
lemma mono_is_regmono:
shows "monomorphism m βΉ regular_monomorphism m"
unfolding regular_monomorphism_def
by (rule exI[where x="characteristic_func m"],
rule exI[where x="π ββ©c Ξ²βcodomain(m)β"],
typecheck_cfuncs, auto simp add: cfunc_type_def monomorphism_equalizes_char_func)
text βΉThe lemma below corresponds to Proposition 2.2.5 in Halvorson.βΊ
lemma epi_mon_is_iso:
assumes "epimorphism f" "monomorphism f"
shows "isomorphism f"
using assms epi_regmon_is_iso mono_is_regmono by auto
text βΉThe lemma below corresponds to Proposition 2.2.8 in Halvorson.βΊ
lemma epi_is_surj:
assumes "p: X β Y" "epimorphism p"
shows "surjective p"
unfolding surjective_def
proof(rule ccontr)
assume a1: "Β¬ (βy. y ββ©c codomain p βΆ (βx. x ββ©c domain p β§ p ββ©c x = y))"
have "βy. y ββ©c Y β§ Β¬(βx. x ββ©c X β§ p ββ©c x = y)"
using a1 assms(1) cfunc_type_def by auto
then obtain y0 where y_def: "y0 ββ©c Y β§ (βx. x ββ©c X βΆ p ββ©c x β y0)"
by auto
have mono: "monomorphism y0"
using element_monomorphism y_def by blast
obtain g where g_def: "g = eq_pred Y ββ©c β¨y0 ββ©c Ξ²βYβ, id Yβ©"
by simp
have g_right_arg_type: "β¨y0 ββ©c Ξ²βYβ, id Yβ© : Y β Y Γβ©c Y"
by (meson cfunc_prod_type comp_type id_type terminal_func_type y_def)
then have g_type[type_rule]: "g: Y β Ξ©"
using comp_type eq_pred_type g_def by blast
have gpx_Eqs_f: "βx. x ββ©c X βΆ g ββ©c p ββ©c x = πΏ"
proof(rule ccontr)
assume "Β¬ (βx. x ββ©c X βΆ g ββ©c p ββ©c x = πΏ)"
then obtain x where x_type: "x ββ©c X" and bwoc: "g ββ©c p ββ©c x β πΏ"
by blast
show False
by (smt (verit) assms(1) bwoc cfunc_type_def comp_associative comp_type eq_pred_false_extract_right eq_pred_type g_def g_right_arg_type x_type y_def)
qed
obtain h where h_def: "h = πΏ ββ©c Ξ²βYβ" and h_type[type_rule]:"h: Y β Ξ©"
by (typecheck_cfuncs, simp)
have hpx_eqs_f: "βx. x ββ©c X βΆ h ββ©c p ββ©c x = πΏ"
by (smt assms(1) cfunc_type_def codomain_comp comp_associative false_func_type h_def id_right_unit2 id_type terminal_func_comp terminal_func_type terminal_func_unique)
have gp_eqs_hp: "g ββ©c p = h ββ©c p"
proof(rule one_separator[where X=X,where Y=Ξ©])
show "g ββ©c p : X β Ξ©"
using assms by typecheck_cfuncs
show "h ββ©c p : X β Ξ©"
using assms by typecheck_cfuncs
show "βx. x ββ©c X βΉ (g ββ©c p) ββ©c x = (h ββ©c p) ββ©c x"
using assms(1) comp_associative2 g_type gpx_Eqs_f h_type hpx_eqs_f by auto
qed
have g_not_h: "g β h"
proof -
have f1: "βc. Ξ²βcodomain cβ ββ©c c = Ξ²βdomain cβ"
by (simp add: cfunc_type_def terminal_func_comp)
have f2: "domain β¨y0 ββ©c Ξ²βYβ,idβ©c Yβ© = Y"
using cfunc_type_def g_right_arg_type by blast
have f3: "codomain β¨y0 ββ©c Ξ²βYβ,idβ©c Yβ© = Y Γβ©c Y"
using cfunc_type_def g_right_arg_type by blast
have f4: "codomain y0 = Y"
using cfunc_type_def y_def by presburger
have "βc. domain (eq_pred c) = c Γβ©c c"
using cfunc_type_def eq_pred_type by auto
then have "g ββ©c y0 β πΏ"
using f4 f3 f2 by (metis (no_types) eq_pred_true_extract_right comp_associative g_def true_false_distinct y_def)
then show ?thesis
using f1 by (metis (no_types) cfunc_type_def comp_associative false_func_type h_def id_right_unit2 id_type one_unique_element terminal_func_type y_def)
qed
then show False
using gp_eqs_hp assms cfunc_type_def epimorphism_def g_type h_type by auto
qed
text βΉThe lemma below corresponds to Proposition 2.2.9 in Halvorson.βΊ
lemma pullback_of_epi_is_epi1:
assumes "f: Y β Z" "epimorphism f" "is_pullback A Y X Z q1 f q0 g"
shows "epimorphism q0"
proof -
have surj_f: "surjective f"
using assms(1,2) epi_is_surj by auto
have "surjective (q0)"
unfolding surjective_def
proof(clarify)
fix y
assume y_type: "y ββ©c codomain q0"
then have codomain_gy: "g ββ©c y ββ©c Z"
using assms(3) cfunc_type_def is_pullback_def by (typecheck_cfuncs, auto)
then have z_exists: "β z. z ββ©c Y β§ f ββ©c z = g ββ©c y"
using assms(1) cfunc_type_def surj_f surjective_def by auto
then obtain z where z_def: "z ββ©c Y β§ f ββ©c z = g ββ©c y"
by blast
then have "β! k. k: π β A β§ q0 ββ©c k = y β§ q1 ββ©c k =z"
by (smt (verit, ccfv_threshold) assms(3) cfunc_type_def is_pullback_def y_type)
then show "βx. x ββ©c domain q0 β§ q0 ββ©c x = y"
using assms(3) cfunc_type_def is_pullback_def by auto
qed
then show ?thesis
using surjective_is_epimorphism by blast
qed
text βΉThe lemma below corresponds to Proposition 2.2.9b in Halvorson.βΊ
lemma pullback_of_epi_is_epi2:
assumes "g: X β Z" "epimorphism g" "is_pullback A Y X Z q1 f q0 g"
shows "epimorphism q1"
proof -
have surj_g: "surjective g"
using assms(1) assms(2) epi_is_surj by auto
have "surjective q1"
unfolding surjective_def
proof(clarify)
fix y
assume y_type: "y ββ©c codomain q1"
then have codomain_gy: "f ββ©c y ββ©c Z"
using assms(3) cfunc_type_def comp_type is_pullback_def by auto
then have z_exists: "β z. z ββ©c X β§ g ββ©c z = f ββ©c y"
using assms(1) cfunc_type_def surj_g surjective_def by auto
then obtain z where z_def: "z ββ©c X β§ g ββ©c z = f ββ©c y"
by blast
then have "β! k. k: π β A β§ q0 ββ©c k = z β§ q1 ββ©c k =y"
by (smt (verit, ccfv_threshold) assms(3) cfunc_type_def is_pullback_def y_type)
then show "βx. x ββ©c domain q1 β§ q1 ββ©c x = y"
using assms(3) cfunc_type_def is_pullback_def by auto
qed
then show ?thesis
using surjective_is_epimorphism by blast
qed
text βΉThe lemma below corresponds to Proposition 2.2.9c in Halvorson.βΊ
lemma pullback_of_mono_is_mono1:
assumes "g: X β Z" "monomorphism f" "is_pullback A Y X Z q1 f q0 g"
shows "monomorphism q0"
unfolding monomorphism_def2
proof(clarify)
fix u v Q a x
assume u_type: "u : Q β a"
assume v_type: "v : Q β a"
assume q0_type: "q0 : a β x"
assume equals: "q0 ββ©c u = q0 ββ©c v"
have a_is_A: "a = A"
using assms(3) cfunc_type_def is_pullback_def q0_type by force
have x_is_X: "x = X"
using assms(3) cfunc_type_def is_pullback_def q0_type by fastforce
have u_type2[type_rule]: "u : Q β A"
using a_is_A u_type by blast
have v_type2[type_rule]: "v : Q β A"
using a_is_A v_type by blast
have q1_type2[type_rule]: "q0 : A β X"
using a_is_A q0_type x_is_X by blast
have eqn1: "g ββ©c (q0 ββ©c u) = f ββ©c (q1 ββ©c v)"
proof -
have "g ββ©c (q0 ββ©c u) = g ββ©c q0 ββ©c v"
by (simp add: equals)
also have "... = f ββ©c (q1 ββ©c v)"
using assms(3) cfunc_type_def comp_associative is_pullback_def by (typecheck_cfuncs, force)
finally show ?thesis.
qed
have eqn2: "q1 ββ©c u = q1 ββ©c v"
proof -
have f1: "f ββ©c q1 ββ©c u = g ββ©c q0 ββ©c u"
using assms(3) comp_associative2 is_pullback_def by (typecheck_cfuncs, auto)
also have "... = g ββ©c q0 ββ©c v"
by (simp add: equals)
also have "... = f ββ©c q1 ββ©c v"
using eqn1 equals by fastforce
then show ?thesis
by (typecheck_cfuncs, smt (verit, ccfv_threshold) f1 assms(2,3) eqn1 is_pullback_def monomorphism_def3)
qed
have uniqueness: "β! j. (j : Q β A β§ q1 ββ©c j = q1 ββ©c v β§ q0 ββ©c j = q0 ββ©c u)"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(3) eqn1 is_pullback_def)
then show "u = v"
using eqn2 equals uniqueness by (typecheck_cfuncs, auto)
qed
text βΉThe lemma below corresponds to Proposition 2.2.9d in Halvorson.βΊ
lemma pullback_of_mono_is_mono2:
assumes "g: X β Z" "monomorphism g" "is_pullback A Y X Z q1 f q0 g"
shows "monomorphism q1"
unfolding monomorphism_def2
proof(clarify)
fix u v Q a y
assume u_type: "u : Q β a"
assume v_type: "v : Q β a"
assume q1_type: "q1 : a β y"
assume equals: "q1 ββ©c u = q1 ββ©c v"
have a_is_A: "a = A"
using assms(3) cfunc_type_def is_pullback_def q1_type by force
have y_is_Y: "y = Y"
using assms(3) cfunc_type_def is_pullback_def q1_type by fastforce
have u_type2[type_rule]: "u : Q β A"
using a_is_A u_type by blast
have v_type2[type_rule]: "v : Q β A"
using a_is_A v_type by blast
have q1_type2[type_rule]: "q1 : A β Y"
using a_is_A q1_type y_is_Y by blast
have eqn1: "f ββ©c (q1 ββ©c u) = g ββ©c (q0 ββ©c v)"
proof -
have "f ββ©c (q1 ββ©c u) = f ββ©c q1 ββ©c v"
by (simp add: equals)
also have "... = g ββ©c (q0 ββ©c v)"
using assms(3) cfunc_type_def comp_associative is_pullback_def by (typecheck_cfuncs, force)
finally show ?thesis.
qed
have eqn2: "q0 ββ©c u = q0 ββ©c v"
proof -
have f1: "g ββ©c q0 ββ©c u = f ββ©c q1 ββ©c u"
using assms(3) comp_associative2 is_pullback_def by (typecheck_cfuncs, auto)
also have "... = f ββ©c q1 ββ©c v"
by (simp add: equals)
also have "... = g ββ©c q0 ββ©c v"
using eqn1 equals by fastforce
then show ?thesis
by (typecheck_cfuncs, smt (verit, ccfv_threshold) f1 assms(2,3) eqn1 is_pullback_def monomorphism_def3)
qed
have uniqueness: "β! j. (j : Q β A β§ q0 ββ©c j = q0 ββ©c v β§ q1 ββ©c j = q1 ββ©c u)"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(3) eqn1 is_pullback_def)
then show "u = v"
using eqn2 equals uniqueness by (typecheck_cfuncs, auto)
qed
subsection βΉFiber Over an Element and its Connection to the Fibered ProductβΊ
text βΉThe definition below corresponds to Definition 2.2.6 in Halvorson.βΊ
definition fiber :: "cfunc β cfunc β cset" ("_β§-β§1{_}" [100,100]100) where
"fβ§-β§1{y} = (fβ§-β§1β¦πβ¦βyβ)"
definition fiber_morphism :: "cfunc β cfunc β cfunc" where
"fiber_morphism f y = left_cart_proj (domain f) π ββ©c inverse_image_mapping f π y"
lemma fiber_morphism_type[type_rule]:
assumes "f : X β Y" "y ββ©c Y"
shows "fiber_morphism f y : fβ§-β§1{y} β X"
unfolding fiber_def fiber_morphism_def
using assms cfunc_type_def element_monomorphism inverse_image_subobject subobject_of_def2
by (typecheck_cfuncs, auto)
lemma fiber_subset:
assumes "f : X β Y" "y ββ©c Y"
shows "(fβ§-β§1{y}, fiber_morphism f y) ββ©c X"
unfolding fiber_def fiber_morphism_def
using assms cfunc_type_def element_monomorphism inverse_image_subobject inverse_image_subobject_mapping_def
by (typecheck_cfuncs, auto)
lemma fiber_morphism_monomorphism:
assumes "f : X β Y" "y ββ©c Y"
shows "monomorphism (fiber_morphism f y)"
using assms cfunc_type_def element_monomorphism fiber_morphism_def inverse_image_monomorphism by auto
lemma fiber_morphism_eq:
assumes "f : X β Y" "y ββ©c Y"
shows "f ββ©c fiber_morphism f y = y ββ©c Ξ²βfβ§-β§1{y}β"
proof -
have "f ββ©c fiber_morphism f y = f ββ©c left_cart_proj (domain f) π ββ©c inverse_image_mapping f π y"
unfolding fiber_morphism_def by auto
also have "... = y ββ©c right_cart_proj X π ββ©c inverse_image_mapping f π y"
using assms cfunc_type_def element_monomorphism inverse_image_mapping_eq by auto
also have "... = y ββ©c Ξ²βfβ§-β§1β¦πβ¦βyββ"
using assms by (typecheck_cfuncs, metis element_monomorphism terminal_func_unique)
also have "... = y ββ©c Ξ²βfβ§-β§1{y}β"
unfolding fiber_def by auto
finally show ?thesis.
qed
text βΉThe lemma below corresponds to Proposition 2.2.7 in Halvorson.βΊ
lemma not_surjective_has_some_empty_preimage:
assumes p_type[type_rule]: "p: X β Y" and p_not_surj: "Β¬ surjective p"
shows "β y. y ββ©c Y β§ is_empty(pβ§-β§1{y})"
proof -
have nonempty: "nonempty(Y)"
using assms cfunc_type_def nonempty_def surjective_def by auto
obtain y0 where y0_type[type_rule]: "y0 ββ©c Y" "β x. x ββ©c X βΆ pββ©c x β y0"
using assms cfunc_type_def surjective_def by auto
have "Β¬nonempty(pβ§-β§1{y0})"
proof (rule ccontr, clarify)
assume a1: "nonempty(pβ§-β§1{y0})"
obtain z where z_type[type_rule]: "z ββ©c pβ§-β§1{y0}"
using a1 nonempty_def by blast
have fiber_z_type: "fiber_morphism p y0 ββ©c z ββ©c X"
using assms(1) comp_type fiber_morphism_type y0_type z_type by auto
have contradiction: "p ββ©c fiber_morphism p y0 ββ©c z = y0"
by (typecheck_cfuncs, smt (z3) comp_associative2 fiber_morphism_eq id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
have "p ββ©c (fiber_morphism p y0 ββ©c z) β y0"
by (simp add: fiber_z_type y0_type)
then show False
using contradiction by blast
qed
then show ?thesis
using is_empty_def nonempty_def y0_type by blast
qed
lemma fiber_iso_fibered_prod:
assumes f_type[type_rule]: "f : X β Y"
assumes y_type[type_rule]: "y : π β Y"
shows "fβ§-β§1{y} β
X βfβΓβ©cβyβπ"
using element_monomorphism equalizers_isomorphic f_type fiber_def fibered_product_equalizer inverse_image_is_equalizer is_isomorphic_def y_type by moura
lemma fib_prod_left_id_iso:
assumes "g : Y β X"
shows "(X βid(X)βΓβ©cβgβ Y) β
Y"
proof -
have is_pullback: "is_pullback (X βid(X)βΓβ©cβgβ Y) Y X X (fibered_product_right_proj X (id(X)) g Y) g (fibered_product_left_proj X (id(X)) g Y) (id(X))"
using assms fibered_product_is_pullback by (typecheck_cfuncs, blast)
then have mono: "monomorphism(fibered_product_right_proj X (id(X)) g Y)"
using assms by (typecheck_cfuncs, meson id_isomorphism iso_imp_epi_and_monic pullback_of_mono_is_mono2)
have "epimorphism(fibered_product_right_proj X (id(X)) g Y)"
by (meson id_isomorphism id_type is_pullback iso_imp_epi_and_monic pullback_of_epi_is_epi2)
then have "isomorphism(fibered_product_right_proj X (id(X)) g Y)"
by (simp add: epi_mon_is_iso mono)
then show ?thesis
using assms fibered_product_right_proj_type id_type is_isomorphic_def by blast
qed
lemma fib_prod_right_id_iso:
assumes "f : X β Y"
shows "(X βfβΓβ©cβid(Y)β Y) β
X"
proof -
have is_pullback: "is_pullback (X βfβΓβ©cβid(Y)β Y) Y X Y (fibered_product_right_proj X f (id(Y)) Y) (id(Y)) (fibered_product_left_proj X f (id(Y)) Y) f "
using assms fibered_product_is_pullback by (typecheck_cfuncs, blast)
then have mono: "monomorphism(fibered_product_left_proj X f (id(Y)) Y)"
using assms by (typecheck_cfuncs, meson id_isomorphism is_pullback iso_imp_epi_and_monic pullback_of_mono_is_mono1)
have "epimorphism(fibered_product_left_proj X f (id(Y)) Y)"
by (meson id_isomorphism id_type is_pullback iso_imp_epi_and_monic pullback_of_epi_is_epi1)
then have "isomorphism(fibered_product_left_proj X f (id(Y)) Y)"
by (simp add: epi_mon_is_iso mono)
then show ?thesis
using assms fibered_product_left_proj_type id_type is_isomorphic_def by blast
qed
text βΉThe lemma below corresponds to the discussion at the top of page 42 in Halvorson.βΊ
lemma kernel_pair_connection:
assumes f_type[type_rule]: "f : X β Y" and g_type[type_rule]: "g : X β E"
assumes g_epi: "epimorphism g"
assumes h_g_eq_f: "h ββ©c g = f"
assumes g_eq: "g ββ©c fibered_product_left_proj X f f X = g ββ©c fibered_product_right_proj X f f X "
assumes h_type[type_rule]: "h : E β Y"
shows "β! b. b : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E β§
fibered_product_left_proj E h h E ββ©c b = g ββ©c fibered_product_left_proj X f f X β§
fibered_product_right_proj E h h E ββ©c b = g ββ©c fibered_product_right_proj X f f X β§
epimorphism b"
proof -
have gxg_fpmorph_eq: "(h ββ©c left_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X
= (h ββ©c right_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
proof -
have "(h ββ©c left_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X
= h ββ©c (left_cart_proj E E ββ©c (g Γβ©f g)) ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = h ββ©c (g ββ©c left_cart_proj X X) ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
also have "... = (h ββ©c g) ββ©c left_cart_proj X X ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = f ββ©c left_cart_proj X X ββ©c fibered_product_morphism X f f X"
by (simp add: h_g_eq_f)
also have "... = f ββ©c right_cart_proj X X ββ©c fibered_product_morphism X f f X"
using f_type fibered_product_left_proj_def fibered_product_proj_eq fibered_product_right_proj_def by auto
also have "... = (h ββ©c g) ββ©c right_cart_proj X X ββ©c fibered_product_morphism X f f X"
by (simp add: h_g_eq_f)
also have "... = h ββ©c (g ββ©c right_cart_proj X X) ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = h ββ©c right_cart_proj E E ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
also have "... = (h ββ©c right_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, smt comp_associative2)
finally show ?thesis.
qed
have h_equalizer: "equalizer (E βhβΓβ©cβhβ E) (fibered_product_morphism E h h E) (h ββ©c left_cart_proj E E) (h ββ©c right_cart_proj E E)"
using fibered_product_morphism_equalizer h_type by auto
then have "βj F. j : F β E Γβ©c E β§ (h ββ©c left_cart_proj E E) ββ©c j = (h ββ©c right_cart_proj E E) ββ©c j βΆ
(β!k. k : F β E βhβΓβ©cβhβ E β§ fibered_product_morphism E h h E ββ©c k = j)"
unfolding equalizer_def using cfunc_type_def fibered_product_morphism_type h_type by (smt (verit))
then have "(g Γβ©f g) ββ©c fibered_product_morphism X f f X : X βfβΓβ©cβfβ X β E Γβ©c E β§ (h ββ©c left_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X = (h ββ©c right_cart_proj E E) ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X βΆ
(β!k. k : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E β§ fibered_product_morphism E h h E ββ©c k = (g Γβ©f g) ββ©c fibered_product_morphism X f f X)"
by auto
then obtain b where b_type[type_rule]: "b : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E"
and b_eq: "fibered_product_morphism E h h E ββ©c b = (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
by (meson cfunc_cross_prod_type comp_type f_type fibered_product_morphism_type g_type gxg_fpmorph_eq)
have "is_pullback (X βfβΓβ©cβfβ X) (X Γβ©c X) (E βhβΓβ©cβhβ E) (E Γβ©c E)
(fibered_product_morphism X f f X) (g Γβ©f g) b (fibered_product_morphism E h h E)"
unfolding is_pullback_def
proof (typecheck_cfuncs, safe, metis b_eq)
fix Z k j
assume k_type[type_rule]: "k : Z β X Γβ©c X" and h_type[type_rule]: "j : Z β E βhβΓβ©cβhβ E"
assume k_h_eq: "(g Γβ©f g) ββ©c k = fibered_product_morphism E h h E ββ©c j"
have left_k_right_k_eq: "f ββ©c left_cart_proj X X ββ©c k = f ββ©c right_cart_proj X X ββ©c k"
proof -
have "f ββ©c left_cart_proj X X ββ©c k = h ββ©c g ββ©c left_cart_proj X X ββ©c k"
by (smt (z3) assms(6) comp_associative2 comp_type g_type h_g_eq_f k_type left_cart_proj_type)
also have "... = h ββ©c left_cart_proj E E ββ©c (g Γβ©f g) ββ©c k"
by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
also have "... = h ββ©c left_cart_proj E E ββ©c fibered_product_morphism E h h E ββ©c j"
by (simp add: k_h_eq)
also have "... = ((h ββ©c left_cart_proj E E) ββ©c fibered_product_morphism E h h E) ββ©c j"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = ((h ββ©c right_cart_proj E E) ββ©c fibered_product_morphism E h h E) ββ©c j"
using equalizer_def h_equalizer by auto
also have "... = h ββ©c right_cart_proj E E ββ©c fibered_product_morphism E h h E ββ©c j"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = h ββ©c right_cart_proj E E ββ©c (g Γβ©f g) ββ©c k"
by (simp add: k_h_eq)
also have "... = h ββ©c g ββ©c right_cart_proj X X ββ©c k"
by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
also have "... = f ββ©c right_cart_proj X X ββ©c k"
using assms(6) comp_associative2 comp_type g_type h_g_eq_f k_type right_cart_proj_type by blast
finally show ?thesis.
qed
have "is_pullback (X βfβΓβ©cβfβ X) X X Y
(fibered_product_right_proj X f f X) f (fibered_product_left_proj X f f X) f"
by (simp add: f_type fibered_product_is_pullback)
then have "right_cart_proj X X ββ©c k : Z β X βΉ left_cart_proj X X ββ©c k : Z β X βΉ f ββ©c right_cart_proj X X ββ©c k = f ββ©c left_cart_proj X X ββ©c k βΉ
(β!j. j : Z β X βfβΓβ©cβfβ X β§
fibered_product_right_proj X f f X ββ©c j = right_cart_proj X X ββ©c k
β§ fibered_product_left_proj X f f X ββ©c j = left_cart_proj X X ββ©c k)"
unfolding is_pullback_def by auto
then obtain z where z_type[type_rule]: "z : Z β X βfβΓβ©cβfβ X"
and k_right_eq: "fibered_product_right_proj X f f X ββ©c z = right_cart_proj X X ββ©c k"
and k_left_eq: "fibered_product_left_proj X f f X ββ©c z = left_cart_proj X X ββ©c k"
and z_unique: "βj. j : Z β X βfβΓβ©cβfβ X
β§ fibered_product_right_proj X f f X ββ©c j = right_cart_proj X X ββ©c k
β§ fibered_product_left_proj X f f X ββ©c j = left_cart_proj X X ββ©c k βΉ z = j"
using left_k_right_k_eq by (typecheck_cfuncs, auto)
have k_eq: "fibered_product_morphism X f f X ββ©c z = k"
using k_right_eq k_left_eq
unfolding fibered_product_right_proj_def fibered_product_left_proj_def
by (typecheck_cfuncs_prems, smt cfunc_prod_comp cfunc_prod_unique)
then show "βl. l : Z β X βfβΓβ©cβfβ X β§ fibered_product_morphism X f f X ββ©c l = k β§ b ββ©c l = j"
proof (intro exI[where x=z], clarify)
assume k_def: "k = fibered_product_morphism X f f X ββ©c z"
have "fibered_product_morphism E h h E ββ©c j = (g Γβ©f g) ββ©c k"
by (simp add: k_h_eq)
also have "... = (g Γβ©f g) ββ©c fibered_product_morphism X f f X ββ©c z"
by (simp add: k_eq)
also have "... = fibered_product_morphism E h h E ββ©c b ββ©c z"
by (typecheck_cfuncs, simp add: b_eq comp_associative2)
then show "z : Z β X βfβΓβ©cβfβ X β§ fibered_product_morphism X f f X ββ©c z = fibered_product_morphism X f f X ββ©c z β§ b ββ©c z = j"
by (typecheck_cfuncs, metis assms(6) fibered_product_morphism_monomorphism fibered_product_morphism_type k_def k_h_eq monomorphism_def3)
qed
show "β j y. j : Z β X βfβΓβ©cβfβ X βΉ y : Z β X βfβΓβ©cβfβ X βΉ
fibered_product_morphism X f f X ββ©c y = fibered_product_morphism X f f X ββ©c j βΉ
j = y"
using fibered_product_morphism_monomorphism monomorphism_def2 by (typecheck_cfuncs_prems, metis)
qed
then have b_epi: "epimorphism b"
using g_epi g_type cfunc_cross_prod_type cfunc_cross_prod_surj pullback_of_epi_is_epi1 h_type
by (meson epi_is_surj surjective_is_epimorphism)
have existence: "βb. b : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E β§
fibered_product_left_proj E h h E ββ©c b = g ββ©c fibered_product_left_proj X f f X β§
fibered_product_right_proj E h h E ββ©c b = g ββ©c fibered_product_right_proj X f f X β§
epimorphism b"
proof (intro exI[where x=b], safe)
show "b : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E"
by typecheck_cfuncs
show "fibered_product_left_proj E h h E ββ©c b = g ββ©c fibered_product_left_proj X f f X"
proof -
have "fibered_product_left_proj E h h E ββ©c b
= left_cart_proj E E ββ©c fibered_product_morphism E h h E ββ©c b"
unfolding fibered_product_left_proj_def by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = left_cart_proj E E ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
by (simp add: b_eq)
also have "... = g ββ©c left_cart_proj X X ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, simp add: comp_associative2 left_cart_proj_cfunc_cross_prod)
also have "... = g ββ©c fibered_product_left_proj X f f X"
unfolding fibered_product_left_proj_def by (typecheck_cfuncs)
finally show ?thesis.
qed
show "fibered_product_right_proj E h h E ββ©c b = g ββ©c fibered_product_right_proj X f f X"
proof -
have "fibered_product_right_proj E h h E ββ©c b
= right_cart_proj E E ββ©c fibered_product_morphism E h h E ββ©c b"
unfolding fibered_product_right_proj_def by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = right_cart_proj E E ββ©c (g Γβ©f g) ββ©c fibered_product_morphism X f f X"
by (simp add: b_eq)
also have "... = g ββ©c right_cart_proj X X ββ©c fibered_product_morphism X f f X"
by (typecheck_cfuncs, simp add: comp_associative2 right_cart_proj_cfunc_cross_prod)
also have "... = g ββ©c fibered_product_right_proj X f f X"
unfolding fibered_product_right_proj_def by (typecheck_cfuncs)
finally show ?thesis.
qed
show "epimorphism b"
by (simp add: b_epi)
qed
show "β!b. b : X βfβΓβ©cβfβ X β E βhβΓβ©cβhβ E β§
fibered_product_left_proj E h h E ββ©c b = g ββ©c fibered_product_left_proj X f f X β§
fibered_product_right_proj E h h E ββ©c b = g ββ©c fibered_product_right_proj X f f X β§
epimorphism b"
by (typecheck_cfuncs, metis epimorphism_def2 existence g_eq iso_imp_epi_and_monic kern_pair_proj_iso_TFAE2 monomorphism_def3)
qed
section βΉSet SubtractionβΊ
definition set_subtraction :: "cset β cset Γ cfunc β cset" (infix "β" 60) where
"Y β X = (SOME E. β m'. equalizer E m' (characteristic_func (snd X)) (πΏ ββ©c Ξ²βYβ))"
lemma set_subtraction_equalizer:
assumes "m : X β Y" "monomorphism m"
shows "β m'. equalizer (Y β (X,m)) m' (characteristic_func m) (πΏ ββ©c Ξ²βYβ)"
proof -
have "β E m'. equalizer E m' (characteristic_func m) (πΏ ββ©c Ξ²βYβ)"
using assms equalizer_exists by (typecheck_cfuncs, auto)
then have "β m'. equalizer (Y β (X,m)) m' (characteristic_func (snd (X,m))) (πΏ ββ©c Ξ²βYβ)"
unfolding set_subtraction_def by (subst someI_ex, auto)
then show "β m'. equalizer (Y β (X,m)) m' (characteristic_func m) (πΏ ββ©c Ξ²βYβ)"
by auto
qed
definition complement_morphism :: "cfunc β cfunc" ("_β§c" [1000]) where
"mβ§c = (SOME m'. equalizer (codomain m β (domain m, m)) m' (characteristic_func m) (πΏ ββ©c Ξ²βcodomain mβ))"
lemma complement_morphism_equalizer:
assumes "m : X β Y" "monomorphism m"
shows "equalizer (Y β (X,m)) mβ§c (characteristic_func m) (πΏ ββ©c Ξ²βYβ)"
proof -
have "β m'. equalizer (codomain m β (domain m, m)) m' (characteristic_func m) (πΏ ββ©c Ξ²βcodomain mβ)"
by (simp add: assms cfunc_type_def set_subtraction_equalizer)
then have "equalizer (codomain m β (domain m, m)) mβ§c (characteristic_func m) (πΏ ββ©c Ξ²βcodomain mβ)"
unfolding complement_morphism_def by (subst someI_ex, auto)
then show "equalizer (Y β (X, m)) mβ§c (characteristic_func m) (πΏ ββ©c Ξ²βYβ)"
using assms unfolding cfunc_type_def by auto
qed
lemma complement_morphism_type[type_rule]:
assumes "m : X β Y" "monomorphism m"
shows "mβ§c : Y β (X,m) β Y"
using assms cfunc_type_def characteristic_func_type complement_morphism_equalizer equalizer_def by auto
lemma complement_morphism_mono:
assumes "m : X β Y" "monomorphism m"
shows "monomorphism mβ§c"
using assms complement_morphism_equalizer equalizer_is_monomorphism by blast
lemma complement_morphism_eq:
assumes "m : X β Y" "monomorphism m"
shows "characteristic_func m ββ©c mβ§c = (πΏ ββ©c Ξ²βYβ) ββ©c mβ§c"
using assms complement_morphism_equalizer unfolding equalizer_def by auto
lemma characteristic_func_true_not_complement_member:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes characteristic_func_true: "characteristic_func m ββ©c x = π"
shows "Β¬ x ββXβ (X β (B, m),mβ§c)"
proof
assume in_complement: "x ββXβ (X β (B, m), mβ§c)"
then obtain x' where x'_type: "x' ββ©c X β (B,m)" and x'_def: "mβ§c ββ©c x' = x"
using assms cfunc_type_def complement_morphism_type factors_through_def relative_member_def2
by auto
then have "characteristic_func m ββ©c mβ§c = (πΏ ββ©c Ξ²βXβ) ββ©c mβ§c"
using assms complement_morphism_equalizer equalizer_def by blast
then have "characteristic_func m ββ©c x = πΏ ββ©c Ξ²βXβ ββ©c x"
using assms x'_type complement_morphism_type
by (typecheck_cfuncs, smt x'_def assms cfunc_type_def comp_associative domain_comp)
then have "characteristic_func m ββ©c x = πΏ"
using assms by (typecheck_cfuncs, metis id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
then show False
using characteristic_func_true true_false_distinct by auto
qed
lemma characteristic_func_false_complement_member:
assumes "m : B β X" "monomorphism m" "x ββ©c X"
assumes characteristic_func_false: "characteristic_func m ββ©c x = πΏ"
shows "x ββXβ (X β (B, m),mβ§c)"
proof -
have x_equalizes: "characteristic_func m ββ©c x = πΏ ββ©c Ξ²βXβ ββ©c x"
by (metis assms(3) characteristic_func_false false_func_type id_right_unit2 id_type one_unique_element terminal_func_comp terminal_func_type)
have "βh F. h : F β X β§ characteristic_func m ββ©c h = (πΏ ββ©c Ξ²βXβ) ββ©c h βΆ
(β!k. k : F β X β (B, m) β§ mβ§c ββ©c k = h)"
using assms complement_morphism_equalizer unfolding equalizer_def
by (smt cfunc_type_def characteristic_func_type)
then obtain x' where x'_type: "x' ββ©c X β (B, m)" and x'_def: "mβ§c ββ©c x' = x"
by (metis assms(3) cfunc_type_def comp_associative false_func_type terminal_func_type x_equalizes)
then show "x ββXβ (X β (B, m),mβ§c)"
unfolding relative_member_def factors_through_def
using assms complement_morphism_mono complement_morphism_type cfunc_type_def by auto
qed
lemma in_complement_not_in_subset:
assumes "m : X β Y" "monomorphism m" "x ββ©c Y"
assumes "x ββYβ (Y β (X,m), mβ§c)"
shows "Β¬ x ββYβ (X, m)"
using assms characteristic_func_false_not_relative_member
characteristic_func_true_not_complement_member characteristic_func_type comp_type
true_false_only_truth_values by blast
lemma not_in_subset_in_complement:
assumes "m : X β Y" "monomorphism m" "x ββ©c Y"
assumes "Β¬ x ββYβ (X, m)"
shows "x ββYβ (Y β (X,m), mβ§c)"
using assms characteristic_func_false_complement_member characteristic_func_true_relative_member
characteristic_func_type comp_type true_false_only_truth_values by blast
lemma complement_disjoint:
assumes "m : X β Y" "monomorphism m"
assumes "x ββ©c X" "x' ββ©c Y β (X,m)"
shows "m ββ©c x β mβ§c ββ©c x'"
proof
assume "m ββ©c x = mβ§c ββ©c x'"
then have "characteristic_func m ββ©c m ββ©c x = characteristic_func m ββ©c mβ§c ββ©c x'"
by auto
then have "(characteristic_func m ββ©c m) ββ©c x = (characteristic_func m ββ©c mβ§c) ββ©c x'"
using assms comp_associative2 by (typecheck_cfuncs, auto)
then have "(π ββ©c Ξ²βXβ) ββ©c x = ((πΏ ββ©c Ξ²βYβ) ββ©c mβ§c) ββ©c x'"
using assms characteristic_func_eq complement_morphism_eq by auto
then have "π ββ©c Ξ²βXβ ββ©c x = πΏ ββ©c Ξ²βYβ ββ©c mβ§c ββ©c x'"
using assms comp_associative2 by (typecheck_cfuncs, smt terminal_func_comp terminal_func_type)
then have "π ββ©c id π = πΏ ββ©c id π"
using assms by (smt cfunc_type_def comp_associative complement_morphism_type id_type one_unique_element terminal_func_comp terminal_func_type)
then have "π = πΏ"
using false_func_type id_right_unit2 true_func_type by auto
then show False
using true_false_distinct by auto
qed
lemma set_subtraction_right_iso:
assumes m_type[type_rule]: "m : A β C" and m_mono[type_rule]: "monomorphism m"
assumes i_type[type_rule]: "i : B β A" and i_iso: "isomorphism i"
shows "C β (A,m) = C β (B, m ββ©c i)"
proof -
have mi_mono[type_rule]: "monomorphism (m ββ©c i)"
using cfunc_type_def composition_of_monic_pair_is_monic i_iso i_type iso_imp_epi_and_monic m_mono m_type by presburger
obtain Οm where Οm_type[type_rule]: "Οm : C β Ξ©" and Οm_def: "Οm = characteristic_func m"
using characteristic_func_type m_mono m_type by blast
obtain Οmi where Οmi_type[type_rule]: "Οmi : C β Ξ©" and Οmi_def: "Οmi = characteristic_func (m ββ©c i)"
by (typecheck_cfuncs, simp)
have "β c. c ββ©c C βΉ (Οm ββ©c c = π) = (Οmi ββ©c c = π)"
proof -
fix c
assume c_type[type_rule]: "c ββ©c C"
have "(Οm ββ©c c = π) = (c ββCβ (A,m))"
by (typecheck_cfuncs, metis Οm_def m_mono not_rel_mem_char_func_false rel_mem_char_func_true true_false_distinct)
also have "... = (β a. a ββ©c A β§ c = m ββ©c a)"
using cfunc_type_def factors_through_def m_mono relative_member_def2 by (typecheck_cfuncs, auto)
also have "... = (β b. b ββ©c B β§ c = m ββ©c i ββ©c b)"
by (typecheck_cfuncs, smt (z3) cfunc_type_def comp_type epi_is_surj i_iso iso_imp_epi_and_monic surjective_def)
also have "... = (c ββCβ (B,m ββ©c i))"
using cfunc_type_def comp_associative2 composition_of_monic_pair_is_monic factors_through_def2 i_iso iso_imp_epi_and_monic m_mono relative_member_def2
by (typecheck_cfuncs, auto)
also have "... = (Οmi ββ©c c = π)"
by (typecheck_cfuncs, metis Οmi_def mi_mono not_rel_mem_char_func_false rel_mem_char_func_true true_false_distinct)
finally show "(Οm ββ©c c = π) = (Οmi ββ©c c = π)".
qed
then have "Οm = Οmi"
by (typecheck_cfuncs, smt (verit, best) comp_type one_separator true_false_only_truth_values)
then show "C β (A,m) = C β (B, m ββ©c i)"
using Οm_def Οmi_def isomorphic_is_reflexive set_subtraction_def by auto
qed
lemma set_subtraction_left_iso:
assumes m_type[type_rule]: "m : C β A" and m_mono[type_rule]: "monomorphism m"
assumes i_type[type_rule]: "i : A β B" and i_iso: "isomorphism i"
shows "A β (C,m) β
B β (C, i ββ©c m)"
proof -
have im_mono[type_rule]: "monomorphism (i ββ©c m)"
using cfunc_type_def composition_of_monic_pair_is_monic i_iso i_type iso_imp_epi_and_monic m_mono m_type by presburger
obtain Οm where Οm_type[type_rule]: "Οm : A β Ξ©" and Οm_def: "Οm = characteristic_func m"
using characteristic_func_type m_mono m_type by blast
obtain Οim where Οim_type[type_rule]: "Οim : B β Ξ©" and Οim_def: "Οim = characteristic_func (i ββ©c m)"
by (typecheck_cfuncs, simp)
have Οim_pullback: "is_pullback C π B Ξ© (Ξ²βCβ) π (i ββ©c m) Οim"
using Οim_def characteristic_func_is_pullback comp_type i_type im_mono m_type by blast
have "is_pullback C π A Ξ© (Ξ²βCβ) π m (Οim ββ©c i)"
unfolding is_pullback_def
proof (typecheck_cfuncs, safe)
show "π ββ©c Ξ²βCβ = (Οim ββ©c i) ββ©c m"
by (typecheck_cfuncs, etcs_assocr, metis Οim_def characteristic_func_eq comp_type im_mono)
next
fix Z k h
assume k_type[type_rule]: "k : Z β π" and h_type[type_rule]: "h : Z β A"
assume eq: "π ββ©c k = (Οim ββ©c i) ββ©c h"
then obtain j where j_type[type_rule]: "j : Z β C" and j_def: "i ββ©c h = (i ββ©c m) ββ©c j"
using Οim_pullback unfolding is_pullback_def by (typecheck_cfuncs, smt (verit, ccfv_threshold) comp_associative2 k_type)
then show "βj. j : Z β C β§ Ξ²βCβ ββ©c j = k β§ m ββ©c j = h"
by (intro exI[where x=j], typecheck_cfuncs, smt comp_associative2 i_iso iso_imp_epi_and_monic monomorphism_def2 terminal_func_unique)
next
fix Z j y
assume j_type[type_rule]: "j : Z β C" and y_type[type_rule]: "y : Z β C"
assume "π ββ©c Ξ²βCβ ββ©c j = (Οim ββ©c i) ββ©c m ββ©c j" "Ξ²βCβ ββ©c y = Ξ²βCβ ββ©c j" "m ββ©c y = m ββ©c j"
then show "j = y"
using m_mono monomorphism_def2 by (typecheck_cfuncs_prems, blast)
qed
then have Οim_i_eq_Οm: "Οim ββ©c i = Οm"
using Οm_def characteristic_func_is_pullback characteristic_function_exists m_mono m_type by blast
then have "Οim ββ©c (i ββ©c mβ§c) = πΏ ββ©c Ξ²βBβ ββ©c (i ββ©c mβ§c)"
by (etcs_assocl, typecheck_cfuncs, smt (verit, best) Οm_def comp_associative2 complement_morphism_eq m_mono terminal_func_comp)
then obtain i' where i'_type[type_rule]: "i' : A β (C, m) β B β (C, i ββ©c m)" and i'_def: "i ββ©c mβ§c = (i ββ©c m)β§c ββ©c i'"
using complement_morphism_equalizer unfolding equalizer_def
by (-, typecheck_cfuncs, smt Οim_def cfunc_type_def comp_associative2 im_mono)
have "Οm ββ©c (iβΒ― ββ©c (i ββ©c m)β§c) = πΏ ββ©c Ξ²βAβ ββ©c (iβΒ― ββ©c (i ββ©c m)β§c)"
proof -
have "Οm ββ©c (iβΒ― ββ©c (i ββ©c m)β§c) = Οim ββ©c (i ββ©c iβΒ―) ββ©c (i ββ©c m)β§c"
by (typecheck_cfuncs, simp add: Οim_i_eq_Οm cfunc_type_def comp_associative i_iso)
also have "... = Οim ββ©c (i ββ©c m)β§c"
using i_iso id_left_unit2 inv_right by (typecheck_cfuncs, auto)
also have "... = πΏ ββ©c Ξ²βBβ ββ©c (i ββ©c m)β§c"
by (typecheck_cfuncs, simp add: Οim_def comp_associative2 complement_morphism_eq im_mono)
also have "... = πΏ ββ©c Ξ²βAβ ββ©c (iβΒ― ββ©c (i ββ©c m)β§c)"
by (typecheck_cfuncs, metis i_iso terminal_func_unique)
finally show ?thesis.
qed
then obtain i'_inv where i'_inv_type[type_rule]: "i'_inv : B β (C, i ββ©c m) β A β (C, m)"
and i'_inv_def: "(i ββ©c m)β§c = (i ββ©c mβ§c) ββ©c i'_inv"
using complement_morphism_equalizer[where m="m", where X=C, where Y=A] unfolding equalizer_def
by (-, typecheck_cfuncs, smt (z3) Οm_def cfunc_type_def comp_associative2 i_iso id_left_unit2 inv_right m_mono)
have "isomorphism i'"
proof (etcs_subst isomorphism_def3, intro exI[where x = "i'_inv"], safe)
show "i'_inv : B β (C, i ββ©c m) β A β (C, m)"
by typecheck_cfuncs
have "i ββ©c mβ§c = (i ββ©c mβ§c) ββ©c i'_inv ββ©c i'"
using i'_inv_def by (etcs_subst i'_def, etcs_assocl, auto)
then show "i'_inv ββ©c i' = idβ©c (A β (C, m))"
by (typecheck_cfuncs_prems, smt (verit, best) cfunc_type_def complement_morphism_mono composition_of_monic_pair_is_monic i_iso id_right_unit2 id_type iso_imp_epi_and_monic m_mono monomorphism_def3)
next
have "(i ββ©c m)β§c = (i ββ©c m)β§c ββ©c i' ββ©c i'_inv"
using i'_def by (etcs_subst i'_inv_def, etcs_assocl, auto)
then show "i' ββ©c i'_inv = idβ©c (B β (C, i ββ©c m))"
by (typecheck_cfuncs_prems, metis complement_morphism_mono id_right_unit2 id_type im_mono monomorphism_def3)
qed
then show "A β (C, m) β
B β (C, i ββ©c m)"
using i'_type is_isomorphic_def by blast
qed
section βΉGraphsβΊ
definition functional_on :: "cset β cset β cset Γ cfunc β bool" where
"functional_on X Y R = (R ββ©c X Γβ©c Y β§
(βx. x ββ©c X βΆ (β! y. y ββ©c Y β§
β¨x,yβ© ββXΓβ©cYβ R)))"
text βΉThe definition below corresponds to Definition 2.3.12 in Halvorson.βΊ
definition graph :: "cfunc β cset" where
"graph f = (SOME E. β m. equalizer E m (f ββ©c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f)))"
lemma graph_equalizer:
"β m. equalizer (graph f) m (f ββ©c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f))"
unfolding graph_def
by (typecheck_cfuncs, rule someI_ex, simp add: cfunc_type_def equalizer_exists)
lemma graph_equalizer2:
assumes "f : X β Y"
shows "β m. equalizer (graph f) m (f ββ©c left_cart_proj X Y) (right_cart_proj X Y)"
using assms by (typecheck_cfuncs, metis cfunc_type_def graph_equalizer)
definition graph_morph :: "cfunc β cfunc" where
"graph_morph f = (SOME m. equalizer (graph f) m (f ββ©c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f)))"
lemma graph_equalizer3:
"equalizer (graph f) (graph_morph f) (f ββ©c left_cart_proj (domain f) (codomain f)) (right_cart_proj (domain f) (codomain f))"
unfolding graph_morph_def by (rule someI_ex, simp add: graph_equalizer)
lemma graph_equalizer4:
assumes "f : X β Y"
shows "equalizer (graph f) (graph_morph f) (f ββ©c left_cart_proj X Y) (right_cart_proj X Y)"
using assms cfunc_type_def graph_equalizer3 by auto
lemma graph_subobject:
assumes "f : X β Y"
shows "(graph f, graph_morph f) ββ©c (X Γβ©c Y)"
by (metis assms cfunc_type_def equalizer_def equalizer_is_monomorphism graph_equalizer3 right_cart_proj_type subobject_of_def2)
lemma graph_morph_type[type_rule]:
assumes "f : X β Y"
shows "graph_morph(f) : graph f β X Γβ©c Y"
using graph_subobject subobject_of_def2 assms by auto
text βΉThe lemma below corresponds to Exercise 2.3.13 in Halvorson.βΊ
lemma graphs_are_functional:
assumes "f : X β Y"
shows "functional_on X Y (graph f, graph_morph f)"
unfolding functional_on_def
proof(safe)
show graph_subobj: "(graph f, graph_morph f) ββ©c (XΓβ©c Y)"
by (simp add: assms graph_subobject)
show "βx. x ββ©c X βΉ βy. y ββ©c Y β§ β¨x,yβ© ββX Γβ©c Yβ (graph f, graph_morph f)"
proof -
fix x
assume x_type[type_rule]: "x ββ©c X"
obtain y where y_def: "y = f ββ©c x"
by simp
then have y_type[type_rule]: "y ββ©c Y"
using assms comp_type x_type y_def by blast
have "β¨x,yβ© ββX Γβ©c Yβ (graph f, graph_morph f)"
unfolding relative_member_def
proof(typecheck_cfuncs, safe)
show "monomorphism (snd (graph f, graph_morph f))"
using graph_subobj subobject_of_def by auto
show " snd (graph f, graph_morph f) : fst (graph f, graph_morph f) β X Γβ©c Y"
by (simp add: assms graph_morph_type)
have "β¨x,yβ© factorsthru graph_morph f"
proof(subst xfactorthru_equalizer_iff_fx_eq_gx[where E = "graph f", where m = "graph_morph f",
where f = "(f ββ©c left_cart_proj X Y)", where g = "right_cart_proj X Y", where X = "X Γβ©c Y", where Y = Y,
where x ="β¨x,yβ©"])
show "f ββ©c left_cart_proj X Y : X Γβ©c Y β Y"
using assms by typecheck_cfuncs
show "right_cart_proj X Y : X Γβ©c Y β Y"
by typecheck_cfuncs
show "equalizer (graph f) (graph_morph f) (f ββ©c left_cart_proj X Y) (right_cart_proj X Y)"
by (simp add: assms graph_equalizer4)
show "β¨x,yβ© ββ©c X Γβ©c Y"
by typecheck_cfuncs
show "(f ββ©c left_cart_proj X Y) ββ©c β¨x,yβ© = right_cart_proj X Y ββ©c β¨x,yβ©"
using assms
by (typecheck_cfuncs, smt (z3) comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_def)
qed
then show "β¨x,yβ© factorsthru snd (graph f, graph_morph f)"
by simp
qed
then show "βy. y ββ©c Y β§ β¨x,yβ© ββX Γβ©c Yβ (graph f, graph_morph f)"
using y_type by blast
qed
show "βx y ya.
x ββ©c X βΉ
y ββ©c Y βΉ
β¨x,yβ© ββX Γβ©c Yβ (graph f, graph_morph f) βΉ
ya ββ©c Y βΉ
β¨x,yaβ© ββX Γβ©c Yβ (graph f, graph_morph f)
βΉ y = ya"
using assms
by (smt (z3) comp_associative2 equalizer_def factors_through_def2 graph_equalizer4 left_cart_proj_cfunc_prod left_cart_proj_type relative_member_def2 right_cart_proj_cfunc_prod)
qed
lemma functional_on_isomorphism:
assumes "functional_on X Y (R,m)"
shows "isomorphism(left_cart_proj X Y ββ©c m)"
proof-
have m_mono: "monomorphism(m)"
using assms functional_on_def subobject_of_def2 by blast
have pi0_m_type[type_rule]: "left_cart_proj X Y ββ©c m : R β X"
using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
have surj: "surjective(left_cart_proj X Y ββ©c m)"
unfolding surjective_def
proof(clarify)
fix x
assume "x ββ©c codomain (left_cart_proj X Y ββ©c m)"
then have [type_rule]: "x ββ©c X"
using cfunc_type_def pi0_m_type by force
then have "β! y. (y ββ©c Y β§ β¨x,yβ© ββXΓβ©cYβ (R,m))"
using assms functional_on_def by force
then show "βz. z ββ©c domain (left_cart_proj X Y ββ©c m) β§ (left_cart_proj X Y ββ©c m) ββ©c z = x"
by (typecheck_cfuncs, smt (verit, best) cfunc_type_def comp_associative factors_through_def2 left_cart_proj_cfunc_prod relative_member_def2)
qed
have inj: "injective(left_cart_proj X Y ββ©c m)"
proof(unfold injective_def, clarify)
fix r1 r2
assume "r1 ββ©c domain (left_cart_proj X Y ββ©c m)" then have r1_type[type_rule]: "r1 ββ©c R"
by (metis cfunc_type_def pi0_m_type)
assume "r2 ββ©c domain (left_cart_proj X Y ββ©c m)" then have r2_type[type_rule]: "r2 ββ©c R"
by (metis cfunc_type_def pi0_m_type)
assume "(left_cart_proj X Y ββ©c m) ββ©c r1 = (left_cart_proj X Y ββ©c m) ββ©c r2"
then have eq: "left_cart_proj X Y ββ©c m ββ©c r1 = left_cart_proj X Y ββ©c m ββ©c r2"
using assms cfunc_type_def comp_associative functional_on_def subobject_of_def2 by (typecheck_cfuncs, auto)
have mx_type[type_rule]: "m ββ©c r1 ββ©c XΓβ©cY"
using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
then obtain x1 and y1 where m1r1_eqs: "m ββ©c r1 = β¨x1, y1β© β§ x1 ββ©c X β§ y1 ββ©c Y"
using cart_prod_decomp by presburger
have my_type[type_rule]: "m ββ©c r2 ββ©c XΓβ©cY"
using assms functional_on_def subobject_of_def2 by (typecheck_cfuncs, blast)
then obtain x2 and y2 where m2r2_eqs:"m ββ©c r2 = β¨x2, y2β© β§ x2 ββ©c X β§ y2 ββ©c Y"
using cart_prod_decomp by presburger
have x_equal: "x1 = x2"
using eq left_cart_proj_cfunc_prod m1r1_eqs m2r2_eqs by force
have functional: "β! y. (y ββ©c Y β§ β¨x1,yβ© ββXΓβ©cYβ (R,m))"
using assms functional_on_def m1r1_eqs by force
then have y_equal: "y1 = y2"
by (metis prod.sel factors_through_def2 m1r1_eqs m2r2_eqs mx_type my_type r1_type r2_type relative_member_def x_equal)
then show "r1 = r2"
by (metis functional cfunc_type_def m1r1_eqs m2r2_eqs monomorphism_def r1_type r2_type relative_member_def2 x_equal)
qed
show "isomorphism(left_cart_proj X Y ββ©c m)"
by (metis epi_mon_is_iso inj injective_imp_monomorphism surj surjective_is_epimorphism)
qed
text βΉThe lemma below corresponds to Proposition 2.3.14 in Halvorson.βΊ
lemma functional_relations_are_graphs:
assumes "functional_on X Y (R,m)"
shows "β! f. f : X β Y β§
(β i. i : R β graph(f) β§ isomorphism(i) β§ m = graph_morph(f) ββ©c i)"
proof safe
have m_type[type_rule]: "m : R β X Γβ©c Y"
using assms unfolding functional_on_def subobject_of_def2 by auto
have m_mono[type_rule]: "monomorphism(m)"
using assms functional_on_def subobject_of_def2 by blast
have isomorphism[type_rule]: "isomorphism(left_cart_proj X Y ββ©c m)"
using assms functional_on_isomorphism by force
obtain h where h_type[type_rule]: "h: X β R" and h_def: "h = (left_cart_proj X Y ββ©c m)βΒ―"
by (typecheck_cfuncs, simp)
obtain f where f_def: "f = (right_cart_proj X Y) ββ©c m ββ©c h"
by auto
then have f_type[type_rule]: "f : X β Y"
by (metis assms comp_type f_def functional_on_def h_type right_cart_proj_type subobject_of_def2)
have eq: "f ββ©c left_cart_proj X Y ββ©c m = right_cart_proj X Y ββ©c m"
unfolding f_def h_def by (typecheck_cfuncs, smt comp_associative2 id_right_unit2 inv_left isomorphism)
show "βf. f : X β Y β§ (βi. i : R β graph f β§ isomorphism i β§ m = graph_morph f ββ©c i)"
proof (intro exI[where x=f], safe, typecheck_cfuncs)
have graph_equalizer: "equalizer (graph f) (graph_morph f) (f ββ©c left_cart_proj X Y) (right_cart_proj X Y)"
by (simp add: f_type graph_equalizer4)
then have "βh F. h : F β X Γβ©c Y β§ (f ββ©c left_cart_proj X Y) ββ©c h = right_cart_proj X Y ββ©c h βΆ
(β!k. k : F β graph f β§ graph_morph f ββ©c k = h)"
unfolding equalizer_def using cfunc_type_def by (typecheck_cfuncs, auto)
then obtain i where i_type[type_rule]: "i : R β graph f" and i_eq: "graph_morph f ββ©c i = m"
by (typecheck_cfuncs, smt comp_associative2 eq left_cart_proj_type)
have "surjective i"
proof (etcs_subst surjective_def2, clarify)
fix y'
assume y'_type[type_rule]: "y' ββ©c graph f"
define x where "x = left_cart_proj X Y ββ©c graph_morph(f) ββ©c y'"
then have x_type[type_rule]: "x ββ©c X"
unfolding x_def by typecheck_cfuncs
obtain y where y_type[type_rule]: "y ββ©c Y" and x_y_in_R: "β¨x,yβ© ββX Γβ©c Yβ (R, m)"
and y_unique: "β z. (z ββ©c Y β§ β¨x,zβ© ββX Γβ©c Yβ (R, m)) βΆ z = y"
by (metis assms functional_on_def x_type)
obtain x' where x'_type[type_rule]: "x' ββ©c R" and x'_eq: "m ββ©c x' = β¨x, yβ©"
using x_y_in_R unfolding relative_member_def2 by (-, etcs_subst_asm factors_through_def2, auto)
have "graph_morph(f) ββ©c i ββ©c x' = graph_morph(f) ββ©c y'"
proof (typecheck_cfuncs, rule cart_prod_eqI, safe)
show left: "left_cart_proj X Y ββ©c graph_morph f ββ©c i ββ©c x' = left_cart_proj X Y ββ©c graph_morph f ββ©c y'"
proof -
have "left_cart_proj X Y ββ©c graph_morph(f) ββ©c i ββ©c x' = left_cart_proj X Y ββ©c m ββ©c x'"
by (typecheck_cfuncs, smt comp_associative2 i_eq)
also have "... = x"
unfolding x'_eq using left_cart_proj_cfunc_prod by (typecheck_cfuncs, blast)
also have "... = left_cart_proj X Y ββ©c graph_morph f ββ©c y'"
unfolding x_def by auto
finally show ?thesis.
qed
show "right_cart_proj X Y ββ©c graph_morph f ββ©c i ββ©c x' = right_cart_proj X Y ββ©c graph_morph f ββ©c y'"
proof -
have "right_cart_proj X Y ββ©c graph_morph f ββ©c i ββ©c x' = f ββ©c left_cart_proj X Y ββ©c graph_morph f ββ©c i ββ©c x'"
by (etcs_assocl, typecheck_cfuncs, metis graph_equalizer equalizer_eq)
also have "... = f ββ©c left_cart_proj X Y ββ©c graph_morph f ββ©c y'"
by (subst left, simp)
also have "... = right_cart_proj X Y ββ©c graph_morph f ββ©c y'"
by (etcs_assocl, typecheck_cfuncs, metis graph_equalizer equalizer_eq)
finally show ?thesis.
qed
qed
then have "i ββ©c x' = y'"
using equalizer_is_monomorphism graph_equalizer monomorphism_def2 by (typecheck_cfuncs_prems, blast)
then show "βx'. x' ββ©c R β§ i ββ©c x' = y'"
by (intro exI[where x=x'], simp add: x'_type)
qed
then have "isomorphism i"
by (metis comp_monic_imp_monic' epi_mon_is_iso f_type graph_morph_type i_eq i_type m_mono surjective_is_epimorphism)
then show "βi. i : R β graph f β§ isomorphism i β§ m = graph_morph f ββ©c i"
by (intro exI[where x=i], simp add: i_type i_eq)
qed
next
fix f1 f2 i1 i2
assume f1_type[type_rule]: "f1 : X β Y"
assume f2_type[type_rule]: "f2 : X β Y"
assume i1_type[type_rule]: "i1 : R β graph f1"
assume i2_type[type_rule]: "i2 : R β graph f2"
assume i1_iso: "isomorphism i1"
assume i2_iso: "isomorphism i2"
assume eq1: "m = graph_morph f1 ββ©c i1"
assume eq2: "graph_morph f1 ββ©c i1 = graph_morph f2 ββ©c i2"
have m_type[type_rule]: "m : R β X Γβ©c Y"
using assms unfolding functional_on_def subobject_of_def2 by auto
have isomorphism[type_rule]: "isomorphism(left_cart_proj X Y ββ©c m)"
using assms functional_on_isomorphism by force
obtain h where h_type[type_rule]: "h: X β R" and h_def: "h = (left_cart_proj X Y ββ©c m)βΒ―"
by (typecheck_cfuncs, simp)
have "f1 ββ©c left_cart_proj X Y ββ©c m = f2 ββ©c left_cart_proj X Y ββ©c m"
proof -
have "f1 ββ©c left_cart_proj X Y ββ©c m = (f1 ββ©c left_cart_proj X Y) ββ©c graph_morph f1 ββ©c i1"
using comp_associative2 eq1 eq2 by (typecheck_cfuncs, force)
also have "... = (right_cart_proj X Y) ββ©c graph_morph f1 ββ©c i1"
by (typecheck_cfuncs, smt comp_associative2 equalizer_def graph_equalizer4)
also have "... = (right_cart_proj X Y) ββ©c graph_morph f2 ββ©c i2"
by (simp add: eq2)
also have "... = (f2 ββ©c left_cart_proj X Y) ββ©c graph_morph f2 ββ©c i2"
by (typecheck_cfuncs, smt comp_associative2 equalizer_eq graph_equalizer4)
also have "... = f2 ββ©c left_cart_proj X Y ββ©c m"
by (typecheck_cfuncs, metis comp_associative2 eq1 eq2)
finally show ?thesis.
qed
then show "f1 = f2"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative h_def h_type id_right_unit2 inverse_def2 isomorphism)
qed
end