Embedding a purely inseparable extension into a field with enough roots

Let M / K be a purely inseparable extension of exponent at most n, so that x ↦ x ^ (p ^ n) is a ring homomorphism M →+* K (IsPurelyInseparable.iterateFrobenius). If a field K' over K contains p ^ n-th roots of the images of a generating set of M, then M embeds into K' over K: the embedding is ψ⁻¹ ∘ φ for φ the Frobenius of M into K and ψ the (injective) Frobenius of K'. Mathlib provides this embedding only into perfect fields (IsPurelyInseparable.instNonemptyAlgHomOfPerfectField); the target that normalization-finiteness needs, k'(X_1, …, X_r), is not perfect.

The companion existence statement — for finitely many elements of a field, a finite extension containing n-th roots of all of them — is TauCeti.exists_finiteDimensional_forall_exists_pow_eq, in TauCeti/FieldTheory/IntermediateField/Adjoin/Roots.lean; nothing about it is specific to purely inseparable extensions.

Main results

• TauCeti.IsPurelyInseparable.nonempty_algHom_of_forall_exists_pow_eq: the embedding of a purely inseparable extension of bounded exponent into any field over K containing p ^ n-th roots of the Frobenius images of a generating set.

Provenance

The mathematics is the field-theoretic half of the "some details omitted" sentence of Stacks 10.161.13 (tag 032O): there is a finite purely inseparable L' / K and q = p ^ e with L ⊂ L'(x^{1/q}).

theorem TauCeti.IsPurelyInseparable.nonempty_algHom_of_forall_exists_pow_eq (K : Type u_1) (M : Type u_2) [Field K] [Field M] [Algebra K M] [IsPurelyInseparable.HasExponent K M] (p : ℕ) [ExpChar K p] {n : ℕ} (hn : IsPurelyInseparable.exponent K M ≤ n) (K' : Type u_3) [Field K'] [Algebra K K'] {s : Set M} (hs : IntermediateField.adjoin K s = ⊤) (h : ∀ x ∈ s, ∃ (y : K'), y ^ p ^ n = (algebraMap K K') ((IsPurelyInseparable.iterateFrobenius K M p hn) x)) : Nonempty (M →ₐ[K] K')

Source: Stacks, Lemma 10.161.13 (tag 032O), proof: "L ⊂ L′(x^{1/q}); some details omitted" — the embedding. Let M / K be purely inseparable of exponent at most n, with Frobenius φ = IsPurelyInseparable.iterateFrobenius K M p hn : M →+* K, and let s generate M over K. If every φ x for x ∈ s has a p ^ n-th root in a field K' over K, then M embeds into K' over K.