Field extensions and algebraic closure

Algebraic field extensions and closures: minimal polynomials, separable and purely inseparable extensions, base change to separably closed fields, algebraic closures of series fields and quasi-algebraically closed fields.

TheoremField generated by the image of a finite algebra is finite-dimensional#✓fully proved

If S is finite over R and χ' : S →+* K sends R into the image of E in K, then the field generated over E by the range of χ' is finite-dimensional over E.

theorem finiteDimensional_adjoin_range_of_finite_of_forall_mem_range
    {R S E K : Type*} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
    [Field E] [Field K] [Algebra E K]
    (χ' : S →+* K) (h : ∀ r : R, χ' (algebraMap R S r) ∈ (algebraMap E K).range) :
    FiniteDimensional E (IntermediateField.adjoin E (Set.range χ'))

TheoremFinite separable extensions are quotients by separable irreducible polynomials#✓fully proved

Let \(L/K\) be a finite field extension. Then \(L/K\) is separable if and only if there is a monic, irreducible, separable polynomial \(f \in K[X]\) such that \(L\) is isomorphic as a \(K\)-algebra to \(K[X]/(f)\).

theorem isSeparable_iff_exists_monic_irreducible_separable :
    Algebra.IsSeparable K L ↔
      ∃ f : K[X], f.Monic ∧ Irreducible f ∧ f.Separable ∧
        Nonempty (L ≃ₐ[K] AdjoinRoot f)

TheoremPurely inseparable extensions of prime degree#✓fully proved

Let \(p\) be a prime, let \(K\) be a field of characteristic \(p\), and let \(L/K\) be a finite purely inseparable field extension of degree \([L : K] = p\). Then there are \(\alpha \in L\) and \(a \in K\) such that the minimal polynomial of \(\alpha\) over \(K\) is \(X^p - a\), \(a\) is not a \(p\)-th power in \(K\) (that is, \(b^p \neq a\) for every \(b \in K\)), and \(L = K(\alpha)\).

theorem exists_minpoly_X_pow_sub_C_of_finrank_eq_prime (hp : p.Prime)
    (hfin : finrank K L = p) :
    ∃ α : L, ∃ a : K,
      minpoly K α = X ^ p - C a ∧
        (∀ b : K, b ^ p ≠ a) ∧ K⟮α⟯ = ⊤

TheoremTsen's theorem#✓fully proved

Let \(k\) be an algebraically closed field and \(k(X)\) the field of rational functions over \(k\). For all natural numbers \(n\) and \(d\) with \(0 < d < n\), every homogeneous polynomial \(f\) of degree \(d\) in \(n\) variables over \(k(X)\) has a nontrivial zero: there is \(x = (x_1, \dots, x_n) \in k(X)^n\) with \(x_i \neq 0\) for some \(i\) and \(f(x) = 0\). In other words, \(k(X)\) is a \(C_1\) field.

theorem tsen :
    ∀ (k : Type*) [Field k] [IsAlgClosed k] (n d : ℕ)
      (f : MvPolynomial (Fin n) (RatFunc k)),
      f.IsHomogeneous d → 0 < d → d < n →
        ∃ (x : Fin n → RatFunc k), (∃ i, x i ≠ 0) ∧ MvPolynomial.eval x f = 0

Sources

C. Tsen, Divisionsalgebren über Funktionenkörpern, Nachr. Ges. Wiss. Göttingen 1933 335–339; reformulated by C. Chevalley and Lang; textbook in Lang, Algebra, rev 3rd ed.

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.