Adjoining roots of finitely many elements

For finitely many elements of a field F and 0 < n, there is a finite extension of F in which each of them has an n-th root: adjoin the roots inside an algebraic closure.

Nothing here is specific to purely inseparable extensions or to a characteristic exponent; the result is stated for an arbitrary positive power.

It has no consumer in this repository yet. The motivating application is the L' of Stacks 10.161.13 (tag 032O), feeding RingTheory/IntegralClosure/NormalizationFinite: the embedding theorem in TauCeti/FieldTheory/PurelyInseparable/Embedding.lean assumes exactly such an extension as a hypothesis rather than building one, so it does not use this lemma.

Main results

• TauCeti.exists_finiteDimensional_forall_exists_pow_eq: a finite extension of F containing n-th roots of finitely many given elements of F.

Provenance

The construction is the finite root-adjoining step appearing in Stacks, Lemma 10.161.13 (tag 032O), in the normalization-finiteness argument described above.

theorem TauCeti.exists_finiteDimensional_forall_exists_pow_eq (F : Type u) [Field F] (s : Finset F) {n : ℕ} (hn : 0 < n) : ∃ (E : Type u) (x : Field E) (x_1 : Algebra F E), FiniteDimensional F E ∧ ∀ c ∈ s, ∃ (d : E), d ^ n = (algebraMap F E) c

For finitely many elements s of a field F and 0 < n, there is a finite extension E of F in which every c ∈ s has an n-th root: adjoin the roots inside an algebraic closure. Both conjuncts concern the same witness E, which is why they are bundled.

This is the shape the construction of the extension L′ in Stacks, Lemma 10.161.13 (tag 032O) needs — "There exists a finite purely inseparable field extension L′/K and q = p^e such that L ⊂ L′(x^{1/q})" — but is NOT that extension: nothing here asserts that E / F is purely inseparable, only that it is finite and contains the required roots.