:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


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
proofend;

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
proofend;

theorem :: AUTGROUP:1
for G being strict Group
for H being Subgroup of G holds
( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) iff H is normal ) by Lm1, Lm2;

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 ) ) ) )
proofend;
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
proofend;
end;

:: deftheorem Def1 defines Aut AUTGROUP:def_1_:_
 for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b2 = Aut G iff ( ( 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 ) ) ) ) );

theorem :: AUTGROUP:2
for G being strict Group holds Aut G c= Funcs ( the carrier of G, the carrier of G)
proofend;

theorem Th3: :: AUTGROUP:3
for G being strict Group holds id the carrier of G is Element of Aut G
proofend;

theorem Th4: :: AUTGROUP:4
for G being strict Group
for h being Homomorphism of G,G holds
( h in Aut G iff h is bijective )
proofend;

Lm3:  for G being strict Group
for f being Element of Aut G holds
( dom f = rng f & dom f = the carrier of G )
proofend;

theorem Th5: :: AUTGROUP:5
for G being strict Group
for f being Element of Aut G holds f " is Homomorphism of G,G
proofend;

theorem Th6: :: AUTGROUP:6
for G being strict Group
for f being Element of Aut G holds f " is Element of Aut G
proofend;

theorem Th7: :: AUTGROUP:7
for G being strict Group
for f1, f2 being Element of Aut G holds f1 * f2 is Element of Aut G
proofend;

definition
let G be strict Group;
func AutComp G ->  BinOp of (Aut G) means :Def2: :: AUTGROUP:def 2
 for x, y being Element of Aut G holds it . (x,y) = x * y;
existence
 ex b1 being BinOp of (Aut G) st
for x, y being Element of Aut G holds b1 . (x,y) = x * y
proofend;
uniqueness
 for b1, b2 being BinOp of (Aut G) st ( for x, y being Element of Aut G holds b1 . (x,y) = x * y ) & ( for x, y being Element of Aut G holds b2 . (x,y) = x * y ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines AutComp AUTGROUP:def_2_:_
 for G being strict Group
for b2 being BinOp of (Aut G) holds
( b2 = AutComp G iff for x, y being Element of Aut G holds b2 . (x,y) = x * y );

definition
let G be strict Group;
func AutGroup G ->  strict Group equals :: AUTGROUP:def 3
 multMagma(# (Aut G),(AutComp G) #);
coherence
 multMagma(# (Aut G),(AutComp G) #) is strict Group
proofend;
end;

:: deftheorem  defines AutGroup AUTGROUP:def_3_:_
 for G being strict Group holds AutGroup G = multMagma(# (Aut G),(AutComp G) #);

theorem :: AUTGROUP:8
for G being strict Group
for x, y being Element of (AutGroup G)
for f, g being Element of Aut G st x = f & y = g holds
x * y = f * g by Def2;

theorem Th9: :: AUTGROUP:9
for G being strict Group holds id the carrier of G = 1_ (AutGroup G)
proofend;

theorem Th10: :: AUTGROUP:10
for G being strict Group
for f being Element of Aut G
for g being Element of (AutGroup G) st f = g holds
f " = g "
proofend;

definition
let G be strict Group;
func InnAut G ->  FUNCTION_DOMAIN of the carrier of G, the carrier of G means :Def4: :: AUTGROUP:def 4
 for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in it iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a );
existence
 ex b1 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st
for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )
proofend;
uniqueness
 for b1, b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b1 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) & ( for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines InnAut AUTGROUP:def_4_:_
 for G being strict Group
for b2 being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b2 = InnAut G iff for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b2 iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) );

theorem :: AUTGROUP:11
for G being strict Group holds InnAut G c= Funcs ( the carrier of G, the carrier of G)
proofend;

theorem Th12: :: AUTGROUP:12
for G being strict Group
for f being Element of InnAut G holds f is Element of Aut G
proofend;

theorem Th13: :: AUTGROUP:13
for G being strict Group holds InnAut G c= Aut G
proofend;

theorem Th14: :: AUTGROUP:14
for G being strict Group
for f, g being Element of InnAut G holds (AutComp G) . (f,g) = f * g
proofend;

theorem Th15: :: AUTGROUP:15
for G being strict Group holds id the carrier of G is Element of InnAut G
proofend;

theorem Th16: :: AUTGROUP:16
for G being strict Group
for f being Element of InnAut G holds f " is Element of InnAut G
proofend;

theorem Th17: :: AUTGROUP:17
for G being strict Group
for f, g being Element of InnAut G holds f * g is Element of InnAut G
proofend;

definition
let G be strict Group;
func InnAutGroup G ->  strict normal Subgroup of AutGroup G means :Def5: :: AUTGROUP:def 5
 the carrier of it = InnAut G;
existence
 ex b1 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G
proofend;
uniqueness
 for b1, b2 being strict normal Subgroup of AutGroup G st the carrier of b1 = InnAut G & the carrier of b2 = InnAut G holds
b1 = b2 by GROUP_2:59;
end;

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def_5_:_
 for G being strict Group
for b2 being strict normal Subgroup of AutGroup G holds
( b2 = InnAutGroup G iff the carrier of b2 = InnAut G );

theorem Th18: :: AUTGROUP:18
for G being strict Group
for x, y being Element of (InnAutGroup G)
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
proofend;

theorem Th19: :: AUTGROUP:19
for G being strict Group holds id the carrier of G = 1_ (InnAutGroup G)
proofend;

theorem :: AUTGROUP:20
for G being strict Group
for f being Element of InnAut G
for g being Element of (InnAutGroup G) st f = g holds
f " = g "
proofend;

definition
let G be strict Group;
let b be Element of G;
func Conjugate b ->  Element of InnAut G means :Def6: :: AUTGROUP:def 6
 for a being Element of G holds it . a = a |^ b;
existence
 ex b1 being Element of InnAut G st
for a being Element of G holds b1 . a = a |^ b
proofend;
uniqueness
 for b1, b2 being Element of InnAut G st ( for a being Element of G holds b1 . a = a |^ b ) & ( for a being Element of G holds b2 . a = a |^ b ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def_6_:_
 for G being strict Group
for b being Element of G
for b3 being Element of InnAut G holds
( b3 = Conjugate b iff for a being Element of G holds b3 . a = a |^ b );

theorem Th21: :: AUTGROUP:21
for G being strict Group
for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)
proofend;

theorem Th22: :: AUTGROUP:22
for G being strict Group holds Conjugate (1_ G) = id the carrier of G
proofend;

theorem Th23: :: AUTGROUP:23
for G being strict Group
for a being Element of G holds (Conjugate (1_ G)) . a = a
proofend;

theorem :: AUTGROUP:24
for G being strict Group
for a being Element of G holds (Conjugate a) * (Conjugate (a ")) = Conjugate (1_ G)
proofend;

theorem Th25: :: AUTGROUP:25
for G being strict Group
for a being Element of G holds (Conjugate (a ")) * (Conjugate a) = Conjugate (1_ G)
proofend;

theorem :: AUTGROUP:26
for G being strict Group
for a being Element of G holds Conjugate (a ") = (Conjugate a) "
proofend;

theorem :: AUTGROUP:27
for G being strict Group
for a being Element of G holds
( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
proofend;

theorem :: AUTGROUP:28
for G being strict Group
for f being Element of InnAut G holds
( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )
proofend;

theorem :: AUTGROUP:29
for G being strict Group holds InnAutGroup G,G ./. (center G) are_isomorphic
proofend;

theorem :: AUTGROUP:30
for G being strict Group st G is commutative Group holds
for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)
proofend;