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


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;

registration
let G be finite Group;
cluster center G -> finite ;
correctness
coherence
center G is finite ;
;
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
ex b1 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : a * b = b * a }
proof end;
uniqueness
for b1, b2 being strict Subgroup of G st the carrier of b1 = { b where b is Element of G : a * b = b * a } & the carrier of b2 = { b where b is Element of G : a * b = b * a } holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Centralizer WEDDWITT:def 1 :
for G being Group
for a being Element of G
for b3 being strict Subgroup of G holds
( b3 = Centralizer a iff the carrier of b3 = { b where b is Element of G : a * b = b * a } );

registration
let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite strict ;
correctness
coherence
Centralizer a is finite ;
;
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
coherence
not con_class a is empty ;
by GROUP_3:83;
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
ex b1 being Function of the carrier of G,(con_class a) st
for x being Element of G holds b1 . x = a |^ x
proof end;
uniqueness
for b1, b2 being Function of the carrier of G,(con_class a) st ( for x being Element of G holds b1 . x = a |^ x ) & ( for x being Element of G holds b2 . x = a |^ x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines -con_map WEDDWITT:def 2 :
for G being Group
for a being Element of G
for b3 being Function of the carrier of G,(con_class a) holds
( b3 = a -con_map iff for x being Element of G holds b3 . x = a |^ x );

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
coherence
{ (con_class a) where a is Element of G : verum } is a_partition of the carrier of G;
proof end;
end;

:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :
for G being Group holds conjugate_Classes G = { (con_class a) where a is Element of G : verum } ;

theorem :: WEDDWITT:14
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;

theorem Th15: :: WEDDWITT:15
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
ex b1 being strict Field st
( the carrier of b1 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R )
proof end;
uniqueness
for b1, b2 being strict Field st the carrier of b1 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R & the carrier of b2 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R holds
b1 = b2 ;
end;

:: deftheorem Def4 defines center WEDDWITT:def 4 :
for R being Skew-Field
for b2 being strict Field holds
( b2 = center R iff ( the carrier of b2 = { x where x is Element of R : for s being Element of R holds x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R ) );

theorem Th16: :: WEDDWITT:16
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
coherence
center R is finite ;
proof end;
end;

theorem Th17: :: WEDDWITT:17
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 Th18: :: WEDDWITT:18
for R being Skew-Field holds 0. R in center R
proof end;

theorem Th19: :: WEDDWITT:19
for R being Skew-Field holds 1_ R in center R
proof end;

theorem Th20: :: WEDDWITT:20
for R being finite Skew-Field holds 1 < card the carrier of (center R)
proof end;

theorem Th21: :: WEDDWITT:21
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 Th22: :: WEDDWITT:22
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;
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
ex b1 being strict Skew-Field st
( the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R )
proof end;
uniqueness
for b1, b2 being strict Skew-Field st the carrier of b1 = { x where x is Element of R : x * s = s * x } & the addF of b1 = the addF of R || the carrier of b1 & the multF of b1 = the multF of R || the carrier of b1 & 0. b1 = 0. R & 1. b1 = 1. R & the carrier of b2 = { x where x is Element of R : x * s = s * x } & the addF of b2 = the addF of R || the carrier of b2 & the multF of b2 = the multF of R || the carrier of b2 & 0. b2 = 0. R & 1. b2 = 1. R holds
b1 = b2 ;
end;

:: deftheorem Def5 defines centralizer WEDDWITT:def 5 :
for R being Skew-Field
for s being Element of R
for b3 being strict Skew-Field holds
( b3 = centralizer s iff ( the carrier of b3 = { x where x is Element of R : x * s = s * x } & the addF of b3 = the addF of R || the carrier of b3 & the multF of b3 = the multF of R || the carrier of b3 & 0. b3 = 0. R & 1. b3 = 1. R ) );

theorem Th23: :: WEDDWITT:23
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 Th24: :: WEDDWITT:24
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:25
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 Th26: :: WEDDWITT:26
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 Th27: :: WEDDWITT:27
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
coherence
centralizer s is finite ;
by Th23, FINSET_1:1;
end;

theorem Th28: :: WEDDWITT:28
for R being finite Skew-Field
for s being Element of R holds 1 < card the carrier of (centralizer s)
proof end;

theorem Th29: :: WEDDWITT:29
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 Th30: :: WEDDWITT:30
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;

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
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] )
proof end;
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of R:] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] holds
b1 = b2 ;
end;

:: deftheorem Def6 defines VectSp_over_center WEDDWITT:def 6 :
for R being Skew-Field
for b2 being strict VectSp of center R holds
( b2 = VectSp_over_center R iff ( addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of R:] ) );

theorem Th31: :: WEDDWITT:31
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 Th32: :: WEDDWITT:32
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
ex b1 being strict VectSp of center R st
( addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] )
proof end;
uniqueness
for b1, b2 being strict VectSp of center R st addLoopStr(# the carrier of b1, the addF of b1, the ZeroF of b1 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b1 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] & addLoopStr(# the carrier of b2, the addF of b2, the ZeroF of b2 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b2 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] holds
b1 = b2 ;
end;

:: deftheorem Def7 defines VectSp_over_center WEDDWITT:def 7 :
for R being Skew-Field
for s being Element of R
for b3 being strict VectSp of center R holds
( b3 = VectSp_over_center s iff ( addLoopStr(# the carrier of b3, the addF of b3, the ZeroF of b3 #) = addLoopStr(# the carrier of (centralizer s), the addF of (centralizer s), the ZeroF of (centralizer s) #) & the lmult of b3 = the multF of R | [: the carrier of (center R), the carrier of (centralizer s):] ) );

theorem Th33: :: WEDDWITT:33
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 Th34: :: WEDDWITT:34
for R being finite Skew-Field
for s being Element of R holds 0 < dim (VectSp_over_center s)
proof end;

theorem Th35: :: WEDDWITT:35
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 Th36: :: WEDDWITT:36
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 Th37: :: WEDDWITT:37
for R being finite Skew-Field holds card the carrier of (center (MultGroup R)) = (card the carrier of (center R)) - 1
proof end;

:: WP: Wedderburn Theorem
theorem :: WEDDWITT:38
for R being finite Skew-Field holds R is commutative
proof end;

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

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