:: On the Group of Inner Automorphisms
:: by Artur Korni{\l}owicz
::
:: Received April 22, 1994
:: 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 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 b₁ being FUNCTION_DOMAIN of the carrier of G, the carrier of G st
( ( for f being Element of b₁ holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b₁ iff ( h is one-to-one & h is onto ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FUNCTION_DOMAIN of the carrier of G, the carrier of G st ( for f being Element of b₁ holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b₁ iff ( h is one-to-one & h is onto ) ) ) & ( for f being Element of b₂ holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b₂ iff ( h is one-to-one & h is onto ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Aut AUTGROUP:def 1 :
for G being strict Group
for b₂ being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b₂ = Aut G iff ( ( for f being Element of b₂ holds f is Homomorphism of G,G ) & ( for h being Homomorphism of G,G holds
( h in b₂ 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 b₁ being BinOp of (Aut G) st
for x, y being Element of Aut G holds b₁ . (x,y) = x * y

proof end;

uniqueness
for b₁, b₂ being BinOp of (Aut G) st ( for x, y being Element of Aut G holds b₁ . (x,y) = x * y ) & ( for x, y being Element of Aut G holds b₂ . (x,y) = x * y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :
for G being strict Group
for b₂ being BinOp of (Aut G) holds
( b₂ = AutComp G iff for x, y being Element of Aut G holds b₂ . (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

proof end;

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)

proof end;

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 "

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 b₁ 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 b₁ iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a )

proof end;

uniqueness
for b₁, b₂ 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 b₁ 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 b₂ iff ex a being Element of G st
for x being Element of G holds f . x = x |^ a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :
for G being strict Group
for b₂ being FUNCTION_DOMAIN of the carrier of G, the carrier of G holds
( b₂ = InnAut G iff for f being Element of Funcs ( the carrier of G, the carrier of G) holds
( f in b₂ 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 (AutComp G) . (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 b₁ being strict normal Subgroup of AutGroup G st the carrier of b₁ = InnAut G

proof end;

uniqueness
for b₁, b₂ being strict normal Subgroup of AutGroup G st the carrier of b₁ = InnAut G & the carrier of b₂ = InnAut G holds
b₁ = b₂ by GROUP_2:59;

end;

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :
for G being strict Group
for b₂ being strict normal Subgroup of AutGroup G holds
( b₂ = InnAutGroup G iff the carrier of b₂ = 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

proof end;

theorem Th19: :: AUTGROUP:19

for G being strict Group holds id the carrier of G = 1_ (InnAutGroup G)

proof end;

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 "

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 b₁ being Element of InnAut G st
for a being Element of G holds b₁ . a = a |^ b

proof end;

uniqueness
for b₁, b₂ being Element of InnAut G st ( for a being Element of G holds b₁ . a = a |^ b ) & ( for a being Element of G holds b₂ . a = a |^ b ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :
for G being strict Group
for b being Element of G
for b₃ being Element of InnAut G holds
( b₃ = Conjugate b iff for a being Element of G holds b₃ . 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)

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 (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 a) = Conjugate (1_ G)

proof end;

theorem :: AUTGROUP:26

for G being strict Group
for a being Element of G holds Conjugate (a ") = (Conjugate a) "

proof end;

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 )

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 ./. (center G) are_isomorphic

proof end;

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)

proof end;