The Frobenius subfield

Every derivation in characteristic p kills p-th powers. Consequently the image of Frobenius is contained in the derivation's constant field. The field extension over that image is purely inseparable. If a parameter z is not a p-th power and the extension over L^p(z) is separable, the two properties force L = L^p(z); Kummer irreducibility then gives the exact degree [L : L^p] = p.

The last two hypotheses are the algebraic boundary at which the geometric notion of a separating parameter enters. They are explicit theorem hypotheses rather than hidden curve axioms.

For such a parameter, polynomial differentiation descends along evaluation at z to a derivation of L. Its constants are exactly the Frobenius subfield: the degree-< p normal form of an element has zero derivative only when it is constant.

@[reducible, inline]

abbrev BGS.CorvajaZannier.frobeniusSubfield (L : Type u_1) [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] : Subfield L

The subfield of p-th powers in a field of prime characteristic p.

Equations

• BGS.CorvajaZannier.frobeniusSubfield L p = (frobenius L p).fieldRange

theorem BGS.CorvajaZannier.derivation_frobenius_eq_zero {R : Type u_1} {L : Type u_2} [CommRing R] [Field L] [Algebra R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (D : Derivation R L L) (x : L) : D ((frobenius L p) x) = 0

Every Frobenius power is killed by every derivation.

theorem BGS.CorvajaZannier.frobenius_fieldRange_is_constant {R : Type u_1} {L : Type u_2} [CommRing R] [Field L] [Algebra R L] {p : ℕ} [Fact (Nat.Prime p)] [CharP L p] (D : Derivation R L L) (x : ↥(frobenius L p).fieldRange) : D ↑x = 0

The Frobenius image subfield is contained in the constant field of every derivation.

theorem BGS.CorvajaZannier.frobeniusSubfield_isPurelyInseparable {L : Type u_3} [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] : IsPurelyInseparable (↥(frobeniusSubfield L p)) L

The extension of a characteristic-p field over its Frobenius image is purely inseparable (of exponent at most one).

theorem BGS.CorvajaZannier.adjoin_frobeniusSubfield_eq_top {L : Type u_3} [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] (z : L) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : (↥(frobeniusSubfield L p))⟮z⟯ = ⊤

A parameter over which the Frobenius-pure extension becomes separable generates the whole field over the Frobenius subfield.

This is the algebraic first assertion of the separating-parameter lemma: the extension over L^p(z) is simultaneously purely inseparable and separable, and is therefore trivial.

theorem BGS.CorvajaZannier.finrank_frobeniusSubfield_eq_char {L : Type u_3} [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ∉ frobeniusSubfield L p) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : Module.finrank (↥(frobeniusSubfield L p)) L = p

A Frobenius-separating parameter gives the exact degree of the Frobenius subfield.

The separability hypothesis implies that the simultaneously purely inseparable extension L / L^p(z) is trivial. Since z is not in L^p, its minimal polynomial over L^p is the irreducible polynomial X ^ p - z ^ p, of degree p.

theorem BGS.CorvajaZannier.exists_derivation_with_exact_frobenius_constants {L : Type u_3} [Field L] (p : ℕ) [Fact (Nat.Prime p)] [CharP L p] (z : L) (hz : z ∉ frobeniusSubfield L p) [Algebra.IsSeparable (↥(↥(frobeniusSubfield L p))⟮z⟯) L] : ∃ (D : Derivation (↥(frobeniusSubfield L p)) L L), D z = 1 ∧ ∀ (x : L), D x = 0 ↔ ∃ (c : ↥(frobeniusSubfield L p)), (algebraMap (↥(frobeniusSubfield L p)) L) c = x

A Frobenius-separating parameter determines a derivation whose constant field is exactly the Frobenius subfield.

The derivation is obtained by descending polynomial differentiation through the surjective evaluation map F[X] → L, where F = L^p. Its kernel is computed from the unique polynomial representative of degree less than p: in characteristic p, a polynomial with zero derivative is an expansion in X ^ p, and the degree bound forces that expansion to be constant.