Finite fields of prime-power order

This file separates the finite-geometric construction from its numerical prime-power indexing. A FiniteFieldModel stores the carrier and the exact field and finiteness structures that are used to compute its cardinality.

For every natural-number prime power q, finiteFieldModelOfPrimePower chooses a Galois field of cardinality exactly q. The subtype PrimePowerIndex is ordered by its underlying natural number, so atTop on this type is literally the filter "as q tends to infinity through prime powers". The cofinality theorem below makes that interpretation explicit.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

structure MooreBound.DegreeDiameter.FiniteFieldModel : Type 1

A finite field together with the particular structures used on its carrier. Keeping the structures explicit makes existential prime-power instantiation straightforward and avoids any hidden choice of instances.

• carrier : Type

  The underlying type of the finite field.

• field : Field self.carrier

  The field structure on the chosen carrier.

• finite : Finite self.carrier

noncomputable def MooreBound.DegreeDiameter.FiniteFieldModel.card (M : FiniteFieldModel) : ℕ

The cardinality of an explicitly packaged finite field.

Equations

• M.card = Nat.card M.carrier

theorem MooreBound.DegreeDiameter.isPrimePow_natCard_finiteField (K : Type u_1) [Field K] [Finite K] : IsPrimePow (Nat.card K)

The cardinality of every finite field is a prime power. Together with exists_finiteFieldModel_of_isPrimePow below, this records both directions of the correspondence used by the prime-power indexing.

theorem MooreBound.DegreeDiameter.exists_finiteFieldModel_of_isPrimePow (q : ℕ) (hq : IsPrimePow q) : ∃ (M : FiniteFieldModel), M.card = q

Every natural-number prime power is the cardinality of an explicitly packaged finite field. The field is the Mathlib Galois field GF(p^e).

theorem MooreBound.DegreeDiameter.isPrimePow_iff_exists_finiteFieldModel (q : ℕ) : IsPrimePow q ↔ ∃ (M : FiniteFieldModel), M.card = q

A natural number is a prime power exactly when it occurs as the cardinality of an explicitly packaged finite field.

@[reducible, inline]

abbrev MooreBound.DegreeDiameter.PrimePowerIndex : Type

Natural numbers that are positive powers of a prime. Its inherited order is the order of the underlying cardinalities.

Equations

• MooreBound.DegreeDiameter.PrimePowerIndex = { q : ℕ // IsPrimePow q }

theorem MooreBound.DegreeDiameter.tendsto_primePowerIndex_val : Filter.Tendsto (fun (q : PrimePowerIndex) => ↑q) Filter.atTop Filter.atTop

Prime powers are cofinal in the natural numbers. Consequently atTop on PrimePowerIndex is precisely "tending to infinity through prime powers".

noncomputable def MooreBound.DegreeDiameter.finiteFieldModelOfPrimePower (q : PrimePowerIndex) : FiniteFieldModel

A chosen finite field model of order q, for each prime power q.

Equations

• MooreBound.DegreeDiameter.finiteFieldModelOfPrimePower q = Classical.choose ⋯

@[simp]

theorem MooreBound.DegreeDiameter.finiteFieldModelOfPrimePower_card (q : PrimePowerIndex) : (finiteFieldModelOfPrimePower q).card = ↑q

@[reducible, inline]

noncomputable abbrev MooreBound.DegreeDiameter.PrimePowerField (q : PrimePowerIndex) : Type

A chosen field of each prime-power cardinality. The construction is noncomputable only because a prime/exponent presentation of q is chosen.

Equations

• MooreBound.DegreeDiameter.PrimePowerField q = (MooreBound.DegreeDiameter.finiteFieldModelOfPrimePower q).carrier

@[instance_reducible]

noncomputable instance MooreBound.DegreeDiameter.primePowerFieldField (q : PrimePowerIndex) : Field (PrimePowerField q)

Equations

• MooreBound.DegreeDiameter.primePowerFieldField q = (MooreBound.DegreeDiameter.finiteFieldModelOfPrimePower q).field

instance MooreBound.DegreeDiameter.primePowerFieldFinite (q : PrimePowerIndex) : Finite (PrimePowerField q)

@[simp]

theorem MooreBound.DegreeDiameter.natCard_primePowerField (q : PrimePowerIndex) : Nat.card (PrimePowerField q) = ↑q

The chosen field really has the prime-power cardinality indexing it.

theorem MooreBound.DegreeDiameter.tendsto_natCard_primePowerField : Filter.Tendsto (fun (q : PrimePowerIndex) => Nat.card (PrimePowerField q)) Filter.atTop Filter.atTop

The cardinalities of the chosen fields tend to infinity along the prime-power index.