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

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)

Equations

• ⋯ = ⋯

theorem galois_poly_separable {K : Type u_1} [Field K] (p : ℕ) (q : ℕ) [CharP K p] (h : p ∣ q) : Polynomial.Separable (Polynomial.X ^ q - Polynomial.X)

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

• GaloisField p n = Polynomial.SplittingField (Polynomial.X ^ p ^ n - Polynomial.X)

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

Equations

• instFieldGaloisField p n = inferInstanceAs (Field (Polynomial.SplittingField (Polynomial.X ^ p ^ n - Polynomial.X)))

instance instInhabitedGaloisFieldOfNatNatInstOfNatNatMkPrimePrime_two : Inhabited (GaloisField 2 1)

Equations

• instInhabitedGaloisFieldOfNatNatInstOfNatNatMkPrimePrime_two = { default := 37 }

instance GaloisField.instAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldToSemiringToDivisionSemiringInstFieldGaloisField (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) : Algebra (ZMod p) (GaloisField p n)

Equations

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

instance GaloisField.instIsSplittingFieldZModGaloisFieldInstFieldInstFieldGaloisFieldInstAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldToSemiringToDivisionSemiringInstFieldGaloisFieldHSubPolynomialPolynomialPolynomialToSemiringToDivisionSemiringToSemifieldHPowNatInstHPowToNatPowToMonoidToMonoidWithZeroSemiringXHPowInstHPowToNatPowInstMonoidX (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) : Polynomial.IsSplittingField (ZMod p) (GaloisField p n) (Polynomial.X ^ p ^ n - Polynomial.X)

Equations

• ⋯ = ⋯

instance GaloisField.instCharPGaloisFieldToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingInstFieldGaloisField (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) : CharP (GaloisField p n) p

Equations

• ⋯ = ⋯

instance GaloisField.instFiniteDimensionalZModGaloisFieldToDivisionRingInstFieldToAddCommGroupToRingInstFieldGaloisFieldToModuleToCommSemiringToSemifieldToSemiringToDivisionSemiringInstAlgebraZModGaloisFieldToCommSemiringToSemifieldInstFieldToSemiringToDivisionSemiringInstFieldGaloisField (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) : FiniteDimensional (ZMod p) (GaloisField p n)

Equations

• ⋯ = ⋯

instance GaloisField.instFintypeGaloisField (p : ℕ) [h_prime : Fact (Nat.Prime p)] (n : ℕ) : Fintype (GaloisField p n)

Equations

• GaloisField.instFintypeGaloisField p n = id (FiniteDimensional.fintypeOfFintype (ZMod p) (GaloisField p n))

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

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

theorem GaloisField.splits_zmod_X_pow_sub_X (p : ℕ) [h_prime : Fact (Nat.Prime p)] : Polynomial.Splits (RingHom.id (ZMod p)) (Polynomial.X ^ p - Polynomial.X)

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

• GaloisField.equivZmodP p = let h := ⋯; let inst := ⋯; AlgEquiv.symm (Polynomial.IsSplittingField.algEquiv (ZMod p) (Polynomial.X ^ p ^ 1 - Polynomial.X))

theorem GaloisField.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.Splits (algebraMap (ZMod p) K) (Polynomial.X ^ Fintype.card K - Polynomial.X)

theorem GaloisField.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)

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

Equations

• ⋯ = ⋯

def GaloisField.algEquivGaloisField (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 non canonically) isomorphic to some Galois field.

Equations

• GaloisField.algEquivGaloisField p n h = Polynomial.IsSplittingField.algEquiv K (Polynomial.X ^ p ^ n - Polynomial.X)

def FiniteField.algEquivOfCardEq {K : Type u_1} [Field K] [Fintype K] {K' : Type u_2} [Field 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 non canonically) isomorphic

Equations

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

def FiniteField.ringEquivOfCardEq {K : Type u_1} [Field K] [Fintype K] {K' : Type u_2} [Field 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 non canonically) isomorphic

Equations

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