Field Theory - Rosetta Stone

• Definition. The Characteristic of a field \(F\), denoted \(\operatorname{ch}(F)\), is defined to be the smallest positive integer \(p\) such that \(p\cdot1_{F}=0\) if such a \(p\) exists and is defined to be 0 otherwise. (ring_3:def 5)
• Proposition 1. The characteristic of a field is either 0 or a prime \(p\). If \(\operatorname{ch}(F)=p\) then for any \(\alpha\in F\) we have \(p\cdot\alpha=0\).
• Examples.
  1. The fields \(\mathbb{Q}\) and \(\mathbb{R}\) both have characteristic 0.
  2. The finite field \(\mathbb{F}_{p}\) has characteristic \(p\)
• Implicit Definition. Let \(F\) be a field. A Subfield of \(F\) is a subring which is a field. (ec_pf_1:def 1)
• Definition. The Prime Subfield of a field \(F\) (ring_3:def 10) is the subfield of \(F\) generated by the multiplicative identity \(1_{F}\) of \(F\). It is isomorphic to either \(\mathbb{Q}\) (if \(\operatorname{ch}(F)=0\) — ring_3:103) or \(\mathbb{F}_{p}\) (if \(\operatorname{ch}(F)=p\) — ring_3:111).
• Definition. If \(K\) Is a field containing the subfield \(F\), then \(K\) is said to be an extension field of \(F\), denoted \(K/F\).
  • This is defined as a type in field_4
  • The "meat" of the definition is an attribute (field_4:def 1)
  • Note: We can really speak of ring extensions analogously, and this is formalized in field_4 a bit
• Implicit definition. If \(K/F\) is a field extension, then \(K\) is a vector space over \(F\). (field_4:def 6)
• Definition. The Degree of a field extension \(K/F\), denoted \([K:F]\), is the dimension of \(K\) as a vector space over \(F\) — so \([K:F]:=\dim_{F}K\). (field_4:def 7)
  • Note: Mizar's convention is to treat \([K:F]=-1\) when \(\dim_{F}K\) is not finite. This is idiomatic in Mizar handling of dim-like things.
• Proposition 2. Let \(\varphi\colon F\to F'\) be a morphism of fields. Then \(\varphi\) is either identically 0 or injective, so that the image of \(\varphi\) is either 0 or isomorphic to \(F\). (This is a registration in ring_2)
• Implicit Definition. Let \(F\) be a field, let \(p(x)\in F[x]\), let \(K/F\) be a field extension, let \(c\in K\). Then we can treat \(p\in K[x]\) and evaluate \(p(c)\) — this is Ext_eval(p,c) (algnum_1:def 1)
• Implicit Definition. Let \(F\) be a field and \(p(x)\in F[x]\), let \(K/F\) be a field extension of \(F\). We say \(p\) has roots in (or "has roots in") \(K\) if there exists an \(\alpha\in K\) such that \(p(\alpha)=0\). (field_4:def 3)

• Theorem 3. Let \(F\) be a field, let \(p(x)\in F[x]\) be an irreducible polynomial. Then there exists a field \(K\) containing a subfield isomorphic to \(F\) in which \(p(x)\) has a root. (field_4:31)

  Identifying \(F\) with this isomorphic copy shows there exists an extension of \(F\) in which \(p(x)\) has a root.

• Theorem 4. Let \(p(x)\in F[x]\) be an irreducible polynomial of degree \(n\) over the field \(F\). Let \(K\) be the field \(F[x]/(p(x))\). Let \(\theta=x\pmod{p(x)}\in K\). Then the elements 1, \(\theta\), …, \(\theta^{n-1}\) are a basis for \(K\) as a vector space over \(F\), so the degree of the extension is \(n\) — that is, \([K:F]=n\).
  • This set \(\{1,\theta,\dots,\theta^{n-1}\}\) is defined in Mizar as (field_6:def 8)
  • That this is a basis of the vector space is proved in field_6:65

• Definition. Let \(K\) be an extension of the field \(F\). Let \(\alpha,\beta,\dots\in K\) be a collection of elements of \(K\). The smallest subfield of \(K\) containing both \(F\) and the elements \(\alpha,\beta,\dots\) — denoted as \(F(\alpha,\beta,\dots)\) — is called the field generated by \(\alpha,\beta,\dots\) over \(F\).

  This is usually called the field adjoined with \(\alpha,\beta,\dots\) (field_6:def 6)

• Definition. If the field \(K\) is generated by a single element \(\alpha\) over \(F\) — that is, \(K = F(\alpha)\) — then we say \(K\) is a Simple extension of \(F\) (field_14:def 7) and the element \(\alpha\) is said to be a Primitive Element of the extension (field_14:def 8).
• Theorem 6. Let \(F\) be a field and let \(p(x)\in F[x]\) be an irreducible polynomial. Suppose \(K\) is an extension field of \(F\) containing a root \(\alpha\) of \(p(x)\) — so \(p(\alpha)=0\). Let \(F(\alpha)\) denote the subfield of \(K\) generated by \(F\) over \(\alpha\). Then \(F(\alpha)\cong F[x]/(p(x))\).
  • This particular theorem seems to be missing in Mizar, but follows from field_6:59
• Corollary 7. Suppose in Theorem 6 that \(p(x)\) is of degree \(n\). Then \(F(\alpha)=\{a_{0}+a_{1}\alpha+\dots+a_{n-1}\alpha^{n-1}\mid a_{i}\in F\}\subset K\). Missing from Mizar
• Theorem 8. Let \(\varphi\colon F\to F'\) be an isomorphism of fields. Let \(p(x)\in F[x]\) be an irreducible polynomial, let \(p'(x)\in F'[x]\) be the irreducible polynomial obtained by applying the map \(\varphi\) to the coefficients of \(p(x)\). Let \(\alpha\) be a root of \(p(x)\) in some field extension of \(F\), let \(\beta\) be a root of \(p'(x)\) in some extension of \(F'\). Then there is an isomorphism \(\sigma\colon F(\alpha)\to F'(\beta)\) sending \(\alpha\) to \(\beta\) and extending \(\varphi\). (field_8:55, and \(\sigma\) in Mizar is Phi)

• Definition. Let \(F\) be a field, let \(K\) be an extension field of \(F\). The element \(\alpha\in K\) is said to be Algebraic over \(F\) if \(\alpha\) is the root of some nonzero polynomial \(f(x)\in F[x]\). (field_6:def 7)

  If \(\alpha\) is not algebraic over \(F\), then \(\alpha\) is said to be Transcendental over \(F\). (Synonym in field_6)

  The extension \(K/F\) is said to be Algebraic if every element of \(K\) is algebraic over \(F\) (field_7:def 11).

• Proposition 9. Let \(\alpha\) be algebraic over \(F\). Then there is a unique monic irreducible polynomial \(m_{\alpha,F}(x)\in F[x]\) which has \(\alpha\) as a root. (Proved in the definition of the minimal polynomial.)

  A polynomial \(f(x)\in F[x]\) has \(\alpha\) as a root if and only if \(m_{\alpha,F}(x)\) divides \(f(x)\) in \(F[x]\). (field_6:53)

• Corollary 10. If \(L/F\) is a field extension and \(\alpha\) is algebraic over \(F\) and \(L\), then \(m_{\alpha,L}(x)\) divides \(m_{\alpha,F}(x)\) in \(L[x]\). Missing from Mizar

• Definition. The polynomial \(m_{\alpha,F}(x)\) — or just \(m_{\alpha}(x)\) — in Proposition 9 is called the Minimal Polynomial for \(\alpha\) over \(F\). (algnum_1:def 9 and in field_6 abbreviated to MinPoly)

  The degree of \(\alpha\) is equal to the degree of the minimal polynomial \(m_{\alpha}(x)\). (algnum_1:def 10)

• Proposition 11. Let \(\alpha\) be algebraic over the field \(F\) and let \(F(\alpha)\) be the field generated by \(\alpha\) over \(F\). Then \(F(\alpha)\cong F[x]/(m_{\alpha}(x))\) (field_6:59) so that \([F(\alpha):F]=\deg(m_{\alpha}(x))\).

• Proposition 12. The element \(\alpha\) is algebraic over \(F\) if and only if the simple extension \(F(\alpha)/F\) is finite (field_6:68).

  More precisely,

  1. if \(\alpha\) is an element of an extension of degree \(n\) over \(F\), then \(\alpha\) satisfies a polynomial of degree at most \(n\) over \(F\); and
  2. if \(\alpha\) satisfies a polynomial of degree \(n\) over \(F\), then the degree of \(F(\alpha)\) over \(F\) is at most \(n\).
• Corollary 13. If the extension \(K/F\) is finite, then it is algebraic. (field_7:37 and also this is registered in field_7)
• Theorem 14. Let \(F\subset K\subset L\) be fields. Then \([L:F]=[L:K][K:F]\). (field_7:30)
• Corollary 15. Suppose \(L/F\) is a finite extension, let \(K\) be any subfield of \(L\) containing \(F\) (so \(F\subset K\subset L\)). Then \([K:F]\) divides \([L:F]\). Missing from Mizar
• Definition. An extension \(K/F\) is Finitely Generated if there are elements \(\alpha_{1}\), …, \(\alpha_{n}\) in \(K\) such that \(K=F(\alpha_{1},\dots,\alpha_{n})\).
• Lemma 16. \(F(\alpha,\beta)=(F(\alpha))(\beta)\) — that is to say, the field generated over \(F\) by \(\alpha\) and \(\beta\) is the field generated by \(\beta\) over \(F(\alpha)\). Missing from Mizar
• Theorem 17. The extension \(K/F\) is finite if and only if \(K\) is generated by a finite number of algebraic elements over \(F\). Missing from Mizar
• Corollary 18. Suppose \(\alpha\) and \(\beta\) are algebraic over \(F\). Then \(\alpha\pm\beta\), \(\alpha\beta\), \(\alpha/\beta\) (for \(\beta\neq0\)) are all algebraic. Missing from Mizar
• Corollary 19. Let \(L/F\) be an arbitrary field extension. Then the collection of elements of \(L\) that are algebraic over \(F\) form a subfield \(K\) of \(L\). Missing from Mizar
• Theorem 20. If \(K\) is algebraic over \(F\), and if \(L\) is algebraic over \(K\), then \(L\) is algebraic over \(F\). (field_7:39)
• Definition. Let \(K_{1}\) and \(K_{2}\) be two subfields of \(K\). Then the Composite Field of \(K_{1}\) and \(K_{2}\), denoted \(K_{1}K_{2}\), is the smallest subfield of \(K\) containing both \(K_{1}\) and \(K_{2}\). Missing from Mizar
• Implicit proposition. The composite \(K_{1}K_{2}\) is the intersection of all subfields of \(K\) containing both \(K_{1}\) and \(K_{2}\). Missing from Mizar
• Proposition 21. Let \(K_{1}\) and \(K_{2}\) be two finite extensions of a field \(F\) contained in \(K\). Then \([K_{1}K_{2}:F]\leq[K_{1}:F][K_{2}:F]\) Missing from Mizar
• Corollary 22. Suppose \([K_{1}:F]=n\) and \([K_{2}:F]=m\) in Proposition 21 where \(m\) and \(n\) are coprime \(\gcd(m,n)=1\). Then \([K_{1}K_{2}:F]=[K_{1}:F][K_{2}:F]=mn\). Missing from Mizar

I'm skipping this section. If you're interested, I can revisit this.

• Definition. The extension \(K\) of \(F\) is called a Splitting Field (field_8:def 1) for the polynomial \(f(x)\in F[x]\) if \(f(x)\) factors completely into linear factors (or Splits Completely field_4: def 5) in \(K[x]\) and \(f(x)\) does not factor completely into linear factors over any proper subfield of \(K\) containing \(F\).
• Theorem 25. For any field \(F\), if \(f(x)\in F[x]\) then there exists an extension \(K\) of \(F\) which is a splitting field for \(f(x)\). (field_8:31)
  • NOTE: Dummit and Foote errs here! We need \(f(x)\) to be a nonconstant polynomial.
• Definition. If \(K\) is an algebraic extension of \(F\) which is the splitting field over \(F\) for a collection of polynomials \(f(x)\in F[x]\) then \(K\) is called a Normal extension of \(F\). (field_13:def 5)
• Proposition 26. A splitting field of a polynomial of degree \(n\) over \(F\) is of degree at most \(n!\) over \(F\). Missing from Mizar
• Definition. A generator of the cyclic group of all n-th roots of unity is called a Primitive n-th root of unity. These are typically denoted \(\zeta_{n}\).
  • Roots of unity are defined in uniroots:def 2
• Definition. The field \(\mathbb{Q}(\zeta_{n})\) is called the Cyclotomic Field of n-th roots of unity. (uniroots:def 5)
• Theorem 27. Let \(\varphi\colon F\to F'\) be an isomorphism of fields. Let \(f(x)\in F[x]\) be a polynomial, let \(f'(x)\in F'[x]\) be a polynomial obtained by applying \(\varphi\) to the coefficients of \(f(x)\). Let \(E\) be a splitting field for \(f(x)\) over \(F\), let \(E'\) be a splitting field for \(f'(x)\) over \(F'\). Then the isomorphism \(\varphi\) extends to an isomorphism \(\sigma\colon E\to E'\). (field_8:57)
• Corollary 28 (Uniqueness of splitting fields). Any two splitting fields for a polynomial \(f(x)\in F[x]\) over a field \(F\) are isomorphic. (field_8:58)
• Definition. The field \(\overline{F}\) is called an Algebraic Closure of \(F\) if \(\overline{F}\) is algebraic over \(F\) and if every polynomial \(f(x)\in F[x]\) splits completely over \(\overline{F}\). (field_12:def 11)
• Definition. A field \(K\) is said to be Algebraically Closed if every polynomial with coefficients in \(K\) has a root over \(K\). (polynom5:def 9)
• Proposition 29. Let \(\overline{F}\) be the algebraic closure of \(F\). Then \(\overline{F}\) is algebraically closed. (This is part of the definition of algebraic closure in Mizar.)
• Proposition 30. For any field \(F\) there exists an algebraically closed field \(K\) containing \(F\). (field_12:29)

• Proposition 31. Let \(K\) be an algebraically closed field, let \(F\) be a subfield of \(K\). Then the collection of elements \(\overline{F}\) of \(K\) which are algebraic over \(F\) is an algebraic closure of \(F\).

  An algebraic closure of \(F\) is unique up to isomorphism. (field_12:63)

• Theorem. The field \(\mathbb{C}\) is algebraically closed. (This is registered in polynom5 and is polynom5:74)
• Corollary 32. The field \(\mathbb{C}\) contains an algebraic closure for any of its subfields. In particular, \(\overline{\mathbb{Q}}\) (the algebraic closure of \(\mathbb{Q}\) in \(\mathbb{C}\)) is an algebraic closure of \(\mathbb{Q}\). Missing from Mizar

• Definition. A polynomial over \(F\) is called Separable if it has no multiple roots (i.e., all its roots are distinct). (field_15:def 3) Otherwise, it is called Inseparable (field_15)
• Definition. The Derivative of the polynomial \(f(x)=a_{n}x^{n}+a_{n-1}x^{n-1}+\dots+a_{1}x+a_{0}\) is the polynomial \(D_{x}f(x)=na_{n}x^{n-1}+(n-1)a_{n-1}x^{n-2}+\dots+2a_{2}x+a_{1}\). (ringder1:def 8 and also aliased in field_14)
• Proposition 33. A polynomial \(f(x)\) has a multiple root \(\alpha\) if and only if \(\alpha\) is also a root of \(D_{x}f(x)\). (field_15:70)

• Corollary 34. Every irreducible polynomial over a field of characteristic 0 is separable. (Registered fact in field_15)

  A polynomial over such a field is separable if and only if it is the product of distinct irreducible polynomials. Missing from Mizar

• Proposition 35. Let \(F\) be a field of characteristic \(p\). Then for any \(a,b\in F\) we have \((a+b)^{p}=a^{p}+b^{p}\) and \((ab)^{p}=a^{p}b^{p}\)
• Definition. The map in Proposition 35 is called the Frobenius Endomorphism of \(F\) (field_16:def 6)
• Corollary 36. Suppose \(F\) isa finite field of characteristic \(p\). Then every element of \(F\) is a \(p^{th}\) power in \(F\) (notationally: \(F=F^{p}\)) (field_15:93 and field_16:25)

• Proposition 37. Every irreducible polynomial over a finite field is separable. Missing from Mizar

  A polynomial in \(F[x]\) is separable if and only if it is the product of distinct irreducible polynomials in \(F[x]\).

• Definition. A field \(K\) of characteristic \(p\) is called Perfect if every element of \(K\) is a p-th power in \(K\). (field_15:def 4)
• Proposition 38. Let \(p(x)\) be an irreducible polynomial over a field \(F\) of characteristic \(p\). Then there exists a unique integer \(k\geq0\) and a unique irreducible separable polynomial \(p_{sep}(x)\in F[x]\) such that \(p(x)=p_{sep}(x^{p^{k}})\). Missing from Mizar

• Definition. Let \(p(x)\) be an irreducible polynomial over a field of characteristic \(p\). The degree of \(p_{sep}(x)\) in the previous proposition is called the Separable Degree of \(p(x)\), denoted \(\deg_{s}p(x)\). Missing from Mizar

  The integer \(p^{k}\) in the last proposition is called the Inseparable Degree of \(p(x)\), denoted \(\deg_{i}p\). Missing from Mizar

• Definition. The field \(K\) is said to be Separable over \(F\) if every element of \(K\) is the root of a separable polynomial over \(F\). (field_15:def 5)

• Definition. Let \(\mu_{n}\) denote the Group of n-th Roots of Unity over \(\mathbb{Q}\) (uniroots:def 3)