Extensions of finite fields

In this file we develop the theory of extensions of finite fields.

If k is a finite field (of cardinality q = p ^ m), then there is a unique (up to in general non-unique isomorphism) extension l of k of any given degree n > 0.

This extension is Galois with cyclic Galois group of degree n, and the (arithmetic) Frobenius map x ↦ x ^ q is a generator.

Main definition

• FiniteField.Extension k p n is a non-canonically chosen extension of k of degree n (for n > 0).

Main Results

• FiniteField.algEquivExtension: any other field extension l/k of degree n is (non-uniquely) isomorphic to our chosen FiniteField.Extension k p n.

def FiniteField.Extension (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CharP k p] : Type

Given a finite field k of characteristic p, we have a non-canoncailly chosen extension of any given degree n > 0.

Equations

• FiniteField.Extension k p n = GaloisField p (Module.finrank (ZMod p) k * n)

instance FiniteField.instFieldExtension (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CharP k p] : Field (Extension k p n)

Equations

• FiniteField.instFieldExtension k p n = instFieldGaloisField p (Module.finrank (ZMod p) k * n)

instance FiniteField.instFiniteExtension (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CharP k p] : Finite (Extension k p n)

Equations

• ⋯ = ⋯

instance FiniteField.instAlgebraZModExtension (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CharP k p] : Algebra (ZMod p) (Extension k p n)

Equations

• FiniteField.instAlgebraZModExtension k p n = instAlgebraZModGaloisField p (Module.finrank (ZMod p) k * n)

instance FiniteField.instFiniteDimensionalZModExtension (k : Type u_1) [Field k] (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) [CharP k p] : FiniteDimensional (ZMod p) (Extension k p n)

Equations

• ⋯ = ⋯

theorem FiniteField.finrank_zmod_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] [Algebra (ZMod p) k] : Module.finrank (ZMod p) (Extension k p n) = Module.finrank (ZMod p) k * n

theorem FiniteField.nonempty_algHom_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] [Algebra (ZMod p) k] : Nonempty (k →ₐ[ZMod p] Extension k p n)

noncomputable instance FiniteField.instAlgebraExtension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Algebra k (Extension k p n)

Equations

• FiniteField.instAlgebraExtension k p n = ⋯.some.toAlgebra

instance FiniteField.instFiniteExtension_1 (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Module.Finite k (Extension k p n)

instance FiniteField.instIsScalarTowerZModExtension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] [Algebra (ZMod p) k] : IsScalarTower (ZMod p) k (Extension k p n)

theorem FiniteField.natCard_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Nat.card (Extension k p n) = Nat.card k ^ n

theorem FiniteField.finrank_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Module.finrank k (Extension k p n) = n

instance FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Polynomial.IsSplittingField k (Extension k p n) (Polynomial.X ^ Nat.card k ^ n - Polynomial.X)

theorem FiniteField.natCard_algEquiv_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Nat.card Gal(Extension k p n/k) = n

theorem FiniteField.card_algEquiv_extension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Fintype.card Gal(Extension k p n/k) = n

noncomputable def FiniteField.Extension.frob (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] : Gal(Extension k p n/k)

The Frobenius automorphism x ↦ x ^ Nat.card k that fixes k.

Equations

• FiniteField.Extension.frob k p n = FiniteField.frobeniusAlgEquivOfAlgebraic k (FiniteField.Extension k p n)

@[simp]

theorem FiniteField.Extension.frob_apply (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] {x : Extension k p n} : (frob k p n) x = x ^ Nat.card k

theorem FiniteField.Extension.exists_frob_pow_eq (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] (g : Gal(Extension k p n/k)) : ∃ i < n, frob k p n ^ i = g

noncomputable def FiniteField.algEquivExtension (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (n : ℕ) [NeZero n] (l : Type u_2) [Field l] [Algebra k l] (h : Module.finrank k l = n) : l ≃ₐ[k] Extension k p n

Given any field extension of finite fields l/k of degree n, we have a non-unique isomorphism between l and our chosen Extension k p n.

Equations

• FiniteField.algEquivExtension k p n l h = ⋯.some