theory Group_ZF_3 imports Group_ZF_2 Finite1
begin
In this theory we consider notions in group theory that are useful for the construction of real numbers in the Real_ZF_x series of theories.
Group valued finite range functions
In this section show that the group valued functions \(f : X\rightarrow G\), with the property that \(f(X)\) is a finite subset of \(G\), is a group. Such functions play an important role in the construction of real numbers in the Real_ZF series.
The following proves the essential condition to show that the set of finite range functions is closed with respect to the lifted group operation.
lemma (in group0) Group_ZF_3_1_L1:
assumes A1: \( F = P \text{ lifted to function space over } X \) and A2: \( s \in \text{FinRangeFunctions}(X,G) \), \( r \in \text{FinRangeFunctions}(X,G) \)
shows \( F\langle s,r\rangle \in \text{FinRangeFunctions}(X,G) \)proof let \( q = F\langle s,r\rangle \)
from A2 have T1: \( s:X\rightarrow G \), \( r:X\rightarrow G \) using FinRangeFunctions_def
with A1 have T2: \( q : X\rightarrow G \) using group0_2_L1, Group_ZF_2_1_L0
moreover
qed
have \( q(X) \in Fin(G) \)proof
ultimately show \( thesis \) using FinRangeFunctions_def
from A2 have \( \{s(x).\ x\in X\} \in Fin(G) \), \( \{r(x).\ x\in X\} \in Fin(G) \) using Finite1_L18
with A1, T1, T2 show \( thesis \) using group_oper_fun, Finite1_L15, Group_ZF_2_1_L3, func_imagedef
qed
The set of group valued finite range functions is closed with respect to the lifted group operation.
lemma (in group0) Group_ZF_3_1_L2:
assumes A1: \( F = P \text{ lifted to function space over } X \)
shows \( \text{FinRangeFunctions}(X,G) \text{ is closed under } F \)proof let \( A = \text{FinRangeFunctions}(X,G) \)
from A1 have \( \forall x\in A.\ \forall y\in A.\ F\langle x,y\rangle \in A \) using Group_ZF_3_1_L1
then show \( thesis \) using IsOpClosed_def
qed
A composition of a finite range function with the group inverse is a finite range function.
lemma (in group0) Group_ZF_3_1_L3:
assumes A1: \( s \in \text{FinRangeFunctions}(X,G) \)
shows \( \text{GroupInv}(G,P)\circ s \in \text{FinRangeFunctions}(X,G) \) using groupAssum, assms, group0_2_T2, Finite1_L20The set of finite range functions is s subgroup of the lifted group.
theorem Group_ZF_3_1_T1:
assumes A1: \( \text{IsAgroup}(G,P) \) and A2: \( F = P \text{ lifted to function space over } X \) and A3: \( X\neq 0 \)
shows \( \text{IsAsubgroup}( \text{FinRangeFunctions}(X,G),F) \)proof let \( e = \text{ TheNeutralElement}(G,P) \)
let \( S = \text{FinRangeFunctions}(X,G) \)
from A1 have T1: \( group0(G,P) \) using group0_def
with A1, A2 have T2: \( group0(X\rightarrow G,F) \) using Group_ZF_2_1_T2, group0_def
moreover
qed
have \( S \neq 0 \)proof
moreover from T1, A3 have \( \text{ConstantFunction}(X,e) \in S \) using group0_2_L1, unit_is_neutral, Finite1_L17
thus \( thesis \)
qed
have \( S \subseteq X\rightarrow G \) using FinRangeFunctions_def
moreover from A2, T1 have \( S \text{ is closed under } F \) using Group_ZF_3_1_L2
moreover from A1, A2, T1 have \( \forall s \in S.\ \text{GroupInv}(X\rightarrow G,F)(s) \in S \) using FinRangeFunctions_def, Group_ZF_2_1_L6, Group_ZF_3_1_L3
ultimately show \( thesis \) using group0_3_T3
Almost homomorphisms
An almost homomorphism is a group valued function defined on a monoid \(M\) with the property that the set \(\{ f(m+n)-f(m)-f(n)\}_{m,n \in M}\) is finite. This term is used by R. D. Arthan in "The Eudoxus Real Numbers". We use this term in the general group context and use the A`Campo's term "slopes" (see his "A natural construction for the real numbers") to mean an almost homomorphism mapping interegers into themselves. We consider almost homomorphisms because we use slopes to define real numbers in the Real_ZF_x series.
HomDiff is an acronym for "homomorphism difference". This is the expression \(s(mn)(s(m)s(n))^{-1}\), or \(s(m+n)-s(m)-s(n)\) in the additive notation. It is equal to the neutral element of the group if \(s\) is a homomorphism.
definition
\( \text{HomDiff}(G,f,s,x) \equiv \) \( f\langle s(f\langle \text{fst}(x),\text{snd}(x)\rangle ) , \) \( ( \text{GroupInv}(G,f)(f\langle s(\text{fst}(x)),s(\text{snd}(x))\rangle ))\rangle \)
Almost homomorphisms are defined as those maps \(s:G\rightarrow G\) such that the homomorphism difference takes only finite number of values on \(G\times G\).
definition
\( \text{AlmostHoms}(G,f) \equiv \) \( \{s \in G\rightarrow G.\ \{ \text{HomDiff}(G,f,s,x).\ x \in G\times G \} \in Fin(G)\} \)
AlHomOp1\((G,f)\) is the group operation on almost homomorphisms defined in a natural way by \((s\cdot r)(n) = s(n)\cdot r(n)\). In the terminology defined in func1.thy this is the group operation \(f\) (on \(G\)) lifted to the function space \(G\rightarrow G\) and restricted to the set AlmostHoms\((G,f)\).
definition
\( \text{AlHomOp1}(G,f) \equiv \) \( \text{restrict}(f \text{ lifted to function space over } G,\) \( \text{AlmostHoms}(G,f)\times \text{AlmostHoms}(G,f)) \)
We also define a composition (binary) operator on almost homomorphisms in a natural way. We call that operator AlHomOp2 - the second operation on almost homomorphisms. Composition of almost homomorphisms is used to define multiplication of real numbers in Real_ZF series.
definition
\( \text{AlHomOp2}(G,f) \equiv \) \( \text{restrict}( \text{Composition}(G), \text{AlmostHoms}(G,f)\times \text{AlmostHoms}(G,f)) \)
This lemma provides more readable notation for the HomDiff definition. Not really intended to be used in proofs, but just to see the definition in the notation defined in the group0 locale.
lemma (in group0) HomDiff_notation:
shows \( \text{HomDiff}(G,P,s,\langle m,n\rangle ) = s(m\cdot n)\cdot (s(m)\cdot s(n))^{-1} \) using HomDiff_defThe next lemma shows the set from the definition of almost homomorphism in a different form.
lemma (in group0) Group_ZF_3_2_L1A:
shows \( \{ \text{HomDiff}(G,P,s,x).\ x \in G\times G \} = \{s(m\cdot n)\cdot (s(m)\cdot s(n))^{-1}.\ \langle m,n\rangle \in G\times G\} \)proof have \( \forall m\in G.\ \forall n\in G.\ \text{HomDiff}(G,P,s,\langle m,n\rangle ) = s(m\cdot n)\cdot (s(m)\cdot s(n))^{-1} \) using HomDiff_notation
then show \( thesis \) by (rule ZF1_1_L4A )
qed
Let's define some notation. We inherit the notation and assumptions from the group0 context (locale) and add some. We will use AH to denote the set of almost homomorphisms. \(\sim\) is the inverse (negative if the group is the group of integers) of almost homomorphisms, \((\sim p)(n)= p(n)^{-1}\). \(\delta \) will denote the homomorphism difference specific for the group (HomDiff\((G,f)\)). The notation \(s \approx r\) will mean that \(s,r\) are almost equal, that is they are in the equivalence relation defined by the group of finite range functions (that is a normal subgroup of almost homomorphisms, if the group is abelian). We show that this is equivalent to the set \(\{ s(n)\cdot r(n)^{-1}: n\in G\}\) being finite. We also add an assumption that the \(G\) is abelian as many needed properties do not hold without that.
locale group1 = group0 +
assumes isAbelian: \( P \text{ is commutative on } G \)
defines \( AH \equiv \text{AlmostHoms}(G,P) \)
defines \( Op1 \equiv \text{AlHomOp1}(G,P) \)
defines \( Op2 \equiv \text{AlHomOp2}(G,P) \)
defines \( FR \equiv \text{FinRangeFunctions}(G,G) \)
defines \( \sim s \equiv \text{GroupInv}(G,P)\circ s \)
defines \( \delta (s,x) \equiv \text{HomDiff}(G,P,s,x) \)
defines \( s \bullet r \equiv \text{AlHomOp1}(G,P)\langle s,r\rangle \)
defines \( s \circ r \equiv \text{AlHomOp2}(G,P)\langle s,r\rangle \)
defines \( s \cong r \equiv \langle s,r\rangle \in \text{QuotientGroupRel}(AH,Op1,FR) \)
HomDiff is a homomorphism on the lifted group structure.
lemma (in group1) Group_ZF_3_2_L1:
assumes A1: \( s:G\rightarrow G \), \( r:G\rightarrow G \) and A2: \( x \in G\times G \) and A3: \( F = P \text{ lifted to function space over } G \)
shows \( \delta (F\langle s,r\rangle ,x) = \delta (s,x)\cdot \delta (r,x) \)proof let \( p = F\langle s,r\rangle \)
from A2 obtain \( m \) \( n \) where D1: \( x = \langle m,n\rangle \), \( m\in G \), \( n\in G \)
then have T1: \( m\cdot n \in G \) using group0_2_L1, group0_1_L1
with A1, D1 have T2: \( s(m)\in G \), \( s(n)\in G \), \( r(m)\in G \), \( r(n)\in G \), \( s(m\cdot n)\in G \), \( r(m\cdot n)\in G \) using apply_funtype
from A3, A1 have T3: \( p : G\rightarrow G \) using group0_2_L1, Group_ZF_2_1_L0
from D1, T3 have \( \delta (p,x) = p(m\cdot n)\cdot ((p(n))^{-1}\cdot (p(m))^{-1}) \) using HomDiff_notation, apply_funtype, group_inv_of_two
also
qed
from A3, A1, D1, T1, isAbelian, T2 have \( \ldots = \delta (s,x)\cdot \delta (r,x) \) using Group_ZF_2_1_L3, group0_4_L3, HomDiff_notation
finally show \( thesis \)
The group operation lifted to the function space over \(G\) preserves almost homomorphisms.
lemma (in group1) Group_ZF_3_2_L2:
assumes A1: \( s \in AH \), \( r \in AH \) and A2: \( F = P \text{ lifted to function space over } G \)
shows \( F\langle s,r\rangle \in AH \)proof let \( p = F\langle s,r\rangle \)
from A1, A2 have \( p : G\rightarrow G \) using AlmostHoms_def, group0_2_L1, Group_ZF_2_1_L0
moreover
qed
have \( \{\delta (p,x).\ x \in G\times G\} \in Fin(G) \)proof
ultimately show \( thesis \) using AlmostHoms_def
from A1 have \( \{\delta (s,x).\ x \in G\times G \} \in Fin(G) \), \( \{\delta (r,x).\ x \in G\times G \} \in Fin(G) \) using AlmostHoms_def
with groupAssum, A1, A2 show \( thesis \) using IsAgroup_def, IsAmonoid_def, IsAssociative_def, Finite1_L15, AlmostHoms_def, Group_ZF_3_2_L1
qed
The set of almost homomorphisms is closed under the lifted group operation.
lemma (in group1) Group_ZF_3_2_L3:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( AH \text{ is closed under } F \) using assms, IsOpClosed_def, Group_ZF_3_2_L2The terms in the homomorphism difference for a function are in the group.
lemma (in group1) Group_ZF_3_2_L4:
assumes \( s:G\rightarrow G \) and \( m\in G \), \( n\in G \)
shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in G \) using assms, group_op_closed, inverse_in_group, apply_funtype, HomDiff_defIt is handy to have a version of Group_ZF_3_2_L4 specifically for almost homomorphisms.
corollary (in group1) Group_ZF_3_2_L4A:
assumes \( s \in AH \) and \( m\in G \), \( n\in G \)
shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in G \) using assms, AlmostHoms_def, Group_ZF_3_2_L4The terms in the homomorphism difference are in the group, a different form.
lemma (in group1) Group_ZF_3_2_L4B:
assumes A1: \( s \in AH \) and A2: \( 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 \)proof let \( m = \text{fst}(x) \)
let \( n = \text{snd}(x) \)
from A1, A2 show \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( s(m)\cdot s(n) \in G \) using Group_ZF_3_2_L4A
from A1, A2 have \( \delta (s,\langle m,n\rangle ) \in G \) using Group_ZF_3_2_L4A
moreover
qed
from A2 have \( \langle m,n\rangle = x \)
ultimately show \( \delta (s,x) \in G \)
What are the values of the inverse of an almost homomorphism?
lemma (in group1) Group_ZF_3_2_L5:
assumes \( s \in AH \) and \( n\in G \)
shows \( (\sim s)(n) = (s(n))^{-1} \) using assms, AlmostHoms_def, comp_fun_applyHomomorphism difference commutes with the inverse for almost homomorphisms.
lemma (in group1) Group_ZF_3_2_L6:
assumes A1: \( s \in AH \) and A2: \( x\in G\times G \)
shows \( \delta (\sim s,x) = (\delta (s,x))^{-1} \)proof let \( m = \text{fst}(x) \)
let \( n = \text{snd}(x) \)
have \( \delta (\sim s,x) = (\sim s)(m\cdot n)\cdot ((\sim s)(m)\cdot (\sim s)(n))^{-1} \) using HomDiff_def
from A1, A2, isAbelian show \( thesis \) using Group_ZF_3_2_L4B, HomDiff_def, Group_ZF_3_2_L5, group0_4_L4A
qed
The inverse of an almost homomorphism maps the group into itself.
lemma (in group1) Group_ZF_3_2_L7:
assumes \( s \in AH \)
shows \( \sim s : G\rightarrow G \) using groupAssum, assms, AlmostHoms_def, group0_2_T2, comp_funThe inverse of an almost homomorphism is an almost homomorphism.
lemma (in group1) Group_ZF_3_2_L8:
assumes A1: \( F = P \text{ lifted to function space over } G \) and A2: \( s \in AH \)
shows \( \text{GroupInv}(G\rightarrow G,F)(s) \in AH \)proof from A2 have \( \{\delta (s,x).\ x \in G\times G\} \in Fin(G) \) using AlmostHoms_def
with groupAssum have \( \text{GroupInv}(G,P)\{\delta (s,x).\ x \in G\times G\} \in Fin(G) \) using group0_2_T2, Finite1_L6A
moreover
have \( \text{GroupInv}(G,P)\{\delta (s,x).\ x \in G\times G\} =\)
\( \{(\delta (s,x))^{-1}.\ x \in G\times G\} \)proof
ultimately have \( \{(\delta (s,x))^{-1}.\ x \in G\times G\} \in Fin(G) \)
from groupAssum have \( \text{GroupInv}(G,P) : G\rightarrow G \) using group0_2_T2
moreover
qed
from A2 have \( \forall x\in G\times G.\ \delta (s,x)\in G \) using Group_ZF_3_2_L4B
ultimately show \( thesis \) using func1_1_L17
moreover
qed
from A2 have \( \{(\delta (s,x))^{-1}.\ x \in G\times G\} = \{\delta (\sim s,x).\ x \in G\times G\} \) using Group_ZF_3_2_L6
ultimately have \( \{\delta (\sim s,x).\ x \in G\times G\} \in Fin(G) \)
with A2, groupAssum, A1 show \( thesis \) using Group_ZF_3_2_L7, AlmostHoms_def, Group_ZF_2_1_L6
The function that assigns the neutral element everywhere is an almost homomorphism.
lemma (in group1) Group_ZF_3_2_L9:
shows \( \text{ConstantFunction}(G,1 ) \in AH \) and \( AH\neq 0 \)proof let \( z = \text{ConstantFunction}(G,1 ) \)
have \( G\times G\neq 0 \) using group0_2_L1, group0_1_L3A
moreover
qed
have \( \forall x\in G\times G.\ \delta (z,x) = 1 \)proof
ultimately have \( \{\delta (z,x).\ x\in G\times G\} = \{1 \} \) by (rule ZF1_1_L5 )
fix \( x \)
assume A1: \( x \in G \times G \)
then obtain \( m \) \( n \) where \( x = \langle m,n\rangle \), \( m\in G \), \( n\in G \)
then show \( \delta (z,x) = 1 \) using group0_2_L1, group0_1_L1, func1_3_L2, HomDiff_def, group0_2_L2, group_inv_of_one
qed
then show \( z \in AH \) using group0_2_L2, Finite1_L16, func1_3_L1, group0_2_L2, AlmostHoms_def
then show \( AH\neq 0 \)
If the group is abelian, then almost homomorphisms form a subgroup of the lifted group.
lemma Group_ZF_3_2_L10:
assumes A1: \( \text{IsAgroup}(G,P) \) and A2: \( P \text{ is commutative on } G \) and A3: \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAsubgroup}( \text{AlmostHoms}(G,P),F) \)proof let \( AH = \text{AlmostHoms}(G,P) \)
from A2, A1 have T1: \( group1(G,P) \) using group1_axioms.intro, group0_def, group1_def
from A1, A3 have \( group0(G\rightarrow G,F) \) using group0_def, Group_ZF_2_1_T2
moreover
qed
from T1 have \( AH\neq 0 \) using Group_ZF_3_2_L9
moreover have T2: \( AH \subseteq G\rightarrow G \) using AlmostHoms_def
moreover from T1, A3 have \( AH \text{ is closed under } F \) using Group_ZF_3_2_L3
moreover from T1, A3 have \( \forall s\in AH.\ \text{GroupInv}(G\rightarrow G,F)(s) \in AH \) using Group_ZF_3_2_L8
ultimately show \( \text{IsAsubgroup}( \text{AlmostHoms}(G,P),F) \) using group0_3_T3
If the group is abelian, then almost homomorphisms form a group with the first operation, hence we can use theorems proven in group0 context aplied to this group.
lemma (in group1) Group_ZF_3_2_L10A:
shows \( \text{IsAgroup}(AH,Op1) \), \( group0(AH,Op1) \) using groupAssum, isAbelian, Group_ZF_3_2_L10, IsAsubgroup_def, AlHomOp1_def, group0_defThe group of almost homomorphisms is abelian
lemma Group_ZF_3_2_L11:
assumes A1: \( \text{IsAgroup}(G,f) \) and A2: \( f \text{ is commutative on } G \)
shows \( \text{IsAgroup}( \text{AlmostHoms}(G,f), \text{AlHomOp1}(G,f)) \), \( \text{AlHomOp1}(G,f) \text{ is commutative on } \text{AlmostHoms}(G,f) \)proof let \( AH = \text{AlmostHoms}(G,f) \)
let \( F = f \text{ lifted to function space over } G \)
from A1, A2 have \( \text{IsAsubgroup}(AH,F) \) using Group_ZF_3_2_L10
then show \( \text{IsAgroup}(AH, \text{AlHomOp1}(G,f)) \) using IsAsubgroup_def, AlHomOp1_def
from A1 have \( F : (G\rightarrow G)\times (G\rightarrow G)\rightarrow (G\rightarrow G) \) using IsAgroup_def, monoid0_def, Group_ZF_2_1_L0A
moreover
qed
have \( AH \subseteq G\rightarrow G \) using AlmostHoms_def
moreover from A1, A2 have \( F \text{ is commutative on } (G\rightarrow G) \) using group0_def, Group_ZF_2_1_L7
ultimately show \( \text{AlHomOp1}(G,f)\text{ is commutative on } AH \) using func_ZF_4_L1, AlHomOp1_def
The first operation on homomorphisms acts in a natural way on its operands.
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) \) using assms, AlHomOp1_def, restrict, AlmostHoms_def, Group_ZF_2_1_L3What is the group inverse in the group of almost homomorphisms?
lemma (in group1) Group_ZF_3_2_L13:
assumes A1: \( s\in AH \)
shows \( \text{GroupInv}(AH,Op1)(s) = \text{GroupInv}(G,P)\circ s \), \( \text{GroupInv}(AH,Op1)(s) \in AH \), \( \text{GroupInv}(G,P)\circ s \in AH \)proof let \( F = P \text{ lifted to function space over } G \)
from groupAssum, isAbelian have \( \text{IsAsubgroup}(AH,F) \) using Group_ZF_3_2_L10
with A1 show I: \( \text{GroupInv}(AH,Op1)(s) = \text{GroupInv}(G,P)\circ s \) using AlHomOp1_def, Group_ZF_2_1_L6A
from A1 show \( \text{GroupInv}(AH,Op1)(s) \in AH \) using Group_ZF_3_2_L10A, inverse_in_group
with I show \( \text{GroupInv}(G,P)\circ s \in AH \)
qed
The group inverse in the group of almost homomorphisms acts in a natural way on its operand.
lemma (in group1) Group_ZF_3_2_L14:
assumes \( s\in AH \) and \( n\in G \)
shows \( ( \text{GroupInv}(AH,Op1)(s))(n) = (s(n))^{-1} \) using isAbelian, assms, Group_ZF_3_2_L13, AlmostHoms_def, comp_fun_applyThe next lemma states that if \(s,r\) are almost homomorphisms, then \(s\cdot r^{-1}\) is also an almost homomorphism.
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 \) using assms, group0_def, group1_axioms.intro, group1_def, Group_ZF_3_2_L10A, group0_2_L1, group0_1_L1, inverse_in_groupA version of Group_ZF_3_2_L15 formulated in notation used in group1 context. States that the product of almost homomorphisms is an almost homomorphism and the the product of an almost homomorphism with a (pointwise) inverse of an almost homomorphism is an almost homomorphism.
corollary (in group1) Group_ZF_3_2_L16:
assumes \( s \in AH \), \( r \in AH \)
shows \( s\bullet r \in AH \), \( s\bullet (\sim r) \in AH \) using assms, isAbelian, group0_def, group1_axioms, group1_def, Group_ZF_3_2_L15, Group_ZF_3_2_L13The classes of almost homomorphisms
In the Real_ZF series we define real numbers as a quotient of the group of integer almost homomorphisms by the integer finite range functions. In this section we setup the background for that in the general group context.
Finite range functions are almost homomorphisms.
lemma (in group1) Group_ZF_3_3_L1:
shows \( FR \subseteq AH \)proof fix \( s \)
assume A1: \( s \in FR \)
then have T1: \( \{s(n).\ n \in G\} \in Fin(G) \), \( \{s(\text{fst}(x)).\ x\in G\times G\} \in Fin(G) \), \( \{s(\text{snd}(x)).\ x\in G\times G\} \in Fin(G) \) using Finite1_L18, Finite1_L6B
have \( \{s(\text{fst}(x)\cdot \text{snd}(x)).\ x \in G\times G\} \in Fin(G) \)proof
have \( \forall x\in G\times G.\ \text{fst}(x)\cdot \text{snd}(x) \in G \) using group0_2_L1, group0_1_L1
moreover
qed
from T1 have \( \{s(n).\ n \in G\} \in Fin(G) \)
ultimately show \( thesis \) by (rule Finite1_L6B )
moreover
qed
have \( \{(s(\text{fst}(x))\cdot s(\text{snd}(x)))^{-1}.\ x\in G\times G\} \in Fin(G) \)proof
ultimately have \( \{\delta (s,x).\ x\in G\times G\} \in Fin(G) \) using HomDiff_def, Finite1_L15, group_oper_fun
have \( \forall g\in G.\ g^{-1} \in G \) using inverse_in_group
moreover
qed
from T1 have \( \{s(\text{fst}(x))\cdot s(\text{snd}(x)).\ x\in G\times G\} \in Fin(G) \) using group_oper_fun, Finite1_L15
ultimately show \( thesis \) by (rule Finite1_L6C )
with A1 show \( s \in AH \) using FinRangeFunctions_def, AlmostHoms_def
Finite range functions valued in an abelian group form a normal subgroup of almost homomorphisms.
lemma Group_ZF_3_3_L2:
assumes A1: \( \text{IsAgroup}(G,f) \) and A2: \( f \text{ is commutative on } G \)
shows \( \text{IsAsubgroup}( \text{FinRangeFunctions}(G,G), \text{AlHomOp1}(G,f)) \), \( \text{IsAnormalSubgroup}( \text{AlmostHoms}(G,f), \text{AlHomOp1}(G,f),\) \( \text{FinRangeFunctions}(G,G)) \)proof let \( H1 = \text{AlmostHoms}(G,f) \)
let \( H2 = \text{FinRangeFunctions}(G,G) \)
let \( F = f \text{ lifted to function space over } G \)
from A1, A2 have T1: \( group0(G,f) \), \( monoid0(G,f) \), \( group1(G,f) \) using group0_def, group0_2_L1, group1_axioms.intro, group1_def
with A1, A2 have \( \text{IsAgroup}(G\rightarrow G,F) \), \( \text{IsAsubgroup}(H1,F) \), \( \text{IsAsubgroup}(H2,F) \) using Group_ZF_2_1_T2, Group_ZF_3_2_L10, group0_1_L3A, Group_ZF_3_1_T1
then have \( \text{IsAsubgroup}(H1\cap H2,\text{restrict}(F,H1\times H1)) \) using group0_3_L7
moreover
qed
from T1 have \( H1\cap H2 = H2 \) using Group_ZF_3_3_L1
ultimately show \( \text{IsAsubgroup}(H2, \text{AlHomOp1}(G,f)) \) using AlHomOp1_def
with A1, A2 show \( \text{IsAnormalSubgroup}( \text{AlmostHoms}(G,f), \text{AlHomOp1}(G,f),\)
\( \text{FinRangeFunctions}(G,G)) \) using Group_ZF_3_2_L11, Group_ZF_2_4_L6
The group of almost homomorphisms divided by the subgroup of finite range functions is an abelian group.
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)) \) using groupAssum, isAbelian, Group_ZF_3_3_L2, Group_ZF_3_2_L10A, Group_ZF_2_4_T1, Group_ZF_3_2_L10A, Group_ZF_3_2_L11, Group_ZF_3_3_L2, IsAnormalSubgroup_def, Group_ZF_2_4_L6It is useful to have a direct statement that the quotient group relation is an equivalence relation for the group of AH and subgroup FR.
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)) \) using groupAssum, isAbelian, QuotientGroupRel_def, Group_ZF_3_3_L2, Group_ZF_3_2_L10A, Group_ZF_2_4_L3The "almost equal" relation is symmetric.
lemma (in group1) Group_ZF_3_3_L3A:
assumes A1: \( s\cong r \)
shows \( r\cong s \)proof let \( R = \text{QuotientGroupRel}(AH,Op1,FR) \)
from A1 have \( \text{equiv}(AH,R) \) and \( \langle s,r\rangle \in R \) using Group_ZF_3_3_L3
then have \( \langle r,s\rangle \in R \) by (rule equiv_is_sym )
then show \( r\cong s \)
qed
Although we have bypassed this fact when proving that group of almost homomorphisms divided by the subgroup of finite range functions is a group, it is still useful to know directly that the first group operation on AH is congruent with respect to the quotient group relation.
lemma (in group1) Group_ZF_3_3_L4:
shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op1) \) using groupAssum, isAbelian, Group_ZF_3_2_L10A, Group_ZF_3_3_L2, Group_ZF_2_4_L5AThe class of an almost homomorphism \(s\) is the neutral element of the quotient group of almost homomorphisms iff \(s\) is a finite range function.
lemma (in group1) Group_ZF_3_3_L5:
assumes \( s \in AH \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( \text{ TheNeutralElement}(AH//r, \text{QuotientGroupOp}(AH,Op1,FR)) = e \)
shows \( r\{s\} = e \longleftrightarrow s \in FR \) using groupAssum, isAbelian, assms, Group_ZF_3_2_L11, group0_def, Group_ZF_3_3_L2, Group_ZF_2_4_L5EThe group inverse of a class of an almost homomorphism \(f\) is the class of the inverse of \(f\).
lemma (in group1) Group_ZF_3_3_L6:
assumes A1: \( s \in AH \) and \( r = \text{QuotientGroupRel}(AH,Op1,FR) \) and \( F = \text{ProjFun2}(AH,r,Op1) \)
shows \( r\{\sim s\} = \text{GroupInv}(AH//r,F)(r\{s\}) \)proof from groupAssum, isAbelian, assms have \( r\{ \text{GroupInv}(AH, Op1)(s)\} = \text{GroupInv}(AH//r,F)(r \{s\}) \) using Group_ZF_3_2_L10A, Group_ZF_3_3_L2, QuotientGroupOp_def, Group_ZF_2_4_L7
with A1 show \( thesis \) using Group_ZF_3_2_L13
qed
Compositions of almost homomorphisms
The goal of this section is to establish some facts about composition of almost homomorphisms that are needed for the real numbers construction in Real_ZF_x series. In particular we show that the set of almost homomorphisms is closed under composition and that composition is congruent with respect to the equivalence relation defined by the group of finite range functions (a normal subgroup of almost homomorphisms).
The next formula restates the definition of the homomorphism difference to express the value an almost homomorphism on a product.
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 ) \) using isAbelian, assms, Group_ZF_3_2_L4A, HomDiff_def, group0_4_L5What is the value of a composition of almost homomorhisms?
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 \) using assms, AlmostHoms_def, func_ZF_5_L3, restrict, AlHomOp2_def, apply_funtypeWhat is the homomorphism difference of a composition?
lemma (in group1) Group_ZF_3_4_L3:
assumes A1: \( s\in AH \), \( r\in AH \) and A2: \( m\in G \), \( n\in G \)
shows \( \delta (s\circ r,\langle m,n\rangle ) = \) \( \delta (s,\langle r(m),r(n)\rangle )\cdot s(\delta (r,\langle m,n\rangle ))\cdot \delta (s,\langle r(m)\cdot r(n),\delta (r,\langle m,n\rangle )\rangle ) \)proof from A1, A2 have T1: \( s(r(m))\cdot s(r(n)) \in G \), \( \delta (s,\langle r(m),r(n)\rangle )\in G \), \( s(\delta (r,\langle m,n\rangle )) \in G \), \( \delta (s,\langle (r(m)\cdot r(n)),\delta (r,\langle m,n\rangle )\rangle ) \in G \) using Group_ZF_3_4_L2, AlmostHoms_def, apply_funtype, Group_ZF_3_2_L4A, group0_2_L1, group0_1_L1
from A1, A2 have \( \delta (s\circ r,\langle m,n\rangle ) =\)
\( s(r(m)\cdot r(n)\cdot \delta (r,\langle m,n\rangle ))\cdot (s((r(m)))\cdot s(r(n)))^{-1} \) using HomDiff_def, group0_2_L1, group0_1_L1, Group_ZF_3_4_L2, Group_ZF_3_4_L1
moreover
qed
from A1, A2 have \( s(r(m)\cdot r(n)\cdot \delta (r,\langle m,n\rangle )) =\)
\( s(r(m)\cdot r(n))\cdot s(\delta (r,\langle m,n\rangle ))\cdot \delta (s,\langle (r(m)\cdot r(n)),\delta (r,\langle m,n\rangle )\rangle ) \), \( s(r(m)\cdot r(n)) = s(r(m))\cdot s(r(n))\cdot \delta (s,\langle r(m),r(n)\rangle ) \) using Group_ZF_3_2_L4A, Group_ZF_3_4_L1
moreover from T1, isAbelian have \( s(r(m))\cdot s(r(n))\cdot \delta (s,\langle r(m),r(n)\rangle )\cdot \)
\( s(\delta (r,\langle m,n\rangle ))\cdot \delta (s,\langle (r(m)\cdot r(n)),\delta (r,\langle m,n\rangle )\rangle )\cdot \)
\( (s((r(m)))\cdot s(r(n)))^{-1} = \)
\( \delta (s,\langle r(m),r(n)\rangle )\cdot s(\delta (r,\langle m,n\rangle ))\cdot \delta (s,\langle (r(m)\cdot r(n)),\delta (r,\langle m,n\rangle )\rangle ) \) using group0_4_L6C
ultimately show \( thesis \)
What is the homomorphism difference of a composition (another form)? Here we split the homomorphism difference of a composition into a product of three factors. This will help us in proving that the range of homomorphism difference for the composition is finite, as each factor has finite range.
lemma (in group1) Group_ZF_3_4_L4:
assumes A1: \( s\in AH \), \( r\in AH \) and A2: \( x \in G\times G \) and A3: \( A = \delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle ) \), \( B = s(\delta (r,x)) \), \( C = \delta (s,\langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle ) \)
shows \( \delta (s\circ r,x) = A\cdot B\cdot C \)proof let \( m = \text{fst}(x) \)
let \( n = \text{snd}(x) \)
note A1
moreover
qed
from A2 have \( m\in G \), \( n\in G \)
ultimately have \( \delta (s\circ r,\langle m,n\rangle ) = \)
\( \delta (s,\langle r(m),r(n)\rangle )\cdot s(\delta (r,\langle m,n\rangle ))\cdot \)
\( \delta (s,\langle (r(m)\cdot r(n)),\delta (r,\langle m,n\rangle )\rangle ) \) by (rule Group_ZF_3_4_L3 )
with A1, A2, A3 show \( thesis \)
The range of the homomorphism difference of a composition of two almost homomorphisms is finite. This is the essential condition to show that a composition of almost homomorphisms is an almost homomorphism.
lemma (in group1) Group_ZF_3_4_L5:
assumes A1: \( s\in AH \), \( r\in AH \)
shows \( \{\delta ( \text{Composition}(G)\langle s,r\rangle ,x).\ x \in G\times G\} \in Fin(G) \)proof from A1 have \( \forall x\in G\times G.\ \langle r(\text{fst}(x)),r(\text{snd}(x))\rangle \in G\times G \) using Group_ZF_3_2_L4B
moreover
from A1 have \( \{\delta (s,x).\ x\in G\times G\} \in Fin(G) \) using AlmostHoms_def
ultimately have \( \{\delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle ).\ x\in G\times G\} \in Fin(G) \) by (rule Finite1_L6B )
moreover
have \( \{s(\delta (r,x)).\ x\in G\times G\} \in Fin(G) \)proof
ultimately have \( \{\delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle )\cdot s(\delta (r,x)).\ x\in G\times G\} \in Fin(G) \) using group_oper_fun, Finite1_L15
from A1 have \( \forall m\in G.\ s(m) \in G \) using AlmostHoms_def, apply_funtype
moreover
qed
from A1 have \( \{\delta (r,x).\ x\in G\times G\} \in Fin(G) \) using AlmostHoms_def
ultimately show \( thesis \) by (rule Finite1_L6C )
moreover
have \( \{\delta (s,\langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle ).\ x\in G\times G\} \in Fin(G) \)proof
ultimately have \( \{\delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle )\cdot s(\delta (r,x))\cdot \)
\( \delta (s,\langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle ).\ x\in G\times G\} \in Fin(G) \) using group_oper_fun, Finite1_L15
from A1 have \( \forall x\in G\times G.\ \langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle \in G\times G \) using Group_ZF_3_2_L4B
moreover
qed
from A1 have \( \{\delta (s,x).\ x\in G\times G\} \in Fin(G) \) using AlmostHoms_def
ultimately show \( thesis \) by (rule Finite1_L6B )
moreover
qed
from A1 have \( \{\delta (s\circ r,x).\ x\in G\times G\} = \)
\( \{\delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle )\cdot s(\delta (r,x))\cdot \)
\( \delta (s,\langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle ).\ x\in G\times G\} \) using Group_ZF_3_4_L4
ultimately have \( \{\delta (s\circ r,x).\ x\in G\times G\} \in Fin(G) \)
with A1 show \( thesis \) using restrict, AlHomOp2_def
Composition of almost homomorphisms is an almost homomorphism.
theorem (in group1) Group_ZF_3_4_T1:
assumes A1: \( s\in AH \), \( r\in AH \)
shows \( \text{Composition}(G)\langle s,r\rangle \in AH \), \( s\circ r \in AH \)proof from A1 have \( \langle s,r\rangle \in (G\rightarrow G)\times (G\rightarrow G) \) using AlmostHoms_def
then have \( \text{Composition}(G)\langle s,r\rangle : G\rightarrow G \) using func_ZF_5_L1, apply_funtype
with A1 show \( \text{Composition}(G)\langle s,r\rangle \in AH \) using Group_ZF_3_4_L5, AlmostHoms_def
with A1 show \( s\circ r \in AH \) using AlHomOp2_def, restrict
qed
The set of almost homomorphisms is closed under composition. The second operation on almost homomorphisms is associative.
lemma (in group1) Group_ZF_3_4_L6:
shows \( AH \text{ is closed under } \text{Composition}(G) \), \( \text{AlHomOp2}(G,P) \text{ is associative on } AH \)proof show \( AH \text{ is closed under } \text{Composition}(G) \) using Group_ZF_3_4_T1, IsOpClosed_def
moreover
qed
have \( AH \subseteq G\rightarrow G \) using AlmostHoms_def
moreover have \( \text{Composition}(G) \text{ is associative on } (G\rightarrow G) \) using func_ZF_5_L5
ultimately show \( \text{AlHomOp2}(G,P) \text{ is associative on } AH \) using func_ZF_4_L3, AlHomOp2_def
Type information related to the situation of two almost homomorphisms.
lemma (in group1) Group_ZF_3_4_L7:
assumes A1: \( s\in AH \), \( r\in AH \) and A2: \( n\in G \)
shows \( s(n) \in G \), \( (r(n))^{-1} \in G \), \( s(n)\cdot (r(n))^{-1} \in G \), \( s(r(n)) \in G \)proof from A1, A2 show \( s(n) \in G \), \( (r(n))^{-1} \in G \), \( s(r(n)) \in G \), \( s(n)\cdot (r(n))^{-1} \in G \) using AlmostHoms_def, apply_type, group0_2_L1, group0_1_L1, inverse_in_group
qed
Type information related to the situation of three almost homomorphisms.
lemma (in group1) Group_ZF_3_4_L8:
assumes A1: \( s\in AH \), \( r\in AH \), \( q\in AH \) and A2: \( n\in G \)
shows \( q(n)\in G \), \( s(r(n)) \in G \), \( r(n)\cdot (q(n))^{-1} \in G \), \( s(r(n)\cdot (q(n))^{-1}) \in G \), \( \delta (s,\langle q(n),r(n)\cdot (q(n))^{-1}\rangle ) \in G \)proof from A1, A2 show \( q(n)\in G \), \( s(r(n)) \in G \), \( r(n)\cdot (q(n))^{-1} \in G \) using AlmostHoms_def, apply_type, group0_2_L1, group0_1_L1, inverse_in_group
with A1, A2 show \( s(r(n)\cdot (q(n))^{-1}) \in G \), \( \delta (s,\langle q(n),r(n)\cdot (q(n))^{-1}\rangle ) \in G \) using AlmostHoms_def, apply_type, Group_ZF_3_2_L4A
qed
A formula useful in showing that the composition of almost homomorphisms is congruent with respect to the quotient group relation.
lemma (in group1) Group_ZF_3_4_L9:
assumes A1: \( s1 \in AH \), \( r1 \in AH \), \( s2 \in AH \), \( r2 \in AH \) and A2: \( n\in G \)
shows \( (s1\circ r1)(n)\cdot ((s2\circ r2)(n))^{-1} =\) \( s1(r2(n))\cdot (s2(r2(n)))^{-1}\cdot s1(r1(n)\cdot (r2(n))^{-1})\cdot \) \( \delta (s1,\langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle ) \)proof from A1, A2, isAbelian have \( (s1\circ r1)(n)\cdot ((s2\circ r2)(n))^{-1} =\)
\( s1(r2(n)\cdot (r1(n)\cdot (r2(n))^{-1}))\cdot (s2(r2(n)))^{-1} \) using Group_ZF_3_4_L2, Group_ZF_3_4_L7, group0_4_L6A, group_oper_assoc
with A1, A2 have \( (s1\circ r1)(n)\cdot ((s2\circ r2)(n))^{-1} = s1(r2(n))\cdot \)
\( s1(r1(n)\cdot (r2(n))^{-1})\cdot \delta (s1,\langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle )\cdot \)
\( (s2(r2(n)))^{-1} \) using Group_ZF_3_4_L8, Group_ZF_3_4_L1
with A1, A2, isAbelian show \( thesis \) using Group_ZF_3_4_L8, group0_4_L7
qed
The next lemma shows a formula that translates an expression in terms of the first group operation on almost homomorphisms and the group inverse in the group of almost homomorphisms to an expression using only the underlying group operations.
lemma (in group1) Group_ZF_3_4_L10:
assumes A1: \( s \in AH \), \( r \in AH \) and A2: \( n \in G \)
shows \( (s\bullet ( \text{GroupInv}(AH,Op1)(r)))(n) = s(n)\cdot (r(n))^{-1} \)proof from A1, A2 show \( thesis \) using isAbelian, Group_ZF_3_2_L13, Group_ZF_3_2_L12, Group_ZF_3_2_L14
qed
A neccessary condition for two a. h. to be almost equal.
lemma (in group1) Group_ZF_3_4_L11:
assumes A1: \( s\cong r \)
shows \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \)proof from A1 have \( s\in AH \), \( r\in AH \) using QuotientGroupRel_def
moreover
qed
from A1 have \( \{(s\bullet ( \text{GroupInv}(AH,Op1)(r)))(n).\ n\in G\} \in Fin(G) \) using QuotientGroupRel_def, Finite1_L18
ultimately show \( thesis \) using Group_ZF_3_4_L10
A sufficient condition for two a. h. to be almost equal.
lemma (in group1) Group_ZF_3_4_L12:
assumes A1: \( s\in AH \), \( r\in AH \) and A2: \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \)
shows \( s\cong r \)proof from groupAssum, isAbelian, A1, A2 show \( thesis \) using Group_ZF_3_2_L15, AlmostHoms_def, Group_ZF_3_4_L10, Finite1_L19, QuotientGroupRel_def
qed
Another sufficient consdition for two a.h. to be almost equal. It is actually just an expansion of the definition of the quotient group relation.
lemma (in group1) Group_ZF_3_4_L12A:
assumes \( s\in AH \), \( r\in AH \) and \( s\bullet ( \text{GroupInv}(AH,Op1)(r)) \in FR \)
shows \( s\cong r \), \( r\cong s \)proof from assms show \( s\cong r \) using assms, QuotientGroupRel_def
then show \( r\cong s \) by (rule Group_ZF_3_3_L3A )
qed
Another necessary condition for two a.h. to be almost equal. It is actually just an expansion of the definition of the quotient group relation.
lemma (in group1) Group_ZF_3_4_L12B:
assumes \( s\cong r \)
shows \( s\bullet ( \text{GroupInv}(AH,Op1)(r)) \in FR \) using assms, QuotientGroupRel_defThe next lemma states the essential condition for the composition of a. h. to be congruent with respect to the quotient group relation for the subgroup of finite range functions.
lemma (in group1) Group_ZF_3_4_L13:
assumes A1: \( s1\cong s2 \), \( r1\cong r2 \)
shows \( (s1\circ r1) \cong (s2\circ r2) \)proof have \( \{s1(r2(n))\cdot (s2(r2(n)))^{-1}.\ n\in G\} \in Fin(G) \)proof
from A1 have \( \forall n\in G.\ r2(n) \in G \) using QuotientGroupRel_def, AlmostHoms_def, apply_funtype
moreover
qed
from A1 have \( \{s1(n)\cdot (s2(n))^{-1}.\ n\in G\} \in Fin(G) \) using Group_ZF_3_4_L11
ultimately show \( thesis \) by (rule Finite1_L6B )
moreover
have \( \{s1(r1(n)\cdot (r2(n))^{-1}).\ n \in G\} \in Fin(G) \)proof
ultimately have \( \{s1(r2(n))\cdot (s2(r2(n)))^{-1}\cdot s1(r1(n)\cdot (r2(n))^{-1}).\ \)
\( n\in G\} \in Fin(G) \) using group_oper_fun, Finite1_L15
from A1 have \( \forall n\in G.\ s1(n)\in G \) using QuotientGroupRel_def, AlmostHoms_def, apply_funtype
moreover
qed
from A1 have \( \{r1(n)\cdot (r2(n))^{-1}.\ n\in G\} \in Fin(G) \) using Group_ZF_3_4_L11
ultimately show \( thesis \) by (rule Finite1_L6C )
moreover
qed
have \( \{\delta (s1,\langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle ).\ n\in G\} \in Fin(G) \)proof
ultimately have \( \{s1(r2(n))\cdot (s2(r2(n)))^{-1}\cdot s1(r1(n)\cdot (r2(n))^{-1})\cdot \)
\( \delta (s1,\langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle ).\ n\in G\} \in Fin(G) \) using group_oper_fun, Finite1_L15
from A1 have \( \forall n\in G.\ \langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle \in G\times G \) using QuotientGroupRel_def, Group_ZF_3_4_L7
moreover
qed
from A1 have \( \{\delta (s1,x).\ x \in G\times G\} \in Fin(G) \) using QuotientGroupRel_def, AlmostHoms_def
ultimately show \( thesis \) by (rule Finite1_L6B )
with A1 show \( thesis \) using QuotientGroupRel_def, Group_ZF_3_4_L9, Group_ZF_3_4_T1, Group_ZF_3_4_L12
Composition of a. h. to is congruent with respect to the quotient group relation for the subgroup of finite range functions. Recall that if an operation say "\(\circ \)" on \(X\) is congruent with respect to an equivalence relation \(R\) then we can define the operation on the quotient space \(X/R\) by \([s]_R\circ [r]_R := [s\circ r]_R\) and this definition will be correct i.e. it will not depend on the choice of representants for the classes \([x]\) and \([y]\). This is why we want it here.
lemma (in group1) Group_ZF_3_4_L13A:
shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op2) \)proof show \( thesis \) using Group_ZF_3_4_L13, Congruent2_def
qed
The homomorphism difference for the identity function is equal to the neutral element of the group (denoted \(e\) in the group1 context).
lemma (in group1) Group_ZF_3_4_L14:
assumes A1: \( x \in G\times G \)
shows \( \delta (id(G),x) = 1 \)proof from A1 show \( thesis \) using group0_2_L1, group0_1_L1, HomDiff_def, id_conv, group0_2_L6
qed
The identity function (\(I(x) = x\)) on \(G\) is an almost homomorphism.
lemma (in group1) Group_ZF_3_4_L15:
shows \( id(G) \in AH \)proof have \( G\times G \neq 0 \) using group0_2_L1, group0_1_L3A
then show \( thesis \) using Group_ZF_3_4_L14, group0_2_L2, id_type, AlmostHoms_def
qed
Almost homomorphisms form a monoid with composition. The identity function on the group is the neutral element there.
lemma (in group1) Group_ZF_3_4_L16:
shows \( \text{IsAmonoid}(AH,Op2) \), \( monoid0(AH,Op2) \), \( id(G) = \text{ TheNeutralElement}(AH,Op2) \)proof let \( i = \text{ TheNeutralElement}(G\rightarrow G, \text{Composition}(G)) \)
have \( \text{IsAmonoid}(G\rightarrow G, \text{Composition}(G)) \), \( monoid0(G\rightarrow G, \text{Composition}(G)) \) using monoid0_def, Group_ZF_2_5_L2
moreover
qed
have \( AH \text{ is closed under } \text{Composition}(G) \) using Group_ZF_3_4_L6
moreover have \( AH \subseteq G\rightarrow G \) using AlmostHoms_def
moreover have \( i \in AH \) using Group_ZF_2_5_L2, Group_ZF_3_4_L15
moreover have \( id(G) = i \) using Group_ZF_2_5_L2
ultimately show \( \text{IsAmonoid}(AH,Op2) \), \( monoid0(AH,Op2) \), \( id(G) = \text{ TheNeutralElement}(AH,Op2) \) using group0_1_T1, group0_1_L6, AlHomOp2_def, monoid0_def
We can project the monoid of almost homomorphisms with composition to the group of almost homomorphisms divided by the subgroup of finite range functions. The class of the identity function is the neutral element of the quotient (monoid).
theorem (in group1) Group_ZF_3_4_T2:
assumes A1: \( 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)) \)proof have \( group0(AH,Op1) \) using Group_ZF_3_2_L10A, group0_def
with A1, groupAssum, isAbelian show \( \text{IsAmonoid}(AH//R, \text{ProjFun2}(AH,R,Op2)) \), \( R\{id(G)\} = \text{ TheNeutralElement}(AH//R, \text{ProjFun2}(AH,R,Op2)) \) using Group_ZF_3_3_L2, Group_ZF_2_4_L3, Group_ZF_3_4_L13A, Group_ZF_3_4_L16, Group_ZF_2_2_T1, Group_ZF_2_2_L1
qed
Shifting almost homomorphisms
In this this section we consider what happens if we multiply an almost homomorphism by a group element. We show that the resulting function is also an a. h., and almost equal to the original one. This is used only for slopes (integer a.h.) in Int_ZF_2 where we need to correct a positive slopes by adding a constant, so that it is at least \(2\) on positive integers.
If \(s\) is an almost homomorphism and \(c\) is some constant from the group, then \(s\cdot c\) is an almost homomorphism.
lemma (in group1) Group_ZF_3_5_L1:
assumes A1: \( s \in AH \) and A2: \( c\in G \) and A3: \( r = \{\langle x,s(x)\cdot c\rangle .\ x\in G\} \)
shows \( \forall x\in G.\ r(x) = s(x)\cdot c \), \( r \in AH \), \( s \cong r \)proof from A1, A2, A3 have I: \( r:G\rightarrow G \) using AlmostHoms_def, apply_funtype, group_op_closed, ZF_fun_from_total
with A3 show II: \( \forall x\in G.\ r(x) = s(x)\cdot c \) using ZF_fun_from_tot_val
with isAbelian, A1, A2 have III: \( \forall p \in G\times G.\ \delta (r,p) = \delta (s,p)\cdot c^{-1} \) using group_op_closed, AlmostHoms_def, apply_funtype, HomDiff_def, group0_4_L7
have \( \{\delta (r,p).\ p \in G\times G\} \in Fin(G) \)proof
from A1, A2 have \( \{\delta (s,p).\ p \in G\times G\} \in Fin(G) \), \( c^{-1}\in G \) using AlmostHoms_def, inverse_in_group
then have \( \{\delta (s,p)\cdot c^{-1}.\ p \in G\times G\} \in Fin(G) \) using group_oper_fun, Finite1_L16AA
moreover
qed
from III have \( \{\delta (r,p).\ p \in G\times G\} = \{\delta (s,p)\cdot c^{-1}.\ p \in G\times G\} \) by (rule ZF1_1_L4B )
ultimately show \( thesis \)
with I show IV: \( r \in AH \) using AlmostHoms_def
from isAbelian, A1, A2, I, II have \( \forall n \in G.\ s(n)\cdot (r(n))^{-1} = c^{-1} \) using AlmostHoms_def, apply_funtype, group0_4_L6AB
then have \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} = \{c^{-1}.\ n\in G\} \) by (rule ZF1_1_L4B )
with A1, A2, IV show \( s \cong r \) using group0_2_L1, group0_1_L3A, inverse_in_group, Group_ZF_3_4_L12
qed
end
Definition of FinRangeFunctions:
\( \text{FinRangeFunctions}(X,Y) \equiv \{f:X\rightarrow Y.\ f(X) \in Fin(Y)\} \)
lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) Group_ZF_2_1_L0:
assumes \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow G \), \( r:X\rightarrow G \)
shows \( F\langle s,r\rangle : X\rightarrow G \) lemma Finite1_L18:
assumes \( f \in \text{FinRangeFunctions}(X,Y) \)
shows \( \{f(x).\ x\in X\} \in Fin(Y) \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma Finite1_L15:
assumes \( \{b(x).\ x\in A\} \in Fin(B) \), \( \{c(x).\ x\in A\} \in Fin(C) \) and \( f : B\times C\rightarrow E \)
shows \( \{f\langle b(x),c(x)\rangle .\ x\in A\} \in Fin(E) \) lemma (in group0) Group_ZF_2_1_L3:
assumes \( F = P \text{ lifted to function space over } X \) and \( s:X\rightarrow G \), \( r:X\rightarrow G \) and \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = s(x)\cdot r(x) \) lemma func_imagedef:
assumes \( f:X\rightarrow Y \) and \( A\subseteq X \)
shows \( f(A) = \{f(x).\ x \in A\} \) lemma (in group0) Group_ZF_3_1_L1:
assumes \( F = P \text{ lifted to function space over } X \) and \( s \in \text{FinRangeFunctions}(X,G) \), \( r \in \text{FinRangeFunctions}(X,G) \)
shows \( F\langle s,r\rangle \in \text{FinRangeFunctions}(X,G) \)Definition of IsOpClosed:
\( A \text{ is closed under } f \equiv \forall x\in A.\ \forall y\in A.\ f\langle x,y\rangle \in A \)
theorem group0_2_T2:
assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \) lemma Finite1_L20:
assumes \( f \in \text{FinRangeFunctions}(X,Y) \) and \( g : Y\rightarrow Z \)
shows \( g\circ f \in \text{FinRangeFunctions}(X,Z) \) theorem (in group0) Group_ZF_2_1_T2:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( \text{IsAgroup}(X\rightarrow G,F) \) lemma (in monoid0) unit_is_neutral:
assumes \( e = \text{ TheNeutralElement}(G,f) \)
shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \) lemma Finite1_L17:
assumes \( c\in Y \) and \( X\neq 0 \)
shows \( \text{ConstantFunction}(X,c) \in \text{FinRangeFunctions}(X,Y) \) lemma (in group0) Group_ZF_3_1_L2:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( \text{FinRangeFunctions}(X,G) \text{ is closed under } F \) lemma (in group0) Group_ZF_2_1_L6:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( \forall s\in (X\rightarrow G).\ \text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s \) lemma (in group0) Group_ZF_3_1_L3:
assumes \( s \in \text{FinRangeFunctions}(X,G) \)
shows \( \text{GroupInv}(G,P)\circ s \in \text{FinRangeFunctions}(X,G) \) theorem (in group0) group0_3_T3:
assumes \( H\neq 0 \) and \( H\subseteq G \) and \( H \text{ is closed under } P \) and \( \forall x\in H.\ x^{-1} \in H \)
shows \( \text{IsAsubgroup}(H,P) \)Definition of HomDiff:
\( \text{HomDiff}(G,f,s,x) \equiv \)
\( f\langle s(f\langle \text{fst}(x),\text{snd}(x)\rangle ) , \)
\( ( \text{GroupInv}(G,f)(f\langle s(\text{fst}(x)),s(\text{snd}(x))\rangle ))\rangle \)
lemma (in group0) HomDiff_notation: shows \( \text{HomDiff}(G,P,s,\langle m,n\rangle ) = s(m\cdot n)\cdot (s(m)\cdot s(n))^{-1} \)
lemma ZF1_1_L4A:
assumes \( \forall x\in X.\ \forall y\in Y.\ a(\langle x,y\rangle ) = b(x,y) \)
shows \( \{a(p).\ p \in X\times Y\} = \{b(x,y).\ \langle x,y\rangle \in X\times Y\} \) lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) lemma (in group0) group_inv_of_two:
assumes \( a\in G \) and \( b\in G \)
shows \( b^{-1}\cdot a^{-1} = (a\cdot b)^{-1} \) lemma (in group0) group0_4_L3:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \) and \( c\in G \), \( d\in G \), \( E\in G \), \( F\in G \)
shows \( a\cdot b\cdot ((c\cdot d)^{-1}\cdot (E\cdot F)^{-1}) = (a\cdot (E\cdot c)^{-1})\cdot (b\cdot (F\cdot d)^{-1}) \)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)\} \)
Definition of IsAgroup:
\( \text{IsAgroup}(G,f) \equiv \)
\( ( \text{IsAmonoid}(G,f) \wedge (\forall g\in G.\ \exists b\in G.\ f\langle g,b\rangle = \text{ TheNeutralElement}(G,f))) \)
Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in group1) Group_ZF_3_2_L1:
assumes \( s:G\rightarrow G \), \( r:G\rightarrow G \) and \( x \in G\times G \) and \( F = P \text{ lifted to function space over } G \)
shows \( \delta (F\langle s,r\rangle ,x) = \delta (s,x)\cdot \delta (r,x) \) lemma (in group1) Group_ZF_3_2_L2:
assumes \( s \in AH \), \( r \in AH \) and \( F = P \text{ lifted to function space over } G \)
shows \( F\langle s,r\rangle \in AH \) lemma (in group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) lemma (in group1) Group_ZF_3_2_L4:
assumes \( s:G\rightarrow G \) and \( m\in G \), \( n\in G \)
shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in G \) corollary (in group1) Group_ZF_3_2_L4A:
assumes \( s \in AH \) and \( m\in G \), \( n\in G \)
shows \( m\cdot n \in G \), \( s(m\cdot n) \in G \), \( s(m) \in G \), \( s(n) \in G \), \( \delta (s,\langle m,n\rangle ) \in G \), \( s(m)\cdot s(n) \in 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 group1) Group_ZF_3_2_L5:
assumes \( s \in AH \) and \( n\in G \)
shows \( (\sim s)(n) = (s(n))^{-1} \) lemma (in group0) group0_4_L4A:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot b\cdot c = c\cdot a\cdot b \), \( a^{-1}\cdot (b^{-1}\cdot c^{-1})^{-1} = (a\cdot (b\cdot c)^{-1})^{-1} \), \( a\cdot (b\cdot c)^{-1} = a\cdot b^{-1}\cdot c^{-1} \), \( a\cdot (b\cdot c^{-1})^{-1} = a\cdot b^{-1}\cdot c \), \( a\cdot b^{-1}\cdot c^{-1} = a\cdot c^{-1}\cdot b^{-1} \) lemma Finite1_L6A:
assumes \( f:X\rightarrow Y \) and \( N \in Fin(X) \)
shows \( f(N) \in Fin(Y) \) lemma func1_1_L17:
assumes \( f \in X\rightarrow Y \) and \( \forall x\in A.\ b(x) \in X \)
shows \( f(\{b(x).\ x\in A\}) = \{f(b(x)).\ x\in A\} \) lemma (in group1) Group_ZF_3_2_L6:
assumes \( s \in AH \) and \( x\in G\times G \)
shows \( \delta (\sim s,x) = (\delta (s,x))^{-1} \) lemma (in group1) Group_ZF_3_2_L7:
assumes \( s \in AH \)
shows \( \sim s : G\rightarrow G \) lemma (in monoid0) group0_1_L3A: shows \( G\neq 0 \)
lemma func1_3_L2:
assumes \( x\in X \)
shows \( \text{ConstantFunction}(X,c)(x) = c \) lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma ZF1_1_L5:
assumes \( X\neq \emptyset \) and \( \forall x\in X.\ b(x) = c \)
shows \( \{b(x).\ x\in X\} = \{c\} \) lemma Finite1_L16:
assumes \( x\in X \)
shows \( \{x\} \in Fin(X) \) lemma func1_3_L1:
assumes \( c\in Y \)
shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \) lemma (in group1) Group_ZF_3_2_L9: shows \( \text{ConstantFunction}(G,1 ) \in AH \) and \( AH\neq 0 \)
lemma (in group1) Group_ZF_3_2_L3:
assumes \( F = P \text{ lifted to function space over } G \)
shows \( AH \text{ is closed under } F \) lemma (in group1) Group_ZF_3_2_L8:
assumes \( F = P \text{ lifted to function space over } G \) and \( s \in AH \)
shows \( \text{GroupInv}(G\rightarrow G,F)(s) \in AH \) lemma Group_ZF_3_2_L10:
assumes \( \text{IsAgroup}(G,P) \) and \( P \text{ is commutative on } G \) and \( F = P \text{ lifted to function space over } G \)
shows \( \text{IsAsubgroup}( \text{AlmostHoms}(G,P),F) \)Definition of IsAsubgroup:
\( \text{IsAsubgroup}(H,P) \equiv \text{IsAgroup}(H, \text{restrict}(P,H\times H)) \)
Definition of AlHomOp1:
\( \text{AlHomOp1}(G,f) \equiv \)
\( \text{restrict}(f \text{ lifted to function space over } G,\)
\( \text{AlmostHoms}(G,f)\times \text{AlmostHoms}(G,f)) \)
lemma (in monoid0) Group_ZF_2_1_L0A:
assumes \( F = f \text{ lifted to function space over } X \)
shows \( F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G) \) lemma (in group0) Group_ZF_2_1_L7:
assumes \( F = P \text{ lifted to function space over } X \) and \( P \text{ is commutative on } G \)
shows \( F \text{ is commutative on } (X\rightarrow G) \) lemma func_ZF_4_L1:
assumes \( f:X\times X\rightarrow Y \) and \( A\subseteq X \) and \( f \text{ is commutative on } X \)
shows \( \text{restrict}(f,A\times A) \text{ is commutative on } A \) lemma (in group0) Group_ZF_2_1_L6A:
assumes \( F = P \text{ lifted to function space over } X \) and \( \text{IsAsubgroup}(H,F) \) and \( g = \text{restrict}(F,H\times H) \) and \( s\in H \)
shows \( \text{GroupInv}(H,g)(s) = \text{GroupInv}(G,P)\circ s \) lemma (in group1) Group_ZF_3_2_L10A: shows \( \text{IsAgroup}(AH,Op1) \), \( group0(AH,Op1) \)
lemma (in group1) Group_ZF_3_2_L13:
assumes \( s\in AH \)
shows \( \text{GroupInv}(AH,Op1)(s) = \text{GroupInv}(G,P)\circ s \), \( \text{GroupInv}(AH,Op1)(s) \in AH \), \( \text{GroupInv}(G,P)\circ s \in AH \) 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 \) 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 Finite1_L6C:
assumes \( \forall y\in Y.\ b(y) \in Z \) and \( \{a(x).\ x\in X\} \in Fin(Y) \)
shows \( \{b(a(x)).\ x\in X\} \in Fin(Z) \) theorem Group_ZF_3_1_T1:
assumes \( \text{IsAgroup}(G,P) \) and \( F = P \text{ lifted to function space over } X \) and \( X\neq 0 \)
shows \( \text{IsAsubgroup}( \text{FinRangeFunctions}(X,G),F) \) lemma group0_3_L7:
assumes \( \text{IsAgroup}(G,f) \) and \( \text{IsAsubgroup}(H_1,f) \) and \( \text{IsAsubgroup}(H_2,f) \)
shows \( \text{IsAsubgroup}(H_1\cap H_2,\text{restrict}(f,H_1\times H_1)) \) lemma (in group1) Group_ZF_3_3_L1: shows \( FR \subseteq AH \)
lemma Group_ZF_3_2_L11:
assumes \( \text{IsAgroup}(G,f) \) and \( f \text{ is commutative on } G \)
shows \( \text{IsAgroup}( \text{AlmostHoms}(G,f), \text{AlHomOp1}(G,f)) \), \( \text{AlHomOp1}(G,f) \text{ is commutative on } \text{AlmostHoms}(G,f) \) lemma Group_ZF_2_4_L6:
assumes \( \text{IsAgroup}(G,P) \) and \( P \text{ is commutative on } G \) and \( \text{IsAsubgroup}(H,P) \)
shows \( \text{IsAnormalSubgroup}(G,P,H) \), \( \text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H)) \) lemma Group_ZF_3_3_L2:
assumes \( \text{IsAgroup}(G,f) \) and \( f \text{ is commutative on } G \)
shows \( \text{IsAsubgroup}( \text{FinRangeFunctions}(G,G), \text{AlHomOp1}(G,f)) \), \( \text{IsAnormalSubgroup}( \text{AlmostHoms}(G,f), \text{AlHomOp1}(G,f),\) \( \text{FinRangeFunctions}(G,G)) \) theorem Group_ZF_2_4_T1:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{IsAgroup}(G// \text{QuotientGroupRel}(G,P,H), \text{QuotientGroupOp}(G,P,H)) \)Definition of IsAnormalSubgroup:
\( \text{IsAnormalSubgroup}(G,P,N) \equiv \text{IsAsubgroup}(N,P) \wedge \)
\( (\forall n\in N.\ \forall g\in G.\ P\langle P\langle g,n \rangle , \text{GroupInv}(G,P)(g) \rangle \in N) \)
Definition of QuotientGroupRel:
\( \text{QuotientGroupRel}(G,P,H) \equiv \)
\( \{\langle a,b\rangle \in G\times G.\ P\langle a, \text{GroupInv}(G,P)(b)\rangle \in H\} \)
lemma (in group0) Group_ZF_2_4_L3:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \) 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 equiv_is_sym:
assumes \( \text{equiv}(X,r) \) and \( \langle x,y\rangle \in r \)
shows \( \langle y,x\rangle \in r \) lemma Group_ZF_2_4_L5A:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \)
shows \( \text{Congruent2}( \text{QuotientGroupRel}(G,P,H),P) \) lemma (in group0) Group_ZF_2_4_L5E:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( a\in G \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e \)
shows \( r\{a\} = e \longleftrightarrow a\in H \)Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
lemma (in group0) Group_ZF_2_4_L7:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( a\in G \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( F = \text{QuotientGroupOp}(G,P,H) \)
shows \( r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\}) \) lemma (in group0) group0_4_L5:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \) and \( c = a\cdot b^{-1} \)
shows \( a = b\cdot c \) lemma func_ZF_5_L3:
assumes \( f:X\rightarrow X \) and \( g:X\rightarrow X \) and \( x\in X \)
shows \( ( \text{Composition}(X)\langle f,g\rangle )(x) = f(g(x)) \)Definition of AlHomOp2:
\( \text{AlHomOp2}(G,f) \equiv \)
\( \text{restrict}( \text{Composition}(G), \text{AlmostHoms}(G,f)\times \text{AlmostHoms}(G,f)) \)
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_L6C:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\cdot b\cdot c\cdot d\cdot a^{-1} = b\cdot c\cdot d \) lemma (in group1) Group_ZF_3_4_L3:
assumes \( s\in AH \), \( r\in AH \) and \( m\in G \), \( n\in G \)
shows \( \delta (s\circ r,\langle m,n\rangle ) = \) \( \delta (s,\langle r(m),r(n)\rangle )\cdot s(\delta (r,\langle m,n\rangle ))\cdot \delta (s,\langle r(m)\cdot r(n),\delta (r,\langle m,n\rangle )\rangle ) \) lemma (in group1) Group_ZF_3_4_L4:
assumes \( s\in AH \), \( r\in AH \) and \( x \in G\times G \) and \( A = \delta (s,\langle r(\text{fst}(x)),r(\text{snd}(x))\rangle ) \), \( B = s(\delta (r,x)) \), \( C = \delta (s,\langle (r(\text{fst}(x))\cdot r(\text{snd}(x))),\delta (r,x)\rangle ) \)
shows \( \delta (s\circ r,x) = A\cdot B\cdot C \) lemma func_ZF_5_L1: shows \( \text{Composition}(X) : (X\rightarrow X)\times (X\rightarrow X)\rightarrow (X\rightarrow X) \)
lemma (in group1) Group_ZF_3_4_L5:
assumes \( s\in AH \), \( r\in AH \)
shows \( \{\delta ( \text{Composition}(G)\langle s,r\rangle ,x).\ x \in G\times G\} \in Fin(G) \) 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 \) lemma func_ZF_5_L5: shows \( \text{Composition}(X) \text{ is associative on } (X\rightarrow X) \)
lemma func_ZF_4_L3:
assumes \( f \text{ is associative on } X \) and \( A\subseteq X \) and \( A \text{ is closed under } f \)
shows \( \text{restrict}(f,A\times A) \text{ is associative on } A \) lemma (in group1) Group_ZF_3_4_L7:
assumes \( s\in AH \), \( r\in AH \) and \( n\in G \)
shows \( s(n) \in G \), \( (r(n))^{-1} \in G \), \( s(n)\cdot (r(n))^{-1} \in G \), \( s(r(n)) \in G \) 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 (in group0) group_oper_assoc:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \) lemma (in group1) Group_ZF_3_4_L8:
assumes \( s\in AH \), \( r\in AH \), \( q\in AH \) and \( n\in G \)
shows \( q(n)\in G \), \( s(r(n)) \in G \), \( r(n)\cdot (q(n))^{-1} \in G \), \( s(r(n)\cdot (q(n))^{-1}) \in G \), \( \delta (s,\langle q(n),r(n)\cdot (q(n))^{-1}\rangle ) \in G \) lemma (in group0) group0_4_L7:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( a\cdot b\cdot c\cdot d^{-1} = a\cdot d^{-1}\cdot b\cdot c \), \( a\cdot d\cdot (b\cdot d\cdot (c\cdot d))^{-1} = a\cdot (b\cdot c)^{-1}\cdot d^{-1} \), \( a\cdot (b\cdot c)\cdot d = a\cdot b\cdot d\cdot c \) 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_2_L14:
assumes \( s\in AH \) and \( n\in G \)
shows \( ( \text{GroupInv}(AH,Op1)(s))(n) = (s(n))^{-1} \) lemma (in group1) Group_ZF_3_4_L10:
assumes \( s \in AH \), \( r \in AH \) and \( n \in G \)
shows \( (s\bullet ( \text{GroupInv}(AH,Op1)(r)))(n) = s(n)\cdot (r(n))^{-1} \) lemma Finite1_L19:
assumes \( f:X\rightarrow Y \) and \( \{f(x).\ x\in X\} \in Fin(Y) \)
shows \( f \in \text{FinRangeFunctions}(X,Y) \) lemma (in group1) Group_ZF_3_3_L3A:
assumes \( s\cong r \)
shows \( r\cong s \) lemma (in group1) Group_ZF_3_4_L11:
assumes \( s\cong r \)
shows \( \{s(n)\cdot (r(n))^{-1}.\ n\in G\} \in Fin(G) \) lemma (in group1) Group_ZF_3_4_L9:
assumes \( s1 \in AH \), \( r1 \in AH \), \( s2 \in AH \), \( r2 \in AH \) and \( n\in G \)
shows \( (s1\circ r1)(n)\cdot ((s2\circ r2)(n))^{-1} =\) \( s1(r2(n))\cdot (s2(r2(n)))^{-1}\cdot s1(r1(n)\cdot (r2(n))^{-1})\cdot \) \( \delta (s1,\langle r2(n),r1(n)\cdot (r2(n))^{-1}\rangle ) \) 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_4_L13:
assumes \( s1\cong s2 \), \( r1\cong r2 \)
shows \( (s1\circ r1) \cong (s2\circ r2) \)Definition of Congruent2:
\( \text{Congruent2}(r,f) \equiv \)
\( (\forall x_1 x_2 y_1 y_2.\ \langle x_1,x_2\rangle \in r \wedge \langle y_1,y_2\rangle \in r \longrightarrow \)
\( \langle f\langle x_1,y_1\rangle , f\langle x_2,y_2\rangle \rangle \in r) \)
lemma (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \) lemma (in group1) Group_ZF_3_4_L14:
assumes \( x \in G\times G \)
shows \( \delta (id(G),x) = 1 \) lemma Group_ZF_2_5_L2: shows \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \), \( id(X) = \text{ TheNeutralElement}(X\rightarrow X, \text{Composition}(X)) \)
lemma (in group1) Group_ZF_3_4_L6: shows \( AH \text{ is closed under } \text{Composition}(G) \), \( \text{AlHomOp2}(G,P) \text{ is associative on } AH \)
lemma (in group1) Group_ZF_3_4_L15: shows \( id(G) \in AH \)
theorem (in monoid0) group0_1_T1:
assumes \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{IsAmonoid}(H,\text{restrict}(f,H\times H)) \) lemma group0_1_L6:
assumes \( \text{IsAmonoid}(G,f) \) and \( H \text{ is closed under } f \) and \( H\subseteq G \) and \( \text{ TheNeutralElement}(G,f) \in H \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(f,H\times H)) = \text{ TheNeutralElement}(G,f) \) lemma (in group1) Group_ZF_3_4_L13A: shows \( \text{Congruent2}( \text{QuotientGroupRel}(AH,Op1,FR),Op2) \)
lemma (in group1) Group_ZF_3_4_L16: shows \( \text{IsAmonoid}(AH,Op2) \), \( monoid0(AH,Op2) \), \( id(G) = \text{ TheNeutralElement}(AH,Op2) \)
theorem (in monoid0) Group_ZF_2_2_T1:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,f) \) and \( F = \text{ProjFun2}(G,r,f) \)
shows \( \text{IsAmonoid}(G//r,F) \) lemma Group_ZF_2_2_L1:
assumes \( \text{IsAmonoid}(G,f) \) and \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,f) \) and \( F = \text{ProjFun2}(G,r,f) \) and \( e = \text{ TheNeutralElement}(G,f) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r,F) \) lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) lemma ZF_fun_from_tot_val:
assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( f(x) = b(x) \) and \( b(x)\in Y \) lemma Finite1_L16AA:
assumes \( \{b(x).\ x\in A\} \in Fin(B) \) and \( c\in C \) and \( f : B\times C\rightarrow E \)
shows \( \{f\langle b(x),c\rangle .\ x\in A\} \in Fin(E) \) lemma ZF1_1_L4B:
assumes \( \forall x\in X.\ a(x) = b(x) \)
shows \( \{a(x).\ x\in X\} = \{b(x).\ x\in X\} \) lemma (in group0) group0_4_L6AB:
assumes \( P \text{ is commutative on } G \) and \( a\in G \), \( b\in G \)
shows \( a\cdot (a\cdot b)^{-1} = b^{-1} \), \( a\cdot (b\cdot a^{-1}) = b \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8