theory Group_ZF_1 imports Group_ZF
begin
In this theory we consider right and left translations and odd functions.
Translations
In this section we consider translations. Translations are maps \(T: G\rightarrow G\) of the form \(T_g (a) = g\cdot a\) or \(T_g (a) = a\cdot g\). We also consider two-dimensional translations \(T_g : G\times G \rightarrow G\times G\), where \(T_g(a,b) = (a\cdot g, b\cdot g)\) or \(T_g(a,b) = (g\cdot a, g\cdot b)\).
For an element \(a\in G\) the right translation is defined a function (set of pairs) such that its value (the second element of a pair) is the value of the group operation on the first element of the pair and \(g\). This looks a bit strange in the raw set notation, when we write a function explicitely as a set of pairs and value of the group operation on the pair \(\langle a,b \rangle\) as \( P\langle a,b\rangle \) instead of the usual infix \(a\cdot b\) or \(a + b\).
Definition
\( RightTranslation(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\} \)
A similar definition of the left translation.
Definition
\( LeftTranslation(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\} \)
Translations map \(G\) into \(G\). Two dimensional translations map \(G\times G\) into itself.
lemma (in group0) group0_5_L1:
assumes A1: \( g\in G \)
shows \( RightTranslation(G,P,g) : G\rightarrow G \), \( LeftTranslation(G,P,g) : G\rightarrow G \)proof from A1 have \( \forall a\in G.\ a\cdot g \in G \) and \( \forall a\in G.\ g\cdot a \in G \) using group_oper_assocA , apply_funtype
then show \( RightTranslation(G,P,g) : G\rightarrow G \), \( LeftTranslation(G,P,g) : G\rightarrow G \) using RightTranslation_def , LeftTranslation_def , func1_1_L11A
qed
The values of the translations are what we expect.
lemma (in group0) group0_5_L2:
assumes \( g\in G \), \( a\in G \)
shows \( RightTranslation(G,P,g)(a) = a\cdot g \), \( LeftTranslation(G,P,g)(a) = g\cdot a \) using assms , group0_5_L1 , RightTranslation_def , LeftTranslation_def , func1_1_L11BComposition of left translations is a left translation by the product.
lemma (in group0) group0_5_L4:
assumes A1: \( g\in G \), \( h\in G \), \( a\in G \) and A2: \( T_g = LeftTranslation(G,P,g) \), \( T_h = LeftTranslation(G,P,h) \)
shows \( T_g(T_h(a)) = g\cdot h\cdot a \), \( T_g(T_h(a)) = LeftTranslation(G,P,g\cdot h)(a) \)proof from A1 have I: \( h\cdot a\in G \), \( g\cdot h\in G \) using group_oper_assocA , apply_funtype
with A1, A2 show \( T_g(T_h(a)) = g\cdot h\cdot a \) using group0_5_L2 , group_oper_assoc
with A1, A2, I show \( T_g(T_h(a)) = LeftTranslation(G,P,g\cdot h)(a) \) using group0_5_L2 , group_oper_assoc
qed
Composition of right translations is a right translation by the product.
lemma (in group0) group0_5_L5:
assumes A1: \( g\in G \), \( h\in G \), \( a\in G \) and A2: \( T_g = RightTranslation(G,P,g) \), \( T_h = RightTranslation(G,P,h) \)
shows \( T_g(T_h(a)) = a\cdot h\cdot g \), \( T_g(T_h(a)) = RightTranslation(G,P,h\cdot g)(a) \)proof from A1 have I: \( a\cdot h\in G \), \( h\cdot g \in G \) using group_oper_assocA , apply_funtype
with A1, A2 show \( T_g(T_h(a)) = a\cdot h\cdot g \) using group0_5_L2 , group_oper_assoc
with A1, A2, I show \( T_g(T_h(a)) = RightTranslation(G,P,h\cdot g)(a) \) using group0_5_L2 , group_oper_assoc
qed
The image of a set under a composition of translations is the same as the image under translation by a product.
lemma (in group0) group0_5_L6:
assumes A1: \( g\in G \), \( h\in G \) and A2: \( A\subseteq G \) and A3: \( T_g = RightTranslation(G,P,g) \), \( T_h = RightTranslation(G,P,h) \)
shows \( T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\} \)proof from A2 have \( \forall a\in A.\ a\in G \)
from A1, A3 have \( T_g : G\rightarrow G \), \( T_h : G\rightarrow G \) using group0_5_L1
with assms, \( \forall a\in A.\ a\in G \) show \( T_g(T_h(A)) = \{a\cdot h\cdot g.\ a\in A\} \) using func1_1_L15C , group0_5_L5
qed
Odd functions
This section is about odd functions.
Odd functions are those that commute with the group inverse: \(f(a^{-1}) = (f(a))^{-1}.\)
Definition
\( IsOdd(G,P,f) \equiv (\forall a\in G.\ f(GroupInv(G,P)(a)) = GroupInv(G,P)(f(a)) ) \)
Let's see the definition of an odd function in a more readable notation.
lemma (in group0) group0_6_L1:
shows \( IsOdd(G,P,p) \longleftrightarrow ( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} ) \) using IsOdd_defWe can express the definition of an odd function in two ways.
lemma (in group0) group0_6_L2:
assumes A1: \( p : G\rightarrow G \)
shows \( (\forall a\in G.\ p(a^{-1}) = (p(a))^{-1}) \longleftrightarrow (\forall a\in G.\ (p(a^{-1}))^{-1} = p(a)) \)proof assume \( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} \)
with A1 show \( \forall a\in G.\ (p(a^{-1}))^{-1} = p(a) \) using apply_funtype , group_inv_of_inv
next
assume A2: \( \forall a\in G.\ (p(a^{-1}))^{-1} = p(a) \)
{
fix \( a \)
assume \( a\in G \)
with A1, A2 have \( p(a^{-1}) \in G \) and \( ((p(a^{-1}))^{-1})^{-1} = (p(a))^{-1} \) using apply_funtype , inverse_in_group
then have \( p(a^{-1}) = (p(a))^{-1} \) using group_inv_of_inv
then show \( \forall a\in G.\ p(a^{-1}) = (p(a))^{-1} \)
qed
end
lemma (in group0) group_oper_assocA: shows \( P : G\times G\rightarrow G \)
Definition of RightTranslation:
\( RightTranslation(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle a,g\rangle = b\} \)
Definition of LeftTranslation:
\( LeftTranslation(G,P,g) \equiv \{\langle a,b\rangle \in G\times G.\ P\langle g,a\rangle = b\} \)
lemma func1_1_L11A: assumes \( \forall x\in X.\ b(x) \in Y \) shows \( \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} : X\rightarrow Y \)
lemma (in group0) group0_5_L1: assumes \( g\in G \) shows \( RightTranslation(G,P,g) : G\rightarrow G \), \( LeftTranslation(G,P,g) : G\rightarrow G \)
lemma func1_1_L11B: assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,y\rangle \in X\times Y.\ b(x) = y\} \) shows \( f(x) = b(x) \)
lemma (in group0) group0_5_L2: assumes \( g\in G \), \( a\in G \) shows \( RightTranslation(G,P,g)(a) = a\cdot g \), \( LeftTranslation(G,P,g)(a) = g\cdot a \)
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 func1_1_L15C: assumes \( f:X\rightarrow Y \) and \( g:Y\rightarrow Z \) and \( A\subseteq X \) shows \( g(f(A)) = \{g(f(x)).\ x\in A\} \), \( g(f(A)) = (g\circ f)(A) \)
lemma (in group0) group0_5_L5: assumes \( g\in G \), \( h\in G \), \( a\in G \) and \( T_g = RightTranslation(G,P,g) \), \( T_h = RightTranslation(G,P,h) \) shows \( T_g(T_h(a)) = a\cdot h\cdot g \), \( T_g(T_h(a)) = RightTranslation(G,P,h\cdot g)(a) \)
Definition of IsOdd:
\( IsOdd(G,P,f) \equiv (\forall a\in G.\ f(GroupInv(G,P)(a)) = GroupInv(G,P)(f(a)) ) \)
lemma (in group0) group_inv_of_inv: assumes \( a\in G \) shows \( a = (a^{-1})^{-1} \)
lemma (in group0) inverse_in_group: assumes \( x\in G \) shows \( x^{-1}\in G \)
