:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1994-2021 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

proof end;

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

proof end;

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 ;

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

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

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 ) by Def1;

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

proof end;

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

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

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
proof end;

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
proof end;
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
proof end;
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),() #);
coherence
multMagma(# (Aut G),() #) is strict Group
proof end;
end;

:: deftheorem defines AutGroup AUTGROUP:def 3 :
for G being strict Group holds AutGroup G = multMagma(# (Aut G),() #);

theorem :: AUTGROUP:8
for G being strict Group
for x, y being Element of ()
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_ ()
proof end;

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

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

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

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

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

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

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

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
proof end;

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
proof end;
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 ()
for f, g being Element of InnAut G st x = f & y = g holds
x * y = f * g
proof end;

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

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

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
proof end;
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
proof end;
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) = () * ()
proof end;

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

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

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

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

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

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

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

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

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