Theory Relation_Algebra_Direct_Products
section ‹Direct Products›
theory Relation_Algebra_Direct_Products
imports Relation_Algebra_Functions
begin
text ‹This section uses the definition of direct products from Schmidt and
Str\"ohlein's book to prove the well known universal property.›
context relation_algebra
begin
definition is_direct_product :: "'a ⇒ 'a ⇒ bool"
where "is_direct_product x y ≡ x⇧⌣ ; x = 1' ∧ y⇧⌣ ; y = 1' ∧ x ; x⇧⌣ ⋅ y ; y⇧⌣ = 1' ∧ x⇧⌣ ; y = 1"
text ‹We collect some basic properties.›
lemma dp_p_fun1: "is_direct_product x y ⟹ is_p_fun x"
by (metis is_direct_product_def eq_refl is_p_fun_def)
lemma dp_sur1: "is_direct_product x y ⟹ is_sur x"
by (metis is_direct_product_def eq_refl is_sur_def)
lemma dp_total1: "is_direct_product x y ⟹ is_total x"
by (metis is_direct_product_def inf_le1 is_total_def)
lemma dp_map1: "is_direct_product x y ⟹ is_map x"
by (metis dp_p_fun1 dp_total1 is_map_def)
lemma dp_p_fun2: "is_direct_product x y ⟹ is_p_fun y"
by (metis is_direct_product_def eq_refl is_p_fun_def)
lemma dp_sur2: "is_direct_product x y ⟹ is_sur y"
by (metis is_direct_product_def eq_refl is_sur_def)
lemma dp_total2: "is_direct_product x y ⟹ is_total y"
by (metis is_direct_product_def inf_le2 is_total_def)
lemma dp_map2: "is_direct_product x y ⟹ is_map y"
by (metis dp_p_fun2 dp_total2 is_map_def)
text ‹Next we prove four auxiliary lemmas.›
lemma dp_aux1 [simp]:
assumes "is_p_fun z"
and "is_total w"
and "x⇧⌣ ; z = 1"
shows "(w ; x⇧⌣ ⋅ y ; z⇧⌣) ; z = y"
by (metis assms inf_top_left mult.assoc ss_422iii total_one inf.commute inf_top_right)
lemma dp_aux2 [simp]:
assumes "is_p_fun z"
and "is_total w"
and "z⇧⌣ ; x = 1"
shows "(w ; x⇧⌣ ⋅ y ; z⇧⌣) ; z = y"
by (metis assms conv_contrav conv_invol conv_one inf_top_left mult.assoc ss_422iii total_one)
lemma dp_aux3 [simp]:
assumes "is_p_fun z"
and "is_total w"
and "x⇧⌣ ; z = 1"
shows "(y ; z⇧⌣ ⋅ w ; x⇧⌣) ; z = y"
by (metis assms dp_aux1 inf.commute)
lemma dp_aux4 [simp]:
assumes "is_p_fun z"
and "is_total w"
and "z⇧⌣ ; x = 1"
shows "( y ; z⇧⌣ ⋅ w ; x⇧⌣) ; z = y"
by (metis assms dp_aux2 inf.commute)
text ‹Next we define a function which is an isomorphism on projections.›
definition Phi :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹Φ›)
where "Φ ≡ (λw x y z. w ; y⇧⌣ ⋅ x ; z⇧⌣)"
lemma Phi_conv: "(Φ w x y z)⇧⌣ = y ; w⇧⌣ ⋅ z ; x⇧⌣"
by (simp add: Phi_def)
text ‹We prove that @{const Phi} is an isomorphism with respect to the
projections.›
lemma mono_dp_1:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "Φ w x y z ; y = w"
by (metis assms dp_aux4 is_direct_product_def dp_p_fun1 dp_total2 Phi_def)
lemma mono_dp_2:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "Φ w x y z ; z = x"
by (metis assms dp_aux1 is_direct_product_def dp_p_fun2 dp_total1 Phi_def)
text ‹We now show that @{const Phi} is an injective function.›
lemma Phi_map:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_map (Φ w x y z)"
proof -
have "Φ w x y z ; -(1') = Φ w x y z ; -(y ; y⇧⌣ ⋅ z ; z⇧⌣)"
by (metis assms(2) is_direct_product_def)
also have "... = Φ w x y z ; y ; -(y⇧⌣) + Φ w x y z ; z ; -(z⇧⌣)"
by (metis compl_inf assms(2) ss43iii dp_map1 dp_map2 mult.assoc distrib_left)
also have "... = w ; -(y⇧⌣) + x ; -(z⇧⌣)"
by (metis assms mono_dp_1 mono_dp_2)
also have "... = -(w ; y⇧⌣) + -(x ; z⇧⌣)"
by (metis assms(1) ss43iii dp_map1 dp_map2)
also have "... = -(Φ w x y z)"
by (metis compl_inf Phi_def)
finally show ?thesis
by (metis is_maprop)
qed
lemma Phi_inj:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_inj (Φ w x y z)"
by (metis Phi_def Phi_conv Phi_map assms inj_p_fun is_map_def)
text ‹Next we show that the converse of @{const Phi} is an injective
function.›
lemma Phi_conv_map:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_map ((Φ w x y z)⇧⌣)"
by (metis Phi_conv Phi_def Phi_map assms)
lemma Phi_conv_inj:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_inj ((Φ w x y z)⇧⌣)"
by (metis Phi_inj Phi_conv Phi_def assms)
lemma Phi_sur:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_sur (Φ w x y z)"
by (metis assms Phi_conv Phi_def Phi_map is_map_def sur_total)
lemma Phi_conv_sur:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_sur ((Φ w x y z)⇧⌣)"
by (metis assms Phi_conv Phi_def Phi_sur)
lemma Phi_bij:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_bij (Φ w x y z)"
by (metis assms Phi_inj Phi_map Phi_sur is_bij_def)
lemma Phi_conv_bij:
assumes "is_direct_product w x"
and "is_direct_product y z"
shows "is_bij ((Φ w x y z)⇧⌣)"
by (metis Phi_bij Phi_def Phi_conv assms)
text ‹Next we construct, for given functions~@{term f} and~@{term g}, a
function~@{term F} which makes the standard product diagram commute, and we
verify these commutation properties.›
definition F :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
where "F ≡ (λf x g y. f ; x⇧⌣ ⋅ g ; y⇧⌣)"
lemma f_proj:
assumes "is_direct_product x y"
and "is_map g"
shows "F f x g y ; x = f"
by (metis assms dp_aux4 F_def is_map_def is_direct_product_def dp_p_fun1)
lemma g_proj:
assumes "is_direct_product x y"
and "is_map f"
shows "F f x g y ; y = g"
by (metis assms dp_aux1 F_def is_map_def is_direct_product_def dp_p_fun2)
text ‹Finally we show uniqueness of~@{const F}, hence universality of the
construction.›
lemma
assumes "is_direct_product x y"
and "is_map f"
and "is_map g"
and "is_map G"
and "f = G ; x"
and "g = G ; y"
shows "G = F f x g y"
proof -
have "F f x g y = G ; (x ; x⇧⌣) ⋅ G ; (y ; y⇧⌣)"
by (metis assms(5) assms(6) F_def mult.assoc)
also have "… = G ; (x ; x⇧⌣ ⋅ y ; y⇧⌣)"
by (metis assms(4) map_distl)
thus ?thesis
by (metis assms(1) is_direct_product_def calculation mult.right_neutral)
qed
end
end