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)] [CharP k p] (n : ℕ) : Type

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

Equations

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

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

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

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)

@[instance_reducible]

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

@[simp]

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

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

theorem FiniteField.exists_forall_apply_eq_pow (k : Type u_1) [Field k] [Finite k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] (l : Type u_2) [Field l] [Algebra k l] [Finite l] (g : Gal(l/k)) : ∃ (i : ℕ), ∀ (x : l), g x = x ^ Nat.card k ^ i

theorem Irreducible.natDegree_dvd_of_dvd_X_pow_card_pow_sub_X {k : Type u_1} [Field k] {f : Polynomial k} (hi : Irreducible f) {n : ℕ} (h : f ∣ Polynomial.X ^ Nat.card k ^ n - Polynomial.X) : f.natDegree ∣ n

theorem Irreducible.natDegree_dvd_iff_dvd_X_pow_card_pow_sub_X {k : Type u_1} [Field k] [Finite k] {f : Polynomial k} (hi : Irreducible f) {n : ℕ} : f.natDegree ∣ n ↔ f ∣ Polynomial.X ^ Nat.card k ^ n - Polynomial.X