Perfect constants inside the Frobenius subfield

The Section 5 specialization of Corvaja--Zannier works over a perfect constant field. Consequently every constant, after embedding in the curve function field, is a p-th power and belongs to the Frobenius subfield. This file records that compatibility without identifying the two fields.

theorem BGS.CorvajaZannier.algebraMap_mem_frobeniusSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (c : K) : (algebraMap K L) c ∈ frobeniusSubfield L p

Constants from a perfect field land in the Frobenius subfield of every field extension of the same prime characteristic.

def BGS.CorvajaZannier.perfectConstantsToFrobeniusSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] : K →+* ↥(frobeniusSubfield L p)

The constant-field embedding, with codomain restricted to the Frobenius subfield.

Equations

• BGS.CorvajaZannier.perfectConstantsToFrobeniusSubfield = (algebraMap K L).codRestrict (BGS.CorvajaZannier.frobeniusSubfield L p) ⋯

@[simp]

theorem BGS.CorvajaZannier.coe_perfectConstantsToFrobeniusSubfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] (c : K) : ↑(perfectConstantsToFrobeniusSubfield c) = (algebraMap K L) c

theorem BGS.CorvajaZannier.perfectConstantsToFrobeniusSubfield_injective {K : Type u_1} {L : Type u_2} [Field K] [Field L] {p : ℕ} [Fact (Nat.Prime p)] [CharP K p] [CharP L p] [PerfectField K] [Algebra K L] : Function.Injective ⇑perfectConstantsToFrobeniusSubfield