mathlib3 documentation

field_theory.finite.galois_field

Galois fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

If p is a prime number, and n a natural number, then galois_field 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 #

Main Results #

source
@[protected, instance]
def finite_field.has_sub.sub.polynomial.is_splitting_field (K : Type u_1) (F : Type u_2) [field K] [fintype K] [field F] [algebra F K] :
polynomial.is_splitting_field F K (polynomial.X ^ fintype.card K - polynomial.X)
source
theorem galois_poly_separable {K : Type u_1} [field K] (p q : ℕ) [char_p K p] (h : p ∣ q) :
(polynomial.X ^ q - polynomial.X).separable
source
@[protected, instance]
noncomputable def galois_field.field (p : ℕ) [fact (nat.prime p)] (n : ℕ) :
field (galois_field p n)
source
def galois_field (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 galois_field
source
@[protected, instance]
noncomputable def galois_field.inhabited  :
inhabited (galois_field 2 1)
Equations
source
@[protected, instance]
noncomputable def galois_field.algebra (p : ℕ) [fact (nat.prime p)] (n : ℕ) :
algebra (zmod p) (galois_field p n)
Equations
source
@[protected, instance]
def galois_field.has_sub.sub.polynomial.is_splitting_field (p : ℕ) [fact (nat.prime p)] (n : ℕ) :
polynomial.is_splitting_field (zmod p) (galois_field p n) (polynomial.X ^ p ^ n - polynomial.X)
source
@[protected, instance]
def galois_field.char_p (p : ℕ) [fact (nat.prime p)] (n : ℕ) :
char_p (galois_field p n) p
source
@[protected, instance]
noncomputable def galois_field.fintype (p : ℕ) [fact (nat.prime p)] (n : ℕ) :
fintype (galois_field p n)
Equations
source
theorem galois_field.finrank (p : ℕ) [fact (nat.prime p)] {n : ℕ} (h : n ≠ 0) :
finite_dimensional.finrank (zmod p) (galois_field p n) = n
source
theorem galois_field.card (p : ℕ) [fact (nat.prime p)] (n : ℕ) (h : n ≠ 0) :
fintype.card (galois_field p n) = p ^ n
source
theorem galois_field.splits_zmod_X_pow_sub_X (p : ℕ) [fact (nat.prime p)] :
polynomial.splits (ring_hom.id (zmod p)) (polynomial.X ^ p - polynomial.X)
source
noncomputable def galois_field.equiv_zmod_p (p : ℕ) [fact (nat.prime p)] :
galois_field p 1 ≃ₐ[zmod p] zmod p

A Galois field with exponent 1 is equivalent to zmod

Equations
source
theorem galois_field.splits_X_pow_card_sub_X (p : ℕ) [fact (nat.prime p)] {K : Type u_1} [field K] [fintype K] [algebra (zmod p) K] :
polynomial.splits (algebra_map (zmod p) K) (polynomial.X ^ fintype.card K - polynomial.X)
source
theorem galois_field.is_splitting_field_of_card_eq (p : ℕ) [fact (nat.prime p)] (n : ℕ) {K : Type u_1} [field K] [fintype K] [algebra (zmod p) K] (h : fintype.card K = p ^ n) :
polynomial.is_splitting_field (zmod p) K (polynomial.X ^ p ^ n - polynomial.X)
source
@[protected, instance]
def galois_field.is_galois {K : Type u_1} {K' : Type u_2} [field K] [field K'] [finite K'] [algebra K K'] :
is_galois K K'
source
noncomputable def galois_field.alg_equiv_galois_field (p : ℕ) [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] galois_field p n

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

Equations
source
noncomputable def finite_field.alg_equiv_of_card_eq {K : Type u_1} [field K] [fintype K] {K' : Type u_2} [field K'] [fintype K'] (p : ℕ) [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
source
noncomputable def finite_field.ring_equiv_of_card_eq {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