theory Ring_ZF_1 imports Ring_ZF Group_ZF_3
begin
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.
The ring of classes of almost homomorphisms
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.
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\in AH \), \( r\in AH \), \( q\in AH \) and A2: \( n\in G \)
shows \( ((s\circ (r\bullet q))(n))\cdot (((s\circ r)\bullet (s\circ q))(n))^{-1}= \delta (s,\langle r(n),q(n)\rangle ) \), \( ((r\bullet q)\circ s)(n) = ((r\circ s)\bullet (q\circ s))(n) \)proof from groupAssum, isAbelian, A1 have T1: \( r\bullet q \in AH \), \( s\circ r \in AH \), \( s\circ q \in AH \), \( (s\circ r)\bullet (s\circ q) \in AH \), \( r\circ s \in AH \), \( q\circ s \in AH \), \( (r\circ s)\bullet (q\circ s) \in AH \) using Group_ZF_3_2_L15 , Group_ZF_3_4_T1
from A1, A2 have T2: \( r(n) \in G \), \( q(n) \in G \), \( s(n) \in G \), \( s(r(n)) \in G \), \( s(q(n)) \in G \), \( \delta (s,\langle r(n),q(n)\rangle ) \in G \), \( s(r(n))\cdot s(q(n)) \in G \), \( r(s(n)) \in G \), \( q(s(n)) \in G \), \( r(s(n))\cdot q(s(n)) \in G \) using AlmostHoms_def , apply_funtype , Group_ZF_3_2_L4B , group0_2_L1 , group0_1_L1
with T1, A1, A2, isAbelian show \( ((s\circ (r\bullet q))(n))\cdot (((s\circ r)\bullet (s\circ q))(n))^{-1}= \delta (s,\langle r(n),q(n)\rangle ) \), \( ((r\bullet q)\circ s)(n) = ((r\circ s)\bullet (q\circ s))(n) \) using Group_ZF_3_2_L12 , Group_ZF_3_4_L2 , Group_ZF_3_4_L1 , group0_4_L6A
qed
The sides of the distributive law equations for almost homomorphisms are almost equal.
lemma (in group1) Ring_ZF_1_1_L2:
assumes A1: \( s\in AH \), \( r\in AH \), \( q\in AH \)
shows \( s\circ (r\bullet q) \approx (s\circ r)\bullet (s\circ q) \), \( (r\bullet q)\circ s = (r\circ s)\bullet (q\circ s) \)proof from A1 have \( \forall n\in G.\ \langle r(n),q(n)\rangle \in G\times G \) using AlmostHoms_def , apply_funtype
moreover
from A1 have \( \{\delta (s,x).\ x \in G\times G\} \in Fin(G) \) using AlmostHoms_def
ultimately have \( \{\delta (s,\langle r(n),q(n)\rangle ).\ n\in G\} \in Fin(G) \) by (rule Finite1_L6B )
with A1 have \( \{((s\circ (r\bullet q))(n))\cdot (((s\circ r)\bullet (s\circ q))(n))^{-1}.\ n \in G\} \in Fin(G) \) using Ring_ZF_1_1_L1
moreover
from groupAssum, isAbelian, A1, A1 have \( s\circ (r\bullet q) \in AH \), \( (s\circ r)\bullet (s\circ q) \in AH \) using Group_ZF_3_2_L15 , Group_ZF_3_4_T1
ultimately show \( s\circ (r\bullet q) \approx (s\circ r)\bullet (s\circ q) \) using Group_ZF_3_4_L12
from groupAssum, isAbelian, A1 have \( (r\bullet q)\circ s : G\rightarrow G \), \( (r\circ s)\bullet (q\circ s) : G\rightarrow G \) using Group_ZF_3_2_L15 , Group_ZF_3_4_T1 , AlmostHoms_def
moreover
qed
from A1 have \( \forall n\in G.\ ((r\bullet q)\circ s)(n) = ((r\circ s)\bullet (q\circ s))(n) \) using Ring_ZF_1_1_L1
ultimately show \( (r\bullet q)\circ s = (r\circ s)\bullet (q\circ s) \) using fun_extension_iff
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 = \text{QuotientGroupRel}(AH,Op1,FR) \) and A2: \( a \in AH//R \), \( b \in AH//R \), \( c \in AH//R \) and A3: \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \)
shows \( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \) \( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle \)proof from A2 obtain \( s \) \( q \) \( r \) where D1: \( s\in AH \), \( r\in AH \), \( q\in AH \), \( a = R\{s\} \), \( b = R\{q\} \), \( c = R\{r\} \) using quotient_def
from A1 have T1: \( \text{equiv}(AH,R) \) using Group_ZF_3_3_L3
with A1, A3, D1, groupAssum, isAbelian have \( M\langle a,A\langle b,c\rangle \rangle = R\{s\circ (q\bullet r)\} \) using Group_ZF_3_3_L4 , EquivClass_1_L10 , Group_ZF_3_2_L15 , Group_ZF_3_4_L13A
also
have \( R\{s\circ (q\bullet r)\} = R\{(s\circ q)\bullet (s\circ r)\} \)proof
also from T1, D1 have \( \text{equiv}(AH,R) \), \( s\circ (q\bullet r)\approx (s\circ q)\bullet (s\circ r) \) using Ring_ZF_1_1_L2
with A1 show \( thesis \) using equiv_class_eq
qed
from A1, T1, D1, A3 have \( R\{(s\circ q)\bullet (s\circ r)\} = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \) 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
finally show \( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \)
from A1, A3, T1, D1, groupAssum, isAbelian show \( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle \) 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
qed
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 = \text{QuotientGroupRel}(AH,Op1,FR) \) and A2: \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \)
shows \( \text{IsDistributive}(AH//R,A,M) \)proof from A1, A2 have \( \forall a\in (AH//R).\ \forall b\in (AH//R).\ \forall c\in (AH//R).\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle , M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle , a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle \) using Ring_ZF_1_1_L3
then show \( thesis \) using IsDistributive_def
qed
The classes of almost homomorphisms form a ring.
theorem (in group1) Ring_ZF_1_1_T1:
assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \)
shows \( \text{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 end
lemma Group_ZF_3_2_L15: assumes \( \text{IsAgroup}(G,f) \) and \( f \text{ is commutative on } G \) and \( AH = \text{AlmostHoms}(G,f) \), \( Op1 = \text{AlHomOp1}(G,f) \) and \( s \in AH \), \( r \in AH \) shows \( Op1\langle s,r\rangle \in AH \), \( \text{GroupInv}(AH,Op1)(r) \in AH \), \( Op1\langle s, \text{GroupInv}(AH,Op1)(r)\rangle \in AH \)
theorem (in group1) Group_ZF_3_4_T1: assumes \( s\in AH \), \( r\in AH \) shows \( \text{Composition}(G)\langle s,r\rangle \in AH \), \( s\circ r \in AH \)
Definition of AlmostHoms:
\( \text{AlmostHoms}(G,f) \equiv \)
\( \{s \in G\rightarrow G.\ \{ \text{HomDiff}(G,f,s,x).\ x \in G\times G \} \in Fin(G)\} \)
lemma (in group1) Group_ZF_3_2_L4B: assumes \( s \in AH \) and \( x\in G\times G \) shows \( \text{fst}(x)\cdot \text{snd}(x) \in G \), \( s(\text{fst}(x)\cdot \text{snd}(x)) \in G \), \( s(\text{fst}(x)) \in G \), \( s(\text{snd}(x)) \in G \), \( \delta (s,x) \in G \), \( s(\text{fst}(x))\cdot s(\text{snd}(x)) \in G \)
lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) group0_1_L1: assumes \( a\in G \), \( b\in G \) shows \( a\oplus b \in G \)
lemma (in group1) Group_ZF_3_2_L12: assumes \( s\in AH \), \( r\in AH \) and \( n\in G \) shows \( (s\bullet r)(n) = s(n)\cdot r(n) \)
lemma (in group1) Group_ZF_3_4_L2: assumes \( s\in AH \), \( r\in AH \) and \( m\in G \) shows \( (s\circ r)(m) = s(r(m)) \), \( s(r(m)) \in G \)
lemma (in group1) Group_ZF_3_4_L1: assumes \( s\in AH \) and \( m\in G \), \( n\in G \) shows \( s(m\cdot n) = s(m)\cdot s(n)\cdot \delta (s,\langle m,n\rangle ) \)
lemma (in group0) group0_4_L6A: assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \) shows \( a\cdot b\cdot a^{-1} = b \), \( a^{-1}\cdot b\cdot a = b \), \( a^{-1}\cdot (b\cdot a) = b \), \( a\cdot (b\cdot a^{-1}) = b \)
lemma Finite1_L6B: assumes \( \forall x\in X.\ a(x) \in Y \) and \( \{b(y).\ y\in Y\} \in Fin(Z) \) shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \)
lemma (in group1) Ring_ZF_1_1_L1: assumes \( s\in AH \), \( r\in AH \), \( q\in AH \) and \( n\in G \) shows \( ((s\circ (r\bullet q))(n))\cdot (((s\circ r)\bullet (s\circ q))(n))^{-1}= \delta (s,\langle r(n),q(n)\rangle ) \), \( ((r\bullet q)\circ s)(n) = ((r\circ s)\bullet (q\circ s))(n) \)
lemma (in group1) Group_ZF_3_4_L12: assumes \( s\in AH \), \( r\in AH \) and \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \) shows \( s\approx r \)
lemma (in group1) Group_ZF_3_3_L3: shows \( \text{QuotientGroupRel}(AH,Op1,FR) \subseteq AH \times AH \) and \( \text{equiv}(AH, \text{QuotientGroupRel}(AH,Op1,FR)) \)
lemma (in group1) Group_ZF_3_3_L4: shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op1) \)
lemma EquivClass_1_L10: assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( x\in A \), \( y\in A \) shows \( \text{ProjFun2}(A,r,f)\langle r\{x\},r\{y\}\rangle = r\{f\langle x,y\rangle \} \)
lemma (in group1) Group_ZF_3_4_L13A: shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op2) \)
lemma (in group1) Ring_ZF_1_1_L2: assumes \( s\in AH \), \( r\in AH \), \( q\in AH \) shows \( s\circ (r\bullet q) \approx (s\circ r)\bullet (s\circ q) \), \( (r\bullet q)\circ s = (r\circ s)\bullet (q\circ s) \)
lemma (in group1) Ring_ZF_1_1_L3: assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( a \in AH//R \), \( b \in AH//R \), \( c \in AH//R \) and \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \) shows \( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle \)
Definition of IsDistributive:
\( \text{IsDistributive}(X,A,M) \equiv (\forall a\in X.\ \forall b\in X.\ \forall c\in X.\ \)
\( M\langle a,A\langle b,c\rangle \rangle = A\langle M\langle a,b\rangle ,M\langle a,c\rangle \rangle \wedge \)
\( M\langle A\langle b,c\rangle ,a\rangle = A\langle M\langle b,a\rangle ,M\langle c,a\rangle \rangle ) \)
Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
theorem (in group1) Group_ZF_3_3_T1: shows \( \text{IsAgroup}(AH// \text{QuotientGroupRel}(AH,Op1,FR), \text{QuotientGroupOp}(AH,Op1,FR)) \) and \( \text{QuotientGroupOp}(AH,Op1,FR) \text{ is commutative on }\)
\( (AH// \text{QuotientGroupRel}(AH,Op1,FR)) \)
theorem (in group1) Group_ZF_3_4_T2: assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \) shows \( \text{IsAmonoid}(AH//R, \text{ProjFun2}(AH,R,Op2)) \), \( R\{id(G)\} = \text{TheNeutralElement}(AH//R, \text{ProjFun2}(AH,R,Op2)) \)
lemma (in group1) Ring_ZF_1_1_L4: assumes \( R = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( A = \text{ProjFun2}(AH,R,Op1) \), \( M = \text{ProjFun2}(AH,R,Op2) \) shows \( \text{IsDistributive}(AH//R,A,M) \)
Definition of IsAring:
\( \text{IsAring}(R,A,M) \equiv \text{IsAgroup}(R,A) \wedge (A \text{ is commutative on } R) \wedge \)
\( \text{IsAmonoid}(R,M) \wedge \text{IsDistributive}(R,A,M) \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 1JzFajFtGwiKiRHbZyCB1KtASgsM1kFU2h