:: Characteristic Subgroups
:: by Alexander M. Nelson
::
:: Received July 23, 2022
:: Copyright (c) 2022-2026 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 MOD_4, GROUP_22, CARD_3, QC_LANG1, RLSUB_1, RELAT_1, TARSKI,
FUNCT_1, ZFMISC_1, XXREAL_1, FINSEQ_1, FINSET_1, NUMBERS, WELLORD1,
SUBSET_1, XBOOLE_0, PARTFUN1, FUNCT_2, CARD_1, ARYTM_3, CQC_SIM1,
ORDINAL1, EQREL_1, STRUCT_0, GROUP_1, GROUP_2, GROUP_3, GROUP_4, GROUP_5,
GROUP_6, BINOP_1, BINOP_2, ALGSTR_0, REALSET1, AUTGROUP, GR_CY_1,
NATTRA_1, NAT_1, INT_2, SETFAM_1, NEWTON, PRE_TOPC, GROUP_10, WEDDWITT;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, FUNCT_1, RELSET_1,
FUNCT_2, PARTFUN1, INT_1, INT_2, SETFAM_1, NUMBERS, BINOP_2, FINSET_1,
STRUCT_0, ALGSTR_0, FINSEQ_1, GROUP_1, GROUP_2, GROUP_3, GROUP_4,
GROUP_5, REALSET1, NAT_D, GRSOLV_1, AUTGROUP, GROUP_10, GR_CY_1, NEWTON,
GROUP_6;
constructors RELSET_1, FINSOP_1, NAT_D, BINOP_2, REALSET1, MONOID_0, GROUP_4,
GROUP_5, GRSOLV_1, AUTGROUP, GROUP_10, NEWTON;
registrations XBOOLE_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, ORDINAL1,
FINSET_1, NUMBERS, NAT_1, INT_1, INT_2, XREAL_0, CARD_1, STRUCT_0,
GROUP_1, GROUP_2, GROUP_3, GROUP_6, GR_CY_1, FOMODEL0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM;
definitions FUNCT_2, FINSEQ_1, INT_1;
equalities REALSET1, GROUP_2, GROUP_3, GROUP_4, GROUP_5, GROUP_6, GR_CY_1,
ALGSTR_0;
expansions TARSKI, GROUP_2, GROUP_6, STRUCT_0, FUNCT_2;
theorems TARSKI, RELSET_1, FUNCT_1, FUNCT_2, XBOOLE_0, INT_2, SETFAM_1, INT_4,
FINSEQ_3, PARTFUN1, ORDINAL1, ZFMISC_1, NAT_D, INT_1, GROUP_1, GROUP_2,
GROUP_3, GROUP_4, GROUP_5, GROUP_6, STRUCT_0, GRSOLV_1, AUTGROUP,
GROUP_9, GROUP_10, GR_CY_1, XCMPLX_1;
schemes FUNCT_2, GROUP_4, FINSEQ_1;
begin :: Preparatory Work
reserve X for set;
theorem Th67a:
for a,b,c being Nat st c <> 0 & c*a divides c*b holds a divides b by INT_4:7;
theorem Th68:
for a,b,c being Nat
st b<>0 & b divides c & a*b,c are_coprime
holds b=1
proof
let a,b,c be Nat;
assume b<>0;
assume A1: b divides c;
assume A2: a*b,c are_coprime;
b divides a*b by INT_1:def 3;
then b divides (a*b gcd c) by A1,INT_2:22;
then b divides 1 by A2, INT_2:def 3;
hence b=1 by INT_2:13;
end;
theorem Th1:
for G1,G2 being Group
for H being Subgroup of G1
for f being Homomorphism of G1,G2
for h being Element of G1
st h in H
holds (f|H).h = f.h
proof
let G1,G2 be Group;
let H be Subgroup of G1;
let f be Homomorphism of G1,G2;
let h be Element of G1;
assume h in H;
then (f|(the carrier of H)).h = f.h by FUNCT_1:49;
hence (f|H).h = f.h by GRSOLV_1:def 2;
end;
theorem Th4:
for X,Y being non empty set
for f being Function of X,Y
st f is bijective
for y being Element of Y
holds f.((f").y) = y
proof
let X,Y be non empty set;
let f be Function of X,Y;
assume A1: f is bijective;
let y be Element of Y;
f is onto by A1;
then reconsider g = f" as Function of Y,X by A1,FUNCT_2:25;
y = (g").(g.y) by A1,FUNCT_2:26
.= f.((f").y) by A1,FUNCT_1:43;
hence thesis;
end;
theorem Th5:
for X,Y being non empty set
for A being non empty Subset of X
for x being Element of X
st not x in A
for f being Function of X,Y
st f is one-to-one
holds not f.x in (f .: A)
proof
let X,Y be non empty set;
let A be non empty Subset of X;
let x be Element of X;
assume A1: not x in A;
let f be Function of X,Y;
assume A2: f is one-to-one;
A3: dom f = X by FUNCT_2:def 1;
f.x in (f .: A) iff ex a being object st a in dom f & a in A & f.x = f.a
by FUNCT_1:def 6;
hence f.x in (f .: A) implies contradiction by A2,A3,A1,FUNCT_1:def 4;
end;
begin :: Nontrivial Groups and Subgroups
registration
cluster strict non trivial for Group;
existence
proof
reconsider G = multMagma (# REAL, addreal #) as Group by GROUP_1:3;
take G;
thus thesis;
end;
end;
registration
let G be Group;
cluster trivial for Subgroup of G;
existence
proof
take (1).G;
thus thesis;
end;
let H be Subgroup of G;
cluster trivial for Subgroup of H;
existence
proof
take (1).H;
thus thesis;
end;
end;
registration
let G be non trivial Group;
cluster non trivial for Subgroup of G;
existence
proof
reconsider H=G as Subgroup of G by GROUP_2:54;
the carrier of H <> {1_G};
hence thesis;
end;
cluster strict non trivial for Subgroup of G;
existence
proof
set H = multMagma (#the carrier of G, the multF of G#);
reconsider H as Group-like non empty multMagma;
the multF of H = (the multF of G)||the carrier of H;
then H is strict Subgroup of G & H is non trivial by GROUP_2:def 5;
hence thesis;
end;
end;
theorem Th6:
for G being Group
holds G is trivial iff the multMagma of G = (1).G
proof
let G be Group;
thus G is trivial implies the multMagma of G = (1).G
proof
assume G is trivial;
then consider x being object such that
A1: the carrier of G = {x};
x = 1_G by A1, TARSKI:def 1;
then the carrier of G = the carrier of (1).G by A1,GROUP_2:def 7;
hence the multMagma of G = (1).G by GROUP_2:61;
end;
thus thesis;
end;
LmFiniteNontrivial:
not INT.Group(2) is trivial
proof
set G = INT.Group(2);
the carrier of (1).G = {1_G} by GROUP_2:def 7
.= {} \/ {0} by GR_CY_1:14
.= succ 0 by ORDINAL1:def 1
.= 1;
then the carrier of (1).G <> the carrier of G by ORDINAL1:def 17;
hence not INT.Group(2) is trivial by Th6;
end;
registration
cluster non trivial for finite Group;
existence by LmFiniteNontrivial;
end;
theorem Th7:
for G being Group
for H being Subgroup of G
st H is trivial
holds the multMagma of H = (1).G
proof
let G be Group;
let H be Subgroup of G;
assume H is trivial;
then the multMagma of H = (1).H by Th6
.= (1).G by GROUP_2:63;
hence thesis;
end;
theorem Th8:
for G being Group
for H being trivial Subgroup of G
for K being trivial Subgroup of G
holds the multMagma of H = the multMagma of K
proof
let G be Group;
let H be trivial Subgroup of G;
let K be trivial Subgroup of G;
the multMagma of H = (1).G by Th7
.= the multMagma of K by Th7;
hence thesis;
end;
theorem Th9:
for G being Group
for K being trivial Subgroup of G
for H being Subgroup of G
st H is Subgroup of K
holds H is trivial Subgroup of G
proof
let G be Group;
let K be trivial Subgroup of G;
let H be Subgroup of G;
assume A1: H is Subgroup of K;
the carrier of H = {1_G}
proof
the multMagma of K = (1).G by Th7;
then the carrier of K = {1_G} by GROUP_2:def 7;
then B1: the carrier of H c= {1_G} by A1,GROUP_2:def 5;
(1).G is Subgroup of H by GROUP_2:65;
then the carrier of (1).G c= the carrier of H by GROUP_2:def 5;
then {1_G} c= the carrier of H by GROUP_2:def 7;
hence the carrier of H = {1_G} by B1,XBOOLE_0:def 10;
end;
hence H is trivial Subgroup of G;
end;
begin :: Proper Subgroups
definition
let G be Group;
let IT be Subgroup of G;
attr IT is proper means
:Def1:
the multMagma of IT <> the multMagma of G;
end;
reserve G for Group;
reserve H for Subgroup of G;
theorem Th10:
H is proper iff the carrier of H <> the carrier of G
proof
(the carrier of H c= the carrier of G) & (the multF of H =
(the multF of G)||(the carrier of H)) by GROUP_2:def 5;
hence thesis;
end;
reserve h,x,y for object;
theorem Th11:
H is proper iff (the carrier of G) \ (the carrier of H) is non empty set
proof
set UG = the carrier of G;
set UH = the carrier of H;
thus H is proper implies UG \ UH is non empty set
proof
assume A1: H is proper;
UH c= UG & UH <> UG by A1,Th10, GROUP_2:def 5;
then (for x holds x in UH implies x in UG) &
not (for x holds x in UH iff x in UG) by TARSKI:2;
hence (the carrier of G) \ (the carrier of H) is non empty set
by XBOOLE_0:def 5;
end;
thus thesis;
end;
registration
let G be non trivial Group;
cluster strict proper for Subgroup of G;
existence
proof
take (1).G;
thus thesis;
end;
end;
registration
let G be non trivial Group;
cluster maximal -> proper for Subgroup of G;
coherence by GROUP_4:def 6;
end;
theorem Th12:
for G being non trivial Group
for H being proper Subgroup of G
for K being Subgroup of G
st H is Subgroup of K & the multMagma of H <> the multMagma of K
holds K is non trivial Subgroup of G
proof
let G be non trivial Group;
let H be proper Subgroup of G;
let K be Subgroup of G;
assume A1: H is Subgroup of K;
assume A2: the multMagma of H <> the multMagma of K;
assume B1: not K is non trivial Subgroup of G;
then H is trivial Subgroup of G by A1,Th9;
hence contradiction by A2,B1,Th8;
end;
begin :: Automorphisms
definition
let G;
mode Endomorphism of G is Homomorphism of G,G;
end;
reserve f for Endomorphism of G;
registration
let G;
cluster bijective for Endomorphism of G;
existence
proof
reconsider i = id the carrier of G as Homomorphism of G,G by GROUP_6:38;
i is bijective;
hence thesis;
end;
end;
definition
let G;
mode Automorphism of G is bijective Endomorphism of G;
end;
reserve phi for Automorphism of G;
theorem Th13:
Image (f|(1).G) = (1).G
proof
Image(f|(1).G) = f .: ((1).G) by GRSOLV_1:def 3
.= (1).G by GRSOLV_1:11;
hence thesis;
end;
:: In particular, the trivial proper subgroup (1).G of G is invariant
:: under inner automorphisms, and thus is a characteristic subgroup.
theorem Th14:
Image(phi|(1).G) is Subgroup of (1).G
proof
(1).G is Subgroup of (1).G by GROUP_2:54;
hence Image(phi|(1).G) is Subgroup of (1).G by Th13;
end;
theorem Th15:
for G1,G2 being Group
for f being Homomorphism of G1,G2
for H being Subgroup of G1
holds Ker(f|H) is Subgroup of Ker(f)
proof
let G1,G2 be Group;
let f be Homomorphism of G1,G2;
let H be Subgroup of G1;
A1: Ker(f|H) is Subgroup of G1 by GROUP_2:56;
for g being Element of G1 st g in Ker(f|H) holds g in Ker(f)
proof
let g be Element of G1;
assume A2: g in Ker(f|H);
then A3: g in H by GROUP_2:40;
(f|H).g = f.g by A2,Th1,GROUP_2:40;
then 1_G2 = f.g by A2,A3,GROUP_6:41;
hence g in Ker(f) by GROUP_6:41;
end;
hence thesis by A1,GROUP_2:58;
end;
Lm2: H is Subgroup of (1).G implies the multMagma of H = the multMagma of (1).G
proof
assume H is Subgroup of (1).G;
then H is Subgroup of (1).G & (1).G is Subgroup of H by GROUP_2:65;
hence thesis by GROUP_2:55;
end;
Lm3:
(phi|H) is Homomorphism of H,Image(phi|H) & (phi|H) is one-to-one
proof
thus phi|H is Homomorphism of H,Image(phi|H) by GROUP_6:49;
Ker(phi) = (1).G by GROUP_6:56;
then Ker(phi|H) is Subgroup of (1).G by Th15;
then Ker(phi|H) = (1).G by Lm2
.= (1).H by GROUP_2:63;
hence (phi|H) is one-to-one by GROUP_6:56;
end;
theorem Th16:
(for f being Automorphism of G holds Image(f|H) is Subgroup of H) implies
ex psi being Automorphism of G
st psi = phi" & Image(phi|Image(psi|H)) is Subgroup of Image(phi|H)
proof
assume A1: for f being Automorphism of G holds Image(f|H) is Subgroup of H;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
take psi;
thus psi = phi";
Image(psi|H) is Subgroup of H by A1;
then phi .: Image(psi|H) is Subgroup of phi .: H by GRSOLV_1:12;
then Image(phi|Image(psi|H)) is Subgroup of phi .: H by GRSOLV_1:def 3;
hence Image(phi|Image(psi|H)) is Subgroup of Image(phi|H) by GRSOLV_1:def 3;
end;
theorem Th17:
ex psi being Automorphism of G
st psi = phi" & Image(phi|Image(psi|H)) = the multMagma of H
proof
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
take psi;
thus psi = phi";
for g being Element of G holds g in Image(phi|Image(psi|H)) iff g in H
proof
let g be Element of G;
thus g in Image(phi|Image(psi|H)) implies g in H
proof
assume g in Image(phi|Image(psi|H));
then consider a being Element of Image(psi|H) such that
B1: g = (phi|Image(psi|H)).a by GROUP_6:45;
M1: a in Image(psi|H) & a is Element of G by GROUP_2:42;
then B2: phi.a = g by B1, Th1;
consider b being Element of H such that
B3: a = (psi|H).b
by M1,GROUP_6:45;
M2: b in H & b is Element of G by GROUP_2:42;
then b = phi.(psi.b) by Th4
.= g by M2,B2,B3,Th1;
hence g in H;
end;
thus g in H implies g in Image(phi|Image(psi|H))
proof
assume B1: g in H;
set a = (psi|H).g;
B2: a in Image(psi|H)
proof
g in dom(psi|H) by B1,FUNCT_2:def 1;
then (psi|H).g in (psi|H) .: (the carrier of H) by FUNCT_1:def 6;
hence a in Image(psi|H) by GROUP_6:def 10;
end;
set K = Image(psi|H);
set b = (phi|Image(psi|H)).a;
B3: b in Image(phi|Image(psi|H))
proof
a in dom(phi|K) by B2, FUNCT_2:def 1;
then (phi|K).a in (phi|K) .: (the carrier of K) by FUNCT_1:def 6;
hence b in Image(phi|K) by GROUP_6:def 10;
end;
thus g in Image(phi|K)
proof
B4: psi.g = a by B1,Th1;
a is Element of G by B2,GROUP_2:42;
then (phi|K).a = phi.a by B2,Th1
.= g by B4,Th4;
hence thesis by B3;
end;
end;
end;
hence Image(phi|Image(psi|H)) = the multMagma of H by GROUP_2:60;
end;
theorem Th18:
for H being strict Subgroup of G
for K being Subgroup of G
st Image(phi|H) is Subgroup of K
holds ex psi being Automorphism of G
st psi = phi" & H is Subgroup of Image(psi|K)
proof
let H be strict Subgroup of G;
let K be Subgroup of G;
assume A1: Image(phi|H) is Subgroup of K;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
take psi;
thus psi = phi";
consider phi0 being Automorphism of G such that
A2: phi0 = psi" and
A3: Image(psi|Image(phi0|H)) = the multMagma of H by Th17;
A4: phi = phi0 by A2,FUNCT_1:43;
psi .: Image(phi|H) is Subgroup of psi .: K by A1,GRSOLV_1:12;
then Image(psi|Image(phi|H)) is Subgroup of psi .: K by GRSOLV_1:def 3;
hence H is Subgroup of Image(psi|K) by A3,A4,GRSOLV_1:def 3;
end;
theorem Th19:
H,phi .: H are_isomorphic
proof
H,Image(phi|H) are_isomorphic by Lm3,GROUP_6:68;
hence H,phi .: H are_isomorphic by GRSOLV_1:def 3;
end;
theorem Th20:
for G being finite Group
for H1,H2 being strict Subgroup of G
st H1,H2 are_isomorphic
holds index H1 = index H2
proof
let G be finite Group;
let H1,H2 be strict Subgroup of G;
assume A1: H1,H2 are_isomorphic;
card H1 * index H1 = card G by GROUP_2:147
.= card H2 * index H2 by GROUP_2:147;
then index H1 * card H1 = index H2 * card H1 by A1,GROUP_6:73;
hence index H1 = index H2 by XCMPLX_1:5;
end;
theorem
G is finite implies
for p being prime Nat
for P being strict Subgroup of G
st P is_Sylow_p-subgroup_of_prime p
holds Image(phi|P) is_Sylow_p-subgroup_of_prime p
proof
assume A0: G is finite;
let p be prime Nat;
let P be strict Subgroup of G;
assume A1: P is_Sylow_p-subgroup_of_prime p;
then A2: P is p-group by GROUP_10:def 18;
set Q = phi .: P;
consider r being Nat such that
A3: card P = p |^ r by A2,GROUP_10:def 17;
card Q = p |^ r by A3,Th19,GROUP_6:75;
then A4: Q is p-group by GROUP_10:def 17;
A5: Q = Image(phi|P) by GRSOLV_1:def 3;
not p divides index P by A1, GROUP_10:def 18;
then not p divides index Q by A0,Th19,Th20;
hence Image(phi|P) is_Sylow_p-subgroup_of_prime p by A4, A5, GROUP_10:def 18;
end;
theorem Th22:
for f being Automorphism of G
st Image(f|H) = the multMagma of H
holds f|H is Automorphism of H
proof
let f be Automorphism of G;
assume A1: Image(f|H) = the multMagma of H;
set UH = the carrier of H;
reconsider fH=f|H as Function of UH,UH by A1,GROUP_6:49;
A2: fH is bijective
proof
thus fH is one-to-one by Lm3;
thus fH is onto by A1,GROUP_6:44;
end;
for x,y being Element of H holds fH.(x*y) = (fH.x) * (fH.y)
proof
let x,y be Element of H;
fH.(x * y) = (f|H).x * (f|H).y by GROUP_6:def 6
.= fH.x * fH.y by GROUP_2:43;
hence thesis;
end;
hence thesis by A2,GROUP_6:def 6;
end;
theorem Th23:
for G being non trivial Group
for H being Subgroup of G
for phi being Automorphism of G
st H is proper Subgroup of G
holds Image(phi|H) is proper Subgroup of G
proof
let G be non trivial Group;
let H be Subgroup of G;
let phi be Automorphism of G;
set UH = the carrier of H;
set UG = the carrier of G;
A1: phi is one-to-one & phi is onto & UH is non empty Subset of UG &
phi is Function of UG,UG by GROUP_2:def 5;
assume H is proper Subgroup of G;
then UG \ UH is non empty by Th11;
then consider x such that
A2: x in UG \ UH by XBOOLE_0:def 1;
A3: x in G & not x in H by A2,XBOOLE_0:def 5;
A4: not (phi.x in phi .: H)
proof
not (phi.x in (phi .: UH)) by A1, A3, Th5;
hence not (phi.x in (phi .: H)) by GRSOLV_1:8;
end;
phi.x is Element of G
proof
dom phi = UG & rng phi = UG by A1, FUNCT_2:def 1;
hence phi.x is Element of G by A2, FUNCT_1:def 3;
end;
then phi .: H is proper by A4;
hence Image(phi|H) is proper Subgroup of G by GRSOLV_1:def 3;
end;
theorem Th24:
for G being non trivial Group
for H being strict Subgroup of G
for phi being Automorphism of G
st H is maximal
holds Image(phi|H) is maximal
proof
let G be non trivial Group;
let H be strict Subgroup of G;
let phi be Automorphism of G;
assume A1: H is maximal;
A2: Image(phi|H) is proper Subgroup of G by A1,Th23;
set UG = the carrier of G;
set UH = the carrier of H;
for K being strict Subgroup of G
st Image(phi|H) <> K & Image(phi|H) is Subgroup of K
holds K = the multMagma of G
proof
let K be strict Subgroup of G;
assume B1: Image(phi|H) <> K;
assume B2: Image(phi|H) is Subgroup of K;
then consider psi being Automorphism of G such that
B3: psi = phi" and
B4: H is Subgroup of Image(psi|K)
by Th18;
set UK = the carrier of K;
reconsider K as non trivial strict Subgroup of G by A2,B1,B2,Th12;
UK \ (the carrier of Image(phi|H)) is non empty by B1,B2,Def1,Th11;
then consider k being object such that
B6: k in UK \ (the carrier of Image(phi|H)) by XBOOLE_0:def 1;
reconsider k as Element of K by B6;
set L = Image(psi|K);
B8: psi.k in L
proof
C1: k in G by GROUP_2:41;
consider l being object such that
C2: l = psi.k;
dom psi = the carrier of G by FUNCT_2:def 1;
then l in psi .: (the carrier of K) by C1,C2,FUNCT_1:def 6;
then l in the carrier of (psi .: K) by GRSOLV_1:8;
hence psi.k in Image(psi|K) by C2,GRSOLV_1:def 3;
end;
B9: the multMagma of H <> L
proof
set UPH = the carrier of Image(phi|H);
C1: phi is one-to-one & phi is onto & UPH is non empty Subset of UG &
phi is Function of UG,UG by GROUP_2:def 5;
C2: k in G & not k in Image(phi|H) by B6, XBOOLE_0:def 5, GROUP_2:41;
consider phi2 being Automorphism of G such that
C3: phi2 = psi" and
C4: Image(psi|Image(phi2|H)) = the multMagma of H
by Th17;
C5: phi2=phi by C3,B3,FUNCT_1:43;
set UPH = the carrier of Image(phi|H);
psi .: UPH = the carrier of (psi .: Image(phi|H)) by GRSOLV_1:8
.= the carrier of Image(psi|Image(phi|H)) by GRSOLV_1:def 3;
hence thesis by B8,C1,C2,C4,C5,Th5;
end;
B10: Image(phi|L) = the multMagma of G
proof
L = the multMagma of G by A1,B4,B9,GROUP_4:def 6;
then phi .: the carrier of L = rng phi by RELSET_1:22
.= UG by FUNCT_2:def 3;
then UG = the carrier of (phi .: L) by GRSOLV_1:8
.= the carrier of Image(phi|L) by GRSOLV_1:def 3;
hence thesis by GROUP_2:61;
end;
Image(phi|L) = K
proof
consider psi2 being Automorphism of G such that
C1: psi2 = phi" and
C2: Image(phi|Image(psi2|K)) = the multMagma of K by Th17;
thus Image(phi|Image(psi|K)) = K by B3,C1,C2;
end;
hence thesis by B10;
end;
hence Image(phi|H) is maximal by A2,Def1,GROUP_4:def 6;
end;
begin :: Inner Automorphisms
definition
let G;
let a be Element of G;
let f be Function;
pred a is_inner_wrt f means
:Def2a:
for x being Element of G holds f.x = x |^ a;
end;
definition
let G;
let IT be Automorphism of G;
attr IT is inner means
:Def2:
ex a being Element of G st a is_inner_wrt IT;
end;
notation
let G be Group, f be Automorphism of G;
antonym f is outer for f is inner;
end;
registration
let G;
cluster inner for Automorphism of G;
existence
proof
reconsider i = id (the carrier of G) as Automorphism of G by GROUP_6:38;
take i;
take 1_G;
thus thesis by GROUP_3:19;
end;
end;
theorem Th26:
for G being strict Group, f being object
holds f in Aut G iff f is Automorphism of G
proof
let G be strict Group;
let f be object;
thus f in Aut G implies f is Automorphism of G
proof
assume A1: f in Aut G;
then reconsider f as Endomorphism of G by AUTGROUP:def 1;
f is bijective by A1,AUTGROUP:def 1;
hence thesis;
end;
thus f is Automorphism of G implies f in Aut G by AUTGROUP:def 1;
end;
Lm6:
for G being strict Group
for f being Element of InnAut G
holds f is Automorphism of G
proof
let G be strict Group;
let f be Element of InnAut G;
f is Element of Aut G by AUTGROUP:12;
hence f is Automorphism of G by Th26;
end;
theorem
for G being strict Group
for f being object
holds f in InnAut G iff f is inner Automorphism of G
proof
let G be strict Group;
let f be object;
A1: f is Automorphism of G implies
f is Element of Funcs (the carrier of G, the carrier of G) by FUNCT_2:9;
thus f in InnAut G implies f is inner Automorphism of G
proof
assume B1: f in InnAut G;
then reconsider f as Automorphism of G by Lm6;
consider a being Element of G such that
B2: for x being Element of G holds f.x = x |^ a by A1,B1,AUTGROUP:def 4;
a is_inner_wrt f by B2;
hence thesis by Def2;
end;
assume f is inner Automorphism of G;
then reconsider f as inner Automorphism of G;
ex a being Element of G st a is_inner_wrt f by Def2;
hence thesis by A1,AUTGROUP:def 4;
end;
theorem Th28:
for a being Element of G
for f being inner Automorphism of G st a is_inner_wrt f
holds Image(f|H) = H |^ a
proof
let a be Element of G,
f be inner Automorphism of G;
assume
A1: for x being Element of G holds f.x = x |^ a;
A2: for h being Element of G st h in H holds (f|H).h = h |^ a
proof
let h be Element of G;
assume h in H;
hence (f|H).h = f.h by Th1
.= h |^ a by A1;
end;
C2: for y being Element of G st y in Image(f|H) holds y in H |^ a
proof
let y be Element of G;
assume y in Image(f|H);
then consider h being Element of H such that
B1: (f|H).h = y by GROUP_6:45;
reconsider h as Element of G by GROUP_2:42;
B2: h in H;
then h |^ a = y by A2,B1;
hence y in H |^ a by B2,GROUP_3:58;
end;
for y being Element of G st y in H |^ a holds y in Image(f|H)
proof
let y be Element of G;
assume y in H |^ a;
then consider g being Element of G such that
B1: y=g|^a and
B2: g in H by GROUP_3:58;
(f|H).g = f.g by Th1,B2
.= y by A1,B1;
hence y in Image(f|H) by B2,GROUP_6:45;
end;
hence (H |^ a) = Image(f|H) by C2;
end;
theorem Th29:
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f
holds Ker f = (1).G
proof
let a be Element of G;
let f be Endomorphism of G;
assume A1: for x being Element of G holds f.x = x |^ a;
for x being Element of G holds x in Ker f implies x in (1).G
proof
let x be Element of G;
assume x in Ker f;
then 1_G = f.x by GROUP_6:41
.= x |^ a by A1;
then x = 1_G by GROUP_3:18;
hence x in (1).G by GROUP_2:46;
end;
then A2: Ker f is Subgroup of (1).G by GROUP_2:58;
(1).G is Subgroup of Ker f by GROUP_2:65;
hence Ker f = (1).G by A2,GROUP_2:55;
end;
theorem Th30:
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f
holds f is Automorphism of G
proof
let a be Element of G;
let f be Endomorphism of G;
assume A1: a is_inner_wrt f;
then Ker f = (1).G by Th29;
then A2: f is one-to-one by GROUP_6:56;
ex fInv being Endomorphism of G st f*fInv = id (the carrier of G)
proof
deffunc F(Element of G) = ($1) |^ a";
consider fInv be Function of the carrier of G, the carrier of G such that
A3: for g being Element of G holds fInv.g = F(g) from FUNCT_2:sch 4;
for x1,x2 being Element of G holds fInv.(x1 * x2) = fInv.x1 * fInv.x2
proof
let x1,x2 be Element of G;
A4: fInv.x1 = x1 |^ a" & fInv.x2 = x2 |^ a" by A3;
fInv.(x1 * x2) = (x1 * x2) |^ a" by A3
.= fInv.x1 * fInv.x2 by A4,GROUP_3:23;
hence thesis;
end;
then reconsider fInv as Endomorphism of G by GROUP_6:def 6;
for x being Element of G holds (f*fInv).x = (id the carrier of G).x
proof
let x be Element of G;
(f * fInv).x = f.(fInv.x) by FUNCT_2:15
.= f.(x |^ a") by A3
.= (x |^ a") |^ a by A1
.= x |^ (a" * a) by GROUP_3:24
.= x |^ 1_G by GROUP_1:def 5
.= (id the carrier of G).x by GROUP_3:19;
hence thesis;
end;
then f*fInv = id the carrier of G;
hence thesis;
end;
then f is onto by FUNCT_2:18;
hence f is Automorphism of G by A2;
end;
theorem
for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f
holds f is inner Automorphism of G by Th30,Def2;
theorem Th32:
for a being Element of G
ex f being inner Automorphism of G st a is_inner_wrt f
proof
let a be Element of G;
deffunc F(Element of G) = ($1) |^ a;
consider f be Function of the carrier of G, the carrier of G such that
A1: for g being Element of G holds f.g = F(g) from FUNCT_2:sch 4;
for x1,x2 being Element of G holds f.(x1 * x2) = f.x1 * f.x2
proof
let x1,x2 be Element of G;
A2: f.x1 = x1 |^ a & f.x2 = x2 |^ a by A1;
f.(x1 * x2) = (x1 * x2) |^ a by A1
.= f.x1 * f.x2 by A2,GROUP_3:23;
hence thesis;
end;
then reconsider f as Endomorphism of G by GROUP_6:def 6;
a is_inner_wrt f & f is inner Automorphism of G by A1,Th30,Def2,Def2a;
hence thesis;
end;
theorem Th33:
for H being strict Subgroup of G
holds H is normal iff for f being inner Automorphism of G holds Image(f|H)=H
proof
let H be strict Subgroup of G;
thus H is normal implies
for f being inner Automorphism of G holds Image(f|H)=H
proof
assume B1: H is normal;
let f be inner Automorphism of G;
consider a being Element of G such that
B2: a is_inner_wrt f by Def2;
Image(f|H) = H |^ a by B2,Th28
.= H by B1,GROUP_3:def 13;
hence Image(f|H)=H;
end;
assume B1: for f being inner Automorphism of G holds Image(f|H)=H;
assume not H is normal;
then consider a being Element of G such that
B2: H |^ a <> the multMagma of H
by GROUP_3:def 13;
consider f being inner Automorphism of G such that
B3: a is_inner_wrt f by Th32;
Image(f|H) = H |^ a by B3,Th28;
hence contradiction by B1,B2;
end;
begin :: Characteristic Subgroups
:: Dummit and Foote, Abstract Algebra, ch.4 section 4
definition
let G;
let IT be Subgroup of G;
attr IT is characteristic means :Def3:
for f being Automorphism of G holds Image (f|IT) = the multMagma of IT;
end;
Lm8: H is Subgroup of (1).G implies the multMagma of H = the multMagma of (1).G
proof
assume H is Subgroup of (1).G;
then reconsider H as Subgroup of (1).G;
H is Subgroup of (1).G & (1).G is Subgroup of H by GROUP_2:65;
hence thesis by GROUP_2:55;
end;
registration
let G;
cluster (1).G -> characteristic;
coherence
proof
let f be Automorphism of G;
reconsider I = Image(f|(1).G) as Subgroup of (1).G by Th14;
(1).G = I by Lm8;
hence thesis;
end;
end;
registration
let G;
cluster characteristic for Subgroup of G;
existence
proof
take (1).G;
thus thesis;
end;
end;
reserve K for characteristic Subgroup of G;
registration
let G be Group;
cluster strict characteristic for Subgroup of G;
existence
proof
take (1).G;
thus thesis;
end;
end;
theorem Th35:
K is normal Subgroup of G
proof
for a being Element of G holds K |^ a = the multMagma of K
proof
let a be Element of G;
consider f being inner Automorphism of G such that
A2: a is_inner_wrt f by Th32;
the multMagma of K = Image(f|K) by Def3
.= K |^ a by A2,Th28;
hence thesis;
end;
hence K is normal Subgroup of G by GROUP_3:def 13;
end;
registration
let G be Group;
cluster characteristic -> normal for Subgroup of G;
coherence by Th35;
end;
theorem Th36:
for G1,G2 being Group
for H1 being Subgroup of G1
for K being Subgroup of H1
for H2 being Subgroup of G2
for f being Homomorphism of G1,G2
for g being Homomorphism of H1,H2
st (for k being Element of G1 st k in K holds f.k=g.k)
holds Image(f|K) = Image(g|K)
proof
let G1,G2 be Group;
let H1 be Subgroup of G1;
let K be Subgroup of H1;
let H2 be Subgroup of G2;
let f be Homomorphism of G1,G2;
let g be Homomorphism of H1,H2;
assume A1: for k being Element of G1 st k in K holds f.k=g.k;
A2: Image(f|K) is strict Subgroup of G2 &
Image(g|K) is strict Subgroup of G2 by GROUP_2:56;
for y being object
holds y in the carrier of Image(f|K) iff y in the carrier of Image(g|K)
proof
let y be object;
thus y in the carrier of Image(f|K) implies y in the carrier of Image(g|K)
proof
assume y in the carrier of Image(f|K);
then consider h being Element of K such that
B1: (f|K).h = y
by STRUCT_0:def 5,GROUP_6:45;
B2: h is Element of G1 & h is Element of H1 & h in K by GROUP_2:42;
f.h = g.h by A1,B2
.= (g|K).h by B2, Th1;
then (g|K).h = y by B1,B2,Th1;
hence y in the carrier of Image(g|K) by STRUCT_0:def 5,GROUP_6:45;
end;
thus y in the carrier of Image(g|K) implies y in the carrier of Image(f|K)
proof
assume y in the carrier of Image(g|K);
then consider h being Element of K such that
C1: (g|K).h = y by STRUCT_0:def 5,GROUP_6:45;
C2: h is Element of H1 & h is Element of G1 & h in K by GROUP_2:42;
g.h = f.h by A1,C2
.= (f|K).h by C2,Th1;
then (f|K).h = y by C1,C2,Th1;
hence y in the carrier of Image(f|K) by STRUCT_0:def 5,GROUP_6:45;
end;
end;
hence Image(f|K) = Image(g|K) by A2,GROUP_2:59,TARSKI:2;
end;
theorem
for H being strict Subgroup of G
st (for K being strict Subgroup of G
st card K = card H
holds H = K)
holds H is characteristic
proof
let H be strict Subgroup of G;
assume A1: for K being strict Subgroup of G st card K = card H holds H = K;
H is characteristic
proof
let phi be Automorphism of G;
Image(phi|H) = phi .: H by GRSOLV_1:def 3;
then card H = card Image(phi|H) by Th19,GROUP_6:73;
hence Image(phi|H) = the multMagma of H by A1;
end;
hence thesis;
end;
theorem
for N being strict normal Subgroup of G
for K being characteristic Subgroup of N
holds K is normal Subgroup of G
proof
let N be strict normal Subgroup of G;
let K be characteristic Subgroup of N;
for a being Element of G holds K |^ a = the multMagma of K
proof
let a be Element of G;
consider g being inner Automorphism of G such that
A1: a is_inner_wrt g by Th32;
Image(g|N) = N by Th33;
then reconsider f = g|N as Automorphism of N by Th22;
A2: Image(f|K) = the multMagma of K by Def3;
for k being Element of G st k in K holds f.k = g.k by Th1,GROUP_2:40;
then Image(g|K) = the multMagma of K & Image(g|K) = K |^ a
by A1,A2,Th28,Th36;
hence thesis;
end;
hence K is normal Subgroup of G by GROUP_3:def 13;
end;
theorem
for N being characteristic Subgroup of G
for K being characteristic Subgroup of N
holds K is characteristic Subgroup of G
proof
let N be characteristic Subgroup of G;
let K be characteristic Subgroup of N;
for g being Automorphism of G holds Image(g|K) = the multMagma of K
proof
let g be Automorphism of G;
Image(g|N) = the multMagma of N by Def3;
then reconsider f = g|N as Automorphism of N by Th22;
A1: Image(f|K) = the multMagma of K by Def3;
for k being Element of G st k in K holds f.k = g.k by Th1, GROUP_2:40;
hence Image(g|K) = the multMagma of K by A1,Th36;
end;
hence K is characteristic Subgroup of G by Def3;
end;
theorem Th40:
for G being Group
for H being Subgroup of G
holds H is characteristic Subgroup of G iff
for phi being Automorphism of G holds Image(phi|H) is Subgroup of H
proof
let G be Group;
let H be Subgroup of G;
thus H is characteristic Subgroup of G implies
(for phi being Automorphism of G holds Image(phi|H) is Subgroup of H)
proof
assume B1: H is characteristic Subgroup of G;
let phi be Automorphism of G;
Image(phi|H) = (Omega).H by B1,Def3;
hence Image(phi|H) is Subgroup of H;
end;
thus (for phi being Automorphism of G holds Image(phi|H) is Subgroup of H)
implies H is characteristic Subgroup of G
proof
assume A1: for phi being Automorphism of G
holds Image(phi|H) is Subgroup of H;
A2: for phi being Automorphism of G holds H is Subgroup of Image(phi|H)
proof
let phi be Automorphism of G;
consider psi being Automorphism of G such that
B1: psi = phi" and
B2: Image(phi|Image(psi|H)) is Subgroup of Image(phi|H) by A1,Th16;
consider psi2 being Automorphism of G such that
B3: psi2 = phi" and
B4: Image(phi|Image(psi2|H)) = the multMagma of H by Th17;
the carrier of H c= the carrier of (Omega).H
& (Omega).H is Subgroup of G by GROUP_2:56;
then B5: H is Subgroup of (Omega).H by GROUP_2:57;
Image(phi|Image(psi2|H)) = (Omega).H by B4;
then (Omega).H is Subgroup of Image(phi|H) by B1,B2,B3;
hence H is Subgroup of Image(phi|H) by B5, GROUP_2:56;
end;
for phi being Automorphism of G holds the multMagma of H = Image(phi|H)
proof
let phi be Automorphism of G;
H is Subgroup of Image(phi|H) & Image(phi|H) is Subgroup of H
by A1,A2;
hence the multMagma of H = Image(phi|H) by GROUP_2:55;
end;
hence H is characteristic Subgroup of G by Def3;
end;
end;
theorem
center G is characteristic Subgroup of G
proof
set Z = center G;
A1: for y,z being Element of G st z in Z holds (phi.z)*y = y*phi.z
proof
let y,z be Element of G;
assume B1: z in Z;
set x = (phi").y;
(phi.z)*y = (phi.z)*(phi.x) by Th4
.= phi.(z*x) by GROUP_6:def 6
.= phi.(x*z) by B1,GROUP_5:77
.= (phi.x)*(phi.z) by GROUP_6:def 6
.= y*(phi.z) by Th4;
hence thesis;
end;
A2: for z being Element of G st z in Z holds (phi|Z).z in Z
proof
let z be Element of G;
assume B1: z in Z;
then for y being Element of G holds (phi.z)*y=y*(phi.z) by A1;
then (phi.z) in Z by GROUP_5:77;
hence ((phi|Z).z) in Z by B1,Th1;
end;
Image(phi|Z) is Subgroup of Z
proof
for w being Element of G st w in rng(phi|Z) holds w in Z
proof
let w be Element of G;
assume w in rng(phi|Z);
then consider z being object such that
C1: z in dom(phi|Z) and
C2: (phi|Z).z = w by FUNCT_1:def 3;
reconsider z as Element of Z by C1;
z is Element of G by GROUP_2:42;
hence w in Z by C2,A2,STRUCT_0:def 5;
end;
then rng(phi|Z) c= the carrier of Z by STRUCT_0:def 5;
then the carrier of Image(phi|Z) c= the carrier of Z by GROUP_6:44;
hence Image(phi|Z) is Subgroup of Z by GROUP_2:57;
end;
hence Z is characteristic Subgroup of G by Th40;
end;
scheme :: sch 1
CharMeet{G() -> Group, P[set]} :
for phi being Automorphism of G()
holds phi .: meet{A where A is Subset of G() : ex K being strict Subgroup
of G() st A = the carrier of K & P[K]} = meet{A where A is Subset of G() :
ex K being strict Subgroup of G() st A = the carrier of K & P[K]}
provided
A1: for phi being Automorphism of G()
for H being strict Subgroup of G()
st P[H]
holds P[Image(phi|H)] and
A2: ex H being strict Subgroup of G() st P[H]
proof
let phi be Automorphism of G();
set UG = the carrier of G();
set Fam = {A where A is Subset of G() : ex K being strict Subgroup
of G() st A = the carrier of K & P[K]};
consider H being strict Subgroup of G() such that
A3: P[H] by A2;
A4: Fam <> {}
proof
consider A being set such that
B1: A = the carrier of H;
the carrier of H is Subset of G() by GROUP_2:def 5;
then A in Fam by A3, B1;
hence thesis;
end;
A5: for phi0 being Automorphism of G()
for x being object st x in meet Fam
holds phi0.x in meet Fam
proof
let phi0 be Automorphism of G();
let x be object;
assume
B1: x in meet Fam;
for A being set holds A in Fam implies phi0.x in A
proof
let A be set;
assume C1: A in Fam;
consider A0 being Subset of G() such that
C2: A0=A & ex H being strict Subgroup of G()
st A0 = the carrier of H & P[H] by C1;
consider K being strict Subgroup of G() such that
C3: A = the carrier of K & P[K] by C2;
consider psi being Automorphism of G() such that
C4: psi = phi0" & Image(phi0|Image(psi|K)) = the multMagma of K
by Th17;
x in K by C1,B1,C3,SETFAM_1:def 1;
then C5: x in G() & dom phi0 = the carrier of G()
by GROUP_2:40,FUNCT_2:def 1;
P[Image(psi|K)] by C3,A1;
then carr Image(psi|K) in Fam;
then x in carr Image(psi|K) by B1,SETFAM_1:def 1;
then phi0.x in phi0 .: (carr Image(psi|K)) by C5, FUNCT_1:def 6;
then phi0.x in carr (phi0 .: Image(psi|K)) by GRSOLV_1:8;
hence phi0.x in A by C3,C4,GRSOLV_1:def 3;
end;
hence thesis by A4, SETFAM_1:def 1;
end;
for x being object st x in meet Fam holds x in phi .: meet Fam
proof
let x be object;
assume B1: x in meet Fam;
then carr H in Fam & for A1 being set holds A1 in Fam implies x in A1
by A3,SETFAM_1:def 1;
then B2: x in H;
then B3: x is Element of G() by GROUP_2:42;
reconsider psi = phi" as Automorphism of G() by GROUP_6:62;
B4: dom phi = the carrier of G() by FUNCT_2:def 1;
B5: psi.x in meet Fam by B1,A5;
B6: phi.(psi.x) = x by B3,Th4;
psi is bijective & x in G() by B2, GROUP_2:40;
then psi.x in dom phi by B4, FUNCT_2:5;
hence x in phi .: meet Fam by B6,B5,FUNCT_1:def 6;
end;
then P1: meet Fam c= phi .: meet Fam;
for y being object st y in phi .: meet Fam
holds y in meet Fam
proof
let y be object;
assume y in phi .: meet Fam;
then consider x being object such that
B1: x in dom phi & x in meet Fam & y = phi.x by FUNCT_1:def 6;
thus y in meet Fam by B1,A5;
end;
then phi .: meet Fam c= meet Fam;
hence thesis by P1,XBOOLE_0:def 10;
end;
scheme :: sch 2
MeetIsChar{G() -> Group, P[set]} :
ex K being strict Subgroup of G() st
the carrier of K = meet {A where A is Subset of G() :
ex H being strict Subgroup of G() st A = the carrier of H & P[H]} &
K is characteristic
provided
A1: for phi being Automorphism of G()
for H being strict Subgroup of G()
st P[H]
holds P[Image(phi|H)] and
A2: ex H being strict Subgroup of G() st P[H]
proof
set Fam = {A where A is Subset of G() :
ex H being strict Subgroup of G()
st A = the carrier of H & P[H]};
A3: for phi being Automorphism of G()
holds phi .: meet Fam = meet Fam from CharMeet(A1,A2);
consider K being strict Subgroup of G() such that
A4: the carrier of K = meet Fam from GROUP_4:sch 1(A2);
take K;
for phi being Automorphism of G() holds Image(phi|K) = K
proof
let phi be Automorphism of G();
the carrier of Image(phi|K)
= the carrier of phi .: K by GRSOLV_1:def 3
.= phi .: (the carrier of K) by GRSOLV_1:8
.= the carrier of K by A3,A4;
hence Image(phi|K) = K by GROUP_2:59;
end;
hence thesis by A4;
end;
theorem
for G being non trivial Group
holds (ex H being strict Subgroup of G st H is maximal) implies
Phi(G) is characteristic Subgroup of G
proof
let G be non trivial Group;
defpred P[Subgroup of G] means $1 is maximal;
assume A1: ex H being strict Subgroup of G st P[H];
set MaxSubCarrs = {A where A is Subset of G :
ex H being strict Subgroup of G
st A = the carrier of H & P[H]};
A2: for phi being Automorphism of G
for H being strict Subgroup of G
st P[H]
holds P[Image(phi|H)] by Th24;
consider K being strict Subgroup of G such that
A3: the carrier of K = meet {A where A is Subset of G :
ex H being strict Subgroup of G st A = the carrier of H & P[H]} and
A4: K is characteristic from MeetIsChar(A2,A1);
thus thesis by A4,A1,A3,GROUP_4:def 7;
end;
theorem Th43:
for phi being Automorphism of G
holds phi .: commutators G = commutators G
proof
let phi be Automorphism of G;
for g being object
st g in commutators G
holds g in phi .: commutators G
proof
let g be object;
assume B1: g in commutators G;
then reconsider g as Element of G;
consider a,b being Element of G such that
B2: g = [.a,b.] by B1, GROUP_5:58;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
set x = psi.a;
set y = psi.b;
set h = [.x,y.];
dom phi = the carrier of G by FUNCT_2:def 1;
then B3: h in dom phi & h in commutators G & phi.((phi").g) = g by Th4;
psi.g = h by B2,GROUP_6:34;
hence thesis by B3, FUNCT_1:def 6;
end;
then P1: commutators G c= phi .: commutators G;
for h being object
st h in phi .: commutators G
holds h in commutators G
proof
let h be object;
assume B1: h in phi .: commutators G;
consider g being object such that
g in dom phi and
B2: g in commutators G and
B3: h = phi.g by B1,FUNCT_1:def 6;
consider a,b be Element of G such that
B4: g = [.a,b.] by B2,GROUP_5:58;
h = [.phi.a, phi.b.] by B3,B4,GROUP_6:34;
hence h in commutators G;
end;
then phi .: commutators G c= commutators G;
hence commutators G = phi .: commutators G by P1,XBOOLE_0:def 10;
end;
theorem Th44:
for G being Group
for phi being Automorphism of G
for H being Subgroup of G
st (for h being Element of H holds phi.h in H)
holds Image(phi|H) is Subgroup of H
proof
let G be Group;
let phi be Automorphism of G;
let H be Subgroup of G;
assume A1: for h being Element of H holds phi.h in H;
for y being object st y in rng(phi|H) holds y in the carrier of H
proof
let y be object;
assume y in rng(phi|H);
then consider x being object such that
B1: x in dom(phi|H) and
B2: y = (phi|H).x by FUNCT_1:def 3;
B3: x in H by B1;
reconsider x as Element of H by B1;
phi.x in H & x is Element of G by A1,GROUP_2:42;
hence y in the carrier of H by B2,B3,Th1;
end;
then rng(phi|H) c= the carrier of H;
then the carrier of Image(phi|H) c= the carrier of H by GROUP_6:44;
hence Image(phi|H) is Subgroup of H by GROUP_2:57;
end;
theorem Th45:
for G being Group
for A being non empty Subset of G
st (for phi being Automorphism of G holds phi .: A = A)
holds gr A is characteristic
proof
let G be Group;
let A be non empty Subset of G;
assume A1: for phi being Automorphism of G holds phi .: A = A;
A2: for phi being Automorphism of G for a being Element of A holds phi.a in A
proof
let phi be Automorphism of G;
let a be Element of A;
dom phi = the carrier of G by FUNCT_2:def 1;
then phi.a in phi .: A by FUNCT_1:def 6;
hence phi.a in A by A1;
end;
set H = gr A;
for phi being Automorphism of G holds Image(phi|H) is Subgroup of H
proof
let phi be Automorphism of G;
B2: for h being Element of G st h in H holds phi.h in H
proof
let h be Element of G;
assume h in H;
then consider F1 being FinSequence of the carrier of G,
I being FinSequence of INT such that
C2: len F1 = len I and
C3: rng F1 c= A and
C4: Product(F1 |^ I) = h by GROUP_4:28;
deffunc F(Nat) = phi.(F1/.$1);
consider F2 being FinSequence such that
C5: len(F2) = len F1 and
C6: for k being Nat st k in dom F2 holds F2.k = F(k)
from FINSEQ_1:sch 2;
C7: dom F2 = dom F1 by C5,FINSEQ_3:29;
C8: F2 is FinSequence of the carrier of G & rng F2 c= A
proof
D1: for y being object st y in rng F2 holds y in A
proof
let y be object;
assume y in rng F2;
then consider k being object such that
E2: k in dom F2 and
E3: y = F2.k by FUNCT_1:def 3;
reconsider k as Element of NAT by E2;
set x = F1.k;
x in rng F1 by FUNCT_1:def 3, E2, C7;
then reconsider x as Element of A by C3;
E4: x = F1/.k by E2,C7,PARTFUN1:def 6;
y = phi.(F1/.k) by E2,E3,C6;
hence y in A by A2,E4;
end;
for y being object st y in rng F2 holds y in the carrier of G
proof
let y be object;
assume y in rng F2;
then y in A by D1;
hence y in the carrier of G;
end;
hence rng F2 c= the carrier of G;
thus rng F2 c= A by D1;
end;
then reconsider F2 as FinSequence of the carrier of G;
set h2 = Product(F2 |^ I);
(for k being Nat st k in dom F1
holds F2.k = phi.(F1.k)) & len F1 = len I & len F2 = len I
proof
thus (for k being Nat st k in dom F1 holds F2.k = phi.(F1.k))
proof
let k be Nat;
assume D1: k in dom F1;
then k in dom F2 by C5,FINSEQ_3:29;
then F2.k = phi.(F1/.k) by C6;
hence F2.k = phi.(F1.k) by D1,PARTFUN1:def 6;
end;
thus len F1 = len I by C2;
thus len F2 = len I by C2,C5;
end;
then len F2 = len I & rng F2 c= A & Product(F2 |^ I) = phi.h
by C4,C8,GROUP_9:125;
hence phi.h in H by GROUP_4:28;
end;
for h being Element of H holds phi.h in H
proof
let h be Element of H;
C1: h in H;
h is Element of G by GROUP_2:42;
hence phi.h in H by B2,C1;
end;
hence Image(phi|H) is Subgroup of H by Th44;
end;
hence gr A is characteristic by Th40;
end;
theorem
G` is characteristic
proof
A1: [.1_G,1_G.] in commutators G;
for phi being Automorphism of G holds phi .: commutators G = commutators G
by Th43;
hence thesis by A1,Th45;
end;
theorem Th47:
for G1,G2 being Group
for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2
holds f.:(a * H) = (f.a) * (f .: H)
proof
let G1,G2 be Group;
let H be Subgroup of G1;
let a be Element of G1;
let f be Homomorphism of G1,G2;
A1: dom f = the carrier of G1 by FUNCT_2:def 1;
for y being object st y in f.:(a * H) holds y in (f.a)*(f.:H)
proof
let y be object;
assume y in f .: (a * H);
then consider x being object such that
B1: x in the carrier of G1 & x in (a * H) and
B2: y = f.x by A1,FUNCT_1:def 6;
consider h being Element of G1 such that
B3: x = a*h & h in H by B1,GROUP_2:103;
B4: y = (f.a)*(f.h) by B2,B3,GROUP_6:def 6;
dom f = the carrier of G1 & h in H & h in G1 by B3,FUNCT_2:def 1;
then f.h in f.:(the carrier of H) by FUNCT_1:def 6;
then f.h in f.:H by GRSOLV_1:8;
hence y in (f.a) * (f .: H) by B4,GROUP_2:103;
end;
then A1: f.:(a * H) c= (f.a) * (f .: H);
for y being object st y in (f.a)*(f.:H) holds y in f.:(a * H)
proof
let y be object;
assume y in (f.a)*(f.:H);
then consider g being Element of G2 such that
B1: y = (f.a)*g and
B2: g in (f.:H) by GROUP_2:103;
g in Image(f|H) by B2,GRSOLV_1:def 3;
then consider x being Element of H such that
B3: g = (f|H).x by GROUP_6:45;
B4: x in H & x is Element of G1 by GROUP_2:42;
reconsider x as Element of G1 by GROUP_2:42;
B5: y = (f.a)*(f.x) by B1,B3,B4,Th1
.= f.(a*x) by GROUP_6:def 6;
a*x in the carrier of G1 & dom f = the carrier of G1 by FUNCT_2:def 1;
then (a*x) in dom f & (a*x) in a*H & y=f.(a*x) by B4,B5,GROUP_2:103;
hence y in f.:(a * H) by FUNCT_1:def 6;
end;
then (f.a) * (f .: H) c= f.:(a * H);
hence f.:(a * H) = (f.a) * (f .: H) by A1,XBOOLE_0:def 10;
end;
theorem Th48:
for G1,G2 being Group
for H being Subgroup of G1
for a being Element of G1
for f being Homomorphism of G1,G2
holds f.:(H * a) = (f .: H) * (f.a)
proof
let G1,G2 be Group;
let H be Subgroup of G1;
let a be Element of G1;
let f be Homomorphism of G1,G2;
A1: dom f = the carrier of G1 by FUNCT_2:def 1;
for y being object st y in f.:(H * a) holds y in (f.:H)*(f.a)
proof
let y be object;
assume y in f .: (H * a);
then consider x being object such that
B1: x in the carrier of G1 & x in (H * a) and
B2: y = f.x by A1,FUNCT_1:def 6;
consider h being Element of G1 such that
B3: x = h*a & h in H by B1,GROUP_2:104;
dom f = the carrier of G1 & h in H & h in G1 by FUNCT_2:def 1, B3;
then f.h in f.:(the carrier of H) by FUNCT_1:def 6;
then f.h in f.:H by GRSOLV_1:8;
then (f.h)*(f.a) in (f.:H)*(f.a) by GROUP_2:104;
hence thesis by B2,B3,GROUP_6:def 6;
end;
then A2: f.:(H * a) c= (f .: H) * (f.a);
for y being object st y in (f.:H)*(f.a) holds y in f.:(H * a)
proof
let y be object;
assume y in (f.:H)*(f.a);
then consider g being Element of G2 such that
B1: y = g*(f.a) and
B2: g in (f.:H) by GROUP_2:104;
g in Image(f|H) by B2,GRSOLV_1:def 3;
then consider x being Element of H such that
B3: g = (f|H).x by GROUP_6:45;
B4: x in H & x is Element of G1 by GROUP_2:42;
reconsider x as Element of G1 by GROUP_2:42;
B5: y = (f.x)*(f.a) by B1,B3,B4,Th1
.= f.(x*a) by GROUP_6:def 6;
x*a in the carrier of G1 & dom f = the carrier of G1 by FUNCT_2:def 1;
then (x*a) in dom f & (x*a) in H*a & y=f.(x*a) by B4,B5,GROUP_2:104;
hence y in f.:(H * a) by FUNCT_1:def 6;
end;
then (f .: H) * (f.a) c= f.:(H * a);
hence f.:(H * a) = (f .: H)*(f.a) by A2,XBOOLE_0:def 10;
end;
theorem Th49:
for G being Group
for N being strict normal Subgroup of G
for phi being Automorphism of G
holds Image(phi|N) is normal Subgroup of G
proof
let G be Group;
let N be strict normal Subgroup of G;
let phi be Automorphism of G;
set H = Image(phi|N);
for g being Element of G holds g * H = H * g
proof
let g be Element of G;
set f = (phi").g;
B1: phi.f = g by Th4;
B2: phi .: (f * N) = (phi.f) * (phi .: N) by Th47
.= g * H by B1,GRSOLV_1:def 3;
phi .: (N * f) = (phi .: N)*(phi.f) by Th48
.= (phi .: N)*g by Th4
.= H*g by GRSOLV_1:def 3;
hence g * H = H * g by B2,GROUP_3:117;
end;
hence H is normal Subgroup of G by GROUP_3:117;
end;
theorem Th50:
for G being Group
for H being Subgroup of G
holds H is characteristic iff
(for phi being Automorphism of G
for x being Element of G
st x in H
holds phi.x in H)
proof
let G be Group;
let H be Subgroup of G;
thus H is characteristic implies (for phi being Automorphism of G
for x being Element of G
st x in H
holds phi.x in H)
proof
assume B1: H is characteristic;
let phi be Automorphism of G;
let x be Element of G;
assume B2: x in H;
B3: the multMagma of H = Image(phi|H) by B1
.= phi .: H by GRSOLV_1:def 3;
dom phi = the carrier of G by FUNCT_2:def 1;
then phi.x in phi .: (the carrier of H) by B2,FUNCT_1:def 6;
hence thesis by B3,GRSOLV_1:8;
end;
thus (for phi being Automorphism of G
for x being Element of G
st x in H
holds phi.x in H)
implies H is characteristic
proof
assume B1: for phi being Automorphism of G
for x being Element of G st x in H holds phi.x in H;
for phi being Automorphism of G holds Image(phi|H) is Subgroup of H
proof
let phi be Automorphism of G;
for x being Element of H holds phi.x in H
proof
let x be Element of H;
reconsider g=x as Element of G by GROUP_2:42;
g in H;
hence thesis by B1;
end;
hence Image(phi|H) is Subgroup of H by Th44;
end;
hence H is characteristic by Th40;
end;
end;
theorem
for G being Group
for H,K being strict characteristic Subgroup of G
holds H /\ K is characteristic Subgroup of G
proof
let G be Group;
let H,K be strict characteristic Subgroup of G;
for phi being Automorphism of G
for x being Element of G st x in H /\ K
holds phi.x in H /\ K
proof
let phi be Automorphism of G;
let x be Element of G;
assume x in H /\ K;
then B1: x in H & x in K by GROUP_2:82;
then B2: phi.x in H by Th50;
phi.x in K by B1,Th50;
hence phi.x in H /\ K by B2, GROUP_2:82;
end;
hence H /\ K is characteristic Subgroup of G by Th50;
end;
theorem
for G being Group
for H,K being strict characteristic Subgroup of G
holds H "\/" K is characteristic Subgroup of G
proof
let G be Group;
let H,K be strict characteristic Subgroup of G;
for phi being Automorphism of G
for g being Element of G st g in H "\/" K
holds phi.g in H "\/" K
proof
let phi be Automorphism of G;
let g be Element of G;
assume g in H "\/" K;
then g in H*K by GROUP_4:53;
then consider h, k being Element of G such that
B1: g = h*k and
B2: h in carr H and
B3: k in carr K;
h in H by B2;
then B4: phi.h in H by Th50;
k in K by B3;
then phi.k in K by Th50;
then phi.h * phi.k in carr H*carr K by B4;
then phi.g in H*K by B1,GROUP_6:def 6;
hence phi.g in H "\/" K by GROUP_4:53;
end;
hence H "\/" K is characteristic Subgroup of G by Th50;
end;
theorem Th53:
for G being Group
for H,K being strict characteristic Subgroup of G
for phi being Automorphism of G
holds phi .: commutators(H,K) = commutators(H,K)
proof
let G be Group;
let H,K be strict characteristic Subgroup of G;
let phi be Automorphism of G;
A1: dom phi = the carrier of G by FUNCT_2:def 1;
for x being object st x in commutators(H,K) holds
x in phi .: commutators(H,K)
proof
let x be object;
assume B0: x in commutators(H,K);
then reconsider g=x as Element of G;
consider h,k being Element of G such that
B1: x = [.h,k.] and
B2: h in H & k in K by B0,GROUP_5:52;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
set a = psi.h;
set b = psi.k;
B3: a in H & b in K by B2,Th50;
B4: psi.x = [.a,b.] by B1,GROUP_6:34;
B5: phi.([. a,b .]) = g by B4,Th4;
[. a, b .] in commutators(H,K) by B3;
hence x in phi .: commutators(H,K) by B5,A1,FUNCT_1:def 6;
end;
then A2: commutators(H,K) c= phi .: commutators(H,K);
for y being object st y in phi .: commutators(H,K) holds
y in commutators(H,K)
proof
let y be object;
assume y in phi .: commutators(H,K);
then consider x being object such that
B2: x in dom phi & x in commutators(H,K) & y = phi.x
by FUNCT_1:def 6;
consider h,k being Element of G such that
B3: x = [.h,k.] and
B4: h in H & k in K by B2,GROUP_5:52;
B5: phi.h in H & phi.k in K by B4,Th50;
phi.x = [. phi.h, phi.k .] by B3,GROUP_6:34;
hence y in commutators(H,K) by B2,B5;
end;
then phi .: commutators(H,K) c= commutators(H,K);
hence phi .: commutators(H,K) = commutators(H,K) by A2,XBOOLE_0:def 10;
end;
theorem
for G being Group
for H,K being strict characteristic Subgroup of G
holds [.H,K.] is characteristic Subgroup of G
proof
let G be Group;
let H,K be strict characteristic Subgroup of G;
set A = commutators(H,K);
reconsider A as non empty Subset of G by GROUP_5:53;
for phi being Automorphism of G holds phi .: A = A by Th53;
hence [.H,K.] is characteristic Subgroup of G by Th45;
end;
begin :: Results concerning meets
scheme :: sch3
MeetIsMinimal{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]} &
(for K being strict Subgroup of G() st P[K] holds H is Subgroup of K)
provided
A1: ex H being strict Subgroup of G() st P[H]
proof
set Fam = {A where A is Subset of G() : ex H being strict Subgroup of G()
st A = the carrier of H & P[H]};
consider H being strict Subgroup of G() such that
A2: 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]}
from GROUP_4:sch 1(A1);
take H;
for K being strict Subgroup of G() st P[K] holds H is Subgroup of K
proof
let K be strict Subgroup of G();
assume P[K];
then carr K in Fam;
hence H is Subgroup of K by A2,GROUP_2:57,SETFAM_1:3;
end;
hence thesis by A2;
end;
theorem Th55:
for G being Group
for H1,H2 being Subgroup of G
st H1 is Subgroup of H2
for a being Element of G
holds H1 |^ a is Subgroup of H2 |^ a
proof
let G be Group;
let H1,H2 be Subgroup of G;
assume A1: H1 is Subgroup of H2;
let a be Element of G;
for h being Element of G st h in H1 |^ a holds h in H2 |^ a
proof
let h be Element of G;
assume h in H1 |^ a;
then consider g being Element of G such that
B1: h = g |^ a & g in H1
by GROUP_3:58;
g in H2 by A1,B1,GROUP_2:40;
hence thesis by B1,GROUP_3:58;
end;
hence H1 |^ a is Subgroup of H2 |^ a by GROUP_2:58;
end;
scheme :: sch4
MeetOfNormsIsNormal{G() -> Group, P[set]} :
for H being strict Subgroup of G()
st the carrier of H = meet {A where A is Subset of G() :
ex N being strict Subgroup of G()
st A = the carrier of N & N is normal & P[N]}
holds H is strict normal Subgroup of G()
provided
A1: ex H being strict normal Subgroup of G() st P[H]
proof
defpred IsNorm[Subgroup of G()] means $1 is normal Subgroup of G();
set Fam = {A where A is Subset of G() : ex N being strict Subgroup of G()
st A = the carrier of N &
N is normal & P[N]};
let H be strict Subgroup of G();
assume A2: the carrier of H = meet Fam;
A3: Fam <> {}
proof
consider N being strict normal Subgroup of G() such that
B1: P[N] by A1;
carr N in Fam by B1;
hence thesis;
end;
A4: for N being strict normal Subgroup of G() st P[N] holds
H is Subgroup of N
proof
let N be strict normal Subgroup of G();
assume P[N];
then carr N in Fam;
hence H is Subgroup of N by A2,GROUP_2:57,SETFAM_1:3;
end;
A5: for N being strict normal Subgroup of G() st carr N in Fam holds P[N]
proof
let N be strict normal Subgroup of G();
assume B1: carr N in Fam;
consider A being Subset of G() such that
B2: A = carr N;
consider A0 being Subset of G() such that
B3: A = A0 and
B4: ex H0 being strict Subgroup of G()
st A0 = the carrier of H0 & H0 is normal & P[H0] by B1,B2;
consider H0 being strict Subgroup of G() such that
B5: A0 = the carrier of H0 & H0 is normal & P[H0] by B4;
thus P[N] by B2,B3,B5,GROUP_2:59;
end;
A6: for a being Element of G()
for N being strict normal Subgroup of G() st carr N in Fam
holds H |^ a is Subgroup of N
proof
let a be Element of G();
let N be strict normal Subgroup of G();
assume carr N in Fam;
then H is Subgroup of N by A4,A5;
then H |^ a is Subgroup of N |^ a by Th55;
hence H |^ a is Subgroup of N by GROUP_3:def 13;
end;
A7: for a being Element of G()
for N being strict normal Subgroup of G() st carr N in Fam
holds carr(H |^ a) c= carr N
proof
let a be Element of G();
let N be strict normal Subgroup of G();
assume carr N in Fam;
then H |^ a is Subgroup of N by A6;
hence carr(H |^ a) c= carr N by GROUP_2:def 5;
end;
for a being Element of G() holds H |^ a is Subgroup of H
proof
let a be Element of G();
B1: for A being Subset of G() st A in Fam holds carr(H |^ a) c= A
proof
let A be Subset of G();
assume A in Fam;
then consider A0 being Subset of G() such that
C1: A = A0 and
C2: ex H0 being strict Subgroup of G()
st A0 = the carrier of H0 & H0 is normal & P[H0];
consider H0 being strict Subgroup of G() such that
C3: A0 = the carrier of H0 & H0 is normal & P[H0] by C2;
reconsider H0 as strict normal Subgroup of G() by C3;
carr H0 in Fam by C3;
hence carr(H |^ a) c= A by A7,C1,C3;
end;
for x being object st x in carr (H |^ a) holds x in meet Fam
proof
let x be object;
assume C1: x in carr(H |^ a);
for A being set st A in Fam holds x in A
proof
let A be set;
assume C2: A in Fam;
then consider A0 being Subset of G() such that
C3: A0 = A and
ex H0 being strict Subgroup of G()
st A0 = the carrier of H0 & H0 is normal & P[H0];
carr(H |^ a) c= A0 by C2,C3,B1;
hence thesis by C1,C3;
end;
hence thesis by A3,SETFAM_1:def 1;
end;
then carr (H |^ a) c= meet Fam;
hence thesis by A2,GROUP_2:57;
end;
hence thesis by GROUP_3:122;
end;
theorem
for G being Group
for X being finite set
st X <> {} & (for A being Element of X
ex N being strict normal Subgroup of G
st A = the carrier of N)
ex N being strict normal Subgroup of G
st the carrier of N = meet X
proof
let G be Group;
let X be finite set;
assume A1: X <> {};
assume A2: for A being Element of X
ex N being strict normal Subgroup of G
st A = the carrier of N;
defpred P[Group] means $1 is normal Subgroup of G & the carrier of $1 in X;
set Fam = {A where A is Subset of G : ex N being strict Subgroup of G
st A = the carrier of N & P[N]};
set Fam2 = {A where A is Subset of G : ex N being strict Subgroup of G
st A = the carrier of N &
N is normal & P[N]};
A3: ex H being strict Subgroup of G st P[H]
proof
consider A being object such that
B1: A in X by A1,XBOOLE_0:def 1;
reconsider A as Element of X by B1;
consider H being strict normal Subgroup of G such that
B2: A = the carrier of H by A2;
take H;
thus P[H] by B1,B2;
end;
consider N being strict Subgroup of G such that
A4: the carrier of N = meet Fam from GROUP_4:sch 1(A3);
for A being object holds A in Fam iff A in Fam2
proof
let A be object;
thus A in Fam implies A in Fam2
proof
assume A in Fam;
then consider A0 being Subset of G such that
B1: A = A0 and
B2: ex N being strict Subgroup of G st A0 = the carrier of N & P[N];
consider N being strict Subgroup of G such that
B3: A0 = the carrier of N & P[N] by B2;
thus A in Fam2 by B1,B3;
end;
thus A in Fam2 implies A in Fam
proof
assume A in Fam2;
then consider A0 being Subset of G such that
B1: A = A0 &
ex N being strict Subgroup of G
st A0 = the carrier of N & N is normal & P[N];
thus A in Fam by B1;
end;
end;
then A5: Fam = Fam2 by TARSKI:2;
A6: ex H being strict normal Subgroup of G st P[H] by A3;
for H being strict Subgroup of G st the carrier of H = meet Fam2
holds H is strict normal Subgroup of G
from MeetOfNormsIsNormal(A6);
then reconsider N as strict normal Subgroup of G by A4,A5;
take N;
for A being object holds A in Fam iff A in X
proof
let A be object;
thus A in Fam implies A in X
proof
assume A in Fam;
then consider A0 being Subset of G such that
B1: A = A0 &
ex N being strict Subgroup of G st A0 = the carrier of N & P[N];
thus thesis by B1;
end;
thus A in X implies A in Fam
proof
assume B1: A in X;
then consider N being strict normal Subgroup of G such that
B2: A = the carrier of N by A2;
A is Subset of G by B2,GROUP_2:def 5;
hence A in Fam by B1,B2;
end;
end;
hence the carrier of N = meet X by A4,TARSKI:2;
end;
begin :: Centralizer of Characteristic Subgroups is Characteristic
definition
let G be Group;
let A be Subset of G;
func Centralizer A -> strict Subgroup of G means
:Def4:
the carrier of it = { b where b is Element of G :
for a being Element of G st a in A holds a*b = b*a };
existence
proof
set Car = {b where b is Element of G :
for a being Element of G st a in A holds a*b = b*a };
C1: 1_G in Car
proof
for a being Element of G st a in A holds 1_G*a = a*1_G
proof
let a be Element of G;
assume a in A;
1_G*a = a by GROUP_1:def 4
.= a*1_G by GROUP_1:def 4;
hence thesis;
end;
hence thesis;
end;
for x being object st x in Car holds x in the carrier of G
proof
let x be object;
assume x in Car;
then ex g being Element of G
st x = g & (for a being Element of G st a in A holds a*g = g*a);
hence thesis;
end;
then C2: Car is Subset of G by TARSKI:def 3;
C3: for g1,g2 being Element of G st g1 in Car & g2 in Car
holds g1*g2 in Car
proof
let g1,g2 be Element of G;
assume B1: g1 in Car;
assume B2: g2 in Car;
B3: ex z1 being Element of G st (z1 = g1) & (for a being Element of G
st a in A holds a*z1 = z1*a) by B1;
B4: ex z2 being Element of G st (z2 = g2) & (for a being Element of G
st a in A holds a*z2 = z2*a) by B2;
for a being Element of G st a in A holds a*(g1*g2)=(g1*g2)*a
proof
let a be Element of G;
assume Z1: a in A;
a*(g1*g2) = (a*g1)*g2 by GROUP_1:def 3
.= (g1*a)*g2 by Z1,B3
.= g1*(a*g2) by GROUP_1:def 3
.= g1*(g2*a) by Z1,B4
.= g1*g2*a by GROUP_1:def 3;
hence thesis;
end;
hence thesis;
end;
for g being Element of G st g in Car holds g" in Car
proof
let g be Element of G;
assume g in Car;
then Z1: ex z1 being Element of G st (z1 = g) & (for a being
Element of G st a in A holds z1*a=a*z1);
for a being Element of G st a in A holds g" * a = a * g"
proof
let a be Element of G;
assume a in A;
then g" * ((a*g) * g") = g" * ((g*a) * g") by Z1
.= (g" * (g * a)) * g" by GROUP_1:def 3
.= ((g" * g) * a) * g" by GROUP_1:def 3
.= (1_G * a) * g" by GROUP_1:def 5
.= a * g" by GROUP_1:def 4;
hence g" * a = a * g" by GROUP_3:1;
end;
hence thesis;
end;
hence thesis by C1,C2,C3,GROUP_2:52;
end;
uniqueness
proof
let H1,H2 be strict Subgroup of G such that
A1: the carrier of H1 = {b where b is Element of G : for a being Element of G
st a in A
holds a*b = b*a } and
A2: the carrier of H2 = {b where b is Element of G : for a being Element of G
st a in A
holds a*b = b*a };
for g being Element of G holds g in H1 iff g in H2 by A1,A2;
hence thesis;
end;
end;
theorem Th57:
for G being Group
for A being Subset of G
for g being Element of G
holds (for a being Element of G st a in A holds g*a = a*g) iff
g is Element of Centralizer A
proof
let G be Group;
let A be Subset of G;
let g be Element of G;
A1: the carrier of Centralizer A = {b where b is Element of G : for a
being Element of G st a in A holds b*a=a*b} by Def4;
hereby
assume for a being Element of G st a in A holds g*a = a*g;
then g in the carrier of Centralizer A by A1;
hence g is Element of Centralizer A;
end;
assume g is Element of Centralizer A;
then g in the carrier of Centralizer A;
then ex b being Element of G st (b = g) & (for a being Element of G st a in A
holds b*a = a*b) by A1;
hence thesis;
end;
theorem
for G being Group
for A,B being Subset of G
st A c= B
holds Centralizer B is Subgroup of Centralizer A
proof
let G be Group;
let A,B be Subset of G;
assume A1: A c= B;
for g being Element of G st g in Centralizer B
holds g in Centralizer A
proof
let g be Element of G;
assume g in Centralizer B;
then for a being Element of G st a in A
holds g*a = a*g by A1,Th57;
then g is Element of Centralizer A by Th57;
hence thesis;
end;
hence Centralizer B is Subgroup of Centralizer A by GROUP_2:58;
end;
definition
let G be Group;
let H be Subgroup of G;
func Centralizer H -> strict Subgroup of G means
:Def5:
it = Centralizer carr H;
correctness;
end;
theorem Th59:
for G being Group
for H being Subgroup of G
holds the carrier of Centralizer H = {b where b is Element of G : for a
being Element of G st a in H holds b*a=a*b}
proof
let G be Group;
let H be Subgroup of G;
set A = carr H;
set Car = {b where b is Element of G : for a being Element of G st a in H
holds b*a=a*b};
A1: the carrier of Centralizer A = {b where b is Element of G : for a
being Element of G st a in A holds b*a=a*b} by Def4;
for x being object st x in Car holds x in the carrier of Centralizer H
proof
let x be object;
assume B1: x in Car;
ex b being Element of G
st x = b & (for a being Element of G st a in carr(H) holds b*a=a*b)
proof
consider b being Element of G such that
B2: x = b and
B3: for a being Element of G st a in H holds b*a=a*b
by B1;
for a being Element of G st a in carr H holds b*a=a*b
proof
let a be Element of G;
assume a in carr H;
then a in H;
hence b*a=a*b by B3;
end;
hence thesis by B2;
end;
then x in the carrier of Centralizer carr H by A1;
hence thesis by Def5;
end;
then A3: Car c= the carrier of Centralizer H;
for x being object st x in the carrier of Centralizer H holds x in Car
proof
let x be object;
assume x in the carrier of Centralizer H;
then B1: x in the carrier of Centralizer carr H by Def5;
ex b being Element of G
st (x=b) & (for a being Element of G st a in H holds b*a=a*b)
proof
consider b being Element of G such that
Z1: x = b & (for a being Element of G st a in carr H holds b*a=a*b)
by A1,B1;
for a being Element of G st a in H holds b*a=a*b by Z1;
hence thesis by Z1;
end;
hence x in Car;
end;
then the carrier of Centralizer H c= Car;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th60:
for G being Group
for H being Subgroup of G
for g being Element of G
holds (for a being Element of G st a in H holds g*a = a*g) iff
g is Element of Centralizer H
proof
let G be Group;
let H be Subgroup of G;
let g be Element of G;
A1: the carrier of Centralizer H = {b where b is Element of G : for a
being Element of G st a in H holds b*a=a*b} by Th59;
hereby
assume for a being Element of G st a in H holds g*a = a*g;
then g in the carrier of Centralizer H by A1;
hence g is Element of Centralizer H;
end;
assume g is Element of Centralizer H;
then g in the carrier of Centralizer H;
then ex b being Element of G st (b = g) & (for a being Element of G st a in H
holds b*a = a*b) by A1;
hence thesis;
end;
theorem
for G being Group
for A being Subset of G
holds A is Subset of Centralizer (Centralizer A)
proof
let G be Group;
let A be Subset of G;
set H = Centralizer A;
for g being object
st g in A
holds g in the carrier of Centralizer H
proof
let g be object;
assume B1: g in A;
then reconsider g as Element of G;
for h being Element of G st h in H
holds g*h = h*g by B1,Th57;
then g is Element of Centralizer H by Th60;
hence thesis;
end;
then A c= the carrier of Centralizer H;
hence A is Subset of Centralizer H;
end;
theorem
for G being Group
for K being strict characteristic Subgroup of G
holds (Centralizer K) is characteristic Subgroup of G
proof
let G be Group;
let K be strict characteristic Subgroup of G;
for phi being Automorphism of G
for x being Element of G
st x in Centralizer K
holds phi.x in Centralizer K
proof
let phi be Automorphism of G;
let x be Element of G;
assume B1: x in Centralizer K;
set y = phi.x;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
for k being Element of G st k in K holds y*k = k*y
proof
let k be Element of G;
assume C1: k in K;
set j = psi.k;
phi.(x*j) = phi.(j*x) by B1,C1,Th50,Th60
.= phi.j * phi.x by GROUP_6:def 6;
then y * phi.(psi.k) = phi.(psi.k) * y by GROUP_6:def 6
.= k * y by Th4;
hence y * k = k * y by Th4;
end;
then y is Element of Centralizer K by Th60;
hence thesis;
end;
hence Centralizer K is characteristic Subgroup of G by Th50;
end;
definition
let G be Group;
let a be Element of G;
redefine func {a} -> Subset of G; :: redefines { (TARSKI, definition)
coherence
proof
for x being object st x in {a}
holds x in the carrier of G
proof
let x be object;
assume x in {a};
then x = a by TARSKI:def 1;
hence thesis;
end;
then {a} c= the carrier of G;
hence {a} is Subset of G;
end;
end;
definition
let G be Group;
let a be Element of G;
func Normalizer a -> strict Subgroup of G equals
Normalizer{a};
correctness;
end;
theorem Th64:
for G being Group
for a,x being Element of G
holds x in Normalizer a iff ex h being Element of G st x = h & a |^ h = a
proof
let G be Group;
let a,x be Element of G;
A1: x in Normalizer{a} iff ex h being Element of G st x = h & {a} |^ h = {a}
by GROUP_3:129;
{a} |^ x = {a |^ x} by GROUP_3:37;
then x in Normalizer{a} iff a |^ x = a by A1,ZFMISC_1:3;
hence thesis;
end;
theorem
for G being Group
for A being non empty Subset of G
holds the carrier of Centralizer A = meet {B where B is Subset of G :
ex H being strict Subgroup of G st B = the carrier of H &
(ex a being Element of G st a in A & H = Normalizer a)}
proof
let G be Group;
let A be non empty Subset of G;
defpred P[strict Subgroup of G] means (ex a being Element of G
st a in A & $1 = Normalizer a);
set Fam = {B where B is Subset of G :
ex H being strict Subgroup of G st B = the carrier of H & P[H]};
A1: Fam <> {}
proof
consider a being object such that
B1: a in A
by XBOOLE_0:def 1;
reconsider a as Element of G by B1;
consider H being strict Subgroup of G such that
B2: H = Normalizer a;
carr H in Fam by B1,B2;
hence thesis;
end;
for x being object st x in the carrier of Centralizer A
holds x in meet Fam
proof
let x be object;
assume B1: x in the carrier of Centralizer A;
then x in Centralizer A;
then x in G by GROUP_2:40;
then reconsider g = x as Element of G;
for X being set st X in Fam holds x in X
proof
let X be set;
assume X in Fam;
then consider B being Subset of G such that
C1: B = X and
C2: ex H being strict Subgroup of G
st B = the carrier of H &
(ex a being Element of G st a in A & H = Normalizer a);
consider H being strict Subgroup of G, a being Element of G such that
C3: B = the carrier of H & a in A & H = Normalizer a by C2;
C4: a |^ g = g" * (a * g) by GROUP_1:def 3
.= g" * (g * a) by B1,C3,Th57
.= (g" * g) * a by GROUP_1:def 3
.= (1_G) * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
{a} |^ g = {a} by C4,GROUP_3:37;
then g in Normalizer a by GROUP_3:129;
hence x in X by C1,C3;
end;
hence x in meet Fam by A1,SETFAM_1:def 1;
end;
then A2: the carrier of Centralizer A c= meet Fam;
for x being object st x in meet Fam
holds x in the carrier of Centralizer A
proof
let x be object;
assume B1: x in meet Fam;
B2: ex H being strict Subgroup of G st P[H]
proof
consider X being object such that
C1: X in Fam by A1, XBOOLE_0:def 1;
consider B being Subset of G such that
C2: B = X & ex H being strict Subgroup of G st
B = the carrier of H & P[H] by C1;
thus thesis by C2;
end;
consider K being strict Subgroup of G such that
B3: the carrier of K = meet Fam
from GROUP_4:sch 1(B2);
reconsider g = x as Element of G by B1,B3,GROUP_2:42;
B4: for a being Element of G st a in A
holds g in Normalizer a
proof
let a be Element of G;
assume a in A;
then carr Normalizer a in Fam;
hence g in Normalizer a by B1,SETFAM_1:def 1;
end;
for a being Element of G st a in A holds g*a = a*g
proof
let a be Element of G;
assume a in A;
then g in Normalizer a by B4;
then consider h being Element of G such that
C1: g = h & a |^ h = a by Th64;
C2: a = g" * (a * g) by C1,GROUP_1:def 3;
g * a = (g * g") * (a * g) by C2,GROUP_1:def 3
.= 1_G * (a * g) by GROUP_1:def 5
.= a * g by GROUP_1:def 4;
hence g*a = a*g;
end;
then g is Element of Centralizer A by Th57;
hence thesis;
end;
then meet Fam c= the carrier of Centralizer A;
hence thesis by A2, XBOOLE_0:def 10;
end;
theorem Th66:
for G being finite Group
for H1,H2 being strict Subgroup of G
st card(H1 /\ H2) = card H1 & card(H1 /\ H2) = card H2
holds H1 = H2
proof
let G be finite Group;
let H1,H2 be strict Subgroup of G;
assume A1: card(H1 /\ H2) = card H1;
assume A2: card(H1 /\ H2) = card H2;
A3: H1 /\ H2 = H1
proof
reconsider H12 = H1 /\ H2 as strict Subgroup of H1 by GROUP_2:88;
multMagma(# the carrier of H12, the multF of H12 #)
= multMagma(# the carrier of H1, the multF of H1 #) by A1,GROUP_2:73;
hence thesis;
end;
H1 /\ H2 = H2
proof
reconsider H12 = H1 /\ H2 as strict Subgroup of H2 by GROUP_2:88;
multMagma(# the carrier of H12, the multF of H12 #)
= multMagma(# the carrier of H2, the multF of H2 #) by A2,GROUP_2:73;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th69:
for G1,G2 being finite Group
for N1 being normal Subgroup of G1
for N2 being normal Subgroup of G2
st G1./.N1, G2./.N2 are_isomorphic
holds card(N2)*card(G1)=card(N1)*card(G2)
proof
let G1,G2 be finite Group;
let N1 be normal Subgroup of G1;
let N2 be normal Subgroup of G2;
assume G1./.N1, G2./.N2 are_isomorphic;
then A1: card(G1./.N1) = card(G2./.N2) by GROUP_6:73
.= index N2 by GROUP_6:27;
set k = index N1;
A2: card(G1) = card(N1) * k by GROUP_2:147;
card(G2) = card(N2) * index(N2) by GROUP_2:147
.= card(N2) * k by A1,GROUP_6:27;
hence thesis by A2;
end;
theorem Th70:
for G being finite Group
for K,N being strict normal Subgroup of G
for m,d being Nat
st m = card N & m = card K & d = card(K /\ N)
holds d*card(N "\/" K) = m*m
proof
let G be finite Group;
let K,N be strict normal Subgroup of G;
let m,d be Nat;
assume A1: m = card N;
assume A2: m = card K;
assume A3: d = card(K /\ N);
reconsider B=K as Subgroup of G;
A4: N is Subgroup of B "\/" N by GROUP_4:60;
(B "\/" N)./.(B "\/" N,N)`*`, B./.(B /\ N) are_isomorphic by GROUP_6:81;
then d*card(B "\/" N) = card(B) * card((B "\/" N,N)`*`) by A3,Th69
.= m*m by A1,A2,A4,GROUP_6:def 1;
hence d*card(N "\/" K) = m*m;
end;
theorem
for G being finite Group
for N being strict normal Subgroup of G
st card N, index N are_coprime
holds N is characteristic Subgroup of G
proof
let G be finite Group;
let N be strict normal Subgroup of G;
assume A1: card N, index N are_coprime;
consider m being Nat such that
A2: m = card N;
consider n being Nat such that
A3: n = index N;
A4: card G = m*n by A2,A3,GROUP_2:147;
for phi being Automorphism of G holds Image(phi|N) = N
proof
let phi be Automorphism of G;
set K = Image(phi|N);
reconsider K as strict normal Subgroup of G by Th49;
K = phi .: N by GRSOLV_1:def 3;
then B1: card K = card N by Th19,GROUP_6:73;
set d = card(N /\ K);
d divides m
proof
N /\ K is Subgroup of N by GROUP_2:88;
hence thesis by A2,GROUP_2:148;
end;
then consider q being Nat such that
B2: m = d*q by NAT_D:def 3;
B3: q<>0 by A2,B2;
card(N "\/" K) = m*q
proof
K /\ N = N /\ K
proof
carr(K /\ N) = (carr K) /\ (carr N) by GROUP_2:def 10
.= carr(N /\ K) by GROUP_2:def 10;
hence thesis by GROUP_2:59;
end;
then d*card(N "\/" K) = m*(d*q) by A2,B1,B2,Th70
.= d*(m*q);
hence card(N "\/" K) = m*q by XCMPLX_1:5;
end;
then q divides n by A2,A4,Th67a,GROUP_2:148;
then q=1 by A1,A2,A3,B2,B3,Th68;
hence Image(phi|N) = N by A2,B1,B2,Th66;
end;
hence N is characteristic Subgroup of G by Def3;
end;
theorem Th72:
for G1,G2,G3 being Group
for f1 being Homomorphism of G1,G2
for f2 being Homomorphism of G2,G3
for A being Subgroup of G1
holds the multMagma of f2 .: (f1 .: A) = the multMagma of ((f2 * f1) .: A)
proof
let G1,G2,G3 be Group;
let f1 be Homomorphism of G1,G2;
let f2 be Homomorphism of G2,G3;
let A be Subgroup of G1;
for z being Element of G3
holds z in f2 .: (f1 .: A) iff z in (f2 * f1) .: A
proof
let z be Element of G3;
thus z in f2 .: (f1 .: A) implies z in (f2 * f1) .: A
proof
assume z in f2 .: (f1 .: A);
then z in f2 .: (the carrier of f1 .: A) by GRSOLV_1:8;
then consider y being object such that
A2: y in dom f2 and
A3: y in the carrier of (f1 .: A) and
A4: z = f2.y by FUNCT_1:def 6;
y in f1 .: (the carrier of A) by A3,GRSOLV_1:8;
then consider x being object such that
A5: x in dom f1 & x in the carrier of A & y = f1.x by FUNCT_1:def 6;
A6: x in dom(f2 * f1) by A2,A5,FUNCT_1:11;
then x in the carrier of A & z = (f2 * f1).x by A4,A5,FUNCT_1:12;
then z in (f2 * f1) .: the carrier of A by A6,FUNCT_1:def 6;
hence thesis by GRSOLV_1:8;
end;
thus z in (f2 * f1) .: A implies z in f2 .: (f1 .: A)
proof
assume z in (f2 * f1) .: A;
then z in (f2 * f1) .: the carrier of A by GRSOLV_1:8;
then consider x being object such that
A2: x in dom (f2 * f1) & x in the carrier of A & z = (f2 * f1).x
by FUNCT_1:def 6;
A3: x in dom f1 & f1.x in dom f2 by A2,FUNCT_1:11;
set y = f1.x;
x in dom f1 & x in the carrier of A & y = f1.x by A2,FUNCT_1:11;
then A5: y in f1 .: (the carrier of A) by FUNCT_1:def 6;
z = f2.y by A2,FUNCT_1:12;
then z in f2 .: (f1 .: (the carrier of A)) by A3,A5,FUNCT_1:def 6;
then z in f2 .: (the carrier of (f1 .: A)) by GRSOLV_1:8;
hence z in f2 .: (f1 .: A) by GRSOLV_1:8;
end;
end;
hence the multMagma of f2 .: (f1 .: A) = the multMagma of ((f2 * f1) .: A)
by GROUP_2:60;
end;
theorem Th73:
for G being Group
for N being strict normal Subgroup of G
for phi being Automorphism of G
st Image(phi|N) = N
ex sigma being Automorphism of G./.N
st (for x being Element of G holds sigma.(x*N) = (phi.x)*N)
proof
let G be Group;
let N be strict normal Subgroup of G;
let phi be Automorphism of G;
assume A1: Image(phi|N) = N;
defpred P[set,set] means ex a being Element of G st
$1 = a*N & $2 = (phi.a)*N;
A2: for x being Element of G./.N ex y being Element of G./.N st P[x,y]
proof
let x be Element of G./.N;
x in Cosets N;
then consider a being Element of G such that
B1: x = a*N by GROUP_2:def 15;
(phi.a)*N in Cosets N by GROUP_2:def 15;
then consider y being Element of G./.N such that
B2: y = (phi.a)*N;
take y;
thus P[x,y] by B1,B2;
end;
consider sigma being Function of G./.N, G./.N such that
A3: for x being Element of G./.N holds P[x, sigma.x]
from FUNCT_2:sch 3(A2);
A4: for a being Element of G holds sigma.(a*N) = (phi.a)*N
proof
let a be Element of G;
a*N in Cosets N by GROUP_2:def 15;
then consider x being Element of G./.N such that
B1: x = a*N;
consider b being Element of G such that
B2: x = b*N & sigma.x = (phi.b)*N by A3;
consider n being Element of G such that
B3: n = b" * a & n in N by B1,B2,GROUP_2:114;
B4: b*n = (b * b") * a by B3,GROUP_1:def 3
.= 1_G * a by GROUP_1:def 5
.= a by GROUP_1:def 4;
dom phi = the carrier of G & n in N by B3, FUNCT_2:def 1;
then phi.n in phi .: (the carrier of N) by FUNCT_1:def 6;
then phi.n in the carrier of (phi .: N) by GRSOLV_1:8;
then B5: phi.n in N by A1,GRSOLV_1:def 3;
phi.a * N = (phi.b * phi.n) * N by B4,GROUP_6:def 6
.= phi.b * (phi.n * N) by GROUP_2:105
.= sigma.x by B2,B5,GROUP_2:113;
hence thesis by B1;
end;
for x,y being Element of G./.N holds sigma.(x*y) = sigma.x * sigma.y
proof
let x,y be Element of G./.N;
consider a being Element of G such that
B1: x = a*N & sigma.x = (phi.a)*N by A3;
consider b being Element of G such that
B2: y = b*N & sigma.y = (phi.b)*N by A3;
B3: for g1,g2 being Element of G holds (g1*N)*(g2*N) = g1*g2*N
proof
let g1,g2 be Element of G;
(g1*N)*(g2*N) = (g1 * N) * (N * g2) by GROUP_3:117
.= g1 * N * N * g2 by GROUP_3:11
.= g1 * (N*N) * g2 by GROUP_4:45
.= g1 * N * g2 by GROUP_2:76
.= g1 * (N * g2) by GROUP_2:106
.= g1 * (g2 * N) by GROUP_3:117
.= g1 * g2 * N by GROUP_2:105;
hence thesis;
end;
B4: x * y = @x * @y by GROUP_6:def 3
.= a * b * N by B1,B2,B3;
sigma.x * sigma.y = @(sigma.x) * @(sigma.y) by GROUP_6:def 3
.= (phi.a) * (phi.b) * N by B1,B2,B3
.= phi.(a*b) * N by GROUP_6:def 6;
hence sigma.(x*y) = sigma.x * sigma.y by A4,B4;
end;
then reconsider sigma as Homomorphism of G./.N, G./.N by GROUP_6:def 6;
sigma is bijective
proof
B1: for x being Element of G holds x*N in Ker sigma iff x in N
proof
let x be Element of G;
reconsider z = x*N as Element of G./.N by GROUP_2:def 15;
C1: (phi").(phi.x) = x by FUNCT_2:26;
thus x*N in Ker sigma implies x in N
proof
assume (x*N) in Ker sigma;
then
D1: sigma.z = 1_(G./.N) by GROUP_6:41;
(phi.x)*N = sigma.(x*N) by A4
.= carr N by D1,GROUP_6:24;
then phi.x in Image(phi|N) by A1,GROUP_2:113;
then D2: phi.x in phi .: N by GRSOLV_1:def 3;
consider psi being Automorphism of G such that
D3: psi = phi" and
Image(phi|Image(psi|N)) = the multMagma of N by Th17;
reconsider i = id the carrier of G as Automorphism of G by GROUP_6:38;
the carrier of G <> {} & phi is onto;
then D4: psi * phi = id the carrier of G by D3,FUNCT_2:29;
dom psi = the carrier of G by FUNCT_2:def 1;
then psi.(phi.x) in psi .: (the carrier of (phi .: N))
by D2,FUNCT_1:def 6;
then psi.(phi.x) in the carrier of (psi .: (phi .: N)) by GRSOLV_1:8;
then x in i .: N by C1,D3,D4,Th72;
then D5: x in (id the carrier of G) .: (the carrier of N)
by GRSOLV_1:8;
the carrier of N is Subset of the carrier of G by GROUP_2:def 5;
hence x in N by D5;
end;
thus x in N implies x*N in Ker sigma
proof
assume x in N;
then D1: x * N = carr N by GROUP_2:113
.= 1_(G./.N) by GROUP_6:24;
then sigma.(x*N) = 1_(G./.N) by GROUP_6:31;
hence x*N in Ker sigma by D1,GROUP_6:41;
end;
end;
for x being Element of G./.N holds x in Ker sigma iff x in (1).(G./.N)
proof
let x be Element of G./.N;
thus x in Ker sigma implies x in (1).(G./.N)
proof
assume C1: x in Ker sigma;
x in G./.N;
then consider g being Element of G such that
C2: x = g*N by GROUP_2:def 15;
g*N = carr N by B1,C1,C2,GROUP_2:113;
then g*N = 1_(G./.N) by GROUP_6:24;
then g*N in {1_(G./.N)} by TARSKI:def 1;
hence x in (1).(G./.N) by C2,GROUP_2:def 7;
end;
thus x in (1).(G./.N) implies x in Ker sigma
proof
assume x in (1).(G./.N);
then x in {1_(G./.N)} by GROUP_2:def 7;
then x = 1_(G./.N) by TARSKI:def 1;
then sigma.x = 1_(G./.N) by GROUP_6:31;
hence x in Ker sigma by GROUP_6:41;
end;
end;
then Ker sigma = (1).(G./.N);
hence sigma is one-to-one by GROUP_6:56;
for y being Element of G./.N holds y in Image sigma
proof
let y be Element of G./.N;
y in G./.N;
then consider b being Element of G such that
C1: y = b*N by GROUP_2:def 15;
reconsider psi = phi" as Automorphism of G by GROUP_6:62;
consider a being Element of G such that
C2: a = psi.b;
a*N in G./.N by GROUP_2:def 15;
then consider x being Element of G./.N such that
C3: x = a*N;
C4: phi.a = b by C2,Th4;
sigma.x = y by A4,C3,C4,C1;
hence y in Image sigma by GROUP_6:45;
end;
hence sigma is onto by GROUP_2:62,GROUP_6:57;
end;
then reconsider sigma as Automorphism of G./.N;
take sigma;
let x be Element of G;
thus sigma.(x*N) = (phi.x)*N by A4;
end;
theorem
for G being finite Group
for H being strict characteristic Subgroup of G
for K being strict Subgroup of G
st H is Subgroup of K
holds H is normal Subgroup of K
proof
let G be finite Group;
let H be strict characteristic Subgroup of G;
let K be strict Subgroup of G;
assume A1: H is Subgroup of K;
A2: for g being Element of G
holds g in Ker (nat_hom H) iff g in H by GROUP_6:43;
reconsider R = Ker ((nat_hom H)|K) as strict Subgroup of K;
A3: for k being Element of K
holds k in H iff k in Ker ((nat_hom H)|K)
proof
let k be Element of K;
reconsider g=k as Element of G by GROUP_2:42;
B1: g in K;
thus k in H implies k in Ker ((nat_hom H)|K)
proof
assume C1: k in H;
C2: g in K;
(nat_hom H).g = 1_(G./.H) by A2,C1,GROUP_6:41;
then ((nat_hom H)|K).g = 1_(G./.H) by C2,Th1;
hence k in Ker ((nat_hom H)|K) by GROUP_6:41;
end;
thus k in Ker ((nat_hom H)|K) implies k in H
proof
assume C1: k in Ker ((nat_hom H)|K);
((nat_hom H)|K).g = (nat_hom H).g by B1,Th1;
then (nat_hom H).g = 1_(G./.H) by C1,GROUP_6:41;
then g in Ker (nat_hom H) by GROUP_6:41;
hence k in H by GROUP_6:43;
end;
end;
reconsider H1=H as strict Subgroup of K by A1;
the multMagma of R = the multMagma of H1 by A3,GROUP_2:60;
hence thesis;
end;
:: Gorenstein, Finite Groups, Theorem 2.1.2 (iv)
theorem
for G being finite Group
for H being strict characteristic Subgroup of G
for K being strict Subgroup of G
st H is Subgroup of K &
K./.(K,H)`*` is characteristic Subgroup of G./.H
holds K is characteristic Subgroup of G
proof
let G be finite Group;
let H be strict characteristic Subgroup of G;
let K be strict Subgroup of G;
assume A1: H is Subgroup of K;
assume A2: K./.(K,H)`*` is characteristic Subgroup of G./.H;
A3: (K,H)`*` = H by A1,GROUP_6:def 1;
for phi being Automorphism of G
for k being Element of G st k in K
holds phi.k in K
proof
let phi be Automorphism of G;
let k be Element of G;
assume B1: k in K;
Image(phi|H) = H by Def3;
then consider sigma being Automorphism of G./.H such that
B2: for x being Element of G holds sigma.(x*H) = (phi.x)*H
by Th73;
consider J being strict characteristic Subgroup of G./.H such that
B3: J = (K./.(K,H)`*`) by A2;
B4: for k1 being Element of G st k1*H in J holds k1 in K
proof
let k1 be Element of G;
assume C1: k1*H in J;
C2: k1*H = k1*(K,H)`*` by A1,GROUP_6:def 1;
set x = k1*(K,H)`*`;
consider a being Element of K such that
C3: x = a*(K,H)`*` by B3,C1,C2,GROUP_2:def 15;
reconsider a1 = a as Element of G by GROUP_2:42;
C4: a1 in K;
for j1 being object holds j1 in a*(K,H)`*` iff j1 in a1*H
proof
let j1 be object;
thus j1 in a*(K,H)`*` implies j1 in a1*H
proof
assume j1 in a*(K,H)`*`;
then consider g1 being Element of K such that
D1: j1 = a*g1 & g1 in (K,H)`*` by GROUP_2:103;
reconsider g=g1 as Element of G by GROUP_2:42;
D2: j1 = a1*g by D1,GROUP_2:43;
g in H by D1,A1,GROUP_6:def 1;
hence j1 in a1*H by D2,GROUP_2:103;
end;
assume j1 in a1*H;
then consider g1 being Element of G such that
D1: j1 = a1*g1 & g1 in H by GROUP_2:103;
reconsider g=g1 as Element of K by A1,D1,GROUP_2:42;
D2: j1 = a*g by D1,GROUP_2:43;
g in (K,H)`*` by D1,A1, GROUP_6:def 1;
hence j1 in a*(K,H)`*` by D2,GROUP_2:103;
end;
then a1*H = x by TARSKI:2,C3
.= k1*H by A1,GROUP_6:def 1;
then (a1") * k1 in H by GROUP_2:114;
then C5: (a1") * k1 in K by A1,GROUP_2:41;
a1 * ((a1") * k1) = (a1 * a1") * k1 by GROUP_1:def 3
.= 1_G * k1 by GROUP_1:def 5
.= k1 by GROUP_1:def 4;
hence k1 in K by C4,C5,GROUP_2:50;
end;
B5: for k1 being Element of G holds k1 in K iff k1*H in J
proof
let k1 be Element of G;
thus k1 in K implies k1*H in J
proof
assume k1 in K;
then reconsider k2=k1 as Element of K;
C1: k2*((K,H)`*`) in J by B3, GROUP_2:def 15;
for x being object holds x in k2*carr((K,H)`*`) iff x in k1*carr(H)
proof
let x be object;
thus x in k2*carr((K,H)`*`) implies x in k1*carr(H)
proof
assume E1: x in k2*carr((K,H)`*`);
x in k2*((K,H)`*`) iff
ex g being Element of K st (x = k2*g & g in (K,H)`*`)
by GROUP_2:103;
then consider huh being Element of K such that
E2: x = k2*huh & huh in (K,H)`*` by E1;
E3: huh in H by A1,E2,GROUP_6:def 1;
reconsider huh2=huh as Element of G by GROUP_2:42;
set x2 = k1*huh2;
x = k1*huh2 by E2,GROUP_2:43;
hence thesis by E3,GROUP_2:27;
end;
assume x in k1*carr(H);
then consider h1 being Element of G such that
D1: x = k1*h1 & h1 in carr(H) by GROUP_2:27;
reconsider h2=h1 as Element of K by A1,D1,GROUP_2:42;
reconsider H1=H as normal Subgroup of K by A3;
D2: the carrier of H = the carrier of ((K,H)`*`) by A1,GROUP_6:def 1;
k2*h2 in k2*carr(H1) by D1,GROUP_2:27;
hence x in k2*carr((K,H)`*`) by D1,D2,GROUP_2:43;
end;
then k2*carr(((K,H)`*`)) = k1*H by TARSKI:2;
hence k1*H in J by C1;
end;
thus k1*H in J implies k1 in K by B4;
end;
then k*H in J by B1;
then reconsider kH = k*H as Element of G./.H by GROUP_2:42;
sigma.(kH) in J by Th50,B1,B5;
then sigma.(k*H) in J & sigma.(k*H) = (phi.k)*H by B2;
hence phi.k in K by B4;
end;
hence K is characteristic Subgroup of G by Th50;
end;
theorem
for G being Group
for H being Subgroup of G
holds H is Subgroup of Centralizer H iff H is commutative Group
proof
let G be Group;
let H be Subgroup of G;
thus H is Subgroup of Centralizer H implies H is commutative Group
proof
assume A1: H is Subgroup of Centralizer H;
A2: for g,h being Element of G st g in H & h in H holds g*h=h*g
proof
let g,h be Element of G;
assume B1: g in H;
assume B2: h in H;
g in Centralizer H by B1,A1,GROUP_2:40;
hence g*h=h*g by B2,Th60;
end;
for g,h being Element of H holds g*h=h*g
proof
let g,h be Element of H;
B1: g in H & h in H;
reconsider g1=g, h1=h as Element of G by GROUP_2:42;
g*h = g1*h1 by GROUP_2:43
.= h1*g1 by A2,B1
.= h*g by GROUP_2:43;
hence thesis;
end;
hence thesis by GROUP_1:def 12;
end;
thus H is commutative Group implies H is Subgroup of Centralizer H
proof
assume A1: H is commutative Group;
A2: for g,h being Element of G st g in H & h in H holds g*h=h*g
proof
let g,h be Element of G;
assume B1: g in H;
assume B2: h in H;
reconsider g1=g,h1=h as Element of H by B1,B2;
g*h = g1*h1 by GROUP_2:43
.= h1*g1 by A1,GROUP_1:def 12
.= h*g by GROUP_2:43;
hence g*h=h*g;
end;
for g being Element of G st g in H holds g in Centralizer H
proof
let g be Element of G;
assume B1: g in H;
for a being Element of G st a in H holds g*a = a*g by B1,A2;
then g is Element of Centralizer H by Th60;
hence g in Centralizer H;
end;
hence thesis by GROUP_2:58;
end;
end;
theorem
for G being Group
holds Centralizer (Omega).G = center G
proof
let G be Group;
for g being Element of G holds g in Centralizer (Omega).G iff g in center G
proof
let g be Element of G;
thus g in Centralizer (Omega).G implies g in center G
proof
assume A1: g in Centralizer (Omega).G;
for a being Element of G holds g*a = a*g
proof
let a be Element of G;
a in (Omega).G;
hence g*a = a*g by A1,Th60;
end;
hence g in center G by GROUP_5:77;
end;
thus g in center G implies g in Centralizer (Omega).G
proof
assume g in center G;
then for b being Element of G st b in (Omega).G holds g*b = b*g
by GROUP_5:77;
then g is Element of Centralizer (Omega).G by Th60;
hence thesis;
end;
end;
hence Centralizer (Omega).G = center G;
end;
theorem
for G being Group
for N being normal Subgroup of G
holds Centralizer N is normal Subgroup of G
proof
let G be Group;
let N be normal Subgroup of G;
A1: for g,n being Element of G st n in N holds n |^ g in N
proof
let g,n be Element of G;
assume B1: n in N;
B2: the multMagma of N = the multMagma of (N |^ g) by GROUP_3:def 13;
n |^ g in N |^ g by B1,GROUP_3:58;
hence thesis by B2;
end;
A2: for g,x,n being Element of G st x in Centralizer N & n in N
holds (x |^ g)*n = n*(x |^ g)
proof
let g,x,n be Element of G;
assume B1: x in Centralizer N;
assume B2: n in N;
consider n2 being Element of G such that
B3: n2 = g * n * g";
B4: n2 = n |^ g" by B3;
then (x * n2) |^ g = (n2 * x) |^ g by B1,B2,A1,Th60
.= (n2 |^ g) * (x |^ g) by GROUP_3:23;
then (x |^ g) * (n2 |^ g) = (n2 |^ g) * (x |^ g) by GROUP_3:23
.= n * (x |^ g) by B4,GROUP_3:25;
hence (x |^ g) * n = n * (x |^ g) by B4,GROUP_3:25;
end;
A3: for g,z being Element of G st z in Centralizer N
holds z |^ g in Centralizer N
proof
let g,z be Element of G;
assume z in Centralizer N;
then for n being Element of G st n in N holds
(z |^ g)*n = n*(z |^ g) by A2;
then (z |^ g) is Element of Centralizer N by Th60;
hence z |^ g in Centralizer N;
end;
for g being Element of G holds (Centralizer N) |^ g = Centralizer N
proof
let g be Element of G;
for z being Element of G
holds z in (Centralizer N) |^ g iff z in (Centralizer N)
proof
let z be Element of G;
hereby
assume z in (Centralizer N) |^ g;
then (z |^ g") in ((Centralizer N) |^ g) |^ g" by GROUP_3:58;
then (z |^ g") in Centralizer N by GROUP_3:62;
then (z |^ g") |^ g in Centralizer N by A3;
hence z in (Centralizer N) by GROUP_3:25;
end;
assume z in (Centralizer N);
then (z |^ g") |^ g in (Centralizer N) |^ g by A3,GROUP_3:58;
hence z in (Centralizer N) |^ g by GROUP_3:25;
end;
hence (Centralizer N) |^ g = Centralizer N;
end;
hence Centralizer N is normal Subgroup of G by GROUP_3:def 13;
end;
theorem Th79:
for G being Group
for H being Subgroup of G
for h,n being Element of G
st h in H & n in Normalizer H
holds h |^ n in H
proof
let G be Group;
let H be Subgroup of G;
let h,n be Element of G;
assume A1: h in H;
assume n in Normalizer H;
then consider g being Element of G such that
A2: n" = g & (carr H) |^ g = carr H by GROUP_2:51,GROUP_3:129;
consider h1 being Element of G such that
A3: h = h1 |^ g & h1 in carr H by A1,A2,GROUP_3:41;
h |^ n = h1 by A2,A3,GROUP_3:25;
hence h |^ n in H by A3;
end;
theorem Th80:
for G being Group
for H being Subgroup of G
holds H is Subgroup of Normalizer H
proof
let G be Group;
let H be Subgroup of G;
A1: for g being Element of G st g in H
for x being Element of G st x in (carr H) |^ g holds x in carr H
proof
let g be Element of G;
assume B1: g in H;
let x be Element of G;
assume x in (carr H) |^ g;
then consider h being Element of G such that
B2: x = h |^ g & h in carr H by GROUP_3:41;
B3: h in H by B2;
g" in H by B1,GROUP_2:51;
then g" * h in H by B3, GROUP_2:50;
then x in H by B1,B2, GROUP_2:50;
hence x in carr H;
end;
for g being Element of G st g in H holds g in Normalizer H
proof
let g be Element of G;
assume B1: g in H;
for x being Element of G st x in carr H holds x in (carr H) |^ g
proof
let x be Element of G;
thus x in carr H implies x in (carr H) |^ g
proof
assume x in carr H;
then C1: x in H;
set h = x |^ g";
g" in H by B1,GROUP_2:51;
then x * g" in H by C1,GROUP_2:50;
then g * (x * g") in H by B1,GROUP_2:50;
then C2: h in (carr H) by GROUP_1:def 3;
h |^ g = x by GROUP_3:25;
hence x in (carr H) |^ g by C2,GROUP_3:41;
end;
end;
then (carr H) |^ g c= carr H & carr H c= (carr H) |^ g by A1,B1;
then (carr H) |^ g = carr H by XBOOLE_0:def 10;
hence g in Normalizer H by GROUP_3:129;
end;
hence H is Subgroup of Normalizer H by GROUP_2:58;
end;
Lm8:
for G being Group
for H being Subgroup of G
holds Centralizer H is strict Subgroup of Normalizer H
proof
let G be Group;
let H be Subgroup of G;
set Z = Centralizer H;
for g being Element of G st g in Centralizer H holds g in Normalizer H
proof
let g be Element of G;
assume A1: g in Centralizer H;
A2: for a being Element of G st a in H holds a = (g")*a*g
proof
let a be Element of G;
assume a in H;
then g" * (a * g) = g" * (g*a) by A1,Th60
.= (g" * g)*a by GROUP_1:def 3
.= (1_G)*a by GROUP_1:def 5
.= a by GROUP_1:def 4;
hence a = (g")*a*g by GROUP_1:def 3;
end;
for a being Element of G holds a in H iff a in (H |^ g)
proof
let a be Element of G;
thus a in H implies a in H |^ g
proof
assume B1: a in H;
then a = a |^ g by A2;
hence a in H |^ g by B1, GROUP_3:58;
end;
thus a in H |^ g implies a in H
proof
assume a in H |^ g;
then consider h being Element of G such that
B1: a = h |^ g & h in H by GROUP_3:58;
thus a in H by A2,B1;
end;
end;
then the multMagma of H = the multMagma of (H |^ g) by GROUP_2:60;
then carr H = carr(H) |^ g by GROUP_3:def 6;
hence g in Normalizer H by GROUP_3:129;
end;
hence Centralizer H is strict Subgroup of Normalizer H by GROUP_2:58;
end;
theorem
for G being Group
for H being Subgroup of G
holds Centralizer H is strict normal Subgroup of Normalizer H
proof
let G be Group;
let H be Subgroup of G;
(Centralizer H) is normal Subgroup of Normalizer H
proof
reconsider Z=Centralizer H as strict Subgroup of Normalizer H by Lm8;
set N = Normalizer H;
B60: for z being Element of N
holds (for n being Element of N st n in H holds z*n = n*z) iff
z is Element of Z
proof
let z be Element of N;
reconsider z1=z as Element of G by GROUP_2:42;
C1: z is Element of Z implies (for n being Element of N st n in H
holds z*n = n*z)
proof
assume D1: z is Element of Z;
let n be Element of N;
assume D2: n in H;
reconsider n1=n as Element of G by GROUP_2:42;
z1*n1 = n1*z1 by D1,D2,Th60
.= n*z by GROUP_2:43;
hence z*n = n*z by GROUP_2:43;
end;
not (z is Element of Z) implies not (for n being Element of N st n in H
holds z*n = n*z)
proof
assume not z is Element of Z;
then consider g being Element of G such that
D1: g in H & g*z1 <> z1 * g by Th60;
H is Subgroup of Normalizer H by Th80;
then g in Normalizer H by D1, GROUP_2:41;
then reconsider n=g as Element of N;
D2: g*z1 = n*z by GROUP_2:43;
take n;
thus thesis by D1,D2,GROUP_2:43;
end;
hence (for n being Element of N st n in H holds z*n = n*z) implies
z is Element of Z;
thus z is Element of Z implies (for n being Element of N st n in H
holds z*n = n*z) by C1;
end;
B1: for z,n,h being Element of N
st z in Z & n in N & h in H
holds h |^ (z |^ n) = h
proof
let z,n,h be Element of N;
assume C1: z in Z;
assume n in N;
assume C2: h in H;
C3: h |^ (z |^ n) = (z" |^ n) * h * (z |^ n) by GROUP_3:26
.= ((n" * z") * n) * h * (n" * (z * n)) by GROUP_1:def 3
.= ((n" * z") * n) * (h * (n" * (z * n))) by GROUP_1:def 3
.= (n" * z") * (n * (h * (n" * (z * n)))) by GROUP_1:def 3
.= (n" * z") * (n * h * (n" * (z * n))) by GROUP_1:def 3
.= (n" * z") * (((n * h) * n") * (z * n)) by GROUP_1:def 3
.= (n" * z") * (n * h * n") * (z * n) by GROUP_1:def 3;
C4: for a,b being Element of G
holds a in N & b in H & b in N implies a*b*a" in H & a*b*a" in N
proof
let a,b be Element of G;
assume D1: a in N;
assume D2: b in H;
assume b in N; then
D4: a*b in N by D1,GROUP_2:50;
D5: a" in N & b in H by D1,D2,GROUP_2:51;
then b |^ a" in H by Th79;
hence a*b*a" in H;
thus a*b*a" in N by D4,D5,GROUP_2:50;
end;
n * h * n" in H
proof
reconsider h1=h,n1=n as Element of G by GROUP_2:42;
n1" = n" by GROUP_2:48;
then h1*n1" = h*n" by GROUP_2:43;
then n1*(h1*n1") = n*(h*n") by GROUP_2:43
.= n*h*n" by GROUP_1:def 3;
then D1: n1*h1*n1" = n*h*n" by GROUP_1:def 3;
h1 in N & n1 in N & h1 in H by C2;
hence thesis by C4,D1;
end;
then consider h2 being Element of N such that
C5: n * h * n" = h2 & h2 in H;
z*h2 = h2*z by B60,C1,C5;
then (z" * z) * h2 = z" * (h2 * z) by GROUP_1:def 3
.= (z" * h2) * z by GROUP_1:def 3;
then (z" * h2) * z = 1_N * h2 by GROUP_1:def 5
.= h2 by GROUP_1:def 4;
then C6: h2 * z" = (z" * h2) * (z * z") by GROUP_1:def 3
.= (z" * h2) * 1_N by GROUP_1:def 5
.= z" * h2 by GROUP_1:def 4;
h |^ (z |^ n) = (n" * z") * (h2 * (z * n)) by C3,C5,GROUP_1:def 3
.= n" * (z" * (h2 * (z * n))) by GROUP_1:def 3
.= n" * ((z" * h2) * (z * n)) by GROUP_1:def 3
.= n" * (h2 * (z" * (z * n))) by C6,GROUP_1:def 3
.= n" * (h2 * ((z" * z) * n)) by GROUP_1:def 3
.= n" * (h2 * (1_N * n)) by GROUP_1:def 5
.= n" * (h2 * n) by GROUP_1:def 4
.= (h |^ n") |^ n by C5,GROUP_1:def 3
.= h by GROUP_3:25;
hence h |^ (z |^ n) = h;
end;
B2: for z,n,h being Element of N
st z in Z & h in H
holds (z |^ n)*h = h*(z |^ n)
proof
let z,n,h be Element of N;
assume C1: z in Z;
assume C2: h in H;
n in N;
then h |^ (z |^ n) = h by C1,C2,B1;
hence (z |^ n)*h = h*(z |^ n) by GROUP_3:22;
end;
B3: for n being Element of N
for z being Element of N st z in Z holds (z |^ n) in Z
proof
let n,z be Element of N;
set g = z |^ n;
assume z in Z; then
for h being Element of N st h in H holds g*h = h*g by B2;
then g is Element of Z by B60;
hence thesis;
end;
for n being Element of Normalizer H
holds Z is Subgroup of Z |^ n
proof
let n be Element of Normalizer H;
for z being Element of N st z in Z holds z in Z |^ n
proof
let z be Element of N;
assume z in Z;
then (z |^ n") |^ n in (Z |^ n) by B3,GROUP_3:58;
hence z in Z |^ n by GROUP_3:25;
end;
hence Z is Subgroup of Z |^ n by GROUP_2:58;
end;
hence thesis by GROUP_3:121;
end;
hence thesis;
end;
:: Addendum AMN, 27.07.2026
theorem ThAlt1:
for G being Group
for H being Subgroup of G
holds H is characteristic
iff (for phi being Homomorphism of G,G st phi is bijective
holds phi .: (the carrier of H) = the carrier of H)
proof
let G be Group;
let H be Subgroup of G;
hereby
assume A1: H is characteristic;
let phi be Homomorphism of G,G;
assume phi is bijective;
then phi is Automorphism of G;
then the carrier of Image(phi|H) = the carrier of H by A1;
then (phi|H) .: (the carrier of H) = the carrier of H
by GROUP_6:def 10;
hence the carrier of H
= (phi|(the carrier of H)) .: (the carrier of H) by GRSOLV_1:def 2
.= phi .: (the carrier of H) by FUNCT_2:97;
end;
assume A3: for phi being Homomorphism of G,G st phi is bijective
holds phi .: (the carrier of H) = the carrier of H;
for phi being Automorphism of G holds Image(phi|H) = the multMagma of H
proof
let phi be Automorphism of G;
the carrier of H
= phi .: (the carrier of H) by A3
.= (phi | (the carrier of H)) .: (the carrier of H)
by FUNCT_2:97
.= (phi|H) .: (the carrier of H) by GRSOLV_1:def 2
.= the carrier of (Image(phi|H)) by GROUP_6:def 10;
hence Image(phi|H) = the multMagma of H by GROUP_2:59;
end;
hence H is characteristic;
end;
:: Addendum AMN, 27.07.2026
theorem
for G being Group
for H being Subgroup of G
holds H is characteristic
iff (for phi being Homomorphism of G,G st phi is bijective
holds phi .: (the carrier of H) c= the carrier of H)
proof
let G be Group;
let H be Subgroup of G;
thus H is characteristic implies
for phi being Homomorphism of G,G st phi is bijective
holds phi .: (the carrier of H) c= the carrier of H by ThAlt1;
assume A3: for phi being Homomorphism of G,G st phi is bijective
holds phi .: (the carrier of H) c= the carrier of H;
for phi being Automorphism of G
holds Image(phi|H) is Subgroup of H
proof
let phi be Automorphism of G;
phi .: (the carrier of H)
= (phi | (the carrier of H)) .: (the carrier of H)
by FUNCT_2:97
.= (phi|H) .: (the carrier of H) by GRSOLV_1:def 2
.= the carrier of (Image(phi|H)) by GROUP_6:def 10;
hence Image(phi|H) is Subgroup of H by A3,GROUP_2:57;
end;
hence H is characteristic by Th40;
end;