theory Group_ZF_1b imports Group_ZF
begin
In a typical textbook a group is defined as a set \(G\) with an associative operation such that two conditions hold:
A: there is an element \(e\in G\) such that for all \(g\in G\) we have \(e\cdot g = g\) and \(g\cdot e =g\). We call this element a "unit" or a "neutral element" of the group. B: for every \(a\in G\) there exists a \(b\in G\) such that \(a\cdot b = e\), where \(e\) is the element of \(G\) whose existence is guaranteed by A.
The validity of this definition is rather dubious to me, as condition A does not define any specific element \(e\) that can be referred to in condition B - it merely states that a set of such units \(e\) is not empty. Of course it does work in the end as we can prove that the set of such neutral elements has exactly one element, but still the definition by itself is not valid. You just can't reference a variable bound by a quantifier outside of the scope of that quantifier. One way around this is to first use condition A to define the notion of a monoid, then prove the uniqueness of \(e\) and then use the condition B to define groups.
Another way is to write conditions A and B together as follows: \(\exists_{e \in G} \ (\forall_{g \in G} \ e\cdot g = g \wedge g\cdot e = g) \wedge (\forall_{a\in G}\exists_{b\in G}\ a\cdot b = e).\)
This is rather ugly.
What I want to talk about is an amusing way to define groups directly without any reference to the neutral elements. Namely, we can define a group as a non-empty set \(G\) with an associative operation "\(\cdot \)" such that C: for every \(a,b\in G\) the equations \(a\cdot x = b\) and \(y\cdot a = b\) can be solved in \(G\). This theory file aims at proving the equivalence of this alternative definition with the usual definition of the group, as formulated in Group_ZF.thy. The informal proofs come from an Aug. 14, 2005 post by buli on the matematyka.org forum.
An alternative definition of group
First we will define notation for writing about groups.
We will use the multiplicative notation for the group operation. To do this, we define a context (locale) that tells Isabelle to interpret \(a\cdot b\) as the value of function \(P\) on the pair \(\langle a,b \rangle\).
locale group2
defines \( a \cdot b \equiv P\langle a,b\rangle \)
The next theorem states that a set \(G\) with an associative operation that satisfies condition C is a group, as defined in IsarMathLib Group_ZF theory.
theorem (in group2) altgroup_is_group:
assumes A1: \( G\neq 0 \) and A2: \( P \text{ is associative on } G \) and A3: \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \) and A4: \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)
shows \( \text{IsAgroup}(G,P) \)proof from A1 obtain \( a \) where \( a\in G \)
with A3 obtain \( x \) where \( x\in G \) and \( a\cdot x = a \)
from A4, \( a\in G \) obtain \( y \) where \( y\in G \) and \( y\cdot a = a \)
have I: \( \forall b\in G.\ b = b\cdot x \wedge b = y\cdot b \)proof
fix \( b \)
assume \( b\in G \)
with A4, \( a\in G \) obtain \( y_b \) where \( y_b\in G \) and \( y_b\cdot a = b \)
from A3, \( a\in G \), \( b\in G \) obtain \( x_b \) where \( x_b\in G \) and \( a\cdot x_b = b \)
from \( a\cdot x = a \), \( y\cdot a = a \), \( y_b\cdot a = b \), \( a\cdot x_b = b \) have \( b = y_b\cdot (a\cdot x) \) and \( b = (y\cdot a)\cdot x_b \)
moreover
qed
from A2, \( a\in G \), \( x\in G \), \( y\in G \), \( x_b\in G \), \( y_b\in G \) have \( (y\cdot a)\cdot x_b = y\cdot (a\cdot x_b) \), \( y_b\cdot (a\cdot x) = (y_b\cdot a)\cdot x \) using IsAssociative_def
moreover from \( y_b\cdot a = b \), \( a\cdot x_b = b \) have \( (y_b\cdot a)\cdot x = b\cdot x \), \( y\cdot (a\cdot x_b) = y\cdot b \)
ultimately show \( b = b\cdot x \wedge b = y\cdot b \)
moreover
qed
have \( x = y \)proof
ultimately have \( \forall b\in G.\ b\cdot x = b \wedge x\cdot b = b \)
from \( x\in G \), I have \( x = y\cdot x \)
also
qed
from \( y\in G \), I have \( y\cdot x = y \)
finally show \( x = y \)
with A2, \( x\in G \) have \( \text{IsAmonoid}(G,P) \) using IsAmonoid_def
with A3 show \( \text{IsAgroup}(G,P) \) using monoid0_def, unit_is_neutral, IsAgroup_def
The converse of altgroup_is_group: in every (classically defined) group condition C holds. In informal mathematics we can say "Obviously condition C holds in any group." In formalized mathematics the word "obviously" is not in the language. The next theorem is proven in the context called group0 defined in the theory Group_ZF.thy. Similarly to the group2 that context defines \(a\cdot b\) as \(P\langle a,b\rangle\) It also defines notation related to the group inverse and adds an assumption that the pair \((G,P)\) is a group to all its theorems. This is why in the next theorem we don't explicitely assume that \((G,P)\) is a group - this assumption is implicit in the context.
theorem (in group0) group_is_altgroup:
shows \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \) and \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)proof{
}
fix \( a \) \( b \)
assume \( a\in G \), \( b\in G \)
let \( x = a^{-1}\cdot b \)
let \( y = b\cdot a^{-1} \)
from \( a\in G \), \( b\in G \) have \( x \in G \), \( y \in G \) and \( a\cdot x = b \), \( y\cdot a = b \) using inverse_in_group, group_op_closed, inv_cancel_two
hence \( \exists x\in G.\ a\cdot x = b \) and \( \exists y\in G.\ y\cdot a = b \)
thus \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \) and \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)
qed
An associative quasigroup is a group. This is a bit weaker than altgroup_is_group as the definition of quasigroup requires uniqueness of solutions of \(a\cdot x = b\) and \(y\cdot a = b\) equations.
lemma assoc_quasigroup_group:
assumes \( \text{IsAquasigroup}(G,P) \) and \( P \text{ is associative on } G \), \( G\neq \emptyset \)
shows \( \text{IsAgroup}(G,P) \)proof from assms(1) have \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ P\langle a,y\rangle = b \) and \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ P\langle x,a\rangle = b \) unfolding IsAquasigroup_def, HasLatinSquareProp_def, HasLeftDiv_def, HasRightDiv_def using ZF1_1_L9(4)
with assms(2,3) show \( thesis \) using altgroup_is_group
qed
end
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 ))) \)
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)))) \)
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) \)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 (in group0) inverse_in_group:
assumes \( x\in G \)
shows \( x^{-1}\in G \) lemma (in group0) group_op_closed:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \) lemma (in group0) inv_cancel_two:
assumes \( a\in G \), \( b\in G \)
shows \( a\cdot b^{-1}\cdot b = a \), \( a\cdot b\cdot b^{-1} = a \), \( a^{-1}\cdot (a\cdot b) = b \), \( a\cdot (a^{-1}\cdot b) = b \)Definition of IsAquasigroup:
\( \text{IsAquasigroup}(G,A) \equiv A:G\times G\rightarrow G \wedge A \text{ has Latin square property on } G \)
Definition of HasLatinSquareProp:
\( A \text{ has Latin square property on } G \equiv Has\text{ LeftDiv}(G,A) \wedge Has\text{ RightDiv}(G,A) \)
Definition of HasLeftDiv:
\( Has\text{ LeftDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle a,x\rangle = b) \)
Definition of HasRightDiv:
\( Has\text{ RightDiv}(G,A) \equiv \forall a\in G.\ \forall b\in G.\ \exists !x.\ (x\in G \wedge A\langle x,a\rangle = b) \)
lemma ZF1_1_L9:
assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)
shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \), \( \exists x\in A.\ \phi (x) \) theorem (in group2) altgroup_is_group:
assumes \( G\neq 0 \) and \( P \text{ is associative on } G \) and \( \forall a\in G.\ \forall b\in G.\ \exists x\in G.\ a\cdot x = b \) and \( \forall a\in G.\ \forall b\in G.\ \exists y\in G.\ y\cdot a = b \)
shows \( \text{IsAgroup}(G,P) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8