begin
This theory continues Group\_ZF.thy and considers lifting the group structure to function spaces and projecting the group structure to quotient spaces, in particular the quotient qroup.
Lifting groups to function spaces
If we have a monoid (group) \(G\) than we get a monoid (group) structure on a space of functions valued in in \(G\) by defining \((f\cdot g)(x) := f(x)\cdot g(x)\). We call this process ''lifting the monoid (group) to function space''. This section formalizes this lifting.
The lifted operation is an operation on the function space.
lemma (in monoid0) Group_ZF_2_1_L0A:
assumes A1: \( F = f \text{ lifted to function space over } X \)
shows \( F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G) \)proof from monoidAssum have \( f : G\times G\rightarrow G \) using IsAmonoid_def, IsAssociative_def
with A1 show \( thesis \) using func_ZF_1_L3, group0_1_L3B
qed
The result of the lifted operation is in the function space.
lemma (in monoid0) Group_ZF_2_1_L0:
assumes A1: \( F = f \text{ lifted to function space over } X \) and A2: \( s:X\rightarrow G \), \( r:X\rightarrow G \)
shows \( F\langle s,r\rangle : X\rightarrow G \)proof from A1 have \( F : (X\rightarrow G)\times (X\rightarrow G)\rightarrow (X\rightarrow G) \) using Group_ZF_2_1_L0A
with A2 show \( thesis \) using apply_funtype
qed
The lifted monoid operation has a neutral element, namely the constant function with the neutral element as the value.
lemma (in monoid0) Group_ZF_2_1_L1:
assumes A1: \( F = f \text{ lifted to function space over } X \) and A2: \( E = \text{ConstantFunction}(X,\text{ TheNeutralElement}(G,f)) \)
shows \( E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s) \)proof from A2 show T1: \( E : X\rightarrow G \) using unit_is_neutral, func1_3_L1
show \( \forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s \)proof
qed
fix \( s \)
assume A3: \( s:X\rightarrow G \)
from monoidAssum have T2: \( f : G\times G\rightarrow G \) using IsAmonoid_def, IsAssociative_def
from A3, A1, T1 have \( F\langle E,s\rangle : X\rightarrow G \), \( F\langle s,E\rangle : X\rightarrow G \), \( s : X\rightarrow G \) using Group_ZF_2_1_L0
moreover
qed
from T2, A1, T1, A2, A3 have \( \forall x\in X.\ (F\langle E,s\rangle )(x) = s(x) \), \( \forall x\in X.\ (F\langle s,E\rangle )(x) = s(x) \) using func_ZF_1_L4, group0_1_L3B, func1_3_L2, apply_type, unit_is_neutral
ultimately show \( F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s \) using fun_extension_iff
Monoids can be lifted to a function space.
lemma (in monoid0) Group_ZF_2_1_T1:
assumes A1: \( F = f \text{ lifted to function space over } X \)
shows \( \text{IsAmonoid}(X\rightarrow G,F) \)proof from monoidAssum, A1 have \( F \text{ is associative on } (X\rightarrow G) \) using IsAmonoid_def, func_ZF_2_L4, group0_1_L3B
moreover
qed
from A1 have \( \exists E \in X\rightarrow G.\ \forall s \in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s \) using Group_ZF_2_1_L1
ultimately show \( thesis \) using IsAmonoid_def
The constant function with the neutral element as the value is the neutral element of the lifted monoid.
lemma Group_ZF_2_1_L2:
assumes A1: \( \text{IsAmonoid}(G,f) \) and A2: \( F = f \text{ lifted to function space over } X \) and A3: \( E = \text{ConstantFunction}(X,\text{ TheNeutralElement}(G,f)) \)
shows \( E = \text{ TheNeutralElement}(X\rightarrow G,F) \)proof from A1, A2 have T1: \( monoid0(G,f) \) and T2: \( monoid0(X\rightarrow G,F) \) using monoid0_def, Group_ZF_2_1_T1
from T1, A2, A3 have \( E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s) \) using Group_ZF_2_1_L1
with T2 show \( thesis \) using group0_1_L4
qed
The lifted operation acts on the functions in a natural way defined by the monoid operation.
lemma (in monoid0) lifted_val:
assumes \( F = f \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) \oplus r(x) \) using monoidAssum, assms, IsAmonoid_def, IsAssociative_def, group0_1_L3B, func_ZF_1_L4The lifted operation acts on the functions in a natural way defined by the group operation. This is the same as lifted_val, but in the group0 context.
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) \) using assms, group0_2_L1, lifted_valIn the group0 context we can apply theorems proven in monoid0 context to the lifted monoid.
lemma (in group0) Group_ZF_2_1_L4:
assumes A1: \( F = P \text{ lifted to function space over } X \)
shows \( monoid0(X\rightarrow G,F) \)proof from A1 show \( thesis \) using group0_2_L1, Group_ZF_2_1_T1, monoid0_def
qed
The compostion of a function \(f:X\rightarrow G\) with the group inverse is a right inverse for the lifted group.
lemma (in group0) Group_ZF_2_1_L5:
assumes A1: \( F = P \text{ lifted to function space over } X \) and A2: \( s : X\rightarrow G \) and A3: \( i = \text{GroupInv}(G,P)\circ s \)
shows \( i: X\rightarrow G \) and \( F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \)proof let \( E = \text{ConstantFunction}(X,1 ) \)
have \( E : X\rightarrow G \) using group0_2_L2, func1_3_L1
moreover
from groupAssum, A2, A3, A1 have \( F\langle s,i\rangle : X\rightarrow G \) using group0_2_T2, comp_fun, Group_ZF_2_1_L4, group0_1_L1
moreover from groupAssum, A2, A3, A1 have \( \forall x\in X.\ (F\langle s,i\rangle )(x) = E(x) \) using group0_2_T2, comp_fun, Group_ZF_2_1_L3, comp_fun_apply, apply_funtype, group0_2_L6, func1_3_L2
moreover from groupAssum, A1 have \( E = \text{ TheNeutralElement}(X\rightarrow G,F) \) using IsAgroup_def, Group_ZF_2_1_L2
ultimately show \( F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \) using fun_extension_iff, IsAgroup_def, Group_ZF_2_1_L2
from groupAssum, A2, A3 show \( i: X\rightarrow G \) using group0_2_T2, comp_fun
qed
Groups can be lifted to the function space.
theorem (in group0) Group_ZF_2_1_T2:
assumes A1: \( F = P \text{ lifted to function space over } X \)
shows \( \text{IsAgroup}(X\rightarrow G,F) \)proof from A1 have \( \text{IsAmonoid}(X\rightarrow G,F) \) using group0_2_L1, Group_ZF_2_1_T1
moreover
qed
have \( \forall s\in X\rightarrow G.\ \exists i\in X\rightarrow G.\ F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \)proof
ultimately show \( thesis \) using IsAgroup_def
fix \( s \)
assume A2: \( s : X\rightarrow G \)
let \( i = \text{GroupInv}(G,P)\circ s \)
from groupAssum, A2 have \( i:X\rightarrow G \) using group0_2_T2, comp_fun
moreover
qed
from A1, A2 have \( F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \) using Group_ZF_2_1_L5
ultimately show \( \exists i\in X\rightarrow G.\ F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \)
The propositions proven in the group0 context are valid in the same context when applied to the function space with the lifted group operation.
lemma (in group0) group0_valid_fun_space:
shows \( group0(X\rightarrow G,P \text{ lifted to function space over } X) \) using Group_ZF_2_1_T2 unfolding group0_defWhat is the group inverse for the lifted group?
lemma (in group0) Group_ZF_2_1_L6:
assumes A1: \( 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 \)proof from A1 have \( group0(X\rightarrow G,F) \) using group0_def, Group_ZF_2_1_T2
moreover
qed
from A1 have \( \forall s\in X\rightarrow G.\ \text{GroupInv}(G,P)\circ s : X\rightarrow G \wedge \)
\( F\langle s, \text{GroupInv}(G,P)\circ s\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \) using Group_ZF_2_1_L5
ultimately have \( \forall s\in (X\rightarrow G).\ \text{GroupInv}(G,P)\circ s = \text{GroupInv}(X\rightarrow G,F)(s) \) by (rule group0_2_L9A )
thus \( thesis \)
What is the value of the group inverse for the lifted group?
corollary (in group0) lift_gr_inv_val:
assumes \( F = P \text{ lifted to function space over } X \) and \( s : X\rightarrow G \) and \( x\in X \)
shows \( ( \text{GroupInv}(X\rightarrow G,F)(s))(x) = (s(x))^{-1} \) using groupAssum, assms, Group_ZF_2_1_L6, group0_2_T2, comp_fun_applyWhat is the group inverse in a subgroup of the lifted group?
lemma (in group0) Group_ZF_2_1_L6A:
assumes A1: \( F = P \text{ lifted to function space over } X \) and A2: \( \text{IsAsubgroup}(H,F) \) and A3: \( g = \text{restrict}(F,H\times H) \) and A4: \( s\in H \)
shows \( \text{GroupInv}(H,g)(s) = \text{GroupInv}(G,P)\circ s \)proof from A1 have T1: \( group0(X\rightarrow G,F) \) using group0_def, Group_ZF_2_1_T2
with A2, A3, A4 have \( \text{GroupInv}(H,g)(s) = \text{GroupInv}(X\rightarrow G,F)(s) \) using group0_3_T1, restrict
moreover
qed
from T1, A1, A2, A4 have \( \text{GroupInv}(X\rightarrow G,F)(s) = \text{GroupInv}(G,P)\circ s \) using group0_3_L2, Group_ZF_2_1_L6
ultimately show \( thesis \)
The neutral element of a subgroup of the lifted group is the constant function with value equal to the neutral element of the group.
lemma (in group0) lift_group_subgr_neut:
assumes \( F = P \text{ lifted to function space over } X \) and \( \text{IsAsubgroup}(H,F) \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(F,H\times H)) = \text{ConstantFunction}(X,1 ) \)proof from assms have \( \text{ TheNeutralElement}(H,\text{restrict}(F,H\times H)) = \text{ TheNeutralElement}(X\rightarrow G,F) \) using group0_valid_fun_space, group0_3_L4
also
qed
from groupAssum, assms(1) have \( .\ .\ .\ = \text{ConstantFunction}(X,1 ) \) using Group_ZF_2_1_L2 unfolding IsAgroup_def
finally show \( thesis \)
If a group is abelian, then its lift to a function space is also abelian.
lemma (in group0) Group_ZF_2_1_L7:
assumes A1: \( F = P \text{ lifted to function space over } X \) and A2: \( P \text{ is commutative on } G \)
shows \( F \text{ is commutative on } (X\rightarrow G) \)proof from A1, A2 have \( F \text{ is commutative on } (X\rightarrow \text{range}(P)) \) using group_oper_fun, func_ZF_2_L2
moreover
qed
from groupAssum have \( \text{range}(P) = G \) using group0_2_L1, group0_1_L3B
ultimately show \( thesis \)
Equivalence relations on groups
The goal of this section is to establish that (under some conditions) given an equivalence relation on a group or (monoid )we can project the group (monoid) structure on the quotient and obtain another group.
The neutral element class is neutral in the projection.
lemma (in monoid0) Group_ZF_2_2_L1:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( F = \text{ProjFun2}(G,r,f) \) and A4: \( e = \text{ TheNeutralElement}(G,f) \)
shows \( r\{e\} \in G//r \wedge \) \( (\forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c) \)proof from A4 show T1: \( r\{e\} \in G//r \) using unit_is_neutral, quotientI
show \( \forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c \)proof
qed
fix \( c \)
assume A5: \( c \in G//r \)
then obtain \( g \) where D1: \( g\in G \), \( c = r\{g\} \) using quotient_def
with A1, A2, A3, A4, D1 show \( F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c \) using unit_is_neutral, EquivClass_1_L10
qed
The projected structure is a monoid.
theorem (in monoid0) Group_ZF_2_2_T1:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,f) \) and A3: \( F = \text{ProjFun2}(G,r,f) \)
shows \( \text{IsAmonoid}(G//r,F) \)proof let \( E = r\{\text{ TheNeutralElement}(G,f)\} \)
from A1, A2, A3 have \( E \in G//r \wedge (\forall c\in G//r.\ F\langle E,c\rangle = c \wedge F\langle c,E\rangle = c) \) using Group_ZF_2_2_L1
hence \( \exists E\in G//r.\ \forall c\in G//r.\ F\langle E,c\rangle = c \wedge F\langle c,E\rangle = c \)
with monoidAssum, A1, A2, A3 show \( thesis \) using IsAmonoid_def, EquivClass_2_T2
qed
The class of the neutral element is the neutral element of the projected monoid.
lemma Group_ZF_2_2_L1:
assumes A1: \( \text{IsAmonoid}(G,f) \) and A2: \( \text{equiv}(G,r) \) and A3: \( \text{Congruent2}(r,f) \) and A4: \( F = \text{ProjFun2}(G,r,f) \) and A5: \( e = \text{ TheNeutralElement}(G,f) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r,F) \)proof from A1, A2, A3, A4 have T1: \( monoid0(G,f) \) and T2: \( monoid0(G//r,F) \) using monoid0_def, Group_ZF_2_2_T1
from T1, A2, A3, A4, A5 have \( r\{e\} \in G//r \wedge \)
\( (\forall c \in G//r.\ F\langle r\{e\},c\rangle = c \wedge F\langle c,r\{e\}\rangle = c) \) using Group_ZF_2_2_L1
with T2 show \( thesis \) using group0_1_L4
qed
The projected operation can be defined in terms of the group operation on representants in a natural way.
lemma (in group0) Group_ZF_2_2_L2:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,P) \) and A3: \( F = \text{ProjFun2}(G,r,P) \) and A4: \( a\in G \), \( b\in G \)
shows \( F\langle r\{a\},r\{b\}\rangle = r\{a\cdot b\} \)proof from A1, A2, A3, A4 show \( thesis \) using EquivClass_1_L10
qed
The class of the inverse is a right inverse of the class.
lemma (in group0) Group_ZF_2_2_L3:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,P) \) and A3: \( F = \text{ProjFun2}(G,r,P) \) and A4: \( a\in G \)
shows \( F\langle r\{a\},r\{a^{-1}\}\rangle = \text{ TheNeutralElement}(G//r,F) \)proof from A1, A2, A3, A4 have \( F\langle r\{a\},r\{a^{-1}\}\rangle = r\{1 \} \) using inverse_in_group, Group_ZF_2_2_L2, group0_2_L6
with groupAssum, A1, A2, A3 show \( thesis \) using IsAgroup_def, Group_ZF_2_2_L1
qed
The group structure can be projected to the quotient space.
theorem (in group0) Group_ZF_3_T2:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,P) \)
shows \( \text{IsAgroup}(G//r, \text{ProjFun2}(G,r,P)) \)proof let \( F = \text{ProjFun2}(G,r,P) \)
let \( E = \text{ TheNeutralElement}(G//r,F) \)
from groupAssum, A1, A2 have \( \text{IsAmonoid}(G//r,F) \) using IsAgroup_def, monoid0_def, Group_ZF_2_2_T1
moreover
qed
have \( \forall c\in G//r.\ \exists b\in G//r.\ F\langle c,b\rangle = E \)proof
ultimately show \( thesis \) using IsAgroup_def
fix \( c \)
assume A3: \( c \in G//r \)
then obtain \( g \) where D1: \( g\in G \), \( c = r\{g\} \) using quotient_def
let \( b = r\{g^{-1}\} \)
from D1 have \( b \in G//r \) using inverse_in_group, quotientI
moreover
qed
from A1, A2, D1 have \( F\langle c,b\rangle = E \) using Group_ZF_2_2_L3
ultimately show \( \exists b\in G//r.\ F\langle c,b\rangle = E \)
The group inverse (in the projected group) of a class is the class of the inverse.
lemma (in group0) Group_ZF_2_2_L4:
assumes A1: \( \text{equiv}(G,r) \) and A2: \( \text{Congruent2}(r,P) \) and A3: \( F = \text{ProjFun2}(G,r,P) \) and A4: \( a\in G \)
shows \( r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\}) \)proof from A1, A2, A3 have \( group0(G//r,F) \) using Group_ZF_3_T2, group0_def
moreover
qed
from A4 have \( r\{a\} \in G//r \), \( r\{a^{-1}\} \in G//r \) using inverse_in_group, quotientI
moreover from A1, A2, A3, A4 have \( F\langle r\{a\},r\{a^{-1}\}\rangle = \text{ TheNeutralElement}(G//r,F) \) using Group_ZF_2_2_L3
ultimately show \( thesis \) by (rule group0_2_L9 )
Normal subgroups and quotient groups
If \(H\) is a subgroup of \(G\), then for every \(a\in G\) we can cosider the sets \(\{a\cdot h. h \in H\}\) and \(\{ h\cdot a. h \in H\}\) (called a left and right ''coset of H'', resp.) These sets sometimes form a group, called the ''quotient group''. This section discusses the notion of quotient groups.
A normal subgorup \(N\) of a group \(G\) is such that \(aba^{-1}\) belongs to \(N\) if \(a\in G, b\in N\).
definition
\( \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) \)
Having a group and a normal subgroup \(N\) we can create another group consisting of eqivalence classes of the relation \(a\sim b \equiv a\cdot b^{-1} \in N\). We will refer to this relation as the quotient group relation. The classes of this relation are in fact cosets of subgroup \(H\).
definition
\( \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\} \)
Next we define the operation in the quotient group as the projection of the group operation on the classses of the quotient group relation.
definition
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
Definition of a normal subgroup in a more readable notation.
lemma (in group0) Group_ZF_2_4_L0:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( g\in G \), \( n\in H \)
shows \( g\cdot n\cdot g^{-1} \in H \) using assms, IsAnormalSubgroup_defThe quotient group relation is reflexive.
lemma (in group0) Group_ZF_2_4_L1:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{refl}(G, \text{QuotientGroupRel}(G,P,H)) \) using assms, group0_2_L6, group0_3_L5, QuotientGroupRel_def, refl_defThe quotient group relation is symmetric.
lemma (in group0) Group_ZF_2_4_L2:
assumes A1: \( \text{IsAsubgroup}(H,P) \)
shows \( sym( \text{QuotientGroupRel}(G,P,H)) \)proof{
}
fix \( a \) \( b \)
assume A2: \( \langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H) \)
with A1 have \( (a\cdot b^{-1})^{-1} \in H \) using QuotientGroupRel_def, group0_3_T3A
moreover
from A2 have \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \) using QuotientGroupRel_def, group0_2_L12
ultimately have \( b\cdot a^{-1} \in H \)
with A2 have \( \langle b,a\rangle \in \text{QuotientGroupRel}(G,P,H) \) using QuotientGroupRel_def
then show \( thesis \) using symI
qed
The quotient group relation is transistive.
lemma (in group0) Group_ZF_2_4_L3A:
assumes A1: \( \text{IsAsubgroup}(H,P) \) and A2: \( \langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H) \) and A3: \( \langle b,c\rangle \in \text{QuotientGroupRel}(G,P,H) \)
shows \( \langle a,c\rangle \in \text{QuotientGroupRel}(G,P,H) \)proof let \( r = \text{QuotientGroupRel}(G,P,H) \)
from A2, A3 have T1: \( a\in G \), \( b\in G \), \( c\in G \) using QuotientGroupRel_def
from A1, A2, A3 have \( (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \in H \) using QuotientGroupRel_def, group0_3_L6
moreover
qed
from T1 have \( a\cdot c^{-1} = (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \) using group0_2_L14A
ultimately have \( a\cdot c^{-1} \in H \)
with T1 show \( thesis \) using QuotientGroupRel_def
The quotient group relation is an equivalence relation. Note we do not need the subgroup to be normal for this to be true.
lemma (in group0) Group_ZF_2_4_L3:
assumes A1: \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \)proof let \( r = \text{QuotientGroupRel}(G,P,H) \)
from A1 have \( \forall a b c.\ (\langle a, b\rangle \in r \wedge \langle b, c\rangle \in r \longrightarrow \langle a, c\rangle \in r) \) using Group_ZF_2_4_L3A
then have \( \text{trans}(r) \) using Fol1_L2
with A1 show \( thesis \) using Group_ZF_2_4_L1, Group_ZF_2_4_L2, QuotientGroupRel_def, equiv_def
qed
The next lemma states the essential condition for congruency of the group operation with respect to the quotient group relation.
lemma (in group0) Group_ZF_2_4_L4:
assumes A1: \( \text{IsAnormalSubgroup}(G,P,H) \) and A2: \( \langle a1,a2\rangle \in \text{QuotientGroupRel}(G,P,H) \) and A3: \( \langle b1,b2\rangle \in \text{QuotientGroupRel}(G,P,H) \)
shows \( \langle a1\cdot b1, a2\cdot b2\rangle \in \text{QuotientGroupRel}(G,P,H) \)proof from A2, A3 have T1: \( a1\in G \), \( a2\in G \), \( b1\in G \), \( b2\in G \), \( a1\cdot b1 \in G \), \( a2\cdot b2 \in G \), \( b1\cdot b2^{-1} \in H \), \( a1\cdot a2^{-1} \in H \) using QuotientGroupRel_def, group0_2_L1, group0_1_L1
with A1 show \( thesis \) using IsAnormalSubgroup_def, group0_3_L6, group0_2_L15, QuotientGroupRel_def
qed
If the subgroup is normal, the group operation is congruent with respect to the quotient group relation.
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) \) using assms, group0_def, Group_ZF_2_4_L4, Congruent2_defThe quotient group is indeed a group.
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)) \) using assms, group0_def, Group_ZF_2_4_L3, IsAnormalSubgroup_def, Group_ZF_2_4_L5A, Group_ZF_3_T2, QuotientGroupOp_defThe class (coset) of the neutral element is the neutral element of the quotient group.
lemma Group_ZF_2_4_L5B:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( e = \text{ TheNeutralElement}(G,P) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) \) using assms, IsAnormalSubgroup_def, group0_def, IsAgroup_def, Group_ZF_2_4_L3, Group_ZF_2_4_L5A, QuotientGroupOp_def, Group_ZF_2_2_L1A group element is equivalent to the neutral element iff it is in the subgroup we divide the group by.
lemma (in group0) Group_ZF_2_4_L5C:
assumes \( a\in G \)
shows \( \langle a,1 \rangle \in \text{QuotientGroupRel}(G,P,H) \longleftrightarrow a\in H \) using assms, QuotientGroupRel_def, group_inv_of_one, group0_2_L2A group element is in \(H\) iff its class is the neutral element of \(G/H\).
lemma (in group0) Group_ZF_2_4_L5D:
assumes A1: \( \text{IsAnormalSubgroup}(G,P,H) \) and A2: \( a\in G \) and A3: \( r = \text{QuotientGroupRel}(G,P,H) \) and A4: \( \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) = e \)
shows \( r\{a\} = e \longleftrightarrow \langle a,1 \rangle \in r \)proof assume \( r\{a\} = e \)
with groupAssum, assms have \( r\{1 \} = r\{a\} \) and I: \( \text{equiv}(G,r) \) using Group_ZF_2_4_L5B, IsAnormalSubgroup_def, Group_ZF_2_4_L3
with A2 have \( \langle 1 ,a\rangle \in r \) using eq_equiv_class
with I show \( \langle a,1 \rangle \in r \) by (rule equiv_is_sym )
next
assume \( \langle a,1 \rangle \in r \)
moreover
qed
from A1, A3 have \( \text{equiv}(G,r) \) using IsAnormalSubgroup_def, Group_ZF_2_4_L3
ultimately have \( r\{a\} = r\{1 \} \) using equiv_class_eq
with groupAssum, A1, A3, A4 show \( r\{a\} = e \) using Group_ZF_2_4_L5B
The class of \(a\in G\) is the neutral element of the quotient \(G/H\) iff \(a\in H\).
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 \) using assms, Group_ZF_2_4_L5C, Group_ZF_2_4_L5DEssential condition to show that every subgroup of an abelian group is normal.
lemma (in group0) Group_ZF_2_4_L5:
assumes A1: \( P \text{ is commutative on } G \) and A2: \( \text{IsAsubgroup}(H,P) \) and A3: \( g\in G \), \( h\in H \)
shows \( g\cdot h\cdot g^{-1} \in H \)proof from A2, A3 have T1: \( h\in G \), \( g^{-1} \in G \) using group0_3_L2, inverse_in_group
with A3, A1 have \( g\cdot h\cdot g^{-1} = g^{-1}\cdot g\cdot h \) using group0_4_L4A
with A3, T1 show \( thesis \) using group0_2_L6, group0_2_L2
qed
Every subgroup of an abelian group is normal. Moreover, the quotient group is also abelian.
lemma Group_ZF_2_4_L6:
assumes A1: \( \text{IsAgroup}(G,P) \) and A2: \( P \text{ is commutative on } G \) and A3: \( \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)) \)proof from A1, A2, A3 show T1: \( \text{IsAnormalSubgroup}(G,P,H) \) using group0_def, IsAnormalSubgroup_def, Group_ZF_2_4_L5
let \( r = \text{QuotientGroupRel}(G,P,H) \)
from A1, A3, T1 have \( \text{equiv}(G,r) \), \( \text{Congruent2}(r,P) \) using group0_def, Group_ZF_2_4_L3, Group_ZF_2_4_L5A
with A2 show \( \text{QuotientGroupOp}(G,P,H) \text{ is commutative on } (G// \text{QuotientGroupRel}(G,P,H)) \) using EquivClass_2_T1, QuotientGroupOp_def
qed
The group inverse (in the quotient group) of a class (coset) is the class of the inverse.
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\}) \) using groupAssum, assms, IsAnormalSubgroup_def, Group_ZF_2_4_L3, Group_ZF_2_4_L5A, QuotientGroupOp_def, Group_ZF_2_2_L4Function spaces as monoids
On every space of functions \(\{f : X\rightarrow X\}\) we can define a natural monoid structure with composition as the operation. This section explores this fact.
The next lemma states that composition has a neutral element, namely the identity function on \(X\) (the one that maps \(x\in X\) into itself).
lemma Group_ZF_2_5_L1:
assumes A1: \( F = \text{Composition}(X) \)
shows \( \exists I\in (X\rightarrow X).\ \forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f \)proof let \( I = id(X) \)
from A1 have \( I \in X\rightarrow X \wedge (\forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f) \) using id_type, func_ZF_6_L1A
thus \( thesis \)
qed
The space of functions that map a set \(X\) into itsef is a monoid with composition as operation and the identity function as the neutral element.
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)) \)proof let \( I = id(X) \)
let \( F = \text{Composition}(X) \)
show \( \text{IsAmonoid}(X\rightarrow X, \text{Composition}(X)) \) using func_ZF_5_L5, Group_ZF_2_5_L1, IsAmonoid_def
then have \( monoid0(X\rightarrow X,F) \) using monoid0_def
moreover
qed
have \( I \in X\rightarrow X \wedge (\forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f) \) using id_type, func_ZF_6_L1A
ultimately show \( I = \text{ TheNeutralElement}(X\rightarrow X,F) \) using group0_1_L4
end
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 ))) \)
theorem func_ZF_1_L3:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \)
shows \( F : (X\rightarrow \text{range}(f))\times (X\rightarrow \text{range}(f))\rightarrow (X\rightarrow \text{range}(f)) \) lemma (in monoid0) group0_1_L3B: shows \( \text{range}(f) = G \)
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 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 func1_3_L1:
assumes \( c\in Y \)
shows \( \text{ConstantFunction}(X,c) : X\rightarrow Y \) 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 \) theorem func_ZF_1_L4:
assumes \( f : Y\times Y\rightarrow Y \) and \( F = f \text{ lifted to function space over } X \) and \( s:X\rightarrow \text{range}(f) \), \( r:X\rightarrow \text{range}(f) \) and \( x\in X \)
shows \( (F\langle s,r\rangle )(x) = f\langle s(x),r(x)\rangle \) lemma func1_3_L2:
assumes \( x\in X \)
shows \( \text{ConstantFunction}(X,c)(x) = c \) lemma func_ZF_2_L4:
assumes \( f \text{ is associative on } G \) and \( F = f \text{ lifted to function space over } X \)
shows \( F \text{ is associative on } (X\rightarrow \text{range}(f)) \) lemma (in monoid0) Group_ZF_2_1_L1:
assumes \( F = f \text{ lifted to function space over } X \) and \( E = \text{ConstantFunction}(X,\text{ TheNeutralElement}(G,f)) \)
shows \( E : X\rightarrow G \wedge (\forall s\in X\rightarrow G.\ F\langle E,s\rangle = s \wedge F\langle s,E\rangle = s) \) lemma (in monoid0) Group_ZF_2_1_T1:
assumes \( F = f \text{ lifted to function space over } X \)
shows \( \text{IsAmonoid}(X\rightarrow G,F) \) lemma (in monoid0) group0_1_L4:
assumes \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)
shows \( e = \text{ TheNeutralElement}(G,f) \) lemma (in group0) group0_2_L1: shows \( monoid0(G,P) \)
lemma (in monoid0) lifted_val:
assumes \( F = f \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) \oplus r(x) \) lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
theorem group0_2_T2:
assumes \( \text{IsAgroup}(G,f) \)
shows \( \text{GroupInv}(G,f) : G\rightarrow G \) lemma (in group0) Group_ZF_2_1_L4:
assumes \( F = P \text{ lifted to function space over } X \)
shows \( monoid0(X\rightarrow G,F) \) lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) 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 (in group0) group0_2_L6:
assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)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))) \)
lemma Group_ZF_2_1_L2:
assumes \( \text{IsAmonoid}(G,f) \) and \( F = f \text{ lifted to function space over } X \) and \( E = \text{ConstantFunction}(X,\text{ TheNeutralElement}(G,f)) \)
shows \( E = \text{ TheNeutralElement}(X\rightarrow G,F) \) lemma (in group0) Group_ZF_2_1_L5:
assumes \( F = P \text{ lifted to function space over } X \) and \( s : X\rightarrow G \) and \( i = \text{GroupInv}(G,P)\circ s \)
shows \( i: X\rightarrow G \) and \( F\langle s,i\rangle = \text{ TheNeutralElement}(X\rightarrow G,F) \) 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 group0) group0_2_L9A:
assumes \( \forall g\in G.\ b(g) \in G \wedge g\cdot b(g) = 1 \)
shows \( \forall g\in G.\ b(g) = g^{-1} \) 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 \) theorem (in group0) group0_3_T1:
assumes \( \text{IsAsubgroup}(H,P) \) and \( g = \text{restrict}(P,H\times H) \)
shows \( \text{GroupInv}(H,g) = \text{restrict}( \text{GroupInv}(G,P),H) \) lemma (in group0) group0_3_L2:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( H \subseteq G \) lemma (in group0) group0_valid_fun_space: shows \( group0(X\rightarrow G,P \text{ lifted to function space over } X) \)
lemma (in group0) group0_3_L4:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{ TheNeutralElement}(H,\text{restrict}(P,H\times H)) = 1 \) lemma (in group0) group_oper_fun: shows \( P : G\times G\rightarrow G \)
lemma func_ZF_2_L2:
assumes \( f : G\times G\rightarrow G \) and \( f \text{ is commutative on } G \) and \( F = f \text{ lifted to function space over } X \)
shows \( F \text{ is commutative on } (X\rightarrow \text{range}(f)) \) 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 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) \) theorem EquivClass_2_T2:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( f \text{ is associative on } A \)
shows \( \text{ProjFun2}(A,r,f) \text{ is associative on } A//r \) 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 (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) lemma (in group0) Group_ZF_2_2_L2:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,P) \) and \( F = \text{ProjFun2}(G,r,P) \) and \( a\in G \), \( b\in G \)
shows \( F\langle r\{a\},r\{b\}\rangle = r\{a\cdot b\} \) lemma (in group0) Group_ZF_2_2_L3:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,P) \) and \( F = \text{ProjFun2}(G,r,P) \) and \( a\in G \)
shows \( F\langle r\{a\},r\{a^{-1}\}\rangle = \text{ TheNeutralElement}(G//r,F) \) theorem (in group0) Group_ZF_3_T2:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,P) \)
shows \( \text{IsAgroup}(G//r, \text{ProjFun2}(G,r,P)) \) lemma (in group0) group0_2_L9:
assumes \( a\in G \) and \( b\in G \) and \( a\cdot b = 1 \)
shows \( a = b^{-1} \) and \( b = a^{-1} \)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) \)
lemma (in group0) group0_3_L5:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( 1 \in H \)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\} \)
theorem (in group0) group0_3_T3A:
assumes \( \text{IsAsubgroup}(H,P) \) and \( h\in H \)
shows \( h^{-1}\in H \) lemma (in group0) group0_2_L12:
assumes \( a\in G \), \( b\in G \)
shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \) lemma (in group0) group0_3_L6:
assumes \( \text{IsAsubgroup}(H,P) \) and \( a\in H \), \( b\in H \)
shows \( a\cdot b \in H \) lemma (in group0) group0_2_L14A:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( a\cdot c^{-1}= (a\cdot b^{-1})\cdot (b\cdot c^{-1}) \), \( a^{-1}\cdot c = (a^{-1}\cdot b)\cdot (b^{-1}\cdot c) \), \( a\cdot (b\cdot c)^{-1} = a\cdot c^{-1}\cdot b^{-1} \), \( a\cdot (b\cdot c^{-1}) = a\cdot b\cdot c^{-1} \), \( (a\cdot b^{-1}\cdot c^{-1})^{-1} = c\cdot b\cdot a^{-1} \), \( a\cdot b\cdot c^{-1}\cdot (c\cdot b^{-1}) = a \), \( a\cdot (b\cdot c)\cdot c^{-1} = a\cdot b \) lemma (in group0) Group_ZF_2_4_L3A:
assumes \( \text{IsAsubgroup}(H,P) \) and \( \langle a,b\rangle \in \text{QuotientGroupRel}(G,P,H) \) and \( \langle b,c\rangle \in \text{QuotientGroupRel}(G,P,H) \)
shows \( \langle a,c\rangle \in \text{QuotientGroupRel}(G,P,H) \) lemma Fol1_L2:
assumes \( \forall x y z.\ \langle x, y\rangle \in r \wedge \langle y, z\rangle \in r \longrightarrow \langle x, z\rangle \in r \)
shows \( \text{trans}(r) \) lemma (in group0) Group_ZF_2_4_L1:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{refl}(G, \text{QuotientGroupRel}(G,P,H)) \) lemma (in group0) Group_ZF_2_4_L2:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( sym( \text{QuotientGroupRel}(G,P,H)) \) lemma (in group0) group0_2_L15:
assumes \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)
shows \( (a\cdot b)\cdot (c\cdot d)^{-1} = a\cdot (b\cdot d^{-1})\cdot a^{-1}\cdot (a\cdot c^{-1}) \) lemma (in group0) Group_ZF_2_4_L4:
assumes \( \text{IsAnormalSubgroup}(G,P,H) \) and \( \langle a1,a2\rangle \in \text{QuotientGroupRel}(G,P,H) \) and \( \langle b1,b2\rangle \in \text{QuotientGroupRel}(G,P,H) \)
shows \( \langle a1\cdot b1, a2\cdot b2\rangle \in \text{QuotientGroupRel}(G,P,H) \)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) Group_ZF_2_4_L3:
assumes \( \text{IsAsubgroup}(H,P) \)
shows \( \text{equiv}(G, \text{QuotientGroupRel}(G,P,H)) \) 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) \)Definition of QuotientGroupOp:
\( \text{QuotientGroupOp}(G,P,H) \equiv \text{ProjFun2}(G, \text{QuotientGroupRel}(G,P,H ),P) \)
lemma (in group0) group_inv_of_one: shows \( 1 ^{-1} = 1 \)
lemma Group_ZF_2_4_L5B:
assumes \( \text{IsAgroup}(G,P) \) and \( \text{IsAnormalSubgroup}(G,P,H) \) and \( r = \text{QuotientGroupRel}(G,P,H) \) and \( e = \text{ TheNeutralElement}(G,P) \)
shows \( r\{e\} = \text{ TheNeutralElement}(G//r, \text{QuotientGroupOp}(G,P,H)) \) lemma equiv_is_sym:
assumes \( \text{equiv}(X,r) \) and \( \langle x,y\rangle \in r \)
shows \( \langle y,x\rangle \in r \) lemma (in group0) Group_ZF_2_4_L5C:
assumes \( a\in G \)
shows \( \langle a,1 \rangle \in \text{QuotientGroupRel}(G,P,H) \longleftrightarrow a\in H \) lemma (in group0) Group_ZF_2_4_L5D:
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 \langle a,1 \rangle \in r \) 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 (in group0) Group_ZF_2_4_L5:
assumes \( P \text{ is commutative on } G \) and \( \text{IsAsubgroup}(H,P) \) and \( g\in G \), \( h\in H \)
shows \( g\cdot h\cdot g^{-1} \in H \) theorem EquivClass_2_T1:
assumes \( \text{equiv}(A,r) \) and \( \text{Congruent2}(r,f) \) and \( f \text{ is commutative on } A \)
shows \( \text{ProjFun2}(A,r,f) \text{ is commutative on } A//r \) lemma (in group0) Group_ZF_2_2_L4:
assumes \( \text{equiv}(G,r) \) and \( \text{Congruent2}(r,P) \) and \( F = \text{ProjFun2}(G,r,P) \) and \( a\in G \)
shows \( r\{a^{-1}\} = \text{GroupInv}(G//r,F)(r\{a\}) \) lemma func_ZF_6_L1A:
assumes \( f : X\rightarrow X \)
shows \( \text{Composition}(X)\langle f,id(X)\rangle = f \), \( \text{Composition}(X)\langle id(X),f\rangle = f \) lemma func_ZF_5_L5: shows \( \text{Composition}(X) \text{ is associative on } (X\rightarrow X) \)
lemma Group_ZF_2_5_L1:
assumes \( F = \text{Composition}(X) \)
shows \( \exists I\in (X\rightarrow X).\ \forall f\in (X\rightarrow X).\ F\langle I,f\rangle = f \wedge F\langle f,I\rangle = f \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8