begin
Lm1:
for G being strict Group
for H being Subgroup of G st ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) holds
H is normal
Lm2:
for G being strict Group
for H being Subgroup of G st H is normal holds
for a, b being Element of G st b is Element of H holds
b |^ a in H
theorem
definition
let G be
strict Group;
func Aut G -> FUNCTION_DOMAIN of the
carrier of
G,the
carrier of
G means :
Def1:
( ( for
f being
Element of
it holds
f is
Homomorphism of
G,
G ) & ( for
h being
Homomorphism of
G,
G holds
(
h in it iff (
h is
one-to-one &
h is
onto ) ) ) );
existence
ex b1 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st
( ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is onto ) ) ) )
uniqueness
for b1, b2 being FUNCTION_DOMAIN of the carrier of G,the carrier of G st ( for f being Element of b1 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b1 iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of b2 holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b2 iff ( h is one-to-one & h is onto ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Aut AUTGROUP:def 1 :
theorem
canceled;
theorem
theorem Th4:
theorem Th5:
Lm3:
for G being strict Group
for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
:: deftheorem defines AutGroup AUTGROUP:def 3 :
theorem
theorem Th10:
theorem Th11:
:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :
theorem
canceled;
theorem Th20:
theorem Th21:
theorem
:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem
theorem
theorem
theorem
theorem