Nested canonical finite-field extensions

If a ∣ b, finite-field theory supplies an embedding from the chosen degree-a extension into the chosen degree-b extension. This file fixes one such embedding and records the scalar-tower and degree consequences used by the constant-extension Hasse--Weil argument.

noncomputable def BGS.HasseWeil.finiteFieldExtensionAlgHomOfDvd (K : Type u_1) [Field K] [Fintype K] (p a b : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] [NeZero b] (h : a ∣ b) : FiniteField.Extension K p a →ₐ[K] FiniteField.Extension K p b

A chosen K-algebra embedding between canonical finite-field extensions whose degrees satisfy a ∣ b.

Equations

• BGS.HasseWeil.finiteFieldExtensionAlgHomOfDvd K p a b h = ⋯.some

@[reducible]

noncomputable def BGS.HasseWeil.finiteFieldExtensionAlgebraOfDvd (K : Type u_1) [Field K] [Fintype K] (p a b : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] [NeZero b] (h : a ∣ b) : Algebra (FiniteField.Extension K p a) (FiniteField.Extension K p b)

The algebra structure selected by finiteFieldExtensionAlgHomOfDvd.

Equations

• BGS.HasseWeil.finiteFieldExtensionAlgebraOfDvd K p a b h = (BGS.HasseWeil.finiteFieldExtensionAlgHomOfDvd K p a b h).toAlgebra

theorem BGS.HasseWeil.finiteFieldExtension_isScalarTower_of_dvd (K : Type u_1) [Field K] [Fintype K] (p a b : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] [NeZero b] (h : a ∣ b) : IsScalarTower K (FiniteField.Extension K p a) (FiniteField.Extension K p b)

The selected divisible-degree embedding is compatible with the original coefficient field.

theorem BGS.HasseWeil.finrank_finiteFieldExtension_of_dvd (K : Type u_1) [Field K] [Fintype K] (p a b : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] [NeZero b] (h : a ∣ b) : Module.finrank (FiniteField.Extension K p a) (FiniteField.Extension K p b) = b / a

The relative degree of the chosen nested extension is the quotient of the two absolute degrees.

theorem BGS.HasseWeil.finrank_double_finiteFieldExtension (K : Type u_1) [Field K] [Fintype K] (p a : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] : Module.finrank (FiniteField.Extension K p a) (FiniteField.Extension K p (2 * a)) = 2

The chosen degree-2a extension is quadratic over the chosen degree-a subfield.

theorem BGS.HasseWeil.natCard_double_finiteFieldExtension_eq_sq (K : Type u_1) [Field K] (p a : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero a] [Finite K] : Nat.card (FiniteField.Extension K p (2 * a)) = Nat.card (FiniteField.Extension K p a) ^ 2

Cardinality of the degree-2a extension is the square of the degree-a extension's cardinality.

theorem BGS.HasseWeil.degree_le_natCard_finiteFieldExtension_mul (K : Type u_1) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] [Finite K] (d n : ℕ) [NeZero (d * n)] (hn : 0 < n) : d ≤ Nat.card (FiniteField.Extension K p (d * n))

A positive multiple of the extension degree is already large enough to dominate that degree. This elementary growth estimate is what makes one fixed multiple work uniformly in the Stepanov construction.