ValuationTheory.DiscreteValuationField.exists_cyclic_artinSchreier_extension_of_prime_parameter
A prime parameter in an integrally closed domain produces an actual cyclic degree-p extension of its characteristic-p fraction field. The power-basis generator is the inverse of the Artin--Schreier generator.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ValuationTheory.DiscreteValuationField
open Polynomial
open scoped Polynomial
universe u vLean source · statement
theorem exists_cyclic_artinSchreier_extension_of_prime_parameter
(R : Type u) (K : Type v)
[CommRing R] [IsDomain R] [IsIntegrallyClosed R]
[Field K] [Algebra R K] [IsFractionRing R K]
(π : R) (hπ : Prime π) (p : ℕ) [Fact p.Prime] [CharP K p] :
∃ (L : Type v) (_ : Field L) (_ : Algebra K L)
(B : PowerBasis K L) (α : L),
Module.finrank K L = p ∧
B.gen = α⁻¹ ∧
α ^ p - α = algebraMap K L ((algebraMap R K π)⁻¹) ∧
Algebra.adjoin K ({α} : Set L) = ⊤ ∧
minpoly K B.gen =
(artinSchreierInversePolynomial π p).map (algebraMap R K) ∧
IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L)