The extension adjoining all p-th roots to a field of characteristic p.

In this file, we introduce the field extension adjoining all p-th roots to a field of (exponential) characteristic p.

Main definitions and results

• AdjoinPthRoots: the field extension adjoining all p-th roots to a field of (exponential) characteristic p.
• AdjoinPthRoots.root: for k a field of (exponential) characteristic p, the p-th root map k → AdjoinPthRoots k, mapping an element to its unique p-th root in AdjoinPthRoots, as a RingEquiv.

def AdjoinPthRoots (k : Type u_1) : Type u_1

Adjoining all p-th root to a field of (exponential) characteristic p.

Equations

• AdjoinPthRoots k = k

@[implicit_reducible]

noncomputable instance instFieldAdjoinPthRoots (k : Type u_1) [Field k] : Field (AdjoinPthRoots k)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance instAlgebraAdjoinPthRoots (k : Type u_1) [Field k] : Algebra k (AdjoinPthRoots k)

Equations

• instAlgebraAdjoinPthRoots k = (frobenius k (ringExpChar k)).toAlgebra

instance instExpCharAdjoinPthRoots (k : Type u_1) [Field k] (p : ℕ) [ExpChar k p] : ExpChar (AdjoinPthRoots k) p

noncomputable def AdjoinPthRoots.root (k : Type u_1) [Field k] : k ≃+* AdjoinPthRoots k

For k a field of (exponential) characteristic p, the p-th root map k → AdjoinPthRoots k, as a RingEquiv.

Equations

• AdjoinPthRoots.root k = RingEquiv.refl k

@[simp]

theorem AdjoinPthRoots.root_pow {k : Type u_1} [Field k] (p : ℕ) [ExpChar k p] (x : k) : (root k) x ^ p = (algebraMap k (AdjoinPthRoots k)) x

theorem AdjoinPthRoots.algebraMap_root_symm {k : Type u_1} [Field k] (p : ℕ) [ExpChar k p] (x : AdjoinPthRoots k) : (algebraMap k (AdjoinPthRoots k)) ((root k).symm x) = x ^ p

instance instIsPurelyInseparableAdjoinPthRoots {k : Type u_1} [Field k] : IsPurelyInseparable k (AdjoinPthRoots k)