section ‹More on rings›
theory Ring_ZF_1 imports Ring_ZF Group_ZF_3
begin
text‹This theory is devoted to the part of ring theory specific the
construction of real numbers in the ‹Real_ZF_x› series of theories.
The goal is to
show that classes of almost homomorphisms form a ring.›
subsection‹The ring of classes of almost homomorphisms›
text‹Almost homomorphisms do not form a ring as the regular homomorphisms
do because the lifted group operation is not distributive with respect to
composition -- we have $s\circ (r\cdot q) \neq s\circ r\cdot s\circ q$ in
general. However, we do have
$s\circ (r\cdot q) \approx s\circ r\cdot s\circ q$ in the sense of the
equivalence relation defined by the group of finite range
functions (that is a normal subgroup of almost homomorphisms,
if the group is abelian). This allows to define a natural ring structure
on the classes of almost homomorphisms.›
text‹The next lemma provides a formula useful for proving that two sides
of the distributive law equation for almost homomorphisms are almost
equal.›
lemma (in group1) Ring_ZF_1_1_L1:
assumes A1: "s∈AH" "r∈AH" "q∈AH" and A2: "n∈G"
shows
"((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
"((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
proof -
from groupAssum isAbelian A1 have T1:
"r∙q ∈ AH" "s∘r ∈ AH" "s∘q ∈ AH" "(s∘r)∙(s∘q) ∈ AH"
"r∘s ∈ AH" "q∘s ∈ AH" "(r∘s)∙(q∘s) ∈ AH"
using Group_ZF_3_2_L15 Group_ZF_3_4_T1 by auto
from A1 A2 have T2: "r`(n) ∈ G" "q`(n) ∈ G" "s`(n) ∈ G"
"s`(r`(n)) ∈ G" "s`(q`(n)) ∈ G" "δ(s,⟨ r`(n),q`(n)⟩) ∈ G"
"s`(r`(n))⋅s`(q`(n)) ∈ G" "r`(s`(n)) ∈ G" "q`(s`(n)) ∈ G"
"r`(s`(n))⋅q`(s`(n)) ∈ G"
using AlmostHoms_def apply_funtype Group_ZF_3_2_L4B
group0_2_L1 monoid0.group0_1_L1 by auto
with T1 A1 A2 isAbelian show
"((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯= δ(s,⟨ r`(n),q`(n)⟩)"
"((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
using Group_ZF_3_2_L12 Group_ZF_3_4_L2 Group_ZF_3_4_L1 group0_4_L6A
by auto
qed
text‹The sides of the distributive law equations for almost homomorphisms
are almost equal.›
lemma (in group1) Ring_ZF_1_1_L2:
assumes A1: "s∈AH" "r∈AH" "q∈AH"
shows
"s∘(r∙q) ≈ (s∘r)∙(s∘q)"
"(r∙q)∘s = (r∘s)∙(q∘s)"
proof -
from A1 have "∀n∈G. ⟨ r`(n),q`(n)⟩ ∈ G×G"
using AlmostHoms_def apply_funtype by auto
moreover from A1 have "{δ(s,x). x ∈ G×G} ∈ Fin(G)"
using AlmostHoms_def by simp
ultimately have "{δ(s,⟨ r`(n),q`(n)⟩). n∈G} ∈ Fin(G)"
by (rule Finite1_L6B)
with A1 have
"{((s∘(r∙q))`(n))⋅(((s∘r)∙(s∘q))`(n))¯. n ∈ G} ∈ Fin(G)"
using Ring_ZF_1_1_L1 by simp
moreover from groupAssum isAbelian A1 A1 have
"s∘(r∙q) ∈ AH" "(s∘r)∙(s∘q) ∈ AH"
using Group_ZF_3_2_L15 Group_ZF_3_4_T1 by auto
ultimately show "s∘(r∙q) ≈ (s∘r)∙(s∘q)"
using Group_ZF_3_4_L12 by simp
from groupAssum isAbelian A1 have
"(r∙q)∘s : G→G" "(r∘s)∙(q∘s) : G→G"
using Group_ZF_3_2_L15 Group_ZF_3_4_T1 AlmostHoms_def
by auto
moreover from A1 have
"∀n∈G. ((r∙q)∘s)`(n) = ((r∘s)∙(q∘s))`(n)"
using Ring_ZF_1_1_L1 by simp
ultimately show "(r∙q)∘s = (r∘s)∙(q∘s)"
using fun_extension_iff by simp
qed
text‹The essential condition to show the distributivity for the
operations defined on classes of almost homomorphisms.›
lemma (in group1) Ring_ZF_1_1_L3:
assumes A1: "R = QuotientGroupRel(AH,Op1,FR)"
and A2: "a ∈ AH//R" "b ∈ AH//R" "c ∈ AH//R"
and A3: "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
shows "M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩ ∧
M`⟨A`⟨ b,c⟩,a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
proof
from A2 obtain s q r where D1: "s∈AH" "r∈AH" "q∈AH"
"a = R``{s}" "b = R``{q}" "c = R``{r}"
using quotient_def by auto
from A1 have T1:"equiv(AH,R)"
using Group_ZF_3_3_L3 by simp
with A1 A3 D1 groupAssum isAbelian have
"M`⟨ a,A`⟨ b,c⟩ ⟩ = R``{s∘(q∙r)}"
using Group_ZF_3_3_L4 EquivClass_1_L10
Group_ZF_3_2_L15 Group_ZF_3_4_L13A by simp
also have "R``{s∘(q∙r)} = R``{(s∘q)∙(s∘r)}"
proof -
from T1 D1 have "equiv(AH,R)" "s∘(q∙r)≈(s∘q)∙(s∘r)"
using Ring_ZF_1_1_L2 by auto
with A1 show ?thesis using equiv_class_eq by simp
qed
also from A1 T1 D1 A3 have
"R``{(s∘q)∙(s∘r)} = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩"
using Group_ZF_3_3_L4 Group_ZF_3_4_T1 EquivClass_1_L10
Group_ZF_3_3_L3 Group_ZF_3_4_L13A EquivClass_1_L10 Group_ZF_3_4_T1
by simp
finally show "M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩,M`⟨ a,c⟩⟩" by simp
from A1 A3 T1 D1 groupAssum isAbelian show
"M`⟨A`⟨ b,c⟩,a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
using Group_ZF_3_3_L4 EquivClass_1_L10 Group_ZF_3_4_L13A
Group_ZF_3_2_L15 Ring_ZF_1_1_L2 Group_ZF_3_4_T1 by simp
qed
text‹The projection of the first group operation on almost homomorphisms
is distributive with respect to the second group operation.›
lemma (in group1) Ring_ZF_1_1_L4:
assumes A1: "R = QuotientGroupRel(AH,Op1,FR)"
and A2: "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
shows "IsDistributive(AH//R,A,M)"
proof -
from A1 A2 have "∀a∈(AH//R).∀b∈(AH//R).∀c∈(AH//R).
M`⟨a,A`⟨ b,c⟩⟩ = A`⟨M`⟨ a,b⟩, M`⟨ a,c⟩⟩ ∧
M`⟨A`⟨ b,c⟩, a⟩ = A`⟨M`⟨ b,a⟩,M`⟨ c,a⟩⟩"
using Ring_ZF_1_1_L3 by simp
then show ?thesis using IsDistributive_def by simp
qed
text‹The classes of almost homomorphisms form a ring.›
theorem (in group1) Ring_ZF_1_1_T1:
assumes "R = QuotientGroupRel(AH,Op1,FR)"
and "A = ProjFun2(AH,R,Op1)" "M = ProjFun2(AH,R,Op2)"
shows "IsAring(AH//R,A,M)"
using assms QuotientGroupOp_def Group_ZF_3_3_T1 Group_ZF_3_4_T2
Ring_ZF_1_1_L4 IsAring_def by simp
end