:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: Copyright (c) 1994 Association of Mizar Users
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 :: AUTGROUP:1
definition
let G be
strict Group;
func Aut G -> FUNCTION_DOMAIN of the
carrier of
G,the
carrier of
G means :
Def1:
:: AUTGROUP:def 1
( ( 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 :: AUTGROUP:2
canceled;
theorem :: AUTGROUP:3
theorem Th4: :: AUTGROUP:4
theorem Th5: :: AUTGROUP:5
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: :: AUTGROUP:6
theorem Th7: :: AUTGROUP:7
theorem Th8: :: AUTGROUP:8
:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
:: deftheorem defines AutGroup AUTGROUP:def 3 :
theorem :: AUTGROUP:9
theorem Th10: :: AUTGROUP:10
theorem Th11: :: AUTGROUP:11
:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
theorem :: AUTGROUP:12
theorem Th13: :: AUTGROUP:13
theorem Th14: :: AUTGROUP:14
theorem Th15: :: AUTGROUP:15
theorem Th16: :: AUTGROUP:16
theorem Th17: :: AUTGROUP:17
theorem Th18: :: AUTGROUP:18
:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :
theorem :: AUTGROUP:19
canceled;
theorem Th20: :: AUTGROUP:20
theorem Th21: :: AUTGROUP:21
theorem :: AUTGROUP:22
:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :
theorem Th23: :: AUTGROUP:23
theorem Th24: :: AUTGROUP:24
theorem Th25: :: AUTGROUP:25
theorem :: AUTGROUP:26
theorem Th27: :: AUTGROUP:27
theorem :: AUTGROUP:28
theorem :: AUTGROUP:29
theorem :: AUTGROUP:30
theorem :: AUTGROUP:31
theorem :: AUTGROUP:32