:: 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;