The field structure on an extension #

toQuot is not just injective but bijective: every class in F[X] / f has a unique representative of degree < d. That gives Ext.ringEquivQuot : Ext P ≃+* AdjoinRoot P.poly, and the separately certified base cardinality gives Nat.card (Ext P) = q ^ d. A Field structure requires [Finite F], [Fact (Nat.card F = P.q)], and irreducibility of the defining polynomial.

Inversion is by Fermat's little theorem, x⁻¹ = x ^ (q^d - 2), matching how CompPoly/Fields/Montgomery/Native32Field.lean inverts in the base field. Exponentiation is binary, so this costs O(d · log q) extension multiplications.

The instance is assembled by hand rather than via Function.Injective.field, for the same reason as Ext.instCommRing: that transport takes toQuot as data and would make the whole structure noncomputable, which then shadows the computable Mul and Pow. The qsmul / nnqsmul fields use the castRec defaults, following mkDivisionRingInstance in CompPoly/Fields/Binary/Tower/Concrete/Core.lean.

Main definitions and statements #

Ext.toQuot_surjective, Ext.ringEquivQuot: Ext P ≃+* AdjoinRoot P.poly.
Ext.inv: Fermat inversion.
Ext.instField: the Field structure, given finite base field, certified Nat.card F = P.q, and irreducibility of P.poly.

Implementation notes #

The inverse candidate is defined in Extension/Arithmetic.lean; its correctness depends on the certificates above. Extension/Cardinality.lean supplies the finite-coordinate facts without importing the polynomial quotient bridge.

source

instance CompPoly.Extension.Ext.instNontrivial {F : Type u_1} [Field F] {P : ExtensionParams F} :

Nontrivial (Ext P)

source

theorem CompPoly.Extension.Ext.four_le_card_pow {F : Type u_1} [Field F] {P : ExtensionParams F} [Finite F] [Fact (Nat.card F = P.q)] :

4 ≤ P.q ^ P.d

4 ≤ q ^ d, since 2 ≤ q and 2 ≤ d. Used to justify the Fermat exponent q ^ d - 2.

Surjectivity and the ring equivalence #

source

theorem CompPoly.Extension.Ext.toQuot_surjective {F : Type u_1} [Field F] {P : ExtensionParams F} :

Function.Surjective toQuot

source

theorem CompPoly.Extension.Ext.toQuot_bijective {F : Type u_1} [Field F] {P : ExtensionParams F} :

Function.Bijective toQuot

source

noncomputable def CompPoly.Extension.Ext.ringEquivQuot {F : Type u_1} [Field F] (P : ExtensionParams F) :

Ext P ≃+* AdjoinRoot P.poly

The extension is isomorphic to its specification F[X] / f.

Instances For

source

@[simp]

theorem CompPoly.Extension.Ext.ringEquivQuot_apply {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) :

(ringEquivQuot P) x = x.toQuot

source

@[instance_reducible]

noncomputable instance CompPoly.Extension.Ext.instFintypeQuot {F : Type u_1} [Field F] {P : ExtensionParams F} [Fintype F] :

Fintype (AdjoinRoot P.poly)

The quotient is finite, transported along the ring equivalence.

source

theorem CompPoly.Extension.Ext.card_quot {F : Type u_1} [Field F] {P : ExtensionParams F} [Fintype F] [Fact (Nat.card F = P.q)] :

Fintype.card (AdjoinRoot P.poly) = P.q ^ P.d

Inversion #

The canonical inverse candidate and its Inv/Div instances come from the raw arithmetic module. The following laws require certified cardinality; cancellation also requires irreducibility.

source

theorem CompPoly.Extension.Ext.inv_zero' {F : Type u_1} [Field F] {P : ExtensionParams F} [Finite F] [Fact (Nat.card F = P.q)] :

0⁻¹ = 0