Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Witt's Proof of the Wedderburn Theorem

**by****Broderic Arneson,****Matthias Baaz, and****Piotr Rudnicki**- Received December 30, 2003
- MML identifier: WEDDWITT

- [ Mizar article, MML identifier index ]

environ vocabulary WEDDWITT, ARYTM_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, RLVECT_1, BOOLE, FINSEQ_2, FINSEQ_4, COMPLEX1, BINOP_1, VECTSP_1, LATTICES, COMPLFLD, GROUP_1, REALSET1, INT_1, NAT_1, TARSKI, CARD_1, GROUP_2, POLYNOM2, FUNCT_4, VECTSP_2, FUNCOP_1, SEQ_1, FUNCT_2, ABSVALUE, UNIROOTS, PREPOWER, FINSET_1, CAT_1, RLSUB_1, GROUP_5, RLVECT_2, SETFAM_1, VECTSP_9, RLVECT_3, MATRLIN, SUBSET_1, EQREL_1, GROUP_3; notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, NUMBERS, ARYTM_0, XREAL_0, ZFMISC_1, REAL_1, INT_1, INT_2, NAT_1, RLVECT_1, VECTSP_1, VECTSP_2, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, BINARITH, RVSUM_1, COMPLFLD, POLYNOM4, CARD_1, GROUP_2, PREPOWER, FINSET_1, GROUP_1, FUNCT_4, CQC_LANG, WSIERP_1, UNIROOTS, SETFAM_1, VECTSP_6, VECTSP_7, GROUP_3, GROUP_5, VECTSP_9, EQREL_1, FRAENKEL, FUNCOP_1, VECTSP_4, EULER_2; constructors ARYTM_0, REAL_1, MONOID_0, WELLORD2, INT_2, COMPLSP1, BINARITH, POLYNOM4, COMPLEX1, POLYNOM5, PREPOWER, DOMAIN_1, PRE_CIRC, FINSEQOP, ALGSTR_1, RLVECT_2, CQC_LANG, WSIERP_1, UPROOTS, UNIROOTS, BINOP_1, VECTSP_6, VECTSP_7, VECTSP_9, GROUP_5, EQREL_1, EULER_2; clusters STRUCT_0, RELSET_1, BINARITH, VECTSP_1, VECTSP_2, FINSEQ_2, POLYNOM1, MONOID_0, NAT_1, INT_1, POLYNOM5, FINSEQ_1, FINSET_1, CARD_1, FSM_1, FUNCT_1, NUMBERS, SUBSET_1, ORDINAL2, CQC_LANG, UNIROOTS, GROUP_2, REAL_1, FUNCOP_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL; begin :: Preliminaries theorem :: WEDDWITT:1 :: Th1: for a being Nat, q being Real st 1 < q & q |^ a = 1 holds a = 0; theorem :: WEDDWITT:2 :: Th2: 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 :: Th3: for q, a, b being Nat st 0 < a & 1 < q & (q |^ a) -' 1 divides (q |^ b)-'1 holds a divides b; theorem :: WEDDWITT:4 :: Lm1: 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 Nat st for j being 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 Nat st i in dom c holds c.i = Card (f.i) holds card X = Sum c; begin :: Class formula for groups definition cluster finite Group; end; definition 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; definition let G be finite Group; let a be Element of G; cluster Centralizer a -> finite; end; theorem :: WEDDWITT:7 :: GCTR2: for G being Group, a being Element of G, x being set st x in Centralizer a holds x in G; theorem :: WEDDWITT:8 :: GCTR1: for G being Group, a, x being Element of G holds a*x = x*a iff x is Element of Centralizer a; definition 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}) = ord 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 { a-con_map"{x} where x is Element of con_class a : not contradiction } is a_partition of the carrier of G; theorem :: WEDDWITT:12 :: Br4: for G being finite Group, a being Element of G holds Card { a-con_map"{x} where x is Element of con_class a : not contradiction} = card con_class a; theorem :: WEDDWITT:13 :: OrdGroup1: for G being finite Group, a being Element of G holds ord G = card con_class a * ord Centralizer a; definition let G be Group; func conjugate_Classes G -> a_partition of the carrier of G equals :: WEDDWITT:def 3 {S where S is Subset of G : ex a being Element of G st S = con_class a }; end; theorem :: WEDDWITT:14 :: Conj1: for G being Group, x being set holds x in conjugate_Classes G iff ex a being Element of G st con_class a = x; theorem :: WEDDWITT:15 :: :: 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 Nat st i in dom c holds c.i = Card (f.i) holds ord G = Sum c; begin :: Centers and centralizers of skew fields theorem :: WEDDWITT:16 :: 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 add of it = (the add of R) | [:the carrier of it,the carrier of it:] & the mult of it = (the mult of R) | [:the carrier of it,the carrier of it:]& the Zero of it = the Zero of R & the unity of it = the unity of R; end; theorem :: WEDDWITT:17 :: Center0: for R being Skew-Field holds the carrier of center R c= the carrier of R; definition let R be finite Skew-Field; cluster center R -> finite; end; theorem :: WEDDWITT:18 :: 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:19 :: Center1a: for R being Skew-Field holds 0.R in center R; theorem :: WEDDWITT:20 :: Center1b: for R being Skew-Field holds 1_ R in center R; theorem :: WEDDWITT:21 :: Center2: for R being finite Skew-Field holds 1 < card (the carrier of center R); theorem :: WEDDWITT:22 :: 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:23 :: 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 add of it = (the add of R) | [:the carrier of it,the carrier of it:] & the mult of it = (the mult of R) | [:the carrier of it,the carrier of it:]& the Zero of it = the Zero of R & the unity of it = the unity of R; end; theorem :: WEDDWITT:24 :: Central00: for R be Skew-Field, s be Element of R holds the carrier of centralizer s c= the carrier of R; theorem :: WEDDWITT:25 :: 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:26 :: 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:27 :: 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:28 :: 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; definition let R be finite Skew-Field; let s be Element of R; cluster centralizer s -> finite; end; theorem :: WEDDWITT:29 :: Central1: for R be finite Skew-Field, s be Element of R holds 1 < card (the carrier of centralizer s); theorem :: WEDDWITT:30 :: 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:31 :: Central2: for R being finite Skew-Field, s being Element of R, t being Element of MultGroup R st t = s holds ord 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 LoopStr of it = the LoopStr of R & the lmult of it = (the mult of R ) | [:the carrier of center R, the carrier of R:]; end; theorem :: WEDDWITT:32 :: 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:33 :: 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 LoopStr of it = the LoopStr of centralizer s & the lmult of it = (the mult of R) | [:the carrier of center R, the carrier of centralizer s:]; end; theorem :: WEDDWITT:34 :: 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:35 :: DimCentral: for R being finite Skew-Field, s being Element of R holds 0 < dim VectSp_over_center s; theorem :: WEDDWITT:36 :: 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:37 :: 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:38 :: 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 theorem :: WEDDWITT:39 for R being finite Skew-Field holds R is commutative;

Back to top