:: Lattice of Subgroups of a Group. Frattini Subgroup
:: by Wojciech A. Trybulec
::
:: Received August 22, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FINSEQ_1, ARYTM_1, GROUP_1, STRUCT_0, GROUP_2,
SETFAM_1, SUBSET_1, RELAT_1, INT_1, TARSKI, GROUP_3, QC_LANG1, NEWTON,
ARYTM_3, CARD_1, XXREAL_0, COMPLEX1, ALGSTR_0, CARD_3, FINSOP_1, BINOP_1,
ORDINAL4, SETWISEO, FINSEQ_2, NAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
ZFMISC_1, RLSUB_1, BVFUNC_2, EQREL_1, PRE_TOPC, RLSUB_2, LATTICES,
GROUP_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, FINSOP_1, ORDINAL1,
NUMBERS, INT_1, SETWISEO, SETFAM_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, BINOP_1, STRUCT_0, ALGSTR_0, GROUP_2,
GROUP_3, LATTICES, GROUP_1, DOMAIN_1, XXREAL_0, NAT_1, INT_2;
constructors PARTFUN1, SETFAM_1, BINOP_1, SETWISEO, XXREAL_0, NAT_1, NAT_D,
FINSEQ_3, FINSEQ_4, FINSOP_1, REALSET1, REAL_1, LATTICES, GROUP_3,
RELSET_1, FINSEQ_2, BINOP_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, NUMBERS, XREAL_0, INT_1,
FINSEQ_1, STRUCT_0, LATTICES, GROUP_1, GROUP_2, GROUP_3, ORDINAL1,
CARD_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
definition
let D be non empty set;
let F be FinSequence of D;
let X be set;
redefine func F - X -> FinSequence of D;
end;
scheme :: GROUP_4:sch 1
MeetSbgEx{G() -> Group, P[set]}: ex H being strict Subgroup of G() st the
carrier of H = meet{A where A is Subset of G() : ex K being strict Subgroup of
G() st A = the carrier of K & P[K]}
provided
ex H being strict Subgroup of G() st P[H];
reserve x,y,X,Y for set,
k,l,n for Nat,
i,i1,i2,i3,j for Integer,
G for Group,
a,b,c,d for Element of G,
A,B,C for Subset of G,
H,H1,H2, H3 for Subgroup of G,
h for Element of H,
F,F1,F2 for FinSequence of the carrier of G,
I,I1,I2 for FinSequence of INT;
scheme :: GROUP_4:sch 2
SubgrSep{G() -> Group,P[set]}:
ex X st X c= Subgroups G() & for H being
strict Subgroup of G() holds H in X iff P[H];
definition
let i;
func @i -> Element of INT equals
:: GROUP_4:def 1
i;
end;
theorem :: GROUP_4:1
a = h implies a |^ n = h |^ n;
theorem :: GROUP_4:2
a = h implies a |^ i = h |^ i;
theorem :: GROUP_4:3
a in H implies a |^ n in H;
theorem :: GROUP_4:4
a in H implies a |^ i in H;
definition
let G be non empty multMagma;
let F be FinSequence of the carrier of G;
func Product F -> Element of G equals
:: GROUP_4:def 2
(the multF of G) "**" F;
end;
theorem :: GROUP_4:5
for G being associative unital non empty multMagma,
F1,F2 being FinSequence of the carrier of G holds
Product(F1 ^ F2) = Product(F1) * Product(F2);
theorem :: GROUP_4:6
for G being unital non empty multMagma, F being FinSequence of the
carrier of G, a being Element of G holds Product(F ^ <* a *>) = Product(F) * a;
theorem :: GROUP_4:7
for G being associative unital non empty multMagma, F being
FinSequence of the carrier of G, a being Element of G holds Product(<* a *> ^ F
) = a * Product(F);
theorem :: GROUP_4:8
for G being unital non empty multMagma holds Product <*> the
carrier of G = 1_G;
theorem :: GROUP_4:9
for G being non empty multMagma, a being Element of G holds Product<*
a *> = a;
theorem :: GROUP_4:10
for G being non empty multMagma, a,b being Element of G holds Product
<* a,b *> = a * b;
theorem :: GROUP_4:11
Product<* a,b,c *> = a * b * c & Product<* a,b,c *> = a * (b * c);
theorem :: GROUP_4:12
Product(n |-> a) = a |^ n;
theorem :: GROUP_4:13
Product(F - {1_G}) = Product(F);
theorem :: GROUP_4:14
len F1 = len F2 & (for k st k in dom F1 holds F2.(len F1 - k + 1
) = (F1/.k)") implies Product(F1) = Product(F2)";
theorem :: GROUP_4:15
G is commutative Group implies for P being Permutation of dom F1 st F2
= F1 * P holds Product(F1) = Product(F2);
theorem :: GROUP_4:16
G is commutative Group & F1 is one-to-one & F2 is one-to-one & rng F1
= rng F2 implies Product(F1) = Product(F2);
theorem :: GROUP_4:17
G is commutative Group & len F = len F1 & len F = len F2 & (for k st k
in dom F holds F.k = (F1/.k) * (F2/.k)) implies Product(F) = Product(F1) *
Product(F2);
theorem :: GROUP_4:18
rng F c= carr H implies Product(F) in H;
definition
let G,I,F;
func F |^ I -> FinSequence of the carrier of G means
:: GROUP_4:def 3
len it = len F & for k st k in dom F holds it.k = (F/.k) |^ @(I/.k);
end;
theorem :: GROUP_4:19
len F1 = len I1 & len F2 = len I2 implies (F1 ^ F2) |^ (I1 ^ I2)
= (F1 |^ I1) ^ (F2 |^ I2);
theorem :: GROUP_4:20
rng F c= carr H implies Product(F |^ I) in H;
theorem :: GROUP_4:21
(<*> the carrier of G) |^ (<*> INT) = {};
theorem :: GROUP_4:22
<* a *> |^ <* @i *> = <* a |^ i *>;
theorem :: GROUP_4:23
<* a,b *> |^ <* @i,@j *> = <* a |^ i,b |^ j *>;
theorem :: GROUP_4:24
<* a,b,c *> |^ <* @i1,@i2,@i3 *> = <* a |^ i1,b |^ i2,c |^ i3 *>;
theorem :: GROUP_4:25
F |^ (len F |-> @(1)) = F;
theorem :: GROUP_4:26
F |^ (len F |-> @(0)) = len F |-> 1_G;
theorem :: GROUP_4:27
len I = n implies (n |-> 1_G) |^ I = n |-> 1_G;
definition
let G,A;
func gr A -> strict Subgroup of G means
:: GROUP_4:def 4
A c= the carrier of it & for
H being strict Subgroup of G st A c= the carrier of H holds it is Subgroup of H
;
end;
theorem :: GROUP_4:28
a in gr A iff ex F,I st len F = len I & rng F c= A & Product(F |^ I) = a;
theorem :: GROUP_4:29
a in A implies a in gr A;
theorem :: GROUP_4:30
gr {} the carrier of G = (1).G;
theorem :: GROUP_4:31
for H being strict Subgroup of G holds gr carr H = H;
theorem :: GROUP_4:32
A c= B implies gr A is Subgroup of gr B;
theorem :: GROUP_4:33
gr(A /\ B) is Subgroup of gr A /\ gr B;
theorem :: GROUP_4:34
the carrier of gr A = meet{B : ex H being strict Subgroup of G
st B = the carrier of H & A c= carr H};
theorem :: GROUP_4:35
gr A = gr(A \ {1_G});
definition
let G,a;
attr a is generating means
:: GROUP_4:def 5
not for A st gr A = the multMagma of G
holds gr(A \ {a}) = the multMagma of G;
end;
theorem :: GROUP_4:36
1_G is non generating;
definition
let G, H;
attr H is maximal means
:: GROUP_4:def 6
the multMagma of H <> the multMagma of G &
for K being strict Subgroup of G st the multMagma of H <> K & H is Subgroup of
K holds K = the multMagma of G;
end;
theorem :: GROUP_4:37
for G being strict Group, H being strict Subgroup of G, a being
Element of G holds H is maximal & not a in H implies gr(carr H \/ {a}) = G;
::
:: Frattini subgroup.
::
definition
let G be Group;
::$N Frattini subgroup
func Phi(G) -> strict Subgroup of G means
:: GROUP_4:def 7
the carrier of it = meet{A
where A is Subset of G : ex H being strict Subgroup of G st A = the carrier of
H & H is maximal} if ex H being strict Subgroup of G st H is maximal otherwise
it = the multMagma of G;
end;
theorem :: GROUP_4:38
for G being Group holds (ex H being strict Subgroup of G st H is
maximal) implies (a in Phi(G) iff for H being strict Subgroup of G st H is
maximal holds a in H);
theorem :: GROUP_4:39
for G being Group, a being Element of G holds (for H being strict
Subgroup of G holds H is not maximal) implies a in Phi(G);
theorem :: GROUP_4:40
for G being Group, H being strict Subgroup of G holds H is
maximal implies Phi(G) is Subgroup of H;
theorem :: GROUP_4:41
for G being strict Group holds the carrier of Phi(G) = {a where
a is Element of G: a is non generating};
theorem :: GROUP_4:42
for G being strict Group, a being Element of G holds a in Phi(G) iff a
is non generating;
definition
let G,H1,H2;
func H1 * H2 -> Subset of G equals
:: GROUP_4:def 8
carr H1 * carr H2;
end;
theorem :: GROUP_4:43
H1 * H2 = carr H1 * carr H2 & H1 * H2 = H1 * carr H2 & H1 * H2 = carr
H1 * H2;
theorem :: GROUP_4:44
H1 * H2 * H3 = H1 * (H2 * H3);
theorem :: GROUP_4:45
a * H1 * H2 = a * (H1 * H2);
theorem :: GROUP_4:46
H1 * H2 * a = H1 * (H2 * a);
theorem :: GROUP_4:47
A * H1 * H2 = A * (H1 * H2);
theorem :: GROUP_4:48
H1 * H2 * A = H1 * (H2 * A);
definition
let G,H1,H2;
func H1 "\/" H2 -> strict Subgroup of G equals
:: GROUP_4:def 9
gr(carr H1 \/ carr H2);
end;
theorem :: GROUP_4:49
a in H1 "\/" H2 iff ex F,I st len F = len I & rng F c= carr H1 \/ carr
H2 & a = Product(F |^ I);
theorem :: GROUP_4:50
H1 "\/" H2 = gr(H1 * H2);
theorem :: GROUP_4:51
H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2;
theorem :: GROUP_4:52
G is commutative Group implies the carrier of H1 "\/" H2 = H1 * H2;
theorem :: GROUP_4:53
for N1,N2 being strict normal Subgroup of G holds the carrier of
N1 "\/" N2 = N1 * N2;
theorem :: GROUP_4:54
for N1,N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal
Subgroup of G;
theorem :: GROUP_4:55
for H being strict Subgroup of G holds H "\/" H = H;
theorem :: GROUP_4:56
H1 "\/" H2 = H2 "\/" H1;
theorem :: GROUP_4:57
H1 "\/" H2 "\/" H3 = H1 "\/" (H2 "\/" H3);
theorem :: GROUP_4:58
for H being strict Subgroup of G holds (1).G "\/" H = H & H "\/" (1).G = H;
theorem :: GROUP_4:59
(Omega).G "\/" H = (Omega).G & H "\/" (Omega).G = (Omega).G;
theorem :: GROUP_4:60
H1 is Subgroup of H1 "\/" H2 & H2 is Subgroup of H1 "\/" H2;
theorem :: GROUP_4:61
for H2 being strict Subgroup of G holds H1 is Subgroup of H2 iff
H1 "\/" H2 = H2;
theorem :: GROUP_4:62
H1 is Subgroup of H2 implies H1 is Subgroup of H2 "\/" H3;
theorem :: GROUP_4:63
for H3 being strict Subgroup of G holds H1 is Subgroup of H3 & H2 is
Subgroup of H3 implies H1 "\/" H2 is Subgroup of H3;
theorem :: GROUP_4:64
for H3,H2 being strict Subgroup of G holds H1 is Subgroup of H2
implies H1 "\/" H3 is Subgroup of H2 "\/" H3;
theorem :: GROUP_4:65
H1 /\ H2 is Subgroup of H1 "\/" H2;
theorem :: GROUP_4:66
for H2 being strict Subgroup of G holds (H1 /\ H2) "\/" H2 = H2;
theorem :: GROUP_4:67
for H1 being strict Subgroup of G holds H1 /\ (H1 "\/" H2) = H1;
theorem :: GROUP_4:68
for H1,H2 being strict Subgroup of G holds H1 "\/" H2 = H2 iff H1 /\ H2 = H1;
reserve S1,S2 for Element of Subgroups G;
definition
let G;
func SubJoin G -> BinOp of Subgroups G means
:: GROUP_4:def 10
for H1,H2 being strict Subgroup of G holds it.(H1,H2) = H1 "\/" H2;
end;
definition
let G;
func SubMeet G -> BinOp of Subgroups G means
:: GROUP_4:def 11
for H1,H2 being strict Subgroup of G holds it.(H1,H2) = H1 /\ H2;
end;
definition
let G be Group;
func lattice G -> strict Lattice equals
:: GROUP_4:def 12
LattStr (# Subgroups G, SubJoin G,
SubMeet G #);
end;
theorem :: GROUP_4:69
the carrier of lattice G = Subgroups G;
theorem :: GROUP_4:70
the L_join of lattice G = SubJoin G;
theorem :: GROUP_4:71
the L_meet of lattice G = SubMeet G;
registration
let G be Group;
cluster lattice G -> lower-bounded upper-bounded;
end;
theorem :: GROUP_4:72
Bottom lattice G = (1).G;
theorem :: GROUP_4:73
Top lattice G = (Omega).G;