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 A H$ , $r \in A H$ , $q \in A H$ and A2: $n \in G$

shows

((s \circ (r ∙ q)) (n)) \cdot (((s \circ r) ∙ (s \circ q)) (n))^{- 1} = δ (s, ⟨ r (n), q (n) ⟩)

((r ∙ q) \circ s) (n) = ((r \circ s) ∙ (q \circ s)) (n)

proof

from groupAssum, isAbelian, A1 have T1:

r ∙ q \in A H

s \circ r \in A H

s \circ q \in A H

(s \circ r) ∙ (s \circ q) \in A H

r \circ s \in A H

q \circ s \in A H

(r \circ s) ∙ (q \circ s) \in A H

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

δ (s, ⟨ r (n), q (n) ⟩) \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 ∙ q)) (n)) \cdot (((s \circ r) ∙ (s \circ q)) (n))^{- 1} = δ (s, ⟨ r (n), q (n) ⟩)

((r ∙ q) \circ s) (n) = ((r \circ s) ∙ (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 A H$ , $r \in A H$ , $q \in A H$

shows

s \circ (r ∙ q) ≅ (s \circ r) ∙ (s \circ q)

(r ∙ q) \circ s = (r \circ s) ∙ (q \circ s)

proof

from A1 have

\forall n \in G . ⟨ r (n), q (n) ⟩ \in G \times G

using AlmostHoms_def, apply_funtype

moreover

from A1 have

{δ (s, x) . x \in G \times G} \in F i n (G)

using AlmostHoms_def

ultimately have

{δ (s, ⟨ r (n), q (n) ⟩) . n \in G} \in F i n (G)

by (rule Finite1_L6B )

with A1 have

{((s \circ (r ∙ q)) (n)) \cdot (((s \circ r) ∙ (s \circ q)) (n))^{- 1} . n \in G} \in F i n (G)

using Ring_ZF_1_1_L1

moreover

from groupAssum, isAbelian, A1, A1 have

s \circ (r ∙ q) \in A H

(s \circ r) ∙ (s \circ q) \in A H

using Group_ZF_3_2_L15, Group_ZF_3_4_T1

ultimately show

s \circ (r ∙ q) ≅ (s \circ r) ∙ (s \circ q)

using Group_ZF_3_4_L12

from groupAssum, isAbelian, A1 have

(r ∙ q) \circ s : G \to G

(r \circ s) ∙ (q \circ s) : G \to G

using Group_ZF_3_2_L15, Group_ZF_3_4_T1, AlmostHoms_def

moreover

from A1 have

\forall n \in G . ((r ∙ q) \circ s) (n) = ((r \circ s) ∙ (q \circ s)) (n)

using Ring_ZF_1_1_L1

ultimately show

(r ∙ q) \circ s = (r \circ s) ∙ (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 = QuotientGroupRel (A H, O p 1, F R)$ and A2: $a \in A H / / R$ , $b \in A H / / R$ , $c \in A H / / R$ and A3: $A = ProjFun2 (A H, R, O p 1)$ , $M = ProjFun2 (A H, R, O p 2)$

shows

M ⟨ a, A ⟨ b, c ⟩ ⟩ = A ⟨ M ⟨ a, b ⟩, M ⟨ a, c ⟩ ⟩ \land

M ⟨ A ⟨ b, c ⟩, a ⟩ = A ⟨ M ⟨ b, a ⟩, M ⟨ c, a ⟩ ⟩

proof

from A2 obtain

s

q

r

where D1:

s \in A H

r \in A H

q \in A H

a = R {s}

b = R {q}

c = R {r}

using quotient_def

from A1 have T1:

equiv (A H, R)

using Group_ZF_3_3_L3

with A1, A3, D1, groupAssum, isAbelian have

M ⟨ a, A ⟨ b, c ⟩ ⟩ = R {s \circ (q ∙ 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 ∙ r)} = R {(s \circ q) ∙ (s \circ r)}

proof

from T1, D1 have

equiv (A H, R)

s \circ (q ∙ r) ≅ (s \circ q) ∙ (s \circ r)

using Ring_ZF_1_1_L2

with A1 show

t h e s i s

using equiv_class_eq

qed

also

from A1, T1, D1, A3 have

R {(s \circ q) ∙ (s \circ 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

finally show

M ⟨ a, A ⟨ b, c ⟩ ⟩ = A ⟨ M ⟨ a, b ⟩, M ⟨ a, c ⟩ ⟩

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

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 = QuotientGroupRel (A H, O p 1, F R)$ and A2: $A = ProjFun2 (A H, R, O p 1)$ , $M = ProjFun2 (A H, R, O p 2)$

shows

IsDistributive (A H / / R, A, M)

proof

from A1, A2 have

\forall a \in (A H / / R) . \forall b \in (A H / / R) . \forall c \in (A H / / R) .

M ⟨ a, A ⟨ b, c ⟩ ⟩ = A ⟨ M ⟨ a, b ⟩, M ⟨ a, c ⟩ ⟩ \land

M ⟨ A ⟨ b, c ⟩, a ⟩ = A ⟨ M ⟨ b, a ⟩, M ⟨ c, a ⟩ ⟩

using Ring_ZF_1_1_L3

then show

t h e s i s

using IsDistributive_def

qed

The classes of almost homomorphisms form a ring.

theorem (in group1) Ring_ZF_1_1_T1:

assumes $R = QuotientGroupRel (A H, O p 1, F R)$ and $A = ProjFun2 (A H, R, O p 1)$ , $M = ProjFun2 (A H, R, O p 2)$

shows

IsAring (A H / / 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 $IsAgroup (G, f)$ and $f is commutative on G$ and $A H = AlmostHoms (G, f)$ , $O p 1 = AlHomOp1 (G, f)$ and $s \in A H$ , $r \in A H$

shows

O p 1 ⟨ s, r ⟩ \in A H

GroupInv (A H, O p 1) (r) \in A H

O p 1 ⟨ s, GroupInv (A H, O p 1) (r) ⟩ \in A H

theorem (in group1) Group_ZF_3_4_T1:

assumes $s \in A H$ , $r \in A H$

shows

Composition (G) ⟨ s, r ⟩ \in A H

s \circ r \in A H

Definition of AlmostHoms:

AlmostHoms (G, f) \equiv

{s \in G \to G . {HomDiff (G, f, s, x) . x \in G \times G} \in F i n (G)}

lemma (in group1) Group_ZF_3_2_L4B:

assumes $s \in A H$ and $x \in G \times G$

shows

fst (x) \cdot snd (x) \in G

s (fst (x) \cdot snd (x)) \in G

s (fst (x)) \in G

s (snd (x)) \in G

δ (s, x) \in G

s (fst (x)) \cdot s (snd (x)) \in G

lemma (in group0) group0_2_L1: shows

m o n o i d 0 (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 A H$ , $r \in A H$ and $n \in G$

shows

(s ∙ r) (n) = s (n) \cdot r (n)

lemma (in group1) Group_ZF_3_4_L2:

assumes $s \in A H$ , $r \in A H$ 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 A H$ and $m \in G$ , $n \in G$

shows

s (m \cdot n) = s (m) \cdot s (n) \cdot δ (s, ⟨ m, n ⟩)

lemma (in group0) group0_4_L6A:

assumes $P 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 F i n (Z)$

shows

{b (a (x)) . x \in X} \in F i n (Z)

lemma (in group1) Ring_ZF_1_1_L1:

assumes $s \in A H$ , $r \in A H$ , $q \in A H$ and $n \in G$

shows

((s \circ (r ∙ q)) (n)) \cdot (((s \circ r) ∙ (s \circ q)) (n))^{- 1} = δ (s, ⟨ r (n), q (n) ⟩)

((r ∙ q) \circ s) (n) = ((r \circ s) ∙ (q \circ s)) (n)

lemma (in group1) Group_ZF_3_4_L12:

assumes $s \in A H$ , $r \in A H$ and ${s (n) \cdot (r (n))^{- 1} . n \in G} \in F i n (G)$

shows

s ≅ r

lemma (in group1) Group_ZF_3_3_L3: shows

QuotientGroupRel (A H, O p 1, F R) \subseteq A H \times A H

and

equiv (A H, QuotientGroupRel (A H, O p 1, F R))

lemma (in group1) Group_ZF_3_3_L4: shows

Congruent2 (QuotientGroupRel (A H, O p 1, F R), O p 1)

lemma EquivClass_1_L10:

assumes $equiv (A, r)$ and $Congruent2 (r, f)$ and $x \in A$ , $y \in A$

shows

ProjFun2 (A, r, f) ⟨ r {x}, r {y} ⟩ = r {f ⟨ x, y ⟩}

lemma (in group1) Group_ZF_3_4_L13A: shows

Congruent2 (QuotientGroupRel (A H, O p 1, F R), O p 2)

lemma (in group1) Ring_ZF_1_1_L2:

assumes $s \in A H$ , $r \in A H$ , $q \in A H$

shows

s \circ (r ∙ q) ≅ (s \circ r) ∙ (s \circ q)

(r ∙ q) \circ s = (r \circ s) ∙ (q \circ s)

lemma (in group1) Ring_ZF_1_1_L3:

assumes $R = QuotientGroupRel (A H, O p 1, F R)$ and $a \in A H / / R$ , $b \in A H / / R$ , $c \in A H / / R$ and $A = ProjFun2 (A H, R, O p 1)$ , $M = ProjFun2 (A H, R, O p 2)$