# IsarMathLib

## Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

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) \cong (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) \cong (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
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
qed

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
from T1, D1 have $$\text{equiv}(AH,R)$$, $$s\circ (q\bullet r) \cong (s\circ q)\bullet (s\circ r)$$ using Ring_ZF_1_1_L2
with A1 show $$thesis$$ using equiv_class_eq
qed
also
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\cong 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) \cong (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)$$