Theory Equalizer
section ‹Equalizers and Subobjects›
theory Equalizer
imports Terminal
begin
subsection ‹Equalizers›
definition equalizer :: "cset ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ bool" where
"equalizer E m f g ⟷ (∃ X Y. (f : X → Y) ∧ (g : X → Y) ∧ (m : E → X)
∧ (f ∘⇩c m = g ∘⇩c m)
∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h)))"
lemma equalizer_def2:
assumes "f : X → Y" "g : X → Y" "m : E → X"
shows "equalizer E m f g ⟷ ((f ∘⇩c m = g ∘⇩c m)
∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h)))"
using assms unfolding equalizer_def by (auto simp add: cfunc_type_def)
lemma equalizer_eq:
assumes "f : X → Y" "g : X → Y" "m : E → X"
assumes "equalizer E m f g"
shows "f ∘⇩c m = g ∘⇩c m"
using assms equalizer_def2 by auto
lemma similar_equalizers:
assumes "f : X → Y" "g : X → Y" "m : E → X"
assumes "equalizer E m f g"
assumes "h : F → X" "f ∘⇩c h = g ∘⇩c h"
shows "∃! k. k : F → E ∧ m ∘⇩c k = h"
using assms equalizer_def2 by auto
text ‹The definition above and the axiomatization below correspond to Axiom 4 (Equalizers) in Halvorson.›
axiomatization where
equalizer_exists: "f : X → Y ⟹ g : X → Y ⟹ ∃ E m. equalizer E m f g"
lemma equalizer_exists2:
assumes "f : X → Y" "g : X → Y"
shows "∃ E m. m : E → X ∧ f ∘⇩c m = g ∘⇩c m ∧ (∀ h F. ((h : F → X) ∧ (f ∘⇩c h = g ∘⇩c h)) ⟶ (∃! k. (k : F → E) ∧ m ∘⇩c k = h))"
proof -
obtain E m where "equalizer E m f g"
using assms equalizer_exists by blast
then show ?thesis
unfolding equalizer_def
proof (intro exI[where x=E], intro exI[where x=m], safe)
fix X' Y'
assume f_type2: "f : X' → Y'"
assume g_type2: "g : X' → Y'"
assume m_type: "m : E → X'"
assume fm_eq_gm: "f ∘⇩c m = g ∘⇩c m"
assume equalizer_unique: "∀h F. h : F → X' ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E ∧ m ∘⇩c k = h)"
show m_type2: "m : E → X"
using assms(2) cfunc_type_def g_type2 m_type by auto
show "⋀ h F. h : F → X ⟹ f ∘⇩c h = g ∘⇩c h ⟹ ∃k. k : F → E ∧ m ∘⇩c k = h"
by (metis m_type2 cfunc_type_def equalizer_unique m_type)
show "⋀ F k y. m ∘⇩c k : F → X ⟹ f ∘⇩c m ∘⇩c k = g ∘⇩c m ∘⇩c k ⟹ k : F → E ⟹ y : F → E
⟹ m ∘⇩c y = m ∘⇩c k ⟹ k = y"
using comp_type equalizer_unique m_type by blast
qed
qed
text ‹The lemma below corresponds to Exercise 2.1.31 in Halvorson.›
lemma equalizers_isomorphic:
assumes "equalizer E m f g" "equalizer E' m' f g"
shows "∃ k. k : E → E' ∧ isomorphism k ∧ m = m' ∘⇩c k"
proof -
have fm_eq_gm: "f ∘⇩c m = g ∘⇩c m"
using assms(1) equalizer_def by blast
have fm'_eq_gm': "f ∘⇩c m' = g ∘⇩c m'"
using assms(2) equalizer_def by blast
obtain X Y where f_type: "f : X → Y" and g_type: "g : X → Y" and m_type: "m : E → X"
using assms(1) unfolding equalizer_def by auto
obtain k where k_type: "k : E' → E" and mk_eq_m': "m ∘⇩c k = m'"
by (metis assms cfunc_type_def equalizer_def)
obtain k' where k'_type: "k' : E → E'" and m'k_eq_m: "m' ∘⇩c k' = m"
by (metis assms cfunc_type_def equalizer_def)
have "f ∘⇩c m ∘⇩c k ∘⇩c k' = g ∘⇩c m ∘⇩c k ∘⇩c k'"
using comp_associative2 m_type fm_eq_gm k'_type k_type m'k_eq_m mk_eq_m' by auto
have "k ∘⇩c k' : E → E ∧ m ∘⇩c k ∘⇩c k' = m"
using comp_associative2 comp_type k'_type k_type m_type m'k_eq_m mk_eq_m' by auto
then have kk'_eq_id: "k ∘⇩c k' = id E"
using assms(1) equalizer_def id_right_unit2 id_type by blast
have "k' ∘⇩c k : E' → E' ∧ m' ∘⇩c k' ∘⇩c k = m'"
by (smt comp_associative2 comp_type k'_type k_type m'k_eq_m m_type mk_eq_m')
then have k'k_eq_id: "k' ∘⇩c k = id E'"
using assms(2) equalizer_def id_right_unit2 id_type by blast
show "∃k. k : E → E' ∧ isomorphism k ∧ m = m' ∘⇩c k"
using cfunc_type_def isomorphism_def k'_type k'k_eq_id k_type kk'_eq_id m'k_eq_m by (intro exI[where x=k'], auto)
qed
lemma isomorphic_to_equalizer_is_equalizer:
assumes "φ: E' → E"
assumes "isomorphism φ"
assumes "equalizer E m f g"
assumes "f : X → Y"
assumes "g : X → Y"
assumes "m : E → X"
shows "equalizer E' (m ∘⇩c φ) f g"
proof -
obtain φ_inv where φ_inv_type[type_rule]: "φ_inv : E → E'" and φ_inv_φ: "φ_inv ∘⇩c φ = id(E')" and φφ_inv: "φ ∘⇩c φ_inv = id(E)"
using assms(1,2) cfunc_type_def isomorphism_def by auto
have equalizes: "f ∘⇩c m ∘⇩c φ = g ∘⇩c m ∘⇩c φ"
using assms comp_associative2 equalizer_def by force
have "∀h F. h : F → X ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E' ∧ (m ∘⇩c φ) ∘⇩c k = h)"
proof(safe)
fix h F
assume h_type[type_rule]: "h : F → X"
assume h_equalizes: "f ∘⇩c h = g ∘⇩c h"
have k_exists_uniquely: "∃! k. k: F → E ∧ m ∘⇩c k = h"
using assms equalizer_def2 h_equalizes by (typecheck_cfuncs, auto)
then obtain k where k_type[type_rule]: "k: F → E" and k_def: "m ∘⇩c k = h"
by blast
then show "∃k. k : F → E' ∧ (m ∘⇩c φ) ∘⇩c k = h"
using assms by (typecheck_cfuncs, smt (z3) φφ_inv φ_inv_type comp_associative2 comp_type id_right_unit2 k_exists_uniquely)
next
fix F k y
assume "(m ∘⇩c φ) ∘⇩c k : F → X"
assume "f ∘⇩c (m ∘⇩c φ) ∘⇩c k = g ∘⇩c (m ∘⇩c φ) ∘⇩c k"
assume k_type[type_rule]: "k : F → E'"
assume y_type[type_rule]: "y : F → E'"
assume "(m ∘⇩c φ) ∘⇩c y = (m ∘⇩c φ) ∘⇩c k"
then show "k = y"
by (typecheck_cfuncs, smt (verit, ccfv_threshold) assms(1,2,3) cfunc_type_def comp_associative comp_type equalizer_def id_left_unit2 isomorphism_def)
qed
then show ?thesis
by (smt (verit, best) assms(1,4,5,6) comp_type equalizer_def equalizes)
qed
text ‹The lemma below corresponds to Exercise 2.1.34 in Halvorson.›
lemma equalizer_is_monomorphism:
"equalizer E m f g ⟹ monomorphism(m)"
unfolding equalizer_def monomorphism_def
proof clarify
fix h1 h2 X Y
assume f_type: "f : X → Y"
assume g_type: "g : X → Y"
assume m_type: "m : E → X"
assume fm_gm: "f ∘⇩c m = g ∘⇩c m"
assume uniqueness: "∀h F. h : F → X ∧ f ∘⇩c h = g ∘⇩c h ⟶ (∃!k. k : F → E ∧ m ∘⇩c k = h)"
assume relation_ga: "codomain h1 = domain m"
assume relation_h: "codomain h2 = domain m"
assume m_ga_mh: "m ∘⇩c h1 = m ∘⇩c h2"
have "f ∘⇩c m ∘⇩c h1 = g ∘⇩c m ∘⇩c h2"
using cfunc_type_def comp_associative f_type fm_gm g_type m_ga_mh m_type relation_h by auto
then obtain z where "z: domain(h1) → E ∧ m ∘⇩c z = m ∘⇩c h1 ∧
(∀ j. j:domain(h1) → E ∧ m ∘⇩c j = m ∘⇩c h1 ⟶ j = z)"
using uniqueness by (smt cfunc_type_def codomain_comp domain_comp m_ga_mh m_type relation_ga)
then show "h1 = h2"
by (metis cfunc_type_def domain_comp m_ga_mh m_type relation_ga relation_h)
qed
text ‹The definition below corresponds to Definition 2.1.35 in Halvorson.›
definition regular_monomorphism :: "cfunc ⇒ bool"
where "regular_monomorphism f ⟷
(∃ g h. domain g = codomain f ∧ domain h = codomain f ∧ equalizer (domain f) f g h)"
text ‹The lemma below corresponds to Exercise 2.1.36 in Halvorson.›
lemma epi_regmon_is_iso:
assumes "epimorphism f" "regular_monomorphism f"
shows "isomorphism f"
proof -
obtain g h where g_type: "domain g = codomain f" and
h_type: "domain h = codomain f" and
f_equalizer: "equalizer (domain f) f g h"
using assms(2) regular_monomorphism_def by auto
then have "g ∘⇩c f = h ∘⇩c f"
using equalizer_def by blast
then have "g = h"
using assms(1) cfunc_type_def epimorphism_def equalizer_def f_equalizer by auto
then have "g ∘⇩c id(codomain f) = h ∘⇩c id(codomain f)"
by simp
then obtain k where k_type: "f ∘⇩c k = id(codomain(f)) ∧ codomain k = domain f"
by (metis cfunc_type_def equalizer_def f_equalizer id_type)
then have "f ∘⇩c id(domain(f)) = f ∘⇩c (k ∘⇩c f)"
by (metis comp_associative domain_comp id_domain id_left_unit id_right_unit)
then have "monomorphism f ⟹ k ∘⇩c f = id(domain f)"
by (metis (mono_tags) codomain_comp domain_comp id_codomain id_domain k_type monomorphism_def)
then have "k ∘⇩c f = id(domain f)"
using equalizer_is_monomorphism f_equalizer by blast
then show "isomorphism f"
by (metis domain_comp id_domain isomorphism_def k_type)
qed
subsection ‹Subobjects›
text ‹The definition below corresponds to Definition 2.1.32 in Halvorson.›
definition factors_through :: "cfunc ⇒ cfunc ⇒ bool" (infix "factorsthru" 90)
where "g factorsthru f ⟷ (∃ h. (h: domain(g)→ domain(f)) ∧ f ∘⇩c h = g)"
lemma factors_through_def2:
assumes "g : X → Z" "f : Y → Z"
shows "g factorsthru f ⟷ (∃ h. h: X → Y ∧ f ∘⇩c h = g)"
unfolding factors_through_def using assms by (simp add: cfunc_type_def)
text ‹The lemma below corresponds to Exercise 2.1.33 in Halvorson.›
lemma xfactorthru_equalizer_iff_fx_eq_gx:
assumes "f: X→ Y" "g:X → Y" "equalizer E m f g" "x∈⇩c X"
shows "x factorsthru m ⟷ f ∘⇩c x = g ∘⇩c x"
proof safe
assume LHS: "x factorsthru m"
then show "f ∘⇩c x = g ∘⇩c x"
using assms(3) cfunc_type_def comp_associative equalizer_def factors_through_def by auto
next
assume RHS: "f ∘⇩c x = g ∘⇩c x"
then show "x factorsthru m"
unfolding cfunc_type_def factors_through_def
by (metis RHS assms(1,3,4) cfunc_type_def equalizer_def)
qed
text ‹The definition below corresponds to Definition 2.1.37 in Halvorson.›
definition subobject_of :: "cset × cfunc ⇒ cset ⇒ bool" (infix "⊆⇩c" 50)
where "B ⊆⇩c X ⟷ (snd B : fst B → X ∧ monomorphism (snd B))"
lemma subobject_of_def2:
"(B,m) ⊆⇩c X = (m : B → X ∧ monomorphism m)"
by (simp add: subobject_of_def)
definition relative_subset :: "cset × cfunc ⇒ cset ⇒ cset × cfunc ⇒ bool" ("_⊆⇘_⇙_" [51,50,51]50)
where "B ⊆⇘X⇙ A ⟷
(snd B : fst B → X ∧ monomorphism (snd B) ∧ snd A : fst A → X ∧ monomorphism (snd A)
∧ (∃ k. k: fst B → fst A ∧ snd A ∘⇩c k = snd B))"
lemma relative_subset_def2:
"(B,m) ⊆⇘X⇙ (A,n) = (m : B → X ∧ monomorphism m ∧ n : A → X ∧ monomorphism n
∧ (∃ k. k: B → A ∧ n ∘⇩c k = m))"
unfolding relative_subset_def by auto
lemma subobject_is_relative_subset: "(B,m) ⊆⇩c A ⟷ (B,m) ⊆⇘A⇙ (A, id(A))"
unfolding relative_subset_def2 subobject_of_def2
using cfunc_type_def id_isomorphism id_left_unit id_type iso_imp_epi_and_monic by auto
text ‹The definition below corresponds to Definition 2.1.39 in Halvorson.›
definition relative_member :: "cfunc ⇒ cset ⇒ cset × cfunc ⇒ bool" ("_ ∈⇘_⇙ _" [51,50,51]50) where
"x ∈⇘X⇙ B ⟷ (x ∈⇩c X ∧ monomorphism (snd B) ∧ snd B : fst B → X ∧ x factorsthru (snd B))"
lemma relative_member_def2:
"x ∈⇘X⇙ (B, m) = (x ∈⇩c X ∧ monomorphism m ∧ m : B → X ∧ x factorsthru m)"
unfolding relative_member_def by auto
text ‹The lemma below corresponds to Proposition 2.1.40 in Halvorson.›
lemma relative_subobject_member:
assumes "(A,n) ⊆⇘X⇙ (B,m)" "x ∈⇩c X"
shows "x ∈⇘X⇙ (A,n) ⟹ x ∈⇘X⇙ (B,m)"
using assms unfolding relative_member_def2 relative_subset_def2
proof clarify
fix k
assume m_type: "m : B → X"
assume k_type: "k : A → B"
assume m_monomorphism: "monomorphism m"
assume mk_monomorphism: "monomorphism (m ∘⇩c k)"
assume n_eq_mk: "n = m ∘⇩c k"
assume factorsthru_mk: "x factorsthru (m ∘⇩c k)"
obtain a where a_assms: "a ∈⇩c A ∧ (m ∘⇩c k) ∘⇩c a = x"
using assms(2) cfunc_type_def domain_comp factors_through_def factorsthru_mk k_type m_type by auto
then show "x factorsthru m "
unfolding factors_through_def
using cfunc_type_def comp_type k_type m_type comp_associative
by (intro exI[where x="k ∘⇩c a"], auto)
qed
subsection ‹Inverse Image›
text‹The definition below corresponds to a definition given by a diagram between Definition 2.1.37 and Proposition 2.1.38 in Halvorson.›
definition inverse_image :: "cfunc ⇒ cset ⇒ cfunc ⇒ cset" ("_⇧-⇧1⦇_⦈⇘_⇙" [101,0,0]100) where
"inverse_image f B m = (SOME A. ∃ X Y k. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
equalizer A k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B))"
lemma inverse_image_is_equalizer:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "∃k. equalizer (f⇧-⇧1⦇B⦈⇘m⇙) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
proof -
obtain A k where "equalizer A k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
by (meson assms(1,2) comp_type equalizer_exists left_cart_proj_type right_cart_proj_type)
then show "∃k. equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
unfolding inverse_image_def using assms cfunc_type_def by (subst someI2_ex, auto)
qed
definition inverse_image_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc" where
"inverse_image_mapping f B m = (SOME k. ∃ X Y. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B))"
lemma inverse_image_is_equalizer2:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
proof -
obtain k where "equalizer (inverse_image f B m) k (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
using assms inverse_image_is_equalizer by blast
then have "∃ X Y. f : X → Y ∧ m : B → Y ∧ monomorphism m ∧
equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
unfolding inverse_image_mapping_def using assms by (subst someI_ex, auto)
then show "equalizer (inverse_image f B m) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B)"
using assms(2) cfunc_type_def by auto
qed
lemma inverse_image_mapping_type[type_rule]:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "inverse_image_mapping f B m : (inverse_image f B m) → X ×⇩c B"
using assms cfunc_type_def domain_comp equalizer_def inverse_image_is_equalizer2 left_cart_proj_type by auto
lemma inverse_image_mapping_eq:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m
= m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m"
using assms cfunc_type_def comp_associative equalizer_def inverse_image_is_equalizer2
by (typecheck_cfuncs, smt (verit))
lemma inverse_image_mapping_monomorphism:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "monomorphism (inverse_image_mapping f B m)"
using assms equalizer_is_monomorphism inverse_image_is_equalizer2 by blast
text ‹The lemma below is the dual of Proposition 2.1.38 in Halvorson.›
lemma inverse_image_monomorphism:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "monomorphism (left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
fix g h A
assume g_type: "g : A → (f⇧-⇧1⦇B⦈⇘m⇙)"
assume h_type: "h : A → (f⇧-⇧1⦇B⦈⇘m⇙)"
assume left_eq: "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
= (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
then have "f ∘⇩c (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
= f ∘⇩c (left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
by auto
then have "m ∘⇩c (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
= m ∘⇩c (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
using assms g_type h_type
by (typecheck_cfuncs, smt cfunc_type_def codomain_comp comp_associative domain_comp inverse_image_mapping_eq left_cart_proj_type)
then have right_eq: "(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c g
= (right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
using assms g_type h_type monomorphism_def3 by (typecheck_cfuncs, auto)
then have "inverse_image_mapping f B m ∘⇩c g = inverse_image_mapping f B m ∘⇩c h"
using assms g_type h_type cfunc_type_def comp_associative left_eq left_cart_proj_type right_cart_proj_type
by (typecheck_cfuncs, subst cart_prod_eq, auto)
then show "g = h"
using assms g_type h_type inverse_image_mapping_monomorphism inverse_image_mapping_type monomorphism_def3
by blast
qed
definition inverse_image_subobject_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc" ("[_⇧-⇧1⦇_⦈⇘_⇙]map" [101,0,0]100) where
"[f⇧-⇧1⦇B⦈⇘m⇙]map = left_cart_proj (domain f) B ∘⇩c inverse_image_mapping f B m"
lemma inverse_image_subobject_mapping_def2:
assumes "f : X → Y"
shows "[f⇧-⇧1⦇B⦈⇘m⇙]map = left_cart_proj X B ∘⇩c inverse_image_mapping f B m"
using assms unfolding inverse_image_subobject_mapping_def cfunc_type_def by auto
lemma inverse_image_subobject_mapping_type[type_rule]:
assumes "f : X → Y" "m : B → Y" "monomorphism m"
shows "[f⇧-⇧1⦇B⦈⇘m⇙]map : f⇧-⇧1⦇B⦈⇘m⇙ → X"
by (smt (verit, best) assms comp_type inverse_image_mapping_type inverse_image_subobject_mapping_def2 left_cart_proj_type)
lemma inverse_image_subobject_mapping_mono:
assumes "f : X → Y" "m : B → Y" "monomorphism m"
shows "monomorphism ([f⇧-⇧1⦇B⦈⇘m⇙]map)"
using assms cfunc_type_def inverse_image_monomorphism inverse_image_subobject_mapping_def by fastforce
lemma inverse_image_subobject:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "(f⇧-⇧1⦇B⦈⇘m⇙, [f⇧-⇧1⦇B⦈⇘m⇙]map) ⊆⇩c X"
unfolding subobject_of_def2
using assms inverse_image_subobject_mapping_mono inverse_image_subobject_mapping_type
by force
lemma inverse_image_pullback:
assumes "m : B → Y" "f : X → Y" "monomorphism m"
shows "is_pullback (f⇧-⇧1⦇B⦈⇘m⇙) B X Y
(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) m
(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) f"
unfolding is_pullback_def using assms
proof safe
show right_type: "right_cart_proj X B ∘⇩c inverse_image_mapping f B m : f⇧-⇧1⦇B⦈⇘m⇙ → B"
using assms cfunc_type_def codomain_comp domain_comp inverse_image_mapping_type
right_cart_proj_type by auto
show left_type: "left_cart_proj X B ∘⇩c inverse_image_mapping f B m : f⇧-⇧1⦇B⦈⇘m⇙ → X"
using assms fst_conv inverse_image_subobject subobject_of_def by (typecheck_cfuncs)
show "m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m =
f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m"
using assms inverse_image_mapping_eq by auto
next
fix Z k h
assume k_type: "k : Z → B" and h_type: "h : Z → X"
assume mk_eq_fh: "m ∘⇩c k = f ∘⇩c h"
have "equalizer (f⇧-⇧1⦇B⦈⇘m⇙) (inverse_image_mapping f B m) (f ∘⇩c left_cart_proj X B) (m ∘⇩c right_cart_proj X B )"
using assms inverse_image_is_equalizer2 by blast
then have "∀h F. h : F → (X ×⇩c B)
∧ (f ∘⇩c left_cart_proj X B) ∘⇩c h = (m ∘⇩c right_cart_proj X B) ∘⇩c h ⟶
(∃!u. u : F → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = h)"
unfolding equalizer_def using assms(2) cfunc_type_def domain_comp left_cart_proj_type by auto
then have "⟨h,k⟩ : Z → X ×⇩c B ⟹
(f ∘⇩c left_cart_proj X B) ∘⇩c ⟨h,k⟩ = (m ∘⇩c right_cart_proj X B) ∘⇩c ⟨h,k⟩ ⟹
(∃!u. u : Z → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩)"
by auto
then have "∃!u. u : Z → (f⇧-⇧1⦇B⦈⇘m⇙) ∧ inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩"
using k_type h_type assms
by (typecheck_cfuncs, smt comp_associative2 left_cart_proj_cfunc_prod left_cart_proj_type
mk_eq_fh right_cart_proj_cfunc_prod right_cart_proj_type)
then show "∃j. j : Z → (f⇧-⇧1⦇B⦈⇘m⇙) ∧
(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = k ∧
(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = h"
proof (clarify)
fix u
assume u_type[type_rule]: "u : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
assume u_eq: "inverse_image_mapping f B m ∘⇩c u = ⟨h,k⟩"
show "∃j. j : Z → f⇧-⇧1⦇B⦈⇘m⇙ ∧
(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = k ∧
(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = h"
proof (rule exI[where x=u], typecheck_cfuncs, safe)
show "(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c u = k"
using assms u_type h_type k_type u_eq
by (typecheck_cfuncs, metis (full_types) comp_associative2 right_cart_proj_cfunc_prod)
show "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c u = h"
using assms u_type h_type k_type u_eq
by (typecheck_cfuncs, metis (full_types) comp_associative2 left_cart_proj_cfunc_prod)
qed
qed
next
fix Z j y
assume j_type: "j : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
assume y_type: "y : Z → (f⇧-⇧1⦇B⦈⇘m⇙)"
assume "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c y =
(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j"
then show "j = y"
using assms j_type y_type inverse_image_mapping_type comp_type
by (smt (verit, ccfv_threshold) inverse_image_monomorphism left_cart_proj_type monomorphism_def3)
qed
text ‹The lemma below corresponds to Proposition 2.1.41 in Halvorson.›
lemma in_inverse_image:
assumes "f : X → Y" "(B,m) ⊆⇩c Y" "x ∈⇩c X"
shows "(x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)) = (f ∘⇩c x ∈⇘Y⇙ (B,m))"
proof
have m_type: "m : B → Y" "monomorphism m"
using assms(2) unfolding subobject_of_def2 by auto
assume "x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
then obtain h where h_type: "h ∈⇩c (f⇧-⇧1⦇B⦈⇘m⇙)"
and h_def: "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h = x"
unfolding relative_member_def2 factors_through_def by (auto simp add: cfunc_type_def)
then have "f ∘⇩c x = f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"
using assms m_type by (typecheck_cfuncs, simp add: comp_associative2 h_def)
then have "f ∘⇩c x = (f ∘⇩c left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
using assms m_type h_type h_def comp_associative2 by (typecheck_cfuncs, blast)
then have "f ∘⇩c x = (m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c h"
using assms h_type m_type by (typecheck_cfuncs, simp add: inverse_image_mapping_eq m_type)
then have "f ∘⇩c x = m ∘⇩c right_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"
using assms m_type h_type by (typecheck_cfuncs, smt cfunc_type_def comp_associative domain_comp)
then have "(f ∘⇩c x) factorsthru m"
unfolding factors_through_def using assms h_type m_type
by (intro exI[where x="right_cart_proj X B ∘⇩c inverse_image_mapping f B m ∘⇩c h"],
typecheck_cfuncs, auto simp add: cfunc_type_def)
then show "f ∘⇩c x ∈⇘Y⇙ (B, m)"
unfolding relative_member_def2 using assms m_type by (typecheck_cfuncs, auto)
next
have m_type: "m : B → Y" "monomorphism m"
using assms(2) unfolding subobject_of_def2 by auto
assume "f ∘⇩c x ∈⇘Y⇙ (B, m)"
then have "∃h. h : domain (f ∘⇩c x) → domain m ∧ m ∘⇩c h = f ∘⇩c x"
unfolding relative_member_def2 factors_through_def by auto
then obtain h where h_type: "h ∈⇩c B" and h_def: "m ∘⇩c h = f ∘⇩c x"
unfolding relative_member_def2 factors_through_def
using assms cfunc_type_def domain_comp m_type by auto
then have "∃j. j ∈⇩c (f⇧-⇧1⦇B⦈⇘m⇙) ∧
(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = h ∧
(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c j = x"
using inverse_image_pullback assms m_type unfolding is_pullback_def by blast
then have "x factorsthru (left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
using m_type assms cfunc_type_def by (typecheck_cfuncs, unfold factors_through_def, auto)
then show "x ∈⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, left_cart_proj X B ∘⇩c inverse_image_mapping f B m)"
unfolding relative_member_def2 using m_type assms
by (typecheck_cfuncs, simp add: inverse_image_monomorphism)
qed
subsection ‹Fibered Products›
text ‹The definition below corresponds to Definition 2.1.42 in Halvorson.›
definition fibered_product :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cset" ("_ ⇘_⇙×⇩c⇘_⇙ _" [66,50,50,65]65) where
"X ⇘f⇙×⇩c⇘g⇙ Y = (SOME E. ∃ Z m. f : X → Z ∧ g : Y → Z ∧
equalizer E m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y))"
lemma fibered_product_equalizer:
assumes "f : X → Z" "g : Y → Z"
shows "∃ m. equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
proof -
obtain E m where "equalizer E m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
using assms equalizer_exists by (typecheck_cfuncs, blast)
then have "∃x Z m. f : X → Z ∧ g : Y → Z ∧
equalizer x m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
using assms by blast
then have "∃ Z m. f : X → Z ∧ g : Y → Z ∧
equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
unfolding fibered_product_def by (rule someI_ex)
then show "∃m. equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
by auto
qed
definition fibered_product_morphism :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
"fibered_product_morphism X f g Y = (SOME m. ∃ Z. f : X → Z ∧ g : Y → Z ∧
equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) m (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y))"
lemma fibered_product_morphism_equalizer:
assumes "f : X → Z" "g : Y → Z"
shows "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
proof -
have "∃x Z. f : X → Z ∧
g : Y → Z ∧ equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) x (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
using assms fibered_product_equalizer by blast
then have "∃Z. f : X → Z ∧ g : Y → Z ∧
equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
unfolding fibered_product_morphism_def by (rule someI_ex)
then show "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
by auto
qed
lemma fibered_product_morphism_type[type_rule]:
assumes "f : X → Z" "g : Y → Z"
shows "fibered_product_morphism X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → X ×⇩c Y"
using assms cfunc_type_def domain_comp equalizer_def fibered_product_morphism_equalizer left_cart_proj_type by auto
lemma fibered_product_morphism_monomorphism:
assumes "f : X → Z" "g : Y → Z"
shows "monomorphism (fibered_product_morphism X f g Y)"
using assms equalizer_is_monomorphism fibered_product_morphism_equalizer by blast
definition fibered_product_left_proj :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
"fibered_product_left_proj X f g Y = (left_cart_proj X Y) ∘⇩c (fibered_product_morphism X f g Y)"
lemma fibered_product_left_proj_type[type_rule]:
assumes "f : X → Z" "g : Y → Z"
shows "fibered_product_left_proj X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → X"
by (metis assms comp_type fibered_product_left_proj_def fibered_product_morphism_type left_cart_proj_type)
definition fibered_product_right_proj :: "cset ⇒ cfunc ⇒ cfunc ⇒ cset ⇒ cfunc" where
"fibered_product_right_proj X f g Y = (right_cart_proj X Y) ∘⇩c (fibered_product_morphism X f g Y)"
lemma fibered_product_right_proj_type[type_rule]:
assumes "f : X → Z" "g : Y → Z"
shows "fibered_product_right_proj X f g Y : X ⇘f⇙×⇩c⇘g⇙ Y → Y"
by (metis assms comp_type fibered_product_right_proj_def fibered_product_morphism_type right_cart_proj_type)
lemma pair_factorsthru_fibered_product_morphism:
assumes "f : X → Z" "g : Y → Z" "x : A → X" "y : A → Y"
shows "f ∘⇩c x = g ∘⇩c y ⟹ ⟨x,y⟩ factorsthru fibered_product_morphism X f g Y"
unfolding factors_through_def
proof -
have equalizer: "equalizer (X ⇘f⇙×⇩c⇘g⇙ Y) (fibered_product_morphism X f g Y) (f ∘⇩c left_cart_proj X Y) (g ∘⇩c right_cart_proj X Y)"
using fibered_product_morphism_equalizer assms by (typecheck_cfuncs, auto)
assume "f ∘⇩c x = g ∘⇩c y"
then have "(f ∘⇩c left_cart_proj X Y) ∘⇩c ⟨x,y⟩ = (g ∘⇩c right_cart_proj X Y) ∘⇩c ⟨x,y⟩"
using assms by (typecheck_cfuncs, smt comp_associative2 left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
then have "∃! h. h : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧ fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
using assms similar_equalizers by (typecheck_cfuncs, smt (verit, del_insts) cfunc_type_def equalizer equalizer_def)
then show "∃h. h : domain ⟨x,y⟩ → domain (fibered_product_morphism X f g Y) ∧
fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
by (metis assms(1,2) cfunc_type_def domain_comp fibered_product_morphism_type)
qed
lemma fibered_product_is_pullback:
assumes f_type[type_rule]: "f : X → Z" and g_type[type_rule]: "g : Y → Z"
shows "is_pullback (X ⇘f⇙×⇩c⇘g⇙ Y) Y X Z (fibered_product_right_proj X f g Y) g (fibered_product_left_proj X f g Y) f"
unfolding is_pullback_def
using assms fibered_product_left_proj_type fibered_product_right_proj_type
proof safe
show "g ∘⇩c fibered_product_right_proj X f g Y = f ∘⇩c fibered_product_left_proj X f g Y"
unfolding fibered_product_right_proj_def fibered_product_left_proj_def
using cfunc_type_def comp_associative2 equalizer_def fibered_product_morphism_equalizer
by (typecheck_cfuncs, auto)
next
fix A k h
assume k_type: "k : A → Y" and h_type: "h : A → X"
assume k_h_commutes: "g ∘⇩c k = f ∘⇩c h"
have "⟨h,k⟩ factorsthru fibered_product_morphism X f g Y"
using assms h_type k_h_commutes k_type pair_factorsthru_fibered_product_morphism by auto
then have f1: "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧ fibered_product_morphism X f g Y ∘⇩c j = ⟨h,k⟩"
by (meson assms cfunc_prod_type factors_through_def2 fibered_product_morphism_type h_type k_type)
then show "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧
fibered_product_right_proj X f g Y ∘⇩c j = k ∧ fibered_product_left_proj X f g Y ∘⇩c j = h"
unfolding fibered_product_right_proj_def fibered_product_left_proj_def
proof (clarify, safe)
fix j
assume j_type: "j : A → X ⇘f⇙×⇩c⇘g⇙ Y"
show "∃j. j : A → X ⇘f⇙×⇩c⇘g⇙ Y ∧
(right_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y) ∘⇩c j = k ∧ (left_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y) ∘⇩c j = h"
by (typecheck_cfuncs, smt (verit, best) f1 comp_associative2 h_type k_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod)
qed
next
fix A j y
assume j_type: "j : A → X ⇘f⇙×⇩c⇘g⇙ Y" and y_type: "y : A → X ⇘f⇙×⇩c⇘g⇙ Y"
assume "fibered_product_right_proj X f g Y ∘⇩c y = fibered_product_right_proj X f g Y ∘⇩c j"
then have right_eq: "right_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c y) =
right_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c j)"
unfolding fibered_product_right_proj_def using assms j_type y_type
by (typecheck_cfuncs, simp add: comp_associative2)
assume "fibered_product_left_proj X f g Y ∘⇩c y = fibered_product_left_proj X f g Y ∘⇩c j"
then have left_eq: "left_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c y) =
left_cart_proj X Y ∘⇩c (fibered_product_morphism X f g Y ∘⇩c j)"
unfolding fibered_product_left_proj_def using assms j_type y_type
by (typecheck_cfuncs, simp add: comp_associative2)
have mono: "monomorphism (fibered_product_morphism X f g Y)"
using assms fibered_product_morphism_monomorphism by auto
have "fibered_product_morphism X f g Y ∘⇩c y = fibered_product_morphism X f g Y ∘⇩c j"
using right_eq left_eq cart_prod_eq fibered_product_morphism_type y_type j_type assms comp_type
by (subst cart_prod_eq[where Z=A, where X=X, where Y=Y], auto)
then show "j = y"
using mono assms cfunc_type_def fibered_product_morphism_type j_type y_type
unfolding monomorphism_def
by auto
qed
lemma fibered_product_proj_eq:
assumes "f : X → Z" "g : Y → Z"
shows "f ∘⇩c fibered_product_left_proj X f g Y = g ∘⇩c fibered_product_right_proj X f g Y"
using fibered_product_is_pullback assms
unfolding is_pullback_def by auto
lemma fibered_product_pair_member:
assumes "f : X → Z" "g : Y → Z" "x ∈⇩c X" "y ∈⇩c Y"
shows "(⟨x, y⟩ ∈⇘X ×⇩c Y⇙ (X⇘f⇙×⇩c⇘g⇙Y, fibered_product_morphism X f g Y)) = (f ∘⇩c x = g ∘⇩c y)"
proof
assume "⟨x,y⟩ ∈⇘X ×⇩c Y⇙ (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)"
then obtain h where
h_type: "h ∈⇩c X⇘f⇙×⇩c⇘g⇙Y" and h_eq: "fibered_product_morphism X f g Y ∘⇩c h = ⟨x,y⟩"
unfolding relative_member_def2 factors_through_def
using assms(3,4) cfunc_prod_type cfunc_type_def by auto
have left_eq: "fibered_product_left_proj X f g Y ∘⇩c h = x"
unfolding fibered_product_left_proj_def
using assms h_type
by (typecheck_cfuncs, smt comp_associative2 h_eq left_cart_proj_cfunc_prod)
have right_eq: "fibered_product_right_proj X f g Y ∘⇩c h = y"
unfolding fibered_product_right_proj_def
using assms h_type
by (typecheck_cfuncs, smt comp_associative2 h_eq right_cart_proj_cfunc_prod)
have "f ∘⇩c fibered_product_left_proj X f g Y ∘⇩c h = g ∘⇩c fibered_product_right_proj X f g Y ∘⇩c h"
using assms h_type by (typecheck_cfuncs, simp add: comp_associative2 fibered_product_proj_eq)
then show "f ∘⇩c x = g ∘⇩c y"
using left_eq right_eq by auto
next
assume f_g_eq: "f ∘⇩c x = g ∘⇩c y"
show "⟨x,y⟩ ∈⇘X ×⇩c Y⇙ (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)"
unfolding relative_member_def factors_through_def
proof (safe)
show "⟨x,y⟩ ∈⇩c X ×⇩c Y"
using assms by typecheck_cfuncs
show "monomorphism (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y))"
using assms(1,2) fibered_product_morphism_monomorphism by auto
show "snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) : fst (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) → X ×⇩c Y"
using assms(1,2) fibered_product_morphism_type by force
have j_exists: "⋀ Z k h. k : Z → Y ⟹ h : Z → X ⟹ g ∘⇩c k = f ∘⇩c h ⟹
(∃!j. j : Z → X ⇘f⇙×⇩c⇘g⇙ Y ∧
fibered_product_right_proj X f g Y ∘⇩c j = k ∧
fibered_product_left_proj X f g Y ∘⇩c j = h)"
using fibered_product_is_pullback assms unfolding is_pullback_def by auto
obtain j where j_type: "j ∈⇩c X ⇘f⇙×⇩c⇘g⇙ Y" and
j_projs: "fibered_product_right_proj X f g Y ∘⇩c j = y" "fibered_product_left_proj X f g Y ∘⇩c j = x"
using j_exists[where Z=𝟭, where k=y, where h=x] assms f_g_eq by auto
show "∃h. h : domain ⟨x,y⟩ → domain (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y)) ∧
snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) ∘⇩c h = ⟨x,y⟩"
proof (intro exI[where x=j], safe)
show "j : domain ⟨x,y⟩ → domain (snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y))"
using assms j_type cfunc_type_def by (typecheck_cfuncs, auto)
have left_eq: "left_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y ∘⇩c j = x"
using j_projs assms j_type comp_associative2
unfolding fibered_product_left_proj_def by (typecheck_cfuncs, auto)
have right_eq: "right_cart_proj X Y ∘⇩c fibered_product_morphism X f g Y ∘⇩c j = y"
using j_projs assms j_type comp_associative2
unfolding fibered_product_right_proj_def by (typecheck_cfuncs, auto)
show "snd (X ⇘f⇙×⇩c⇘g⇙ Y, fibered_product_morphism X f g Y) ∘⇩c j = ⟨x,y⟩"
using left_eq right_eq assms j_type by (typecheck_cfuncs, simp add: cfunc_prod_unique)
qed
qed
qed
lemma fibered_product_pair_member2:
assumes "f : X → Y" "g : X → E" "x ∈⇩c X" "y ∈⇩c X"
assumes "g ∘⇩c fibered_product_left_proj X f f X = g ∘⇩c fibered_product_right_proj X f f X"
shows "∀x y. x ∈⇩c X ⟶ y ∈⇩c X ⟶ ⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⟶ g ∘⇩c x = g ∘⇩c y"
proof(clarify)
fix x y
assume x_type[type_rule]: "x ∈⇩c X"
assume y_type[type_rule]: "y ∈⇩c X"
assume a3: "⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
then obtain h where
h_type: "h ∈⇩c X⇘f⇙×⇩c⇘f⇙X" and h_eq: "fibered_product_morphism X f f X ∘⇩c h = ⟨x,y⟩"
by (meson factors_through_def2 relative_member_def2)
have left_eq: "fibered_product_left_proj X f f X ∘⇩c h = x"
unfolding fibered_product_left_proj_def
by (typecheck_cfuncs, smt (z3) assms(1) comp_associative2 h_eq h_type left_cart_proj_cfunc_prod y_type)
have right_eq: "fibered_product_right_proj X f f X ∘⇩c h = y"
unfolding fibered_product_right_proj_def
by (typecheck_cfuncs, metis (full_types) a3 comp_associative2 h_eq h_type relative_member_def2 right_cart_proj_cfunc_prod x_type)
then show "g ∘⇩c x = g ∘⇩c y"
using assms(1,2,5) cfunc_type_def comp_associative fibered_product_left_proj_type fibered_product_right_proj_type h_type left_eq right_eq by fastforce
qed
lemma kernel_pair_subset:
assumes "f: X → Y"
shows "(X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⊆⇩c X ×⇩c X"
using assms fibered_product_morphism_monomorphism fibered_product_morphism_type subobject_of_def2 by auto
text ‹The three lemmas below correspond to Exercise 2.1.44 in Halvorson.›
lemma kern_pair_proj_iso_TFAE1:
assumes "f: X → Y" "monomorphism f"
shows "(fibered_product_left_proj X f f X) = (fibered_product_right_proj X f f X)"
proof (cases "∃x. x∈⇩c X⇘f⇙×⇩c⇘f⇙X", clarify)
fix x
assume x_type: "x∈⇩c X⇘f⇙×⇩c⇘f⇙X"
then have "(f ∘⇩c (fibered_product_left_proj X f f X))∘⇩c x = (f∘⇩c (fibered_product_right_proj X f f X))∘⇩c x"
using assms cfunc_type_def comp_associative equalizer_def fibered_product_morphism_equalizer
unfolding fibered_product_right_proj_def fibered_product_left_proj_def
by (typecheck_cfuncs, smt (verit))
then have "f ∘⇩c (fibered_product_left_proj X f f X) = f∘⇩c (fibered_product_right_proj X f f X)"
using assms fibered_product_is_pullback is_pullback_def by auto
then show "(fibered_product_left_proj X f f X) = (fibered_product_right_proj X f f X)"
using assms cfunc_type_def fibered_product_left_proj_type fibered_product_right_proj_type monomorphism_def by auto
next
assume "∄x. x ∈⇩c X ⇘f⇙×⇩c⇘f⇙ X"
then show "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
using assms fibered_product_left_proj_type fibered_product_right_proj_type one_separator by blast
qed
lemma kern_pair_proj_iso_TFAE2:
assumes "f: X → Y" "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
shows "monomorphism f ∧ isomorphism (fibered_product_left_proj X f f X) ∧ isomorphism (fibered_product_right_proj X f f X)"
using assms
proof safe
have "injective f"
unfolding injective_def
proof clarify
fix x y
assume x_type: "x ∈⇩c domain f" and y_type: "y ∈⇩c domain f"
then have x_type2: "x ∈⇩c X" and y_type2: "y ∈⇩c X"
using assms(1) cfunc_type_def by auto
have x_y_type: "⟨x,y⟩ : 𝟭 → X ×⇩c X"
using x_type2 y_type2 by (typecheck_cfuncs)
have fibered_product_type: "fibered_product_morphism X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X ×⇩c X"
using assms by typecheck_cfuncs
assume "f ∘⇩c x = f ∘⇩c y"
then have factorsthru: "⟨x,y⟩ factorsthru fibered_product_morphism X f f X"
using assms(1) pair_factorsthru_fibered_product_morphism x_type2 y_type2 by auto
then obtain xy where xy_assms: "xy : 𝟭 → X ⇘f⇙×⇩c⇘f⇙ X" "fibered_product_morphism X f f X ∘⇩c xy = ⟨x,y⟩"
using factors_through_def2 fibered_product_type x_y_type by blast
have left_proj: "fibered_product_left_proj X f f X ∘⇩c xy = x"
unfolding fibered_product_left_proj_def using assms xy_assms
by (typecheck_cfuncs, metis cfunc_type_def comp_associative left_cart_proj_cfunc_prod x_type2 xy_assms(2) y_type2)
have right_proj: "fibered_product_right_proj X f f X ∘⇩c xy = y"
unfolding fibered_product_right_proj_def using assms xy_assms
by (typecheck_cfuncs, metis cfunc_type_def comp_associative right_cart_proj_cfunc_prod x_type2 xy_assms(2) y_type2)
show "x = y"
using assms(2) left_proj right_proj by auto
qed
then show "monomorphism f"
using injective_imp_monomorphism by blast
next
have "diagonal X factorsthru fibered_product_morphism X f f X"
using assms(1) diagonal_def id_type pair_factorsthru_fibered_product_morphism by fastforce
then obtain xx where xx_assms: "xx : X → X ⇘f⇙×⇩c⇘f⇙ X" "diagonal X = fibered_product_morphism X f f X ∘⇩c xx"
using assms(1) cfunc_type_def diagonal_type factors_through_def fibered_product_morphism_type by fastforce
have eq1: "fibered_product_right_proj X f f X ∘⇩c xx = id X"
by (smt assms(1) comp_associative2 diagonal_def fibered_product_morphism_type fibered_product_right_proj_def id_type right_cart_proj_cfunc_prod right_cart_proj_type xx_assms)
have eq2: "xx ∘⇩c fibered_product_right_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
proof (rule one_separator[where X="X ⇘f⇙×⇩c⇘f⇙ X", where Y="X ⇘f⇙×⇩c⇘f⇙ X"])
show "xx ∘⇩c fibered_product_right_proj X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X ⇘f⇙×⇩c⇘f⇙ X"
using assms(1) comp_type fibered_product_right_proj_type xx_assms by blast
show "id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) : X ⇘f⇙×⇩c⇘f⇙ X → X ⇘f⇙×⇩c⇘f⇙ X"
by (simp add: id_type)
next
fix x
assume x_type: "x ∈⇩c X ⇘f⇙×⇩c⇘f⇙ X"
then obtain a where a_assms: "⟨a,a⟩ = fibered_product_morphism X f f X ∘⇩c x" "a ∈⇩c X"
by (smt assms cfunc_prod_comp cfunc_prod_unique comp_type fibered_product_left_proj_def
fibered_product_morphism_type fibered_product_right_proj_def fibered_product_right_proj_type)
have "(xx ∘⇩c fibered_product_right_proj X f f X) ∘⇩c x = xx ∘⇩c right_cart_proj X X ∘⇩c ⟨a,a⟩"
using xx_assms x_type a_assms assms comp_associative2
unfolding fibered_product_right_proj_def
by (typecheck_cfuncs, auto)
also have "... = xx ∘⇩c a"
using a_assms(2) right_cart_proj_cfunc_prod by auto
also have "... = x"
proof -
have f2: "∀c. c : 𝟭 → X ⟶ fibered_product_morphism X f f X ∘⇩c xx ∘⇩c c = diagonal X ∘⇩c c"
proof safe
fix c
assume "c ∈⇩c X"
then show "fibered_product_morphism X f f X ∘⇩c xx ∘⇩c c = diagonal X ∘⇩c c"
using assms xx_assms by (typecheck_cfuncs, simp add: comp_associative2 xx_assms(2))
qed
have f4: "xx : X → codomain xx"
using cfunc_type_def xx_assms by presburger
have f5: "diagonal X ∘⇩c a = ⟨a,a⟩"
using a_assms diag_on_elements by blast
have f6: "codomain (xx ∘⇩c a) = codomain xx"
using f4 by (meson a_assms cfunc_type_def comp_type)
then have f9: "x : domain x → codomain xx"
using cfunc_type_def x_type xx_assms by auto
have f10: "∀c ca. domain (ca ∘⇩c a) = 𝟭 ∨ ¬ ca : X → c"
by (meson a_assms cfunc_type_def comp_type)
then have "domain ⟨a,a⟩ = 𝟭"
using diagonal_type f5 by force
then have f11: "domain x = 𝟭"
using cfunc_type_def x_type by blast
have "xx ∘⇩c a ∈⇩c codomain xx"
using a_assms comp_type f4 by auto
then show ?thesis
using f11 f9 f5 f2 a_assms assms(1) cfunc_type_def fibered_product_morphism_monomorphism
fibered_product_morphism_type monomorphism_def x_type
by auto
qed
also have "... = id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) ∘⇩c x"
by (metis cfunc_type_def id_left_unit x_type)
finally show "(xx ∘⇩c fibered_product_right_proj X f f X) ∘⇩c x = id⇩c (X ⇘f⇙×⇩c⇘f⇙ X) ∘⇩c x".
qed
show "isomorphism (fibered_product_left_proj X f f X)"
unfolding isomorphism_def
by (metis assms cfunc_type_def eq1 eq2 fibered_product_right_proj_type xx_assms(1))
then show "isomorphism (fibered_product_right_proj X f f X)"
unfolding isomorphism_def
using assms(2) isomorphism_def by auto
qed
lemma kern_pair_proj_iso_TFAE3:
assumes "f: X → Y"
assumes "isomorphism (fibered_product_left_proj X f f X)" "isomorphism (fibered_product_right_proj X f f X)"
shows "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
proof -
obtain q0 where
q0_assms: "q0 : X → X ⇘f⇙×⇩c⇘f⇙ X"
"fibered_product_left_proj X f f X ∘⇩c q0 = id X"
"q0 ∘⇩c fibered_product_left_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
using assms(1,2) cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)
obtain q1 where
q1_assms: "q1 : X → X ⇘f⇙×⇩c⇘f⇙ X"
"fibered_product_right_proj X f f X ∘⇩c q1 = id X"
"q1 ∘⇩c fibered_product_right_proj X f f X = id (X ⇘f⇙×⇩c⇘f⇙ X)"
using assms(1,3) cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)
have "⋀x. x ∈⇩c domain f ⟹ q0 ∘⇩c x = q1 ∘⇩c x"
proof -
fix x
have fxfx: "f∘⇩c x = f∘⇩c x"
by simp
assume x_type: "x ∈⇩c domain f"
have factorsthru: "⟨x,x⟩ factorsthru fibered_product_morphism X f f X"
using assms(1) cfunc_type_def fxfx pair_factorsthru_fibered_product_morphism x_type by auto
then obtain xx where xx_assms: "xx : 𝟭 → X ⇘f⇙×⇩c⇘f⇙ X" "⟨x,x⟩ = fibered_product_morphism X f f X ∘⇩c xx"
by (smt assms(1) cfunc_type_def diag_on_elements diagonal_type domain_comp factors_through_def factorsthru fibered_product_morphism_type x_type)
have projection_prop: "q0 ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx) =
q1 ∘⇩c ((fibered_product_right_proj X f f X)∘⇩c xx)"
using q0_assms q1_assms xx_assms assms by (typecheck_cfuncs, simp add: comp_associative2)
then have fun_fact: "x = ((fibered_product_left_proj X f f X) ∘⇩c q1)∘⇩c (((fibered_product_left_proj X f f X)∘⇩c xx))"
by (smt assms(1) cfunc_type_def comp_associative2 fibered_product_left_proj_def
fibered_product_left_proj_type fibered_product_morphism_type fibered_product_right_proj_def
fibered_product_right_proj_type id_left_unit2 left_cart_proj_cfunc_prod left_cart_proj_type
q1_assms right_cart_proj_cfunc_prod right_cart_proj_type x_type xx_assms)
then have "q1 ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx) =
q0 ∘⇩c ((fibered_product_left_proj X f f X)∘⇩c xx)"
using q0_assms q1_assms xx_assms assms
by (typecheck_cfuncs, smt cfunc_type_def comp_associative2 fibered_product_left_proj_def
fibered_product_morphism_type fibered_product_right_proj_def left_cart_proj_cfunc_prod
left_cart_proj_type projection_prop right_cart_proj_cfunc_prod right_cart_proj_type x_type xx_assms(2))
then show "q0 ∘⇩c x = q1 ∘⇩c x"
by (smt assms(1) cfunc_type_def codomain_comp comp_associative fibered_product_left_proj_type
fun_fact id_left_unit2 q0_assms q1_assms xx_assms)
qed
then have "q0 = q1"
by (metis assms(1) cfunc_type_def one_separator_contrapos q0_assms(1) q1_assms(1))
then show "fibered_product_left_proj X f f X = fibered_product_right_proj X f f X"
by (smt assms(1) comp_associative2 fibered_product_left_proj_type fibered_product_right_proj_type
id_left_unit2 id_right_unit2 q0_assms q1_assms)
qed
lemma terminal_fib_prod_iso:
assumes "terminal_object(T)"
assumes f_type: "f : Y → T"
assumes g_type: "g : X → T"
shows "(X ⇘g⇙×⇩c⇘f⇙ Y) ≅ X ×⇩c Y"
proof -
have "(is_pullback (X ⇘g⇙×⇩c⇘f⇙ Y) Y X T (fibered_product_right_proj X g f Y) f (fibered_product_left_proj X g f Y) g)"
using assms pullback_iff_product fibered_product_is_pullback by (typecheck_cfuncs, blast)
then have "(is_cart_prod (X ⇘g⇙×⇩c⇘f⇙ Y) (fibered_product_left_proj X g f Y) (fibered_product_right_proj X g f Y) X Y)"
using assms by (meson one_terminal_object pullback_iff_product terminal_func_type)
then show ?thesis
using assms by (metis canonical_cart_prod_is_cart_prod cart_prods_isomorphic fst_conv is_isomorphic_def snd_conv)
qed
end