:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, ARYTM_3, NEWTON, CARD_1, XXREAL_0,
PREPOWER, NAT_1, RELAT_1, ARYTM_1, INT_1, FUNCT_2, XBOOLE_0, FUNCT_1,
TARSKI, FUNCT_4, FUNCOP_1, FINSET_1, FINSEQ_1, PARTFUN1, CARD_3,
ORDINAL4, EQREL_1, ZFMISC_1, GROUP_1, GROUP_5, STRUCT_0, GROUP_2,
GROUP_3, VECTSP_1, RLVECT_5, RLVECT_3, RLSUB_1, SUPINF_2, FINSEQ_2,
RLVECT_2, VALUED_1, VECTSP_2, ALGSTR_0, REALSET1, MESFUNC1, BINOP_1,
RLVECT_1, LATTICES, UNIROOTS, COMPLFLD, POLYNOM2, COMPLEX1, WEDDWITT,
XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
ZFMISC_1, XXREAL_0, XREAL_0, INT_1, INT_2, NAT_1, NAT_D, FINSET_1,
BINOP_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FINSEQ_1, FINSEQ_2, RVSUM_1, COMPLFLD, POLYNOM4, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, GROUP_2, PREPOWER, FUNCT_4,
UNIROOTS, VECTSP_6, VECTSP_7, GROUP_3, GROUP_5, MATRLIN, VECTSP_9,
EQREL_1, FUNCOP_1, VECTSP_4, WSIERP_1, NEWTON;
constructors WELLORD2, BINOP_1, FUNCT_4, NAT_D, NEWTON, PREPOWER, WSIERP_1,
REALSET2, VECTSP_6, VECTSP_7, GROUP_5, MONOID_0, POLYNOM4, UPROOTS,
UNIROOTS, BINOP_2, VECTSP_9, RELSET_1, REAL_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, CARD_1, FINSEQ_1, EQREL_1, FINSEQ_2,
NEWTON, STRUCT_0, VECTSP_1, COMPLFLD, GROUP_2, MONOID_0, UNIROOTS,
VALUED_0, ALGSTR_0, PREPOWER, RVSUM_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Preliminaries
theorem :: WEDDWITT:1
for a being Element of NAT, q being Real st 1 < q & q |^ a = 1 holds a = 0;
theorem :: WEDDWITT:2
for a, k, r being Nat, x being Real
st 1 < x & 0 < k holds x |^ (a*k + r) = (x |^ a)*(x |^ (a*(k-'1)+r));
theorem :: 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;
theorem :: WEDDWITT:4
for n, q being Nat st 0 < q holds card Funcs(n,q) = q |^ n;
theorem :: WEDDWITT:5 :: SumDivision:
for f being FinSequence of NAT, 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;
theorem :: WEDDWITT:6 :: Partition1:
for X being finite set, Y being a_partition of X,
f being FinSequence of Y st f is one-to-one & rng f = Y
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;
begin :: Class formula for groups
registration
let G be finite Group;
cluster center G -> finite;
end;
definition
let G be Group, a be Element of G;
func Centralizer a -> strict Subgroup of G means
:: WEDDWITT:def 1
the carrier of it = { b where b is Element of G : a*b = b*a };
end;
registration
let G be finite Group;
let a be Element of G;
cluster Centralizer a -> finite;
end;
theorem :: WEDDWITT:7
for G being Group, a being Element of G, x being set
st x in Centralizer a holds x in G;
theorem :: WEDDWITT:8
for G being Group, a, x being Element of G
holds a*x = x*a iff x is Element of Centralizer a;
registration
let G be Group, a be Element of G;
cluster con_class a -> non empty;
end;
definition
let G be Group, a be Element of G;
func a-con_map -> Function of the carrier of G, con_class a means
:: WEDDWITT:def 2
for x being Element of G holds it.x = a |^ x;
end;
theorem :: WEDDWITT:9 :: Br1:
for G being finite Group, a being Element of G, x being Element of con_class a
holds card (a-con_map"{x}) = card Centralizer a;
theorem :: WEDDWITT:10 :: Br2:
for G being Group, a being Element of G, x, y being Element of con_class a
st x<>y holds (a-con_map"{x}) misses (a-con_map"{y});
theorem :: WEDDWITT:11 :: Br3:
for G being Group, a being Element of G
holds the set of all a-con_map"{x} where x is Element of con_class a
is a_partition of the carrier of G;
theorem :: WEDDWITT:12
for G being finite Group, a being Element of G
holds card the set of all a-con_map"{x} where x is Element of con_class a
= card con_class a;
theorem :: WEDDWITT:13
for G being finite Group, a being Element of G
holds card G = card con_class a * card Centralizer a;
definition
let G be Group;
func conjugate_Classes G -> a_partition of the carrier of G equals
:: WEDDWITT:def 3
the set of all con_class a where a is Element of G;
end;
theorem :: WEDDWITT:14 :: ClassFormula Class formula for finite groups
for G being finite Group, f being FinSequence of conjugate_Classes G
st f is one-to-one & rng f = conjugate_Classes G
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;
begin :: Centers and centralizers of skew fields
theorem :: WEDDWITT:15 :: DIM:
for F being finite Field, V being VectSp of F, 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;
definition
let R be Skew-Field;
func center R -> strict Field means
:: 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;
end;
theorem :: WEDDWITT:16 :: Center0:
for R being Skew-Field holds the carrier of center R c= the carrier of R;
registration
let R be finite Skew-Field;
cluster center R -> finite;
end;
theorem :: WEDDWITT:17 :: Center1:
for R being Skew-Field, y being Element of R
holds y in center R iff for s being Element of R holds y*s = s*y;
theorem :: WEDDWITT:18 :: Center1a:
for R being Skew-Field holds 0.R in center R;
theorem :: WEDDWITT:19 :: Center1b:
for R being Skew-Field holds 1_R in center R;
theorem :: WEDDWITT:20 :: Center2:
for R being finite Skew-Field holds 1 < card (the carrier of center R);
theorem :: WEDDWITT:21 :: Center3:
for R being finite Skew-Field holds
card the carrier of center R = card the carrier of R iff R is commutative;
theorem :: WEDDWITT:22 :: Center4:
for R being Skew-Field
holds the carrier of center R = (the carrier of center MultGroup R) \/ {0.R};
definition
let R be Skew-Field, s be Element of R;
func centralizer s -> strict Skew-Field means
:: 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;
end;
theorem :: WEDDWITT:23 :: Central00:
for R be Skew-Field, s be Element of R
holds the carrier of centralizer s c= the carrier of R;
theorem :: WEDDWITT:24 :: Central02a:
for R be Skew-Field, s, a be Element of R
holds a in the carrier of centralizer s iff a*s = s*a;
theorem :: WEDDWITT:25 :: Central02b:
for R be Skew-Field, s be Element of R
holds the carrier of center R c= the carrier of centralizer s;
theorem :: WEDDWITT:26 :: Central02:
for R be Skew-Field, s, a, b be 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;
theorem :: WEDDWITT:27 :: Central0:
for R be Skew-Field, s be Element of R
holds 0.R is Element of centralizer s & 1_R is Element of centralizer s;
registration
let R be finite Skew-Field;
let s be Element of R;
cluster centralizer s -> finite;
end;
theorem :: WEDDWITT:28 :: Central1:
for R be finite Skew-Field, s be Element of R
holds 1 < card (the carrier of centralizer s);
theorem :: WEDDWITT:29 :: Central2a:
for R being Skew-Field, s being Element of R, t being Element of MultGroup R
st t = s
holds the carrier of centralizer s = (the carrier of Centralizer t) \/ {0.R};
theorem :: WEDDWITT:30 :: Central2:
for R being finite Skew-Field, s being Element of R,
t being Element of MultGroup R st t = s
holds card Centralizer t = card (the carrier of centralizer s) - 1;
begin :: Vector spaces over centers of skew fields
definition
let R be Skew-Field;
func VectSp_over_center R -> strict VectSp of center R means
:: WEDDWITT:def 6
the addLoopStr of it = the addLoopStr of R &
the lmult of it = (the multF of R )
| [:the carrier of center R, the carrier of R:];
end;
theorem :: WEDDWITT:31 :: CardCenter1:
for R being finite Skew-Field holds card the carrier of R =
(card (the carrier of center R)) |^ (dim VectSp_over_center R);
theorem :: WEDDWITT:32 :: DimCenter:
for R being finite Skew-Field holds 0 < dim VectSp_over_center R;
definition
let R be Skew-Field, s be Element of R;
func VectSp_over_center s -> strict VectSp of center R means
:: WEDDWITT:def 7
the addLoopStr of it = the addLoopStr of centralizer s &
the lmult of it = (the multF of R)
| [:the carrier of center R, the carrier of centralizer s:];
end;
theorem :: WEDDWITT:33 :: CardCentral:
for R being finite Skew-Field, s being Element of R
holds card the carrier of (centralizer s) =
(card (the carrier of center R)) |^ (dim VectSp_over_center s);
theorem :: WEDDWITT:34 :: DimCentral:
for R being finite Skew-Field, s being Element of R
holds 0 < dim VectSp_over_center s;
theorem :: WEDDWITT:35 :: Skew1:
for R being finite Skew-Field, 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);
theorem :: WEDDWITT:36 :: Skew2:
for R being finite Skew-Field, s being Element of R
st s is Element of MultGroup R
holds (dim VectSp_over_center s) divides (dim VectSp_over_center R);
theorem :: WEDDWITT:37 :: MGC1:
for R being finite Skew-Field holds
card the carrier of center MultGroup R = card (the carrier of center R) - 1;
begin :: Witt's proof of Wedderburn's theorem
::$N Wedderburn Theorem
theorem :: WEDDWITT:38
for R being finite Skew-Field holds R is commutative;
theorem :: WEDDWITT:39
for R being Skew-Field holds 1.center R = 1.R;
theorem :: WEDDWITT:40
for R being Skew-Field, s being Element of R holds 1.centralizer s = 1.R;