:: AUTGROUP semantic presentation

Lemma1: for b₁ being strict Group
for b₂ being Subgroup of b₁ st ( for b₃, b₄ being Element of b₁ st b₄ is Element of b₂ holds
b₄ |^ b₃ in b₂ ) holds
b₂ is normal

proof end;

Lemma2: for b₁ being strict Group
for b₂ being Subgroup of b₁ st b₂ is normal holds
for b₃, b₄ being Element of b₁ st b₄ is Element of b₂ holds
b₄ |^ b₃ in b₂

proof end;

theorem Th1: :: AUTGROUP:1

for b₁ being strict Group
for b₂ being Subgroup of b₁ holds
( ( for b₃, b₄ being Element of b₁ st b₄ is Element of b₂ holds
b₄ |^ b₃ in b₂ ) iff b₂ is normal ) by Lemma1, Lemma2;

definition

let c₁ be strict Group;
func Aut c₁ -> FUNCTION_DOMAIN of the carrier of a₁,the carrier of a₁ means :Def1: :: AUTGROUP:def 1
( ( for b₁ being Element of a₂ holds b₁ is Homomorphism of a₁,a₁ ) & ( for b₁ being Homomorphism of a₁,a₁ holds
( b₁ in a₂ iff ( b₁ is one-to-one & b₁ is_epimorphism ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Aut AUTGROUP:def 1 :

theorem Th2: :: AUTGROUP:2

canceled;

theorem Th3: :: AUTGROUP:3

for b₁ being strict Group holds Aut b₁ c= Funcs the carrier of b₁,the carrier of b₁

proof end;

theorem Th4: :: AUTGROUP:4

for b₁ being strict Group holds id the carrier of b₁ is Element of Aut b₁

proof end;

theorem Th5: :: AUTGROUP:5

for b₁ being strict Group
for b₂ being Homomorphism of b₁,b₁ holds
( b₂ in Aut b₁ iff b₂ is_isomorphism )

proof end;

Lemma6: for b₁ being strict Group
for b₂ being Element of Aut b₁ holds
( dom b₂ = rng b₂ & dom b₂ = the carrier of b₁ )

proof end;

theorem Th6: :: AUTGROUP:6

for b₁ being strict Group
for b₂ being Element of Aut b₁ holds b₂ " is Homomorphism of b₁,b₁

proof end;

theorem Th7: :: AUTGROUP:7

for b₁ being strict Group
for b₂ being Element of Aut b₁ holds b₂ " is Element of Aut b₁

proof end;

theorem Th8: :: AUTGROUP:8

for b₁ being strict Group
for b₂, b₃ being Element of Aut b₁ holds b₂ * b₃ is Element of Aut b₁

proof end;

definition

let c₁ be strict Group;
func AutComp c₁ -> BinOp of Aut a₁ means :Def2: :: AUTGROUP:def 2
for b₁, b₂ being Element of Aut a₁ holds a₂ . b₁,b₂ = b₁ * b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines AutComp AUTGROUP:def 2 :

definition

let c₁ be strict Group;
func AutGroup c₁ -> strict Group equals :: AUTGROUP:def 3
HGrStr(# (Aut a₁),(AutComp a₁) #);
coherence

proof end;

end;

:: deftheorem Def3 defines AutGroup AUTGROUP:def 3 :

theorem Th9: :: AUTGROUP:9

for b₁ being strict Group
for b₂, b₃ being Element of (AutGroup b₁)
for b₄, b₅ being Element of Aut b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₄ * b₅ by Def2;

theorem Th10: :: AUTGROUP:10

for b₁ being strict Group holds id the carrier of b₁ = 1. (AutGroup b₁)

proof end;

theorem Th11: :: AUTGROUP:11

for b₁ being strict Group
for b₂ being Element of Aut b₁
for b₃ being Element of (AutGroup b₁) st b₂ = b₃ holds
b₂ " = b₃ "

proof end;

definition

let c₁ be strict Group;
func InnAut c₁ -> FUNCTION_DOMAIN of the carrier of a₁,the carrier of a₁ means :Def4: :: AUTGROUP:def 4
for b₁ being Element of Funcs the carrier of a₁,the carrier of a₁ holds
( b₁ in a₂ iff ex b₂ being Element of a₁ st
for b₃ being Element of a₁ holds b₁ . b₃ = b₃ |^ b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines InnAut AUTGROUP:def 4 :

theorem Th12: :: AUTGROUP:12

for b₁ being strict Group holds InnAut b₁ c= Funcs the carrier of b₁,the carrier of b₁

proof end;

theorem Th13: :: AUTGROUP:13

for b₁ being strict Group
for b₂ being Element of InnAut b₁ holds b₂ is Element of Aut b₁

proof end;

theorem Th14: :: AUTGROUP:14

for b₁ being strict Group holds InnAut b₁ c= Aut b₁

proof end;

theorem Th15: :: AUTGROUP:15

for b₁ being strict Group
for b₂, b₃ being Element of InnAut b₁ holds (AutComp b₁) . b₂,b₃ = b₂ * b₃

proof end;

theorem Th16: :: AUTGROUP:16

for b₁ being strict Group holds id the carrier of b₁ is Element of InnAut b₁

proof end;

theorem Th17: :: AUTGROUP:17

for b₁ being strict Group
for b₂ being Element of InnAut b₁ holds b₂ " is Element of InnAut b₁

proof end;

theorem Th18: :: AUTGROUP:18

for b₁ being strict Group
for b₂, b₃ being Element of InnAut b₁ holds b₂ * b₃ is Element of InnAut b₁

proof end;

definition

let c₁ be strict Group;
func InnAutGroup c₁ -> strict normal Subgroup of AutGroup a₁ means :Def5: :: AUTGROUP:def 5
the carrier of a₂ = InnAut a₁;
existence

proof end;

uniqueness by GROUP_2:68;

end;

:: deftheorem Def5 defines InnAutGroup AUTGROUP:def 5 :

theorem Th19: :: AUTGROUP:19

canceled;

theorem Th20: :: AUTGROUP:20

for b₁ being strict Group
for b₂, b₃ being Element of (InnAutGroup b₁)
for b₄, b₅ being Element of InnAut b₁ st b₂ = b₄ & b₃ = b₅ holds
b₂ * b₃ = b₄ * b₅

proof end;

theorem Th21: :: AUTGROUP:21

for b₁ being strict Group holds id the carrier of b₁ = 1. (InnAutGroup b₁)

proof end;

theorem Th22: :: AUTGROUP:22

for b₁ being strict Group
for b₂ being Element of InnAut b₁
for b₃ being Element of (InnAutGroup b₁) st b₂ = b₃ holds
b₂ " = b₃ "

proof end;

definition

let c₁ be strict Group;
let c₂ be Element of c₁;
func Conjugate c₂ -> Element of InnAut a₁ means :Def6: :: AUTGROUP:def 6
for b₁ being Element of a₁ holds a₃ . b₁ = b₁ |^ a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :

theorem Th23: :: AUTGROUP:23

for b₁ being strict Group
for b₂, b₃ being Element of b₁ holds Conjugate (b₂ * b₃) = (Conjugate b₃) * (Conjugate b₂)

proof end;

theorem Th24: :: AUTGROUP:24

for b₁ being strict Group holds Conjugate (1. b₁) = id the carrier of b₁

proof end;

theorem Th25: :: AUTGROUP:25

for b₁ being strict Group
for b₂ being Element of b₁ holds (Conjugate (1. b₁)) . b₂ = b₂

proof end;

theorem Th26: :: AUTGROUP:26

for b₁ being strict Group
for b₂ being Element of b₁ holds (Conjugate b₂) * (Conjugate (b₂ " )) = Conjugate (1. b₁)

proof end;

theorem Th27: :: AUTGROUP:27

for b₁ being strict Group
for b₂ being Element of b₁ holds (Conjugate (b₂ " )) * (Conjugate b₂) = Conjugate (1. b₁)

proof end;

theorem Th28: :: AUTGROUP:28

for b₁ being strict Group
for b₂ being Element of b₁ holds Conjugate (b₂ " ) = (Conjugate b₂) "

proof end;

theorem Th29: :: AUTGROUP:29

for b₁ being strict Group
for b₂ being Element of b₁ holds
( (Conjugate b₂) * (Conjugate (1. b₁)) = Conjugate b₂ & (Conjugate (1. b₁)) * (Conjugate b₂) = Conjugate b₂ )

proof end;

theorem Th30: :: AUTGROUP:30

for b₁ being strict Group
for b₂ being Element of InnAut b₁ holds
( b₂ * (Conjugate (1. b₁)) = b₂ & (Conjugate (1. b₁)) * b₂ = b₂ )

proof end;

theorem Th31: :: AUTGROUP:31

for b₁ being strict Group holds InnAutGroup b₁,b₁ ./. (center b₁) are_isomorphic

proof end;

theorem Th32: :: AUTGROUP:32

for b₁ being strict Group st b₁ is commutative Group holds
for b₂ being Element of (InnAutGroup b₁) holds b₂ = 1. (InnAutGroup b₁)

proof end;