Frobenius power subfields over perfect constants

If k is perfect of exponential characteristic p, the p^n-th powers in an extension F form an intermediate field of F / k. Iterated Frobenius identifies F with this field, semilinearly over the corresponding Frobenius automorphism of k. The construction uses Mathlib's RingHom.fieldRange and RingHom.rangeRestrictFieldEquiv.

This distinguishes an isomorphism of abstract fields preserving the constant subfield from a k-algebra isomorphism: Frobenius need not fix each element of k.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, second edition, Section III.10.

noncomputable def TauCeti.frobeniusPowers (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) : IntermediateField k F

The intermediate field F^{p^n} of iterated Frobenius powers. Perfectness ensures that it contains every constant from k.

Equations

• TauCeti.frobeniusPowers k F p n = (iterateFrobenius F p n).fieldRange.toIntermediateField ⋯

theorem TauCeti.frobeniusPowers_toSubfield (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) : (frobeniusPowers k F p n).toSubfield = (iterateFrobenius F p n).fieldRange

The underlying subfield is Mathlib's field range of iterated Frobenius.

@[simp]

theorem TauCeti.mem_frobeniusPowers (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) (z : F) : z ∈ frobeniusPowers k F p n ↔ ∃ (x : F), x ^ p ^ n = z

Membership in the Frobenius power subfield means being a p^n-th power in F.

noncomputable def TauCeti.iterateFrobeniusEquivPowers (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) : F ≃+* ↥(frobeniusPowers k F p n)

Iterated Frobenius as an isomorphism from F onto its power subfield. It is semilinear, not generally linear, over k.

Equations

• TauCeti.iterateFrobeniusEquivPowers k F p n = id (iterateFrobenius F p n).rangeRestrictFieldEquiv

@[simp]

theorem TauCeti.coe_iterateFrobeniusEquivPowers (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) (x : F) : ↑((iterateFrobeniusEquivPowers k F p n) x) = x ^ p ^ n

The field isomorphism onto the power subfield sends x to x^{p^n}.

@[simp]

theorem TauCeti.iterateFrobeniusEquivPowers_algebraMap (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) (c : k) : (iterateFrobeniusEquivPowers k F p n) ((algebraMap k F) c) = (algebraMap k ↥(frobeniusPowers k F p n)) ((iterateFrobeniusEquiv k p n) c)

On constants, the power-subfield isomorphism acts by the Frobenius automorphism of k.

instance TauCeti.isPurelyInseparable_frobeniusPowers (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] (p : ℕ) [ExpChar k p] [PerfectRing k p] (n : ℕ) : IsPurelyInseparable (↥(frobeniusPowers k F p n)) F

The ambient field is purely inseparable over its iterated Frobenius power subfield.