Theory Equivalence
section ‹Equivalence Classes and Coequalizers›
theory Equivalence
imports Truth
begin
definition reflexive_on :: "cset ⇒ cset × cfunc ⇒ bool" where
"reflexive_on X R = (R ⊆⇩c X×⇩cX ∧
(∀x. x ∈⇩c X ⟶ (⟨x,x⟩ ∈⇘X×⇩cX⇙ R)))"
definition symmetric_on :: "cset ⇒ cset × cfunc ⇒ bool" where
"symmetric_on X R = (R ⊆⇩c X×⇩cX ∧
(∀x y. x ∈⇩c X ∧ y ∈⇩c X ⟶
(⟨x,y⟩ ∈⇘X×⇩cX⇙ R ⟶ ⟨y,x⟩ ∈⇘X×⇩cX⇙ R)))"
definition transitive_on :: "cset ⇒ cset × cfunc ⇒ bool" where
"transitive_on X R = (R ⊆⇩c X×⇩cX ∧
(∀x y z. x ∈⇩c X ∧ y ∈⇩c X ∧ z ∈⇩c X ⟶
(⟨x,y⟩ ∈⇘X×⇩cX⇙ R ∧ ⟨y,z⟩ ∈⇘X×⇩cX⇙ R ⟶ ⟨x,z⟩ ∈⇘X×⇩cX⇙ R)))"
definition equiv_rel_on :: "cset ⇒ cset × cfunc ⇒ bool" where
"equiv_rel_on X R ⟷ (reflexive_on X R ∧ symmetric_on X R ∧ transitive_on X R)"
definition const_on_rel :: "cset ⇒ cset × cfunc ⇒ cfunc ⇒ bool" where
"const_on_rel X R f = (∀x y. x ∈⇩c X ⟶ y ∈⇩c X ⟶ ⟨x, y⟩ ∈⇘X×⇩cX⇙ R ⟶ f ∘⇩c x = f ∘⇩c y)"
lemma reflexive_def2:
assumes reflexive_Y: "reflexive_on X (Y, m)"
assumes x_type: "x ∈⇩c X"
shows "∃y. y ∈⇩c Y ∧ m ∘⇩c y = ⟨x,x⟩"
using assms unfolding reflexive_on_def relative_member_def factors_through_def2
proof -
assume a1: "(Y, m) ⊆⇩c X ×⇩c X ∧ (∀x. x ∈⇩c X ⟶ ⟨x,x⟩ ∈⇩c X ×⇩c X ∧ monomorphism (snd (Y, m)) ∧ snd (Y, m) : fst (Y, m) → X ×⇩c X ∧ ⟨x,x⟩ factorsthru snd (Y, m))"
have xx_type: "⟨x,x⟩ ∈⇩c X ×⇩c X"
by (typecheck_cfuncs, simp add: x_type)
have "⟨x,x⟩ factorsthru m"
using a1 x_type by auto
then show ?thesis
using a1 xx_type cfunc_type_def factors_through_def subobject_of_def2 by force
qed
lemma symmetric_def2:
assumes symmetric_Y: "symmetric_on X (Y, m)"
assumes x_type: "x ∈⇩c X"
assumes y_type: "y ∈⇩c X"
assumes relation: "∃v. v ∈⇩c Y ∧ m ∘⇩c v = ⟨x,y⟩"
shows "∃w. w ∈⇩c Y ∧ m ∘⇩c w = ⟨y,x⟩"
using assms unfolding symmetric_on_def relative_member_def factors_through_def2
by (metis cfunc_prod_type factors_through_def2 fst_conv snd_conv subobject_of_def2)
lemma transitive_def2:
assumes transitive_Y: "transitive_on X (Y, m)"
assumes x_type: "x ∈⇩c X"
assumes y_type: "y ∈⇩c X"
assumes z_type: "z ∈⇩c X"
assumes relation1: "∃v. v ∈⇩c Y ∧ m ∘⇩c v = ⟨x,y⟩"
assumes relation2: "∃w. w ∈⇩c Y ∧ m ∘⇩c w = ⟨y,z⟩"
shows "∃u. u ∈⇩c Y ∧ m ∘⇩c u = ⟨x,z⟩"
using assms unfolding transitive_on_def relative_member_def factors_through_def2
by (metis cfunc_prod_type factors_through_def2 fst_conv snd_conv subobject_of_def2)
text ‹The lemma below corresponds to Exercise 2.3.3 in Halvorson.›
lemma kernel_pair_equiv_rel:
assumes "f : X → Y"
shows "equiv_rel_on X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
proof (unfold equiv_rel_on_def, safe)
show "reflexive_on X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
proof (unfold reflexive_on_def, safe)
show "(X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⊆⇩c X ×⇩c X"
using assms kernel_pair_subset by auto
next
fix x
assume x_type: "x ∈⇩c X"
then show "⟨x,x⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by (smt assms comp_type diag_on_elements diagonal_type fibered_product_morphism_monomorphism
fibered_product_morphism_type pair_factorsthru_fibered_product_morphism relative_member_def2)
qed
show "symmetric_on X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
proof (unfold symmetric_on_def, safe)
show "(X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⊆⇩c X ×⇩c X"
using assms kernel_pair_subset by auto
next
fix x y
assume x_type: "x ∈⇩c X" and y_type: "y ∈⇩c X"
assume xy_in: "⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
then have "f ∘⇩c x = f ∘⇩c y"
using assms fibered_product_pair_member x_type y_type by blast
then show "⟨y,x⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
using assms fibered_product_pair_member x_type y_type by auto
qed
show "transitive_on X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
proof (unfold transitive_on_def, safe)
show "(X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) ⊆⇩c X ×⇩c X"
using assms kernel_pair_subset by auto
next
fix x y z
assume x_type: "x ∈⇩c X" and y_type: "y ∈⇩c X" and z_type: "z ∈⇩c X"
assume xy_in: "⟨x,y⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
assume yz_in: "⟨y,z⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
have eqn1: "f ∘⇩c x = f ∘⇩c y"
using assms fibered_product_pair_member x_type xy_in y_type by blast
have eqn2: "f ∘⇩c y = f ∘⇩c z"
using assms fibered_product_pair_member y_type yz_in z_type by blast
show "⟨x,z⟩ ∈⇘X ×⇩c X⇙ (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
using assms eqn1 eqn2 fibered_product_pair_member x_type z_type by auto
qed
qed
text ‹The axiomatization below corresponds to Axiom 6 (Equivalence Classes) in Halvorson.›
axiomatization
quotient_set :: "cset ⇒ (cset × cfunc) ⇒ cset" (infix "⫽" 50) and
equiv_class :: "cset × cfunc ⇒ cfunc" and
quotient_func :: "cfunc ⇒ cset × cfunc ⇒ cfunc"
where
equiv_class_type[type_rule]: "equiv_rel_on X R ⟹ equiv_class R : X → quotient_set X R" and
equiv_class_eq: "equiv_rel_on X R ⟹ ⟨x, y⟩ ∈⇩c X×⇩cX ⟹
⟨x, y⟩ ∈⇘X×⇩cX⇙ R ⟷ equiv_class R ∘⇩c x = equiv_class R ∘⇩c y" and
quotient_func_type[type_rule]:
"equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
quotient_func f R : quotient_set X R → Y" and
quotient_func_eq: "equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
quotient_func f R ∘⇩c equiv_class R = f" and
quotient_func_unique: "equiv_rel_on X R ⟹ f : X → Y ⟹ (const_on_rel X R f) ⟹
h : quotient_set X R → Y ⟹ h ∘⇩c equiv_class R = f ⟹ h = quotient_func f R"
text ‹Note that @{const quotient_set} corresponds to $X/R$, @{const equiv_class} corresponds to the
canonical quotient mapping $q$, and @{const quotient_func} corresponds to $\bar{f}$ in Halvorson's
formulation of this axiom.›
abbreviation equiv_class' :: "cfunc ⇒ cset × cfunc ⇒ cfunc" ("[_]⇘_⇙") where
"[x]⇘R⇙ ≡ equiv_class R ∘⇩c x"
subsection ‹Coequalizers›
text ‹The definition below corresponds to a comment after Axiom 6 (Equivalence Classes) in Halvorson.›
definition coequalizer :: "cset ⇒ cfunc ⇒ cfunc ⇒ cfunc ⇒ bool" where
"coequalizer E m f g ⟷ (∃ X Y. (f : Y → X) ∧ (g : Y → X) ∧ (m : X → E)
∧ (m ∘⇩c f = m ∘⇩c g)
∧ (∀ h F. ((h : X → F) ∧ (h ∘⇩c f = h ∘⇩c g)) ⟶ (∃! k. (k : E → F) ∧ k ∘⇩c m = h)))"
lemma coequalizer_def2:
assumes "f : Y → X" "g : Y → X" "m : X → E"
shows "coequalizer E m f g ⟷
(m ∘⇩c f = m ∘⇩c g)
∧ (∀ h F. ((h : X → F) ∧ (h ∘⇩c f = h ∘⇩c g)) ⟶ (∃! k. (k : E → F) ∧ k ∘⇩c m = h))"
using assms unfolding coequalizer_def cfunc_type_def by auto
text ‹The lemma below corresponds to Exercise 2.3.1 in Halvorson.›
lemma coequalizer_unique:
assumes "coequalizer E m f g" "coequalizer F n f g"
shows "E ≅ F"
proof -
obtain k where k_def: "k: E → F ∧ k ∘⇩c m = n"
by (typecheck_cfuncs, metis assms cfunc_type_def coequalizer_def)
obtain k' where k'_def: "k': F → E ∧ k' ∘⇩c n = m"
by (typecheck_cfuncs, metis assms cfunc_type_def coequalizer_def)
obtain k'' where k''_def: "k'': F → F ∧ k'' ∘⇩c n = n"
by (typecheck_cfuncs, smt (verit) assms(2) cfunc_type_def coequalizer_def)
have k''_def2: "k'' = id F"
using assms(2) coequalizer_def id_left_unit2 k''_def by (typecheck_cfuncs, blast)
have kk'_idF: "k ∘⇩c k' = id F"
by (typecheck_cfuncs, smt (verit) assms(2) cfunc_type_def coequalizer_def comp_associative k''_def k''_def2 k'_def k_def)
have k'k_idE: "k' ∘⇩c k = id E"
by (typecheck_cfuncs, smt (verit) assms(1) coequalizer_def comp_associative2 id_left_unit2 k'_def k_def)
show "E ≅ F"
using cfunc_type_def is_isomorphic_def isomorphism_def k'_def k'k_idE k_def kk'_idF by fastforce
qed
text ‹The lemma below corresponds to Exercise 2.3.2 in Halvorson.›
lemma coequalizer_is_epimorphism:
"coequalizer E m f g ⟹ epimorphism(m)"
unfolding coequalizer_def epimorphism_def
proof clarify
fix k h X Y
assume f_type: "f : Y → X"
assume g_type: "g : Y → X"
assume m_type: "m : X → E"
assume fm_gm: "m ∘⇩c f = m ∘⇩c g"
assume uniqueness: "∀h F. h : X → F ∧ h ∘⇩c f = h ∘⇩c g ⟶ (∃!k. k : E → F ∧ k ∘⇩c m = h)"
assume relation_k: "domain k =codomain m "
assume relation_h: "domain h = codomain m"
assume m_k_mh: "k ∘⇩c m = h ∘⇩c m"
have "k ∘⇩c m ∘⇩c f = h ∘⇩c m ∘⇩c g"
using cfunc_type_def comp_associative fm_gm g_type m_k_mh m_type relation_k relation_h by auto
then obtain z where "z: E → codomain(k) ∧ z ∘⇩c m = k ∘⇩c m ∧
(∀ j. j:E → codomain(k) ∧ j ∘⇩c m = k ∘⇩c m ⟶ j = z)"
using uniqueness by (smt cfunc_type_def codomain_comp comp_associative domain_comp f_type g_type m_k_mh m_type relation_k relation_h)
then show "k = h"
by (metis cfunc_type_def codomain_comp m_k_mh m_type relation_k relation_h)
qed
lemma canonical_quotient_map_is_coequalizer:
assumes "equiv_rel_on X (R,m)"
shows "coequalizer (X ⫽ (R,m)) (equiv_class (R,m))
(left_cart_proj X X ∘⇩c m) (right_cart_proj X X ∘⇩c m)"
unfolding coequalizer_def
proof(rule exI[where x=X], intro exI[where x= R], safe)
have m_type: "m: R → X ×⇩c X"
using assms equiv_rel_on_def subobject_of_def2 transitive_on_def by blast
show "left_cart_proj X X ∘⇩c m : R → X"
using m_type by typecheck_cfuncs
show "right_cart_proj X X ∘⇩c m : R → X"
using m_type by typecheck_cfuncs
show "equiv_class (R, m) : X → X ⫽ (R, m)"
by (simp add: assms equiv_class_type)
show "[left_cart_proj X X ∘⇩c m]⇘(R, m)⇙ = [right_cart_proj X X ∘⇩c m]⇘(R, m)⇙"
proof(rule one_separator[where X="R", where Y = "X ⫽ (R,m)"], typecheck_cfuncs)
show "[left_cart_proj X X ∘⇩c m]⇘(R, m)⇙ : R → X ⫽ (R, m)"
using m_type assms by typecheck_cfuncs
show "[right_cart_proj X X ∘⇩c m]⇘(R, m)⇙ : R → X ⫽ (R, m)"
using m_type assms by typecheck_cfuncs
next
fix x
assume x_type: "x ∈⇩c R"
then have m_x_type: "m ∘⇩c x ∈⇩c X ×⇩c X"
using m_type by typecheck_cfuncs
then obtain a b where a_type: "a ∈⇩c X" and b_type: "b ∈⇩c X" and m_x_eq: "m ∘⇩c x = ⟨a,b⟩"
using cart_prod_decomp by blast
then have ab_inR_relXX: "⟨a,b⟩ ∈⇘X ×⇩c X⇙(R,m)"
using assms cfunc_type_def equiv_rel_on_def factors_through_def m_x_type reflexive_on_def relative_member_def2 x_type by auto
then have "equiv_class (R, m) ∘⇩c a = equiv_class (R, m) ∘⇩c b"
using equiv_class_eq assms relative_member_def by blast
then have "equiv_class (R, m) ∘⇩c left_cart_proj X X ∘⇩c ⟨a,b⟩ = equiv_class (R, m) ∘⇩c right_cart_proj X X ∘⇩c ⟨a,b⟩"
using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod by auto
then have "equiv_class (R, m) ∘⇩c left_cart_proj X X ∘⇩c m ∘⇩c x = equiv_class (R, m) ∘⇩c right_cart_proj X X ∘⇩c m ∘⇩c x"
by (simp add: m_x_eq)
then show "[left_cart_proj X X ∘⇩c m]⇘(R, m)⇙ ∘⇩c x = [right_cart_proj X X ∘⇩c m]⇘(R, m)⇙ ∘⇩c x"
using x_type m_type assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative m_x_eq)
qed
next
fix h F
assume h_type: " h : X → F"
assume h_proj1_eqs_h_proj2: "h ∘⇩c left_cart_proj X X ∘⇩c m = h ∘⇩c right_cart_proj X X ∘⇩c m"
have m_type: "m : R → X ×⇩c X"
using assms equiv_rel_on_def reflexive_on_def subobject_of_def2 by blast
have "const_on_rel X (R, m) h"
proof (unfold const_on_rel_def, clarify)
fix x y
assume x_type: "x ∈⇩c X" and y_type: "y ∈⇩c X"
assume "⟨x,y⟩ ∈⇘X ×⇩c X⇙ (R, m)"
then obtain xy where xy_type: "xy ∈⇩c R" and m_h_eq: "m ∘⇩c xy = ⟨x,y⟩"
unfolding relative_member_def2 factors_through_def using cfunc_type_def by auto
have "h ∘⇩c left_cart_proj X X ∘⇩c m ∘⇩c xy = h ∘⇩c right_cart_proj X X ∘⇩c m ∘⇩c xy"
using h_type m_type xy_type by (typecheck_cfuncs, smt comp_associative2 comp_type h_proj1_eqs_h_proj2)
then have "h ∘⇩c left_cart_proj X X ∘⇩c ⟨x,y⟩ = h ∘⇩c right_cart_proj X X ∘⇩c ⟨x,y⟩"
using m_h_eq by auto
then show "h ∘⇩c x = h ∘⇩c y"
using left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod x_type y_type by auto
qed
then show "∃k. k : X ⫽ (R, m) → F ∧ k ∘⇩c equiv_class (R, m) = h"
using assms h_type quotient_func_type quotient_func_eq
by (intro exI[where x="quotient_func h (R, m)"], safe)
next
fix F k y
assume k_type[type_rule]: "k : X ⫽ (R, m) → F"
assume y_type[type_rule]: "y : X ⫽ (R, m) → F"
assume k_equiv_class_type[type_rule]: "k ∘⇩c equiv_class (R, m) : X → F"
assume k_equiv_class_eq: "(k ∘⇩c equiv_class (R, m)) ∘⇩c left_cart_proj X X ∘⇩c m =
(k ∘⇩c equiv_class (R, m)) ∘⇩c right_cart_proj X X ∘⇩c m"
assume y_k_eq: "y ∘⇩c equiv_class (R, m) = k ∘⇩c equiv_class (R, m)"
have m_type[type_rule]: "m : R → X ×⇩c X"
using assms equiv_rel_on_def reflexive_on_def subobject_of_def2 by blast
have y_eq: "y = quotient_func (y ∘⇩c equiv_class (R, m)) (R, m)"
using assms y_k_eq
proof (etcs_rule quotient_func_unique[where X=X, where Y=F], unfold const_on_rel_def, safe)
fix a b
assume a_type[type_rule]: "a ∈⇩c X" and b_type[type_rule]: "b ∈⇩c X"
assume ab_in_R: "⟨a,b⟩ ∈⇘X ×⇩c X⇙ (R, m)"
then obtain h where h_type[type_rule]: "h ∈⇩c R" and m_h_eq: "m ∘⇩c h = ⟨a, b⟩"
unfolding relative_member_def factors_through_def using cfunc_type_def by auto
have "(k ∘⇩c equiv_class (R, m)) ∘⇩c left_cart_proj X X ∘⇩c m ∘⇩c h =
(k ∘⇩c equiv_class (R, m)) ∘⇩c right_cart_proj X X ∘⇩c m ∘⇩c h"
using assms
by (typecheck_cfuncs, smt comp_associative2 comp_type k_equiv_class_eq)
then have "(k ∘⇩c equiv_class (R, m)) ∘⇩c left_cart_proj X X ∘⇩c ⟨a, b⟩ =
(k ∘⇩c equiv_class (R, m)) ∘⇩c right_cart_proj X X ∘⇩c ⟨a, b⟩"
by (simp add: m_h_eq)
then show "(y ∘⇩c equiv_class (R, m)) ∘⇩c a = (y ∘⇩c equiv_class (R, m)) ∘⇩c b"
using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_k_eq by auto
qed
have k_eq: "k = quotient_func (y ∘⇩c equiv_class (R, m)) (R, m)"
using assms sym[OF y_k_eq]
proof (etcs_rule quotient_func_unique[where X=X, where Y=F], unfold const_on_rel_def, safe)
fix a b
assume a_type: "a ∈⇩c X" and b_type: "b ∈⇩c X"
assume ab_in_R: "⟨a,b⟩ ∈⇘X ×⇩c X⇙ (R, m)"
then obtain h where h_type: "h ∈⇩c R" and m_h_eq: "m ∘⇩c h = ⟨a, b⟩"
unfolding relative_member_def factors_through_def using cfunc_type_def by auto
have "(k ∘⇩c equiv_class (R, m)) ∘⇩c left_cart_proj X X ∘⇩c m ∘⇩c h =
(k ∘⇩c equiv_class (R, m)) ∘⇩c right_cart_proj X X ∘⇩c m ∘⇩c h"
using k_type m_type h_type assms
by (typecheck_cfuncs, smt comp_associative2 comp_type k_equiv_class_eq)
then have "(k ∘⇩c equiv_class (R, m)) ∘⇩c left_cart_proj X X ∘⇩c ⟨a, b⟩ =
(k ∘⇩c equiv_class (R, m)) ∘⇩c right_cart_proj X X ∘⇩c ⟨a, b⟩"
by (simp add: m_h_eq)
then show "(y ∘⇩c equiv_class (R, m)) ∘⇩c a = (y ∘⇩c equiv_class (R, m)) ∘⇩c b"
using a_type b_type left_cart_proj_cfunc_prod right_cart_proj_cfunc_prod y_k_eq by auto
qed
show "k = y"
using y_eq k_eq by auto
qed
lemma canonical_quot_map_is_epi:
assumes "equiv_rel_on X (R,m)"
shows "epimorphism((equiv_class (R,m)))"
by (meson assms canonical_quotient_map_is_coequalizer coequalizer_is_epimorphism)
subsection ‹Regular Epimorphisms›
text ‹The definition below corresponds to Definition 2.3.4 in Halvorson.›
definition regular_epimorphism :: "cfunc ⇒ bool" where
"regular_epimorphism f = (∃ g h. coequalizer (codomain f) f g h)"
text ‹The lemma below corresponds to Exercise 2.3.5 in Halvorson.›
lemma reg_epi_and_mono_is_iso:
assumes "f : X → Y" "regular_epimorphism f" "monomorphism f"
shows "isomorphism f"
proof -
obtain g h where gh_def: "coequalizer (codomain f) f g h"
using assms(2) regular_epimorphism_def by auto
obtain W where W_def: "(g: W → X) ∧ (h: W → X) ∧ (coequalizer Y f g h)"
using assms(1) cfunc_type_def coequalizer_def gh_def by fastforce
have fg_eqs_fh: "f ∘⇩c g = f ∘⇩c h"
using coequalizer_def gh_def by blast
then have "id(X)∘⇩c g = id(X) ∘⇩c h"
using W_def assms(1,3) monomorphism_def2 by blast
then obtain j where j_def: "j: Y → X ∧ j ∘⇩c f = id(X)"
using assms(1) W_def coequalizer_def2 by (typecheck_cfuncs, blast)
have "id(Y) ∘⇩c f = f ∘⇩c id(X)"
using assms(1) id_left_unit2 id_right_unit2 by auto
also have "... = (f ∘⇩c j) ∘⇩c f"
using assms(1) comp_associative2 j_def by fastforce
ultimately have "id(Y) = f ∘⇩c j"
by (typecheck_cfuncs, metis W_def assms(1) coequalizer_is_epimorphism epimorphism_def3 j_def)
then show "isomorphism f"
using assms(1) cfunc_type_def isomorphism_def j_def by fastforce
qed
text ‹The two lemmas below correspond to Proposition 2.3.6 in Halvorson.›
lemma epimorphism_coequalizer_kernel_pair:
assumes "f : X → Y" "epimorphism f"
shows "coequalizer Y f (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)"
unfolding coequalizer_def
proof (rule exI[where x = X], rule exI[where x="X ⇘f⇙×⇩c⇘f⇙ X"], safe)
show "fibered_product_left_proj X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X"
using assms by typecheck_cfuncs
show "fibered_product_right_proj X f f X : X ⇘f⇙×⇩c⇘f⇙ X → X"
using assms by typecheck_cfuncs
show "f : X →Y"
using assms by typecheck_cfuncs
show "f ∘⇩c fibered_product_left_proj X f f X = f ∘⇩c fibered_product_right_proj X f f X"
using fibered_product_is_pullback assms unfolding is_pullback_def by auto
next
fix g E
assume g_type: "g : X → E"
assume g_eq: "g ∘⇩c fibered_product_left_proj X f f X = g ∘⇩c fibered_product_right_proj X f f X"
define F where F_def: "F = quotient_set X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
obtain q where q_def: "q = equiv_class (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)" and
q_type[type_rule]: "q : X → F"
using F_def assms(1) equiv_class_type kernel_pair_equiv_rel by auto
obtain f_bar where f_bar_def: "f_bar = quotient_func f (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)" and
f_bar_type[type_rule]: "f_bar : F → Y"
using F_def assms(1) const_on_rel_def fibered_product_pair_member kernel_pair_equiv_rel quotient_func_type by auto
have fibr_proj_left_type[type_rule]: "fibered_product_left_proj F (f_bar) (f_bar) F : F ⇘(f_bar)⇙×⇩c⇘(f_bar)⇙ F → F"
by typecheck_cfuncs
have fibr_proj_right_type[type_rule]: "fibered_product_right_proj F (f_bar) (f_bar) F : F ⇘(f_bar)⇙×⇩c⇘(f_bar)⇙ F → F"
by typecheck_cfuncs
have f_eqs: "f_bar ∘⇩c q = f"
proof -
have fact1: "equiv_rel_on X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by (meson assms(1) kernel_pair_equiv_rel)
have fact2: "const_on_rel X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) f"
using assms(1) const_on_rel_def fibered_product_pair_member by presburger
show ?thesis
using assms(1) f_bar_def fact1 fact2 q_def quotient_func_eq by blast
qed
have "∃! b. b : X ⇘f⇙×⇩c⇘f⇙ X → F ⇘(f_bar)⇙×⇩c⇘(f_bar)⇙ F ∧
fibered_product_left_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X ∧
fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_right_proj X f f X ∧
epimorphism b"
proof(rule kernel_pair_connection[where Y = Y])
show "f : X → Y"
using assms by typecheck_cfuncs
show "q : X → F"
by typecheck_cfuncs
show "epimorphism q"
using assms(1) canonical_quot_map_is_epi kernel_pair_equiv_rel q_def by blast
show "f_bar ∘⇩c q = f"
by (simp add: f_eqs)
show "q ∘⇩c fibered_product_left_proj X f f X = q ∘⇩c fibered_product_right_proj X f f X"
by (metis assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def)
show "f_bar : F → Y"
by typecheck_cfuncs
qed
then obtain b where b_type[type_rule]: "b : X ⇘f⇙×⇩c⇘f⇙ X → F ⇘(f_bar)⇙×⇩c⇘(f_bar)⇙ F" and
left_b_eqs: "fibered_product_left_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X" and
right_b_eqs: "fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_right_proj X f f X" and
epi_b: "epimorphism b"
by auto
have "fibered_product_left_proj F (f_bar) (f_bar) F = fibered_product_right_proj F (f_bar) (f_bar) F"
proof -
have "(fibered_product_left_proj F (f_bar) (f_bar) F) ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X"
by (simp add: left_b_eqs)
also have "... = q ∘⇩c fibered_product_right_proj X f f X"
using assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
also have "... = fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b"
by (simp add: right_b_eqs)
finally have "fibered_product_left_proj F (f_bar) (f_bar) F ∘⇩c b = fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b".
then show ?thesis
using b_type epi_b epimorphism_def2 fibr_proj_left_type fibr_proj_right_type by blast
qed
then obtain b where b_type[type_rule]: "b : X ⇘f⇙×⇩c⇘f⇙ X → F ⇘(f_bar)⇙×⇩c⇘(f_bar)⇙ F" and
left_b_eqs: "fibered_product_left_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X" and
right_b_eqs: "fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b = q ∘⇩c fibered_product_right_proj X f f X" and
epi_b: "epimorphism b"
using b_type epi_b left_b_eqs right_b_eqs by blast
have "fibered_product_left_proj F (f_bar) (f_bar) F = fibered_product_right_proj F (f_bar) (f_bar) F"
proof -
have "(fibered_product_left_proj F (f_bar) (f_bar) F) ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X"
by (simp add: left_b_eqs)
also have "... = q ∘⇩c fibered_product_right_proj X f f X"
using assms(1) canonical_quotient_map_is_coequalizer coequalizer_def fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
also have "... = fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b"
by (simp add: right_b_eqs)
finally have "fibered_product_left_proj F (f_bar) (f_bar) F ∘⇩c b = fibered_product_right_proj F (f_bar) (f_bar) F ∘⇩c b".
then show ?thesis
using b_type epi_b epimorphism_def2 fibr_proj_left_type fibr_proj_right_type by blast
qed
then have mono_fbar: "monomorphism(f_bar)"
by (typecheck_cfuncs, simp add: kern_pair_proj_iso_TFAE2)
have "epimorphism(f_bar)"
by (typecheck_cfuncs, metis assms(2) cfunc_type_def comp_epi_imp_epi f_eqs q_type)
then have "isomorphism(f_bar)"
by (simp add: epi_mon_is_iso mono_fbar)
obtain f_bar_inv where f_bar_inv_type[type_rule]: "f_bar_inv: Y → F" and
f_bar_inv_eq1: "f_bar_inv ∘⇩c f_bar = id(F)" and
f_bar_inv_eq2: "f_bar ∘⇩c f_bar_inv = id(Y)"
using ‹isomorphism f_bar› cfunc_type_def isomorphism_def by (typecheck_cfuncs, force)
obtain g_bar where g_bar_def: "g_bar = quotient_func g (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by auto
have "const_on_rel X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) g"
unfolding const_on_rel_def
by (meson assms(1) fibered_product_pair_member2 g_eq g_type)
then have g_bar_type[type_rule]: "g_bar : F → E"
using F_def assms(1) g_bar_def g_type kernel_pair_equiv_rel quotient_func_type by blast
obtain k where k_def: "k = g_bar ∘⇩c f_bar_inv" and k_type[type_rule]: "k : Y → E"
by (typecheck_cfuncs, simp)
then show "∃k. k : Y → E ∧ k ∘⇩c f = g"
by (smt (z3) ‹const_on_rel X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) g› assms(1) comp_associative2 f_bar_inv_eq1 f_bar_inv_type f_bar_type f_eqs g_bar_def g_bar_type g_type id_left_unit2 kernel_pair_equiv_rel q_def q_type quotient_func_eq)
next
show "⋀F k y.
k ∘⇩c f : X → F ⟹
(k ∘⇩c f) ∘⇩c fibered_product_left_proj X f f X = (k ∘⇩c f) ∘⇩c fibered_product_right_proj X f f X ⟹
k : Y → F ⟹ y : Y → F ⟹ y ∘⇩c f = k ∘⇩c f ⟹ k = y"
using assms epimorphism_def2 by blast
qed
lemma epimorphisms_are_regular:
assumes "f : X → Y" "epimorphism f"
shows "regular_epimorphism f"
by (meson assms(2) cfunc_type_def epimorphism_coequalizer_kernel_pair regular_epimorphism_def)
subsection ‹Epi-monic Factorization›
lemma epi_monic_factorization:
assumes f_type[type_rule]: "f : X → Y"
shows "∃ g m E. g : X → E ∧ m : E → Y
∧ coequalizer E g (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)
∧ monomorphism m ∧ f = m ∘⇩c g
∧ (∀x. x : E → Y ⟶ f = x ∘⇩c g ⟶ x = m)"
proof -
obtain q where q_def: "q = equiv_class (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by auto
obtain E where E_def: "E = quotient_set X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by auto
obtain m where m_def: "m = quotient_func f (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X)"
by auto
show "∃ g m E. g : X → E ∧ m : E → Y
∧ coequalizer E g (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)
∧ monomorphism m ∧ f = m ∘⇩c g
∧ (∀x. x : E → Y ⟶ f = x ∘⇩c g ⟶ x = m)"
proof (rule exI[where x=q], rule exI [where x=m], rule exI[where x=E], safe)
show q_type[type_rule]: "q : X → E"
unfolding q_def E_def using kernel_pair_equiv_rel by (typecheck_cfuncs, blast)
have f_const: "const_on_rel X (X ⇘f⇙×⇩c⇘f⇙ X, fibered_product_morphism X f f X) f"
unfolding const_on_rel_def using assms fibered_product_pair_member by auto
then show m_type[type_rule]: "m : E → Y"
unfolding m_def E_def using kernel_pair_equiv_rel by (typecheck_cfuncs, blast)
show q_coequalizer: "coequalizer E q (fibered_product_left_proj X f f X) (fibered_product_right_proj X f f X)"
unfolding q_def fibered_product_left_proj_def fibered_product_right_proj_def E_def
using canonical_quotient_map_is_coequalizer f_type kernel_pair_equiv_rel by auto
then have q_epi: "epimorphism q"
using coequalizer_is_epimorphism by auto
show m_mono: "monomorphism m"
proof -
have q_eq: "q ∘⇩c fibered_product_left_proj X f f X = q ∘⇩c fibered_product_right_proj X f f X"
using canonical_quotient_map_is_coequalizer coequalizer_def f_type fibered_product_left_proj_def fibered_product_right_proj_def kernel_pair_equiv_rel q_def by fastforce
then have "∃!b. b : X ⇘f⇙×⇩c⇘f⇙ X → E ⇘m⇙×⇩c⇘m⇙ E ∧
fibered_product_left_proj E m m E ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X ∧
fibered_product_right_proj E m m E ∘⇩c b = q ∘⇩c fibered_product_right_proj X f f X ∧
epimorphism b"
by (typecheck_cfuncs, intro kernel_pair_connection,
simp_all add: q_epi, metis f_const kernel_pair_equiv_rel m_def q_def quotient_func_eq)
then obtain b where b_type[type_rule]: "b : X ⇘f⇙×⇩c⇘f⇙ X → E ⇘m⇙×⇩c⇘m⇙ E" and
b_left_eq: "fibered_product_left_proj E m m E ∘⇩c b = q ∘⇩c fibered_product_left_proj X f f X" and
b_right_eq: "fibered_product_right_proj E m m E ∘⇩c b = q ∘⇩c fibered_product_right_proj X f f X" and
b_epi: "epimorphism b"
by auto
have "fibered_product_left_proj E m m E ∘⇩c b = fibered_product_right_proj E m m E ∘⇩c b"
using b_left_eq b_right_eq q_eq by force
then have "fibered_product_left_proj E m m E = fibered_product_right_proj E m m E"
using b_epi cfunc_type_def epimorphism_def by (typecheck_cfuncs_prems, auto)
then show "monomorphism m"
using kern_pair_proj_iso_TFAE2 m_type by auto
qed
show f_eq_m_q: "f = m ∘⇩c q"
using f_const f_type kernel_pair_equiv_rel m_def q_def quotient_func_eq by fastforce
show "⋀x. x : E → Y ⟹ f = x ∘⇩c q ⟹ x = m"
proof -
fix x
assume x_type[type_rule]: "x : E → Y"
assume f_eq_x_q: "f = x ∘⇩c q"
have "x ∘⇩c q = m ∘⇩c q"
using f_eq_m_q f_eq_x_q by auto
then show "x = m"
using epimorphism_def2 m_type q_epi q_type x_type by blast
qed
qed
qed
lemma epi_monic_factorization2:
assumes f_type[type_rule]: "f : X → Y"
shows "∃ g m E. g : X → E ∧ m : E → Y
∧ epimorphism g ∧ monomorphism m ∧ f = m ∘⇩c g
∧ (∀x. x : E → Y ⟶ f = x ∘⇩c g ⟶ x = m)"
using epi_monic_factorization coequalizer_is_epimorphism by (meson f_type)
subsubsection ‹Image of a Function›
text ‹The definition below corresponds to Definition 2.3.7 in Halvorson.›
definition image_of :: "cfunc ⇒ cset ⇒ cfunc ⇒ cset" ("_⦇_⦈⇘_⇙" [101,0,0]100) where
"image_of f A n = (SOME fA. ∃g m.
g : A → fA ∧
m : fA → codomain f ∧
coequalizer fA g (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism m ∧ f ∘⇩c n = m ∘⇩c g ∧ (∀x. x : fA → codomain f ⟶ f ∘⇩c n = x ∘⇩c g ⟶ x = m))"
lemma image_of_def2:
assumes "f : X → Y" "n : A → X"
shows "∃g m.
g : A → f⦇A⦈⇘n⇙ ∧
m : f⦇A⦈⇘n⇙ → Y ∧
coequalizer (f⦇A⦈⇘n⇙) g (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism m ∧ f ∘⇩c n = m ∘⇩c g ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘⇩c n = x ∘⇩c g ⟶ x = m)"
proof -
have "∃g m.
g : A → f⦇A⦈⇘n⇙ ∧
m : f⦇A⦈⇘n⇙ → codomain f ∧
coequalizer (f⦇A⦈⇘n⇙) g (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism m ∧ f ∘⇩c n = m ∘⇩c g ∧ (∀x. x : f⦇A⦈⇘n⇙ → codomain f ⟶ f ∘⇩c n = x ∘⇩c g ⟶ x = m)"
using assms cfunc_type_def comp_type epi_monic_factorization[where f="f ∘⇩c n", where X=A, where Y="codomain f"]
by (unfold image_of_def, subst someI_ex, auto)
then show ?thesis
using assms(1) cfunc_type_def by auto
qed
definition image_restriction_mapping :: "cfunc ⇒ cset × cfunc ⇒ cfunc" ("_↾⇘_⇙" [101,0]100) where
"image_restriction_mapping f An = (SOME g. ∃ m. g : fst An → f⦇fst An⦈⇘snd An⇙ ∧ m : f⦇fst An⦈⇘snd An⇙ → codomain f ∧
coequalizer (f⦇fst An⦈⇘snd An⇙) g (fibered_product_left_proj (fst An) (f ∘⇩c snd An) (f ∘⇩c snd An) (fst An)) (fibered_product_right_proj (fst An) (f ∘⇩c snd An) (f ∘⇩c snd An) (fst An)) ∧
monomorphism m ∧ f ∘⇩c snd An = m ∘⇩c g ∧ (∀x. x : f⦇fst An⦈⇘snd An⇙ → codomain f ⟶ f ∘⇩c snd An = x ∘⇩c g ⟶ x = m))"
lemma image_restriction_mapping_def2:
assumes "f : X → Y" "n : A → X"
shows "∃ m. f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ m : f⦇A⦈⇘n⇙ → Y ∧
coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism m ∧ f ∘⇩c n = m ∘⇩c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘⇩c n = x ∘⇩c (f↾⇘(A, n)⇙) ⟶ x = m)"
proof -
have codom_f: "codomain f = Y"
using assms(1) cfunc_type_def by auto
have "∃ m. f↾⇘(A, n)⇙ : fst (A, n) → f⦇fst (A, n)⦈⇘snd (A, n)⇙ ∧ m : f⦇fst (A, n)⦈⇘snd (A, n)⇙ → codomain f ∧
coequalizer (f⦇fst (A, n)⦈⇘snd (A, n)⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj (fst (A, n)) (f ∘⇩c snd (A, n)) (f ∘⇩c snd (A, n)) (fst (A, n))) (fibered_product_right_proj (fst (A, n)) (f ∘⇩c snd (A, n)) (f ∘⇩c snd (A, n)) (fst (A, n))) ∧
monomorphism m ∧ f ∘⇩c snd (A, n) = m ∘⇩c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇fst (A, n)⦈⇘snd (A, n)⇙ → codomain f ⟶ f ∘⇩c snd (A, n) = x ∘⇩c (f↾⇘(A, n)⇙) ⟶ x = m)"
unfolding image_restriction_mapping_def by (rule someI_ex, insert assms image_of_def2 codom_f, auto)
then show ?thesis
using codom_f by simp
qed
definition image_subobject_mapping :: "cfunc ⇒ cset ⇒ cfunc ⇒ cfunc" ("[_⦇_⦈⇘_⇙]map" [101,0,0]100) where
"[f⦇A⦈⇘n⇙]map = (THE m. f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ m : f⦇A⦈⇘n⇙ → codomain f ∧
coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism m ∧ f ∘⇩c n = m ∘⇩c (f↾⇘(A, n)⇙) ∧ (∀x. x : (f⦇A⦈⇘n⇙) → codomain f ⟶ f ∘⇩c n = x ∘⇩c (f↾⇘(A, n)⇙) ⟶ x = m))"
lemma image_subobject_mapping_def2:
assumes "f : X → Y" "n : A → X"
shows "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ [f⦇A⦈⇘n⇙]map : f⦇A⦈⇘n⇙ → Y ∧
coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism ([f⦇A⦈⇘n⇙]map) ∧ f ∘⇩c n = [f⦇A⦈⇘n⇙]map ∘⇩c (f↾⇘(A, n)⇙) ∧ (∀x. x : f⦇A⦈⇘n⇙ → Y ⟶ f ∘⇩c n = x ∘⇩c (f↾⇘(A, n)⇙) ⟶ x = [f⦇A⦈⇘n⇙]map)"
proof -
have codom_f: "codomain f = Y"
using assms(1) cfunc_type_def by auto
have "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙ ∧ ([f⦇A⦈⇘n⇙]map) : f⦇A⦈⇘n⇙ → codomain f ∧
coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A) ∧
monomorphism ([f⦇A⦈⇘n⇙]map) ∧ f ∘⇩c n = ([f⦇A⦈⇘n⇙]map) ∘⇩c (f↾⇘(A, n)⇙) ∧
(∀x. x : (f⦇A⦈⇘n⇙) → codomain f ⟶ f ∘⇩c n = x ∘⇩c (f↾⇘(A, n)⇙) ⟶ x = ([f⦇A⦈⇘n⇙]map))"
unfolding image_subobject_mapping_def
by (rule theI', insert assms codom_f image_restriction_mapping_def2, blast)
then show ?thesis
using codom_f by fastforce
qed
lemma image_rest_map_type[type_rule]:
assumes "f : X → Y" "n : A → X"
shows "f↾⇘(A, n)⇙ : A → f⦇A⦈⇘n⇙"
using assms image_restriction_mapping_def2 by blast
lemma image_rest_map_coequalizer:
assumes "f : X → Y" "n : A → X"
shows "coequalizer (f⦇A⦈⇘n⇙) (f↾⇘(A, n)⇙) (fibered_product_left_proj A (f ∘⇩c n) (f ∘⇩c n) A) (fibered_product_right_proj A (f ∘⇩c n) (f ∘⇩c n) A)"
using assms image_restriction_mapping_def2 by blast
lemma image_rest_map_epi:
assumes "f : X → Y" "n : A → X"
shows "epimorphism (f↾⇘(A, n)⇙)"
using assms image_rest_map_coequalizer coequalizer_is_epimorphism by blast
lemma image_subobj_map_type[type_rule]:
assumes "f : X → Y" "n : A → X"
shows "[f⦇A⦈⇘n⇙]map : f⦇A⦈⇘n⇙ → Y"
using assms image_subobject_mapping_def2 by blast
lemma image_subobj_map_mono:
assumes "f : X → Y" "n : A → X"
shows "monomorphism ([f⦇A⦈⇘n⇙]map)"
using assms image_subobject_mapping_def2 by blast
lemma image_subobj_comp_image_rest:
assumes "f : X → Y" "n : A → X"
shows "[f⦇A⦈⇘n⇙]map ∘⇩c (f↾⇘(A, n)⇙) = f ∘⇩c n"
using assms image_subobject_mapping_def2 by auto
lemma image_subobj_map_unique:
assumes "f : X → Y" "n : A → X"
shows "x : f⦇A⦈⇘n⇙ → Y ⟹ f ∘⇩c n = x ∘⇩c (f↾⇘(A, n)⇙) ⟹ x = [f⦇A⦈⇘n⇙]map"
using assms image_subobject_mapping_def2 by blast
lemma image_self:
assumes "f : X → Y" and "monomorphism f"
assumes "a : A → X" and "monomorphism a"
shows "f⦇A⦈⇘a⇙ ≅ A"
proof -
have "monomorphism (f ∘⇩c a)"
using assms cfunc_type_def composition_of_monic_pair_is_monic by auto
then have "monomorphism ([f⦇A⦈⇘a⇙]map ∘⇩c (f↾⇘(A, a)⇙))"
using assms image_subobj_comp_image_rest by auto
then have "monomorphism (f↾⇘(A, a)⇙)"
by (meson assms comp_monic_imp_monic' image_rest_map_type image_subobj_map_type)
then have "isomorphism (f↾⇘(A, a)⇙)"
using assms epi_mon_is_iso image_rest_map_epi by blast
then have "A ≅ f⦇A⦈⇘a⇙"
using assms unfolding is_isomorphic_def by (intro exI[where x="f↾⇘(A, a)⇙"], typecheck_cfuncs)
then show ?thesis
by (simp add: isomorphic_is_symmetric)
qed
text ‹The lemma below corresponds to Proposition 2.3.8 in Halvorson.›
lemma image_smallest_subobject:
assumes f_type[type_rule]: "f : X → Y" and a_type[type_rule]: "a : A → X"
shows "(B, n) ⊆⇩c Y ⟹ f factorsthru n ⟹ (f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, n)"
proof -
assume "(B, n) ⊆⇩c Y"
then have n_type[type_rule]: "n : B → Y" and n_mono: "monomorphism n"
unfolding subobject_of_def2 by auto
assume "f factorsthru n"
then obtain g where g_type[type_rule]: "g : X → B" and f_eq_ng: "n ∘⇩c g = f"
using factors_through_def2 by (typecheck_cfuncs, auto)
have fa_type[type_rule]: "f ∘⇩c a : A → Y"
by (typecheck_cfuncs)
obtain p0 where p0_def[simp]: "p0 = fibered_product_left_proj A (f∘⇩ca) (f∘⇩ca) A"
by auto
obtain p1 where p1_def[simp]: "p1 = fibered_product_right_proj A (f∘⇩ca) (f∘⇩ca) A"
by auto
obtain E where E_def[simp]: "E = A ⇘f ∘⇩c a⇙×⇩c⇘f ∘⇩c a⇙ A"
by auto
have fa_coequalizes: "(f ∘⇩c a) ∘⇩c p0 = (f ∘⇩c a) ∘⇩c p1"
using fa_type fibered_product_proj_eq by auto
have ga_coequalizes: "(g ∘⇩c a) ∘⇩c p0 = (g ∘⇩c a) ∘⇩c p1"
proof -
from fa_coequalizes have "n ∘⇩c ((g ∘⇩c a) ∘⇩c p0) = n ∘⇩c ((g ∘⇩c a) ∘⇩c p1)"
by (auto, typecheck_cfuncs, auto simp add: f_eq_ng comp_associative2)
then show "(g ∘⇩c a) ∘⇩c p0 = (g ∘⇩c a) ∘⇩c p1"
using n_mono unfolding monomorphism_def2 by (auto, typecheck_cfuncs_prems, meson)
qed
have "∀h F. h : A → F ∧ h ∘⇩c p0 = h ∘⇩c p1 ⟶ (∃!k. k : f⦇A⦈⇘a⇙ → F ∧ k ∘⇩c f↾⇘(A, a)⇙ = h)"
using image_rest_map_coequalizer[where n=a] unfolding coequalizer_def
by (simp, typecheck_cfuncs, auto simp add: cfunc_type_def)
then obtain k where k_type[type_rule]: "k : f⦇A⦈⇘a⇙ → B" and k_e_eq_g: "k ∘⇩c f↾⇘(A, a)⇙ = g ∘⇩c a"
using ga_coequalizes by (typecheck_cfuncs, blast)
then have "n ∘⇩c k = [f⦇A⦈⇘a⇙]map"
by (typecheck_cfuncs, smt (z3) comp_associative2 f_eq_ng g_type image_rest_map_type image_subobj_map_unique k_e_eq_g)
then show "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, n)"
unfolding relative_subset_def2
using image_subobj_map_mono k_type n_mono by (typecheck_cfuncs, blast)
qed
lemma images_iso:
assumes f_type[type_rule]: "f : X → Y"
assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z"
shows "(f ∘⇩c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘⇩c n⇙"
proof -
have f_m_image_coequalizer:
"coequalizer ((f ∘⇩c m)⦇A⦈⇘n⇙) ((f ∘⇩c m)↾⇘(A, n)⇙)
(fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)
(fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)"
by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
have f_image_coequalizer:
"coequalizer (f⦇A⦈⇘m ∘⇩c n⇙) (f↾⇘(A, m ∘⇩c n)⇙)
(fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)
(fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)"
by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
from f_m_image_coequalizer f_image_coequalizer
show "(f ∘⇩c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘⇩c n⇙"
by (meson coequalizer_unique)
qed
lemma image_subset_conv:
assumes f_type[type_rule]: "f : X → Y"
assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z"
shows "∃i. ((f ∘⇩c m)⦇A⦈⇘n⇙, i) ⊆⇩c B ⟹ ∃j. (f⦇A⦈⇘m ∘⇩c n⇙, j) ⊆⇩c B"
proof -
assume "∃i. ((f ∘⇩c m)⦇A⦈⇘n⇙, i) ⊆⇩c B"
then obtain i where
i_type[type_rule]: "i : (f ∘⇩c m)⦇A⦈⇘n⇙ → B" and
i_mono: "monomorphism i"
unfolding subobject_of_def by force
have "(f ∘⇩c m)⦇A⦈⇘n⇙ ≅ f⦇A⦈⇘m ∘⇩c n⇙"
using f_type images_iso m_type n_type by blast
then obtain k where
k_type[type_rule]: "k : f⦇A⦈⇘m ∘⇩c n⇙ → (f ∘⇩c m)⦇A⦈⇘n⇙" and
k_mono: "monomorphism k"
by (meson is_isomorphic_def iso_imp_epi_and_monic isomorphic_is_symmetric)
then show "∃j. (f⦇A⦈⇘m ∘⇩c n⇙, j) ⊆⇩c B"
unfolding subobject_of_def using composition_of_monic_pair_is_monic i_mono
by (intro exI[where x="i ∘⇩c k"], typecheck_cfuncs, simp add: cfunc_type_def)
qed
lemma image_rel_subset_conv:
assumes f_type[type_rule]: "f : X → Y"
assumes m_type[type_rule]: "m : Z → X" and n_type[type_rule]: "n : A → Z"
assumes rel_sub1: "((f ∘⇩c m)⦇A⦈⇘n⇙, [(f ∘⇩c m)⦇A⦈⇘n⇙]map) ⊆⇘Y⇙ (B,b)"
shows "(f⦇A⦈⇘m ∘⇩c n⇙, [f⦇A⦈⇘m ∘⇩c n⇙]map) ⊆⇘Y⇙ (B,b)"
using rel_sub1 image_subobj_map_mono
unfolding relative_subset_def2
proof (typecheck_cfuncs, safe)
fix k
assume k_type[type_rule]: "k : (f ∘⇩c m)⦇A⦈⇘n⇙ → B"
assume b_type[type_rule]: "b : B → Y"
assume b_mono: "monomorphism b"
assume b_k_eq_map: "b ∘⇩c k = [(f ∘⇩c m)⦇A⦈⇘n⇙]map"
have f_m_image_coequalizer:
"coequalizer ((f ∘⇩c m)⦇A⦈⇘n⇙) ((f ∘⇩c m)↾⇘(A, n)⇙)
(fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)
(fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)"
by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
then have f_m_image_coequalises:
"(f ∘⇩c m)↾⇘(A, n)⇙ ∘⇩c fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A
= (f ∘⇩c m)↾⇘(A, n)⇙ ∘⇩c fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A"
by (typecheck_cfuncs_prems, unfold coequalizer_def2, auto)
have f_image_coequalizer:
"coequalizer (f⦇A⦈⇘m ∘⇩c n⇙) (f↾⇘(A, m ∘⇩c n)⇙)
(fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)
(fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A)"
by (typecheck_cfuncs, smt comp_associative2 image_restriction_mapping_def2)
then have "⋀ h F. h : A → F ⟹
h ∘⇩c fibered_product_left_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A =
h ∘⇩c fibered_product_right_proj A (f ∘⇩c m ∘⇩c n) (f ∘⇩c m ∘⇩c n) A ⟹
(∃!k. k : f⦇A⦈⇘m ∘⇩c n⇙ → F ∧ k ∘⇩c f↾⇘(A, m ∘⇩c n)⇙ = h)"
by (typecheck_cfuncs_prems, unfold coequalizer_def2, auto)
then have "∃!k. k : f⦇A⦈⇘m ∘⇩c n⇙ → (f ∘⇩c m)⦇A⦈⇘n⇙ ∧ k ∘⇩c f↾⇘(A, m ∘⇩c n)⇙ = (f ∘⇩c m)↾⇘(A, n)⇙"
using f_m_image_coequalises by (typecheck_cfuncs, presburger)
then obtain k' where
k'_type[type_rule]: "k' : f⦇A⦈⇘m ∘⇩c n⇙ → (f ∘⇩c m)⦇A⦈⇘n⇙" and
k'_eq: "k' ∘⇩c f↾⇘(A, m ∘⇩c n)⇙ = (f ∘⇩c m)↾⇘(A, n)⇙"
by auto
have k'_maps_eq: "[f⦇A⦈⇘m ∘⇩c n⇙]map = [(f ∘⇩c m)⦇A⦈⇘n⇙]map ∘⇩c k'"
by (typecheck_cfuncs, smt (z3) comp_associative2 image_subobject_mapping_def2 k'_eq)
have k_mono: "monomorphism k"
by (metis b_k_eq_map cfunc_type_def comp_monic_imp_monic k_type rel_sub1 relative_subset_def2)
have k'_mono: "monomorphism k'"
by (smt (verit, ccfv_SIG) cfunc_type_def comp_monic_imp_monic comp_type f_type image_subobject_mapping_def2 k'_maps_eq k'_type m_type n_type)
show "∃k. k : f⦇A⦈⇘m ∘⇩c n⇙ → B ∧ b ∘⇩c k = [f⦇A⦈⇘m ∘⇩c n⇙]map"
by (intro exI[where x="k ∘⇩c k'"], typecheck_cfuncs, simp add: b_k_eq_map comp_associative2 k'_maps_eq)
qed
text ‹The lemma below corresponds to Proposition 2.3.9 in Halvorson.›
lemma subset_inv_image_iff_image_subset:
assumes "(A,a) ⊆⇩c X" "(B,m) ⊆⇩c Y"
assumes[type_rule]: "f : X → Y"
shows "((A, a) ⊆⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙,[f⇧-⇧1⦇B⦈⇘m⇙]map)) = ((f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B,m))"
proof safe
have b_mono: "monomorphism(m)"
using assms(2) subobject_of_def2 by blast
have b_type[type_rule]: "m : B → Y"
using assms(2) subobject_of_def2 by blast
obtain m' where m'_def: "m' = [f⇧-⇧1⦇B⦈⇘m⇙]map"
by blast
then have m'_type[type_rule]: "m' : f⇧-⇧1⦇B⦈⇘m⇙ → X"
using assms(3) b_mono inverse_image_subobject_mapping_type m'_def by (typecheck_cfuncs, force)
assume "(A, a) ⊆⇘X⇙ (f⇧-⇧1⦇B⦈⇘m⇙, [f⇧-⇧1⦇B⦈⇘m⇙]map)"
then have a_type[type_rule]: "a : A → X" and
a_mono: "monomorphism a" and
k_exists: "∃k. k : A → f⇧-⇧1⦇B⦈⇘m⇙ ∧ [f⇧-⇧1⦇B⦈⇘m⇙]map ∘⇩c k = a"
unfolding relative_subset_def2 by auto
then obtain k where k_type[type_rule]: "k : A → f⇧-⇧1⦇B⦈⇘m⇙" and k_a_eq: "[f⇧-⇧1⦇B⦈⇘m⇙]map ∘⇩c k = a"
by auto
obtain d where d_def: "d = m' ∘⇩c k"
by simp
obtain j where j_def: "j = [f⦇A⦈⇘d⇙]map"
by simp
then have j_type[type_rule]: "j : f⦇A⦈⇘d⇙ → Y"
using assms(3) comp_type d_def m'_type image_subobj_map_type k_type by presburger
obtain e where e_def: "e = f↾⇘(A, d)⇙"
by simp
then have e_type[type_rule]: "e : A → f⦇A⦈⇘d⇙"
using assms(3) comp_type d_def image_rest_map_type k_type m'_type by blast
have je_equals: "j ∘⇩c e = f ∘⇩c m' ∘⇩c k"
by (typecheck_cfuncs, simp add: d_def e_def image_subobj_comp_image_rest j_def)
have "(f ∘⇩c m' ∘⇩c k) factorsthru m"
proof(typecheck_cfuncs, unfold factors_through_def2)
obtain middle_arrow where middle_arrow_def:
"middle_arrow = (right_cart_proj X B) ∘⇩c (inverse_image_mapping f B m)"
by simp
then have middle_arrow_type[type_rule]: "middle_arrow : f⇧-⇧1⦇B⦈⇘m⇙ → B"
unfolding middle_arrow_def using b_mono by (typecheck_cfuncs)
show "∃h. h : A → B ∧ m ∘⇩c h = f ∘⇩c m' ∘⇩c k"
by (intro exI[where x="middle_arrow ∘⇩c k"], typecheck_cfuncs,
simp add: b_mono cfunc_type_def comp_associative2 inverse_image_mapping_eq inverse_image_subobject_mapping_def m'_def middle_arrow_def)
qed
then have "((f ∘⇩c m' ∘⇩c k)⦇A⦈⇘id⇩c A⇙, [(f ∘⇩c m' ∘⇩c k)⦇A⦈⇘id⇩c A⇙]map) ⊆⇘Y⇙ (B, m)"
by (typecheck_cfuncs, meson assms(2) image_smallest_subobject)
then have "((f ∘⇩c a)⦇A⦈⇘id⇩c A⇙, [(f ∘⇩c a)⦇A⦈⇘id⇩c A⇙]map) ⊆⇘Y⇙ (B, m)"
by (simp add: k_a_eq m'_def)
then show "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map)⊆⇘Y⇙(B, m)"
by (typecheck_cfuncs, metis id_right_unit2 id_type image_rel_subset_conv)
next
have m_mono: "monomorphism(m)"
using assms(2) subobject_of_def2 by blast
have m_type[type_rule]: "m : B → Y"
using assms(2) subobject_of_def2 by blast
assume "(f⦇A⦈⇘a⇙, [f⦇A⦈⇘a⇙]map) ⊆⇘Y⇙ (B, m)"
then obtain s where
s_type[type_rule]: "s : f⦇A⦈⇘a⇙ → B" and
m_s_eq_subobj_map: "m ∘⇩c s = [f⦇A⦈⇘a⇙]map"
unfolding relative_subset_def2 by auto
have a_mono: "monomorphism a"
using assms(1) unfolding subobject_of_def2 by auto
have pullback_map1_type[type_rule]: "s ∘⇩c f↾⇘(A, a)⇙ : A → B"
using assms(1) unfolding subobject_of_def2 by (auto, typecheck_cfuncs)
have pullback_map2_type[type_rule]: "a : A → X"
using assms(1) unfolding subobject_of_def2 by auto
have pullback_maps_commute: "m ∘⇩c s ∘⇩c f↾⇘(A, a)⇙ = f ∘⇩c a"
by (typecheck_cfuncs, simp add: comp_associative2 image_subobj_comp_image_rest m_s_eq_subobj_map)
have "⋀Z k h. k : Z → B ⟹ h : Z → X ⟹ m ∘⇩c k = f ∘⇩c h ⟹
(∃!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)"
using inverse_image_pullback assms(3) m_mono m_type unfolding is_pullback_def by simp
then obtain k where k_type[type_rule]: "k : A → f⇧-⇧1⦇B⦈⇘m⇙" and
k_right_eq: "(right_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c k = s ∘⇩c f↾⇘(A, a)⇙" and
k_left_eq: "(left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c k = a"
using pullback_map1_type pullback_map2_type pullback_maps_commute by blast
have "monomorphism ((left_cart_proj X B ∘⇩c inverse_image_mapping f B m) ∘⇩c k) ⟹ monomorphism k"
using comp_monic_imp_monic' m_mono by (typecheck_cfuncs, blast)
then have "monomorphism k"
by (simp add: a_mono k_left_eq)
then show "(A, a)⊆⇘X⇙(f⇧-⇧1⦇B⦈⇘m⇙, [f⇧-⇧1⦇B⦈⇘m⇙]map)"
unfolding relative_subset_def2
using assms a_mono m_mono inverse_image_subobject_mapping_mono
proof (typecheck_cfuncs, safe)
assume "monomorphism k"
then show "∃k. k : A → f⇧-⇧1⦇B⦈⇘m⇙ ∧ [f⇧-⇧1⦇B⦈⇘m⇙]map ∘⇩c k = a"
using assms(3) inverse_image_subobject_mapping_def2 k_left_eq k_type
by (intro exI[where x=k], force)
qed
qed
text ‹The lemma below corresponds to Exercise 2.3.10 in Halvorson.›
lemma in_inv_image_of_image:
assumes "(A,m) ⊆⇩c X"
assumes[type_rule]: "f : X → Y"
shows "(A,m) ⊆⇘X⇙ (f⇧-⇧1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙, [f⇧-⇧1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙]map)"
proof -
have m_type[type_rule]: "m : A → X"
using assms(1) unfolding subobject_of_def2 by auto
have m_mono: "monomorphism m"
using assms(1) unfolding subobject_of_def2 by auto
have "((f⦇A⦈⇘m⇙, [f⦇A⦈⇘m⇙]map) ⊆⇘Y⇙ (f⦇A⦈⇘m⇙, [f⦇A⦈⇘m⇙]map))"
unfolding relative_subset_def2
using m_mono image_subobj_map_mono id_right_unit2 id_type by (typecheck_cfuncs, blast)
then show "(A,m) ⊆⇘X⇙ (f⇧-⇧1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙, [f⇧-⇧1⦇f⦇A⦈⇘m⇙⦈⇘[f⦇A⦈⇘m⇙]map⇙]map)"
by (meson assms relative_subset_def2 subobject_of_def2 subset_inv_image_iff_image_subset)
qed
subsection ‹@{term distribute_left} and @{term distribute_right} as Equivalence Relations›
lemma left_pair_subset:
assumes "m : Y → X ×⇩c X" "monomorphism m"
shows "(Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ⊆⇩c (X ×⇩c Z) ×⇩c (X ×⇩c Z)"
unfolding subobject_of_def2 using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
fix g h A
assume g_type: "g : A → Y ×⇩c Z"
assume h_type: "h : A → Y ×⇩c Z"
assume "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c g = (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c h"
then have "distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c g = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c h"
using assms g_type h_type by (typecheck_cfuncs, simp add: comp_associative2)
then have "(m ×⇩f id⇩c Z) ∘⇩c g = (m ×⇩f id⇩c Z) ∘⇩c h"
using assms g_type h_type distribute_right_mono distribute_right_type monomorphism_def2
by (typecheck_cfuncs, blast)
then show "g = h"
proof -
have "monomorphism (m ×⇩f id⇩c Z)"
using assms cfunc_cross_prod_mono id_isomorphism iso_imp_epi_and_monic by (typecheck_cfuncs, blast)
then show "(m ×⇩f id⇩c Z) ∘⇩c g = (m ×⇩f id⇩c Z) ∘⇩c h ⟹ g = h"
using assms g_type h_type unfolding monomorphism_def2 by (typecheck_cfuncs, blast)
qed
qed
lemma right_pair_subset:
assumes "m : Y → X ×⇩c X" "monomorphism m"
shows "(Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ⊆⇩c (Z ×⇩c X) ×⇩c (Z ×⇩c X)"
unfolding subobject_of_def2 using assms
proof (typecheck_cfuncs, unfold monomorphism_def3, clarify)
fix g h A
assume g_type: "g : A → Z ×⇩c Y"
assume h_type: "h : A → Z ×⇩c Y"
assume "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c g = (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c h"
then have "distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c g = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c h"
using assms g_type h_type by (typecheck_cfuncs, simp add: comp_associative2)
then have "(id⇩c Z ×⇩f m) ∘⇩c g = (id⇩c Z ×⇩f m) ∘⇩c h"
using assms g_type h_type distribute_left_mono distribute_left_type monomorphism_def2
by (typecheck_cfuncs, blast)
then show "g = h"
proof -
have "monomorphism (id⇩c Z ×⇩f m)"
using assms cfunc_cross_prod_mono id_isomorphism id_type iso_imp_epi_and_monic by blast
then show "(id⇩c Z ×⇩f m) ∘⇩c g = (id⇩c Z ×⇩f m) ∘⇩c h ⟹ g = h"
using assms g_type h_type unfolding monomorphism_def2 by (typecheck_cfuncs, blast)
qed
qed
lemma left_pair_reflexive:
assumes "reflexive_on X (Y, m)"
shows "reflexive_on (X ×⇩c Z) (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z))"
proof (unfold reflexive_on_def, safe)
have "m : Y → X ×⇩c X ∧ monomorphism m"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
then show "(Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ⊆⇩c (X ×⇩c Z) ×⇩c X ×⇩c Z"
by (simp add: left_pair_subset)
next
fix xz
have m_type: "m : Y → X ×⇩c X"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
assume xz_type: "xz ∈⇩c X ×⇩c Z"
then obtain x z where x_type: "x ∈⇩c X" and z_type: "z ∈⇩c Z" and xz_def: "xz = ⟨x, z⟩"
using cart_prod_decomp by blast
then show "⟨xz,xz⟩ ∈⇘(X ×⇩c Z) ×⇩c X ×⇩c Z⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using m_type
proof (clarify, typecheck_cfuncs, unfold relative_member_def2, safe)
have "monomorphism m"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
then show "monomorphism (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using cfunc_cross_prod_mono cfunc_type_def composition_of_monic_pair_is_monic distribute_right_mono id_isomorphism iso_imp_epi_and_monic m_type by (typecheck_cfuncs, auto)
next
have xzxz_type: "⟨⟨x,z⟩,⟨x,z⟩⟩ ∈⇩c (X ×⇩c Z) ×⇩c X ×⇩c Z"
using xz_type cfunc_prod_type xz_def by blast
obtain y where y_def: "y ∈⇩c Y" "m ∘⇩c y = ⟨x, x⟩"
using assms reflexive_def2 x_type by blast
have mid_type: "m ×⇩f id⇩c Z : Y ×⇩c Z → (X ×⇩c X) ×⇩c Z"
by (simp add: cfunc_cross_prod_type id_type m_type)
have dist_mid_type:"distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z : Y ×⇩c Z → (X ×⇩c Z) ×⇩c X ×⇩c Z"
using comp_type distribute_right_type mid_type by force
have yz_type: "⟨y,z⟩ ∈⇩c Y ×⇩c Z"
by (typecheck_cfuncs, simp add: ‹z ∈⇩c Z› y_def)
have "(distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c ⟨y,z⟩ = distribute_right X X Z ∘⇩c (m ×⇩f id(Z)) ∘⇩c ⟨y,z⟩"
using comp_associative2 mid_type yz_type by (typecheck_cfuncs, auto)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c y,id(Z) ∘⇩c z⟩"
using z_type cfunc_cross_prod_comp_cfunc_prod m_type y_def by (typecheck_cfuncs, auto)
also have distxxz: "... = distribute_right X X Z ∘⇩c ⟨ ⟨x, x⟩, z⟩"
using z_type id_left_unit2 y_def by auto
also have "... = ⟨⟨x,z⟩,⟨x,z⟩⟩"
by (meson z_type distribute_right_ap x_type)
ultimately show "⟨⟨x,z⟩,⟨x,z⟩⟩ factorsthru (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using dist_mid_type distxxz factors_through_def2 xzxz_type yz_type by (typecheck_cfuncs, auto)
qed
qed
lemma right_pair_reflexive:
assumes "reflexive_on X (Y, m)"
shows "reflexive_on (Z ×⇩c X) (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
proof (unfold reflexive_on_def, safe)
have "m : Y → X ×⇩c X ∧ monomorphism m"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
then show "(Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ⊆⇩c (Z ×⇩c X) ×⇩c Z ×⇩c X"
by (simp add: right_pair_subset)
next
fix zx
have m_type: "m : Y → X ×⇩c X"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
assume zx_type: "zx ∈⇩c Z ×⇩c X"
then obtain z x where x_type: "x ∈⇩c X" and z_type: "z ∈⇩c Z" and zx_def: "zx = ⟨z, x⟩"
using cart_prod_decomp by blast
then show "⟨zx,zx⟩ ∈⇘(Z ×⇩c X) ×⇩c Z ×⇩c X⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using m_type
proof (clarify, typecheck_cfuncs, unfold relative_member_def2, safe)
have "monomorphism m"
using assms unfolding reflexive_on_def subobject_of_def2 by auto
then show "monomorphism (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using cfunc_cross_prod_mono cfunc_type_def composition_of_monic_pair_is_monic distribute_left_mono id_isomorphism iso_imp_epi_and_monic m_type by (typecheck_cfuncs, auto)
next
have zxzx_type: "⟨⟨z,x⟩,⟨z,x⟩⟩ ∈⇩c (Z ×⇩c X) ×⇩c Z ×⇩c X"
using zx_type cfunc_prod_type zx_def by blast
obtain y where y_def: "y ∈⇩c Y" "m ∘⇩c y = ⟨x, x⟩"
using assms reflexive_def2 x_type by blast
have mid_type: "(id⇩c Z ×⇩f m) : Z ×⇩c Y → Z ×⇩c (X ×⇩c X)"
by (simp add: cfunc_cross_prod_type id_type m_type)
have dist_mid_type:"distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) : Z ×⇩c Y → (Z ×⇩c X) ×⇩c Z ×⇩c X"
using comp_type distribute_left_type mid_type by force
have yz_type: "⟨z,y⟩ ∈⇩c Z ×⇩c Y"
by (typecheck_cfuncs, simp add: ‹z ∈⇩c Z› y_def)
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c ⟨z,y⟩ = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c ⟨z,y⟩"
using comp_associative2 mid_type yz_type by (typecheck_cfuncs, auto)
also have "... = distribute_left Z X X ∘⇩c ⟨id⇩c Z ∘⇩c z , m ∘⇩c y ⟩"
using z_type cfunc_cross_prod_comp_cfunc_prod m_type y_def by (typecheck_cfuncs, auto)
also have distxxz: "... = distribute_left Z X X ∘⇩c ⟨z, ⟨x, x⟩⟩"
using z_type id_left_unit2 y_def by auto
also have "... = ⟨⟨z,x⟩,⟨z,x⟩⟩"
by (meson z_type distribute_left_ap x_type)
ultimately show "⟨⟨z,x⟩,⟨z,x⟩⟩ factorsthru (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using z_type distribute_left_ap x_type dist_mid_type factors_through_def2 yz_type zxzx_type by auto
qed
qed
lemma left_pair_symmetric:
assumes "symmetric_on X (Y, m)"
shows "symmetric_on (X ×⇩c Z) (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z))"
proof (unfold symmetric_on_def, safe)
have "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 symmetric_on_def by auto
then show "(Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ⊆⇩c (X ×⇩c Z) ×⇩c X ×⇩c Z"
by (simp add: left_pair_subset)
next
have m_def[type_rule]: "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 symmetric_on_def by auto
fix s t
assume s_type[type_rule]: "s ∈⇩c X ×⇩c Z"
assume t_type[type_rule]: "t ∈⇩c X ×⇩c Z"
assume st_relation: "⟨s,t⟩ ∈⇘(X ×⇩c Z) ×⇩c X ×⇩c Z⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
obtain sx sz where s_def[type_rule]: " sx ∈⇩c X" "sz ∈⇩c Z" "s = ⟨sx,sz⟩"
using cart_prod_decomp s_type by blast
obtain tx tz where t_def[type_rule]: "tx ∈⇩c X" "tz ∈⇩c Z" "t = ⟨tx,tz⟩"
using cart_prod_decomp t_type by blast
show "⟨t,s⟩ ∈⇘(X ×⇩c Z) ×⇩c (X ×⇩c Z)⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z))"
using s_def t_def m_def
proof (typecheck_cfuncs, clarify, unfold relative_member_def2, safe)
show "monomorphism (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using relative_member_def2 st_relation by blast
have "⟨⟨sx,sz⟩, ⟨tx,tz⟩⟩ factorsthru (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using st_relation s_def t_def unfolding relative_member_def2 by auto
then obtain yz where yz_type[type_rule]: "yz ∈⇩c Y ×⇩c Z"
and yz_def: "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c yz = ⟨⟨sx,sz⟩, ⟨tx,tz⟩⟩"
using s_def t_def m_def by (typecheck_cfuncs, unfold factors_through_def2, auto)
then obtain y z where
y_type[type_rule]: "y ∈⇩c Y" and z_type[type_rule]: "z ∈⇩c Z" and yz_pair: "yz = ⟨y, z⟩"
using cart_prod_decomp by blast
then obtain my1 my2 where my_types[type_rule]: "my1 ∈⇩c X" "my2 ∈⇩c X" and my_def: "m ∘⇩c y = ⟨my1,my2⟩"
by (metis cart_prod_decomp cfunc_type_def codomain_comp domain_comp m_def(1))
then obtain y' where y'_type[type_rule]: "y' ∈⇩c Y" and y'_def: "m ∘⇩c y' = ⟨my2,my1⟩"
using assms symmetric_def2 y_type by blast
have "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c yz = ⟨⟨my1,z⟩, ⟨my2,z⟩⟩"
proof -
have "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c yz = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c ⟨y, z⟩"
unfolding yz_pair by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c y, id⇩c Z ∘⇩c z⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = distribute_right X X Z ∘⇩c ⟨⟨my1,my2⟩, z⟩"
unfolding my_def by (typecheck_cfuncs, simp add: id_left_unit2)
also have "... = ⟨⟨my1,z⟩, ⟨my2,z⟩⟩"
using distribute_right_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
then have "⟨⟨sx,sz⟩,⟨tx,tz⟩⟩ = ⟨⟨my1,z⟩,⟨my2,z⟩⟩"
using yz_def by auto
then have "⟨sx,sz⟩ = ⟨my1,z⟩ ∧ ⟨tx,tz⟩ = ⟨my2,z⟩"
using element_pair_eq by (typecheck_cfuncs, auto)
then have eqs: "sx = my1 ∧ sz = z ∧ tx = my2 ∧ tz = z"
using element_pair_eq by (typecheck_cfuncs, auto)
have "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c ⟨y',z⟩ = ⟨⟨tx,tz⟩, ⟨sx,sz⟩⟩"
proof -
have "(distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z)) ∘⇩c ⟨y',z⟩ = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c ⟨y',z⟩"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c y',id⇩c Z ∘⇩c z⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = distribute_right X X Z ∘⇩c ⟨⟨my2,my1⟩, z⟩"
unfolding y'_def by (typecheck_cfuncs, simp add: id_left_unit2)
also have "... = ⟨⟨my2,z⟩, ⟨my1,z⟩⟩"
using distribute_right_ap by (typecheck_cfuncs, auto)
also have "... = ⟨⟨tx,tz⟩, ⟨sx,sz⟩⟩"
using eqs by auto
finally show ?thesis.
qed
then show "⟨⟨tx,tz⟩,⟨sx,sz⟩⟩ factorsthru (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
by (typecheck_cfuncs, metis cfunc_prod_type eqs factors_through_def2 y'_type)
qed
qed
lemma right_pair_symmetric:
assumes "symmetric_on X (Y, m)"
shows "symmetric_on (Z ×⇩c X) (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
proof (unfold symmetric_on_def, safe)
have "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 symmetric_on_def by auto
then show "(Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ⊆⇩c (Z ×⇩c X) ×⇩c Z ×⇩c X"
by (simp add: right_pair_subset)
next
have m_def[type_rule]: "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 symmetric_on_def by auto
fix s t
assume s_type[type_rule]: "s ∈⇩c Z ×⇩c X"
assume t_type[type_rule]: "t ∈⇩c Z ×⇩c X"
assume st_relation: "⟨s,t⟩ ∈⇘(Z ×⇩c X) ×⇩c Z ×⇩c X⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
obtain xs zs where s_def[type_rule]: " xs ∈⇩c Z" "zs ∈⇩c X" "s = ⟨xs,zs⟩"
using cart_prod_decomp s_type by blast
obtain xt zt where t_def[type_rule]: "xt ∈⇩c Z" "zt ∈⇩c X" "t = ⟨xt,zt⟩"
using cart_prod_decomp t_type by blast
show "⟨t,s⟩ ∈⇘(Z ×⇩c X) ×⇩c (Z ×⇩c X)⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using s_def t_def m_def
proof (typecheck_cfuncs, clarify, unfold relative_member_def2, safe)
show "monomorphism (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using relative_member_def2 st_relation by blast
have "⟨⟨xs,zs⟩, ⟨xt,zt⟩⟩ factorsthru (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
using st_relation s_def t_def unfolding relative_member_def2 by auto
then obtain zy where zy_type[type_rule]: "zy ∈⇩c Z ×⇩c Y"
and zy_def: "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c zy = ⟨⟨xs,zs⟩, ⟨xt,zt⟩⟩"
using s_def t_def m_def by (typecheck_cfuncs, unfold factors_through_def2, auto)
then obtain y z where
y_type[type_rule]: "y ∈⇩c Y" and z_type[type_rule]: "z ∈⇩c Z" and yz_pair: "zy = ⟨z, y⟩"
using cart_prod_decomp by blast
then obtain my1 my2 where my_types[type_rule]: "my1 ∈⇩c X" "my2 ∈⇩c X" and my_def: "m ∘⇩c y = ⟨my2,my1⟩"
by (metis cart_prod_decomp cfunc_type_def codomain_comp domain_comp m_def(1))
then obtain y' where y'_type[type_rule]: "y' ∈⇩c Y" and y'_def: "m ∘⇩c y' = ⟨my1,my2⟩"
using assms symmetric_def2 y_type by blast
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c zy = ⟨⟨z,my2⟩, ⟨z,my1⟩⟩"
proof -
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c zy = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c zy"
unfolding yz_pair by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = distribute_left Z X X ∘⇩c ⟨id⇩c Z ∘⇩c z , m ∘⇩c y⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod yz_pair)
also have "... = distribute_left Z X X ∘⇩c ⟨z , ⟨my2,my1⟩⟩"
unfolding my_def by (typecheck_cfuncs, simp add: id_left_unit2)
also have "... = ⟨⟨z,my2⟩, ⟨z,my1⟩⟩"
using distribute_left_ap by (typecheck_cfuncs, auto)
finally show ?thesis.
qed
then have "⟨⟨xs,zs⟩,⟨xt,zt⟩⟩ = ⟨⟨z,my2⟩,⟨z,my1⟩⟩"
using zy_def by auto
then have "⟨xs,zs⟩ = ⟨z,my2⟩ ∧ ⟨xt,zt⟩ = ⟨z, my1⟩"
using element_pair_eq by (typecheck_cfuncs, auto)
then have eqs: "xs = z ∧ zs = my2 ∧ xt = z ∧ zt = my1"
using element_pair_eq by (typecheck_cfuncs, auto)
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c ⟨z,y'⟩ = ⟨⟨xt,zt⟩, ⟨xs,zs⟩⟩"
proof -
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c ⟨z,y'⟩ = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c ⟨z,y'⟩"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = distribute_left Z X X ∘⇩c ⟨id⇩c Z ∘⇩c z, m ∘⇩c y'⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
also have "... = distribute_left Z X X ∘⇩c ⟨z, ⟨my1,my2⟩⟩"
unfolding y'_def by (typecheck_cfuncs, simp add: id_left_unit2)
also have "... = ⟨⟨z,my1⟩, ⟨z,my2⟩⟩"
using distribute_left_ap by (typecheck_cfuncs, auto)
also have "... = ⟨⟨xt,zt⟩, ⟨xs,zs⟩⟩"
using eqs by auto
finally show ?thesis.
qed
then show "⟨⟨xt,zt⟩,⟨xs,zs⟩⟩ factorsthru (distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
by (typecheck_cfuncs, metis cfunc_prod_type eqs factors_through_def2 y'_type)
qed
qed
lemma left_pair_transitive:
assumes "transitive_on X (Y, m)"
shows "transitive_on (X ×⇩c Z) (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z))"
proof (unfold transitive_on_def, safe)
have "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 transitive_on_def by auto
then show "(Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ⊆⇩c (X ×⇩c Z) ×⇩c X ×⇩c Z"
by (simp add: left_pair_subset)
next
have m_def[type_rule]: "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 transitive_on_def by auto
fix s t u
assume s_type[type_rule]: "s ∈⇩c X ×⇩c Z"
assume t_type[type_rule]: "t ∈⇩c X ×⇩c Z"
assume u_type[type_rule]: "u ∈⇩c X ×⇩c Z"
assume st_relation: "⟨s,t⟩ ∈⇘(X ×⇩c Z) ×⇩c X ×⇩c Z⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
then obtain h where h_type[type_rule]: "h ∈⇩c Y ×⇩c Z" and h_def: "(distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c h = ⟨s,t⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
then obtain hy hz where h_part_types[type_rule]: "hy ∈⇩c Y" "hz ∈⇩c Z" and h_decomp: "h = ⟨hy, hz⟩"
using cart_prod_decomp by blast
then obtain mhy1 mhy2 where mhy_types[type_rule]: "mhy1 ∈⇩c X" "mhy2 ∈⇩c X" and mhy_decomp: "m ∘⇩c hy = ⟨mhy1, mhy2⟩"
using cart_prod_decomp by (typecheck_cfuncs, blast)
have "⟨s,t⟩ = ⟨⟨mhy1, hz⟩, ⟨mhy2, hz⟩⟩"
proof -
have "⟨s,t⟩ = (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c ⟨hy, hz⟩"
using h_decomp h_def by auto
also have "... = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c ⟨hy, hz⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c hy, hz⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨mhy1, hz⟩, ⟨mhy2, hz⟩⟩"
unfolding mhy_decomp by (typecheck_cfuncs, simp add: distribute_right_ap)
finally show ?thesis.
qed
then have s_def: "s = ⟨mhy1, hz⟩" and t_def: "t = ⟨mhy2, hz⟩"
using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)
assume tu_relation: "⟨t,u⟩ ∈⇘(X ×⇩c Z) ×⇩c X ×⇩c Z⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
then obtain g where g_type[type_rule]: "g ∈⇩c Y ×⇩c Z" and g_def: "(distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c g = ⟨t,u⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
then obtain gy gz where g_part_types[type_rule]: "gy ∈⇩c Y" "gz ∈⇩c Z" and g_decomp: "g = ⟨gy, gz⟩"
using cart_prod_decomp by blast
then obtain mgy1 mgy2 where mgy_types[type_rule]: "mgy1 ∈⇩c X" "mgy2 ∈⇩c X" and mgy_decomp: "m ∘⇩c gy = ⟨mgy1, mgy2⟩"
using cart_prod_decomp by (typecheck_cfuncs, blast)
have "⟨t,u⟩ = ⟨⟨mgy1, gz⟩, ⟨mgy2, gz⟩⟩"
proof -
have "⟨t,u⟩ = (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c ⟨gy, gz⟩"
using g_decomp g_def by auto
also have "... = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c ⟨gy, gz⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c gy, gz⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨mgy1, gz⟩, ⟨mgy2, gz⟩⟩"
unfolding mgy_decomp by (typecheck_cfuncs, simp add: distribute_right_ap)
finally show ?thesis.
qed
then have t_def2: "t = ⟨mgy1, gz⟩" and u_def: "u = ⟨mgy2, gz⟩"
using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)
have mhy2_eq_mgy1: "mhy2 = mgy1"
using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
have gy_eq_gz: "hz = gz"
using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
have mhy_in_Y: "⟨mhy1, mhy2⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using m_def h_part_types mhy_decomp
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
have mgy_in_Y: "⟨mhy2, mgy2⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using m_def g_part_types mgy_decomp mhy2_eq_mgy1
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
have "⟨mhy1, mgy2⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using assms mhy_in_Y mgy_in_Y mgy_types mhy2_eq_mgy1 unfolding transitive_on_def
by (typecheck_cfuncs, blast)
then obtain y where y_type[type_rule]: "y ∈⇩c Y" and y_def: "m ∘⇩c y = ⟨mhy1, mgy2⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
show " ⟨s,u⟩ ∈⇘(X ×⇩c Z) ×⇩c X ×⇩c Z⇙ (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z))"
proof (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, safe)
show "monomorphism (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z)"
using relative_member_def2 st_relation by blast
show "∃h. h ∈⇩c Y ×⇩c Z ∧ (distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c h = ⟨s,u⟩"
unfolding s_def u_def gy_eq_gz
proof (intro exI[where x="⟨y,gz⟩"], safe, typecheck_cfuncs)
have "(distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c ⟨y,gz⟩ = distribute_right X X Z ∘⇩c (m ×⇩f id⇩c Z) ∘⇩c ⟨y,gz⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_right X X Z ∘⇩c ⟨m ∘⇩c y, gz⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨mhy1,gz⟩,⟨mgy2,gz⟩⟩"
unfolding y_def by (typecheck_cfuncs, simp add: distribute_right_ap)
finally show "(distribute_right X X Z ∘⇩c m ×⇩f id⇩c Z) ∘⇩c ⟨y,gz⟩ = ⟨⟨mhy1,gz⟩,⟨mgy2,gz⟩⟩".
qed
qed
qed
lemma right_pair_transitive:
assumes "transitive_on X (Y, m)"
shows "transitive_on (Z ×⇩c X) (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m))"
proof (unfold transitive_on_def, safe)
have "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 transitive_on_def by auto
then show "(Z ×⇩c Y, distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ⊆⇩c (Z ×⇩c X) ×⇩c Z ×⇩c X"
by (simp add: right_pair_subset)
next
have m_def[type_rule]: "m : Y → X ×⇩c X" "monomorphism m"
using assms subobject_of_def2 transitive_on_def by auto
fix s t u
assume s_type[type_rule]: "s ∈⇩c Z ×⇩c X"
assume t_type[type_rule]: "t ∈⇩c Z ×⇩c X"
assume u_type[type_rule]: "u ∈⇩c Z ×⇩c X"
assume st_relation: "⟨s,t⟩ ∈⇘(Z ×⇩c X) ×⇩c Z ×⇩c X⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m)"
then obtain h where h_type[type_rule]: "h ∈⇩c Z ×⇩c Y" and h_def: "(distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c h = ⟨s,t⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
then obtain hy hz where h_part_types[type_rule]: "hy ∈⇩c Y" "hz ∈⇩c Z" and h_decomp: "h = ⟨hz, hy⟩"
using cart_prod_decomp by blast
then obtain mhy1 mhy2 where mhy_types[type_rule]: "mhy1 ∈⇩c X" "mhy2 ∈⇩c X" and mhy_decomp: "m ∘⇩c hy = ⟨mhy1, mhy2⟩"
using cart_prod_decomp by (typecheck_cfuncs, blast)
have "⟨s,t⟩ = ⟨⟨hz, mhy1⟩, ⟨hz, mhy2⟩⟩"
proof -
have "⟨s,t⟩ = (distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c ⟨hz, hy⟩"
using h_decomp h_def by auto
also have "... = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c ⟨hz, hy⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_left Z X X ∘⇩c ⟨ hz, m ∘⇩c hy⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨hz, mhy1⟩, ⟨hz, mhy2⟩⟩"
unfolding mhy_decomp by (typecheck_cfuncs, simp add: distribute_left_ap)
finally show ?thesis.
qed
then have s_def: "s = ⟨hz, mhy1⟩" and t_def: "t = ⟨hz, mhy2⟩"
using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)
assume tu_relation: "⟨t,u⟩ ∈⇘(Z ×⇩c X) ×⇩c
Z ×⇩c X⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m)"
then obtain g where g_type[type_rule]: "g ∈⇩c Z ×⇩c Y" and g_def: "(distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c g = ⟨t,u⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
then obtain gy gz where g_part_types[type_rule]: "gy ∈⇩c Y" "gz ∈⇩c Z" and g_decomp: "g = ⟨gz, gy⟩"
using cart_prod_decomp by blast
then obtain mgy1 mgy2 where mgy_types[type_rule]: "mgy1 ∈⇩c X" "mgy2 ∈⇩c X" and mgy_decomp: "m ∘⇩c gy = ⟨mgy2, mgy1⟩"
using cart_prod_decomp by (typecheck_cfuncs, blast)
have "⟨t,u⟩ = ⟨⟨gz, mgy2⟩, ⟨gz, mgy1⟩⟩"
proof -
have "⟨t,u⟩ = (distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c ⟨gz, gy⟩"
using g_decomp g_def by auto
also have "... = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c ⟨gz, gy⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_left Z X X ∘⇩c ⟨gz, m ∘⇩c gy⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨gz, mgy2⟩, ⟨gz, mgy1⟩⟩"
unfolding mgy_decomp by (typecheck_cfuncs, simp add: distribute_left_ap)
finally show ?thesis.
qed
then have t_def2: "t = ⟨gz, mgy2⟩" and u_def: "u = ⟨gz, mgy1⟩"
using cart_prod_eq2 by (typecheck_cfuncs, auto, presburger)
have mhy2_eq_mgy2: "mhy2 = mgy2"
using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
have gy_eq_gz: "hz = gz"
using t_def2 t_def cart_prod_eq2 by (typecheck_cfuncs_prems, auto)
have mhy_in_Y: "⟨mhy1, mhy2⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using m_def h_part_types mhy_decomp
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
have mgy_in_Y: "⟨mhy2, mgy1⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using m_def g_part_types mgy_decomp mhy2_eq_mgy2
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
have "⟨mhy1, mgy1⟩ ∈⇘X ×⇩c X⇙ (Y, m)"
using assms mhy_in_Y mgy_in_Y mgy_types mhy2_eq_mgy2 unfolding transitive_on_def
by (typecheck_cfuncs, blast)
then obtain y where y_type[type_rule]: "y ∈⇩c Y" and y_def: "m ∘⇩c y = ⟨mhy1, mgy1⟩"
by (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, auto)
show " ⟨s,u⟩ ∈⇘(Z ×⇩c X) ×⇩c Z ×⇩c X⇙ (Z ×⇩c Y, distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m)"
proof (typecheck_cfuncs, unfold relative_member_def2 factors_through_def2, safe)
show "monomorphism (distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m)"
using relative_member_def2 st_relation by blast
show "∃h. h ∈⇩c Z ×⇩c Y ∧ (distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c h = ⟨s,u⟩"
unfolding s_def u_def gy_eq_gz
proof (intro exI[where x="⟨gz,y⟩"], safe, typecheck_cfuncs)
have "(distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m)) ∘⇩c ⟨gz,y⟩ = distribute_left Z X X ∘⇩c (id⇩c Z ×⇩f m) ∘⇩c ⟨gz,y⟩"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = distribute_left Z X X ∘⇩c ⟨gz, m ∘⇩c y⟩"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = ⟨⟨gz,mhy1⟩,⟨gz,mgy1⟩⟩"
by (typecheck_cfuncs, simp add: distribute_left_ap y_def)
finally show "(distribute_left Z X X ∘⇩c id⇩c Z ×⇩f m) ∘⇩c ⟨gz,y⟩ = ⟨⟨gz,mhy1⟩,⟨gz,mgy1⟩⟩".
qed
qed
qed
lemma left_pair_equiv_rel:
assumes "equiv_rel_on X (Y, m)"
shows "equiv_rel_on (X ×⇩c Z) (Y ×⇩c Z, distribute_right X X Z ∘⇩c (m ×⇩f id Z))"
using assms left_pair_reflexive left_pair_symmetric left_pair_transitive
by (unfold equiv_rel_on_def, auto)
lemma right_pair_equiv_rel:
assumes "equiv_rel_on X (Y, m)"
shows "equiv_rel_on (Z ×⇩c X) (Z ×⇩c Y, distribute_left Z X X ∘⇩c (id Z ×⇩f m))"
using assms right_pair_reflexive right_pair_symmetric right_pair_transitive
by (unfold equiv_rel_on_def, auto)
end