WEDDWITT: Witt's Proof of the {W}edderburn Theorem

:: Witt's Proof of the {W}edderburn Theorem
:: by Broderick Arneson , Matthias Baaz and Piotr Rudnicki
::
:: Received December 30, 2003
:: Copyright (c) 2003-2011 Association of Mizar Users

begin

theorem Th1: :: WEDDWITT:1

for a being Element of NAT
for q being Real st 1 < q & q |^ a = 1 holds
a = 0

proof end;

theorem Th2: :: WEDDWITT:2

for a, k, r being Nat
for x being Real st 1 < x & 0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))

proof end;

theorem Th3: :: WEDDWITT:3

for q, a, b being Element of NAT st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b) -' 1 holds
a divides b

proof end;

theorem Th4: :: WEDDWITT:4

for n, q being Nat st 0 < q holds
card (Funcs (n,q)) = q |^ n

proof end;

theorem Th5: :: WEDDWITT:5

for f being FinSequence of NAT
for i being Element of NAT st ( for j being Element of NAT st j in dom f holds
i divides f /. j ) holds
i divides Sum f

proof end;

theorem Th6: :: WEDDWITT:6

for X being finite set
for Y being a_partition of X
for f being FinSequence of Y st f is one-to-one & rng f = Y holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card X = Sum c

proof end;

begin

registration

let G be finite Group;
cluster center G -> finite ;
correctness ;

end;

definition

let G be Group;
let a be Element of G;
func Centralizer a -> strict Subgroup of G means :Def1: :: WEDDWITT:def 1
the carrier of it = { b where b is Element of G : a * b = b * a } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :

registration

let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite strict ;
correctness ;

end;

theorem Th7: :: WEDDWITT:7

for G being Group
for a being Element of G
for x being set st x in Centralizer a holds
x in G

proof end;

theorem Th8: :: WEDDWITT:8

for G being Group
for a, x being Element of G holds
( a * x = x * a iff x is Element of (Centralizer a) )

proof end;

registration

let G be Group;
let a be Element of G;
cluster con_class a -> non empty ;
correctness by GROUP_3:98;

end;

definition

let G be Group;
let a be Element of G;
func a -con_map -> Function of the carrier of G,(con_class a) means :Def2: :: WEDDWITT:def 2
for x being Element of G holds it . x = a |^ x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :

theorem Th9: :: WEDDWITT:9

for G being finite Group
for a being Element of G
for x being Element of con_class a holds card ((a -con_map) " {x}) = card (Centralizer a)

proof end;

theorem Th10: :: WEDDWITT:10

for G being Group
for a being Element of G
for x, y being Element of con_class a st x <> y holds
(a -con_map) " {x} misses (a -con_map) " {y}

proof end;

theorem Th11: :: WEDDWITT:11

for G being Group
for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G

proof end;

theorem Th12: :: WEDDWITT:12

for G being finite Group
for a being Element of G holds card { ((a -con_map) " {x}) where x is Element of con_class a : verum } = card (con_class a)

proof end;

theorem Th13: :: WEDDWITT:13

for G being finite Group
for a being Element of G holds card G = (card (con_class a)) * (card (Centralizer a))

proof end;

definition

let G be Group;
func conjugate_Classes G -> a_partition of the carrier of G equals :: WEDDWITT:def 3
{ (con_class a) where a is Element of G : verum } ;
correctness

proof end;

end;

:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :

theorem :: WEDDWITT:14

canceled;

theorem :: WEDDWITT:15

for G being finite Group
for f being FinSequence of conjugate_Classes G st f is one-to-one & rng f = conjugate_Classes G holds
for c being FinSequence of NAT st len c = len f & ( for i being Element of NAT st i in dom c holds
c . i = card (f . i) ) holds
card G = Sum c by Th6;

begin

theorem Th16: :: WEDDWITT:16

for F being finite Field
for V being VectSp of F
for n, q being Nat st V is finite-dimensional & n = dim V & q = card the carrier of F holds
card the carrier of V = q |^ n

proof end;

definition

let R be Skew-Field;
func center R -> strict Field means :Def4: :: WEDDWITT:def 4
( the carrier of it = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines center WEDDWITT:def 4 :

theorem Th17: :: WEDDWITT:17

for R being Skew-Field holds the carrier of (center R) c= the carrier of R

proof end;

registration

let R be finite Skew-Field;
cluster center R -> finite strict ;
correctness

proof end;

end;

theorem Th18: :: WEDDWITT:18

for R being Skew-Field
for y being Element of R holds
( y in center R iff for s being Element of R holds y * s = s * y )

proof end;

theorem Th19: :: WEDDWITT:19

for R being Skew-Field holds 0. R in center R

proof end;

theorem Th20: :: WEDDWITT:20

for R being Skew-Field holds 1_ R in center R

proof end;

theorem Th21: :: WEDDWITT:21

for R being finite Skew-Field holds 1 < card the carrier of (center R)

proof end;

theorem Th22: :: WEDDWITT:22

for R being finite Skew-Field holds
( card the carrier of (center R) = card the carrier of R iff R is commutative )

proof end;

theorem Th23: :: WEDDWITT:23

for R being Skew-Field holds the carrier of (center R) = the carrier of (center (MultGroup R)) \/ {(0. R)}

proof end;

definition

let R be Skew-Field;
let s be Element of R;
A1: 1. R = 1_ R ;
func centralizer s -> strict Skew-Field means :Def5: :: WEDDWITT:def 5
( the carrier of it = { x where x is Element of R : x * s = s * x } & the addF of it = the addF of R || the carrier of it & the multF of it = the multF of R || the carrier of it & 0. it = 0. R & 1. it = 1. R );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :

theorem Th24: :: WEDDWITT:24

for R being Skew-Field
for s being Element of R holds the carrier of (centralizer s) c= the carrier of R

proof end;

theorem Th25: :: WEDDWITT:25

for R being Skew-Field
for s, a being Element of R holds
( a in the carrier of (centralizer s) iff a * s = s * a )

proof end;

theorem :: WEDDWITT:26

for R being Skew-Field
for s being Element of R holds the carrier of (center R) c= the carrier of (centralizer s)

proof end;

theorem Th27: :: WEDDWITT:27

for R being Skew-Field
for s, a, b being Element of R st a in the carrier of (center R) & b in the carrier of (centralizer s) holds
a * b in the carrier of (centralizer s)

proof end;

theorem Th28: :: WEDDWITT:28

for R being Skew-Field
for s being Element of R holds
( 0. R is Element of (centralizer s) & 1_ R is Element of (centralizer s) )

proof end;

registration

let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite strict ;
correctness by Th24, FINSET_1:13;

end;

theorem Th29: :: WEDDWITT:29

for R being finite Skew-Field
for s being Element of R holds 1 < card the carrier of (centralizer s)

proof end;

theorem Th30: :: WEDDWITT:30

for R being Skew-Field
for s being Element of R
for t being Element of (MultGroup R) st t = s holds
the carrier of (centralizer s) = the carrier of (Centralizer t) \/ {(0. R)}

proof end;

theorem Th31: :: WEDDWITT:31

for R being finite Skew-Field
for s being Element of R
for t being Element of (MultGroup R) st t = s holds
card (Centralizer t) = (card the carrier of (centralizer s)) - 1

proof end;

begin

definition

let R be Skew-Field;
func VectSp_over_center R -> strict VectSp of center R means :Def6: :: WEDDWITT:def 6
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of R:] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def 6 :

theorem Th32: :: WEDDWITT:32

for R being finite Skew-Field holds card the carrier of R = (card the carrier of (center R)) |^ (dim (VectSp_over_center R))

proof end;

theorem Th33: :: WEDDWITT:33

for R being finite Skew-Field holds 0 < dim (VectSp_over_center R)

proof end;

definition

let R be Skew-Field;
let s be Element of R;
func VectSp_over_center s -> strict VectSp of center R means :Def7: :: WEDDWITT:def 7
( addLoopStr(# the carrier of it, the addF of it, the ZeroF of it #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of it = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :

theorem Th34: :: WEDDWITT:34

for R being finite Skew-Field
for s being Element of R holds card the carrier of (centralizer s) = (card the carrier of (center R)) |^ (dim (VectSp_over_center s))

proof end;

theorem Th35: :: WEDDWITT:35

for R being finite Skew-Field
for s being Element of R holds 0 < dim (VectSp_over_center s)

proof end;

theorem Th36: :: WEDDWITT:36

for R being finite Skew-Field
for r being Element of R st r is Element of (MultGroup R) holds
((card the carrier of (center R)) |^ (dim (VectSp_over_center r))) - 1 divides ((card the carrier of (center R)) |^ (dim (VectSp_over_center R))) - 1

proof end;

theorem Th37: :: WEDDWITT:37

for R being finite Skew-Field
for s being Element of R st s is Element of (MultGroup R) holds
dim (VectSp_over_center s) divides dim (VectSp_over_center R)

proof end;

theorem Th38: :: WEDDWITT:38

for R being finite Skew-Field holds card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1

proof end;

begin

theorem :: WEDDWITT:39

for R being finite Skew-Field holds R is commutative

proof end;

theorem :: WEDDWITT:40

for R being Skew-Field holds 1. (center R) = 1. R by Def4;

theorem :: WEDDWITT:41

for R being Skew-Field
for s being Element of R holds 1. (centralizer s) = 1. R by Def5;