Galois fields #

If p is a prime number, and n a natural number, then GaloisField p n is defined as the splitting field of X^(p^n) - X over ZMod p. It is a finite field with p ^ n elements.

Main definition #

GaloisField p n is a field with p ^ n elements

Main Results #

GaloisField.algEquivGaloisField: Any finite field is isomorphic to some Galois field
FiniteField.algEquivOfCardEq: Uniqueness of finite fields : algebra isomorphism
FiniteField.ringEquivOfCardEq: Uniqueness of finite fields : ring isomorphism
card_algHom_of_finrank_dvd: if [K:F] ∣ [L:F] then #(K →ₐ[F] L) = [K:F]
nonempty_algHom_iff_finrank_dvd: (K →ₐ[F] L) is nonempty iff [K:F] ∣ [L:F]. This and the above result helps to classify the category of finite fields.

source

instance FiniteField.isSplittingField_sub (K : Type u_1) (F : Type u_2) [Field K] [Fintype K] [Field F] [Algebra F K] :

Polynomial.IsSplittingField F K (Polynomial.X ^ Fintype.card K - Polynomial.X)

source

theorem galois_poly_separable {K : Type u_1} [CommRing K] (p q : ℕ) [CharP K p] (h : p ∣ q) :

(Polynomial.X ^ q - Polynomial.X).Separable

source

def GaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Type

A finite field with p ^ n elements. Every field with the same cardinality is (non-canonically) isomorphic to this field.

Equations

Instances For

source

instance instInhabitedGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Inhabited (GaloisField p n)

Equations

source

instance instFieldGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Field (GaloisField p n)

Equations

source

instance instCharPGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

CharP (GaloisField p n) p

Equations

source

instance instAlgebraZModGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Algebra (ZMod p) (GaloisField p n)

Equations

source

instance instFiniteGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Finite (GaloisField p n)

Equations

source

instance instFiniteDimensionalZModGaloisField (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

FiniteDimensional (ZMod p) (GaloisField p n)

Equations

source

instance instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) :

Polynomial.IsSplittingField (ZMod p) (GaloisField p n) (Polynomial.X ^ p ^ n - Polynomial.X)

Equations

source

theorem GaloisField.finrank (p : ℕ) [h_prime : Fact (Nat.Prime p)] {n : ℕ} (h : n ≠ 0) :

Module.finrank (ZMod p) (GaloisField p n) = n

source

theorem GaloisField.card (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) (h : n ≠ 0) :

Nat.card (GaloisField p n) = p ^ n

source

theorem GaloisField.splits_zmod_X_pow_sub_X (p : ℕ) [h_prime : Fact (Nat.Prime p)] :

(Polynomial.X ^ p - Polynomial.X).Splits

source

def GaloisField.equivZmodP (p : ℕ) [h_prime : Fact (Nat.Prime p)] :

GaloisField p 1 ≃ₐ[ZMod p] ZMod p

A Galois field with exponent 1 is equivalent to ZMod

Equations

Instances For

source

theorem FiniteField.splits_X_pow_card_sub_X (p : ℕ) [h_prime : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] :

(Polynomial.map (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)).Splits

source

theorem FiniteField.isSplittingField_of_card_eq (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] (h : Fintype.card K = p ^ n) :

Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)

source

def GaloisField.algEquivGaloisFieldOfFintype (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [Field K] [Fintype K] [Algebra (ZMod p) K] (h : Fintype.card K = p ^ n) :

K ≃ₐ[ZMod p] GaloisField p n

Any finite field is (possibly noncanonically) isomorphic to some Galois field.

Equations

Instances For

source

theorem FiniteField.splits_X_pow_nat_card_sub_X (p : ℕ) [h_prime : Fact (Nat.Prime p)] {K : Type u_1} [Field K] [Algebra (ZMod p) K] [Finite K] :

(Polynomial.map (algebraMap (ZMod p) K) (Polynomial.X ^ Nat.card K - Polynomial.X)).Splits

source

theorem FiniteField.isSplittingField_of_nat_card_eq (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [Field K] [Algebra (ZMod p) K] (h : Nat.card K = p ^ n) :

Polynomial.IsSplittingField (ZMod p) K (Polynomial.X ^ p ^ n - Polynomial.X)

source

@[instance 100]

instance GaloisField.instIsGaloisOfFinite {K : Type u_2} {K' : Type u_3} [Field K] [Field K'] [Finite K'] [Algebra K K'] :

IsGalois K K'

source

def GaloisField.algEquivGaloisField (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) {K : Type u_1} [Field K] [Algebra (ZMod p) K] (h : Nat.card K = p ^ n) :

K ≃ₐ[ZMod p] GaloisField p n

Any finite field is (possibly noncanonically) isomorphic to some Galois field.

Equations

Instances For

source

theorem FiniteField.algebraMap_norm_eq_pow {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Algebra K K'] [Finite K'] {x : K'} :

(algebraMap K K') ((Algebra.norm K) x) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))

source

theorem FiniteField.unitsMap_norm_surjective (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] [Finite K'] :

Function.Surjective ⇑(Units.map (Algebra.norm K))

source

theorem FiniteField.norm_surjective (K : Type u_1) (K' : Type u_2) [Field K] [Field K'] [Algebra K K'] [Finite K'] :

Function.Surjective ⇑(Algebra.norm K)

source

def FiniteField.algEquivOfCardEq {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Fintype K] [Fintype K'] (p : ℕ) [h_prime : Fact (Nat.Prime p)] [Algebra (ZMod p) K] [Algebra (ZMod p) K'] (hKK' : Fintype.card K = Fintype.card K') :

K ≃ₐ[ZMod p] K'

Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly noncanonically) isomorphic

Equations

Instances For

source

def FiniteField.ringEquivOfCardEq {K : Type u_1} {K' : Type u_2} [Field K] [Field K'] [Fintype K] [Fintype K'] (hKK' : Fintype.card K = Fintype.card K') :

K ≃+* K'

Uniqueness of finite fields: Any two finite fields of the same cardinality are (possibly noncanonically) isomorphic

Equations

Instances For

source

theorem FiniteField.pow_finrank_eq_natCard (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_3) [AddCommGroup k] [Finite k] [Module (ZMod p) k] :

p ^ Module.finrank (ZMod p) k = Nat.card k

source

theorem FiniteField.pow_finrank_eq_card (p : ℕ) [Fact (Nat.Prime p)] (k : Type u_3) [AddCommGroup k] [Fintype k] [Module (ZMod p) k] :

p ^ Module.finrank (ZMod p) k = Fintype.card k

source

theorem FiniteField.nonempty_algHom_of_finrank_dvd {F : Type u_3} {K : Type u_4} {L : Type u_5} [Field F] [Field K] [Algebra F K] [Field L] [Algebra F L] [Finite L] (h : Module.finrank F K ∣ Module.finrank F L) :

Nonempty (K →ₐ[F] L)

source

theorem FiniteField.natCard_algHom_of_finrank_dvd {F : Type u_3} {K : Type u_4} {L : Type u_5} [Field F] [Field K] [Algebra F K] [Field L] [Algebra F L] [Finite L] (h : Module.finrank F K ∣ Module.finrank F L) :

Nat.card (K →ₐ[F] L) = Module.finrank F K

source

theorem FiniteField.card_algHom_of_finrank_dvd {F : Type u_3} {K : Type u_4} {L : Type u_5} [Field F] [Field K] [Algebra F K] [Field L] [Algebra F L] [Finite L] [Finite K] (h : Module.finrank F K ∣ Module.finrank F L) :

Fintype.card (K →ₐ[F] L) = Module.finrank F K

source

theorem FiniteField.nonempty_algHom_iff_finrank_dvd {F : Type u_3} {K : Type u_4} {L : Type u_5} [Field F] [Field K] [Algebra F K] [Field L] [Algebra F L] [Finite L] :

Nonempty (K →ₐ[F] L) ↔ Module.finrank F K ∣ Module.finrank F L

Documentation

Mathlib.FieldTheory.Finite.GaloisField

Galois fields #

Main definition #

Main Results #