def HexGFqMathlib.ofPolyHom {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible) : Hex.FpPoly p →+* Hex.GFqField.FiniteField f hf hp hirr

Reduction into the executable finite field is a ring homomorphism.

The component facts live on the quotient-ring layer; this bundles them so that Mathlib constructions needing a RingHom can be pointed at the executable field.

Equations

• HexGFqMathlib.ofPolyHom f hf hp hirr = { toFun := Hex.GFqField.ofPoly f hf hp hirr, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HexGFqMathlib.ofPolyHom_apply {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (g : Hex.FpPoly p) : (ofPolyHom f hf hp hirr) g = Hex.GFqField.ofPoly f hf hp hirr g

def HexGFqMathlib.constPolyHom {p : ℕ} [Hex.ZMod64.Bounds p] : ZMod p →+* Hex.FpPoly p

The constant embedding ZMod p →+* FpPoly p, routing Mathlib's coefficient ring through the executable ZMod64 p.

Equations

• HexGFqMathlib.constPolyHom = { toFun := fun (c : ZMod p) => Hex.DensePoly.C (HexModArithMathlib.ZMod64.ofZMod c), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def HexGFqMathlib.constHom {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible) : ZMod p →+* Hex.GFqField.FiniteField f hf hp hirr

Constants of the executable finite field, as a ring homomorphism from Mathlib's coefficient ring. This is what instantiates Polynomial.eval₂RingHom.

Equations

• HexGFqMathlib.constHom f hf hp hirr = (HexGFqMathlib.ofPolyHom f hf hp hirr).comp HexGFqMathlib.constPolyHom

theorem HexGFqMathlib.ofPolyHom_compose_eq_eval₂ {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (b g : Hex.FpPoly p) : (ofPolyHom f hf hp hirr) (Hex.DensePoly.compose g b) = Polynomial.eval₂ (constHom f hf hp hirr) ((ofPolyHom f hf hp hirr) b) (HexPolyFpMathlib.fpPolyEquiv g)

Substituting b and reducing agrees with evaluating at the reduction of b, for every polynomial.

noncomputable def HexGFqMathlib.substHom {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (hf : 0 < f.degree) (hp : Hex.Nat.Prime p) (hirr : f.Irreducible) (b : Hex.FpPoly p) : Hex.FpPoly p →+* Hex.GFqField.FiniteField f hf hp hirr

Substitution into the executable field, as a ring homomorphism out of the executable polynomials: g ↦ g(b) in F_p[x] / (f).

Equations

• HexGFqMathlib.substHom f hf hp hirr b = (Polynomial.eval₂RingHom (HexGFqMathlib.constHom f hf hp hirr) ((HexGFqMathlib.ofPolyHom f hf hp hirr) b)).comp HexPolyFpMathlib.fpPolyEquiv.toRingHom

theorem HexGFqMathlib.substHom_apply {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (b g : Hex.FpPoly p) : (substHom f hf hp hirr b) g = (ofPolyHom f hf hp hirr) (Hex.DensePoly.compose g b)

theorem HexGFqMathlib.substHom_reduceMod {p : ℕ} [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree} {hp : Hex.Nat.Prime p} {hirr : f.Irreducible} (b fm : Hex.FpPoly p) (hzero : (substHom f hf hp hirr b) fm = 0) (g : Hex.FpPoly p) : (substHom f hf hp hirr b) (Hex.GFqRing.reduceMod fm g) = (substHom f hf hp hirr b) g

Substitution is insensitive to reduction modulo a polynomial it kills.

This is the descent step: two representatives of the same residue differ by a multiple of the modulus, so if the modulus is sent to zero they have the same image.

noncomputable def HexGFqMathlib.conwayX (p n : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hn : Hex.Conway.SupportedEntry p n) : Hex.GFq p n hn

The class of X in the Conway presentation of GFq p n.

Equations

• HexGFqMathlib.conwayX p n hn = (HexGFqMathlib.ofPolyHom (Hex.Conway.conwayPoly p n hn) ⋯ ⋯ ⋯) Hex.FpPoly.X

noncomputable def HexGFqMathlib.conwayGen (p m n : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hn : Hex.Conway.SupportedEntry p n) : Hex.GFq p n hn

The norm element of GFq p n, as a field element rather than a representative: where the generator of the degree-m subfield goes.

Equations

• HexGFqMathlib.conwayGen p m n hn = (HexGFqMathlib.ofPolyHom (Hex.Conway.conwayPoly p n hn) ⋯ ⋯ ⋯) (Hex.Conway.normX (Hex.Conway.conwayPoly p n hn) ⋯ m (n / m))

theorem HexGFqMathlib.conwayGen_eq_norm {m n : ℕ} (p : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hn : Hex.Conway.SupportedEntry p n) (hm_pos : 0 < m) (hmn : m ∣ n) : conwayGen p m n hn = conwayX p n hn ^ ((p ^ n - 1) / (p ^ m - 1))

The computed Conway subfield generator is the explicit finite-field norm power of the ambient class of X.

theorem HexGFqMathlib.substHom_conwayPoly_eq_zero {m n : ℕ} (p : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) (hcompat : Hex.Conway.Compatible p m n hm hn) : (substHom (Hex.Conway.conwayPoly p n hn) ⋯ ⋯ ⋯ (Hex.Conway.normX (Hex.Conway.conwayPoly p n hn) ⋯ m (n / m))) (Hex.Conway.conwayPoly p m hm) = 0

Substituting the norm element kills the smaller Conway polynomial.

This is Tier 2 compatibility, carried from the executable Bool check to the statement a descent needs.

noncomputable def HexGFqMathlib.conwayEmbed (p m n : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) (hcompat : Hex.Conway.Compatible p m n hm hn) : Hex.GFq p m hm →+* Hex.GFq p n hn

The canonical embedding of the degree-m Conway field into the degree-n one.

Given m ∣ n and compatibility of the two committed entries, this is a genuine ring homomorphism GFq p m →+* GFq p n: substitute the norm element for the generator. It is canonical because the target is the Conway norm rather than an arbitrary root of C(p, m), so two callers embedding GF(p^m) into GF(p^n) land on the same copy. That is the property the Conway table exists to provide, and Tier 2 compatibility is what makes the substitution well defined.

Equations

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

theorem HexGFqMathlib.conwayEmbed_X {m n : ℕ} (p : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) (hcompat : Hex.Conway.Compatible p m n hm hn) : (conwayEmbed p m n hm hn hcompat) (conwayX p m hm) = conwayGen p m n hn

The Conway embedding sends the source class of X to the computed subfield generator. Together with conwayGen_eq_norm, this identifies its image with the finite-field norm power in the target.

theorem HexGFqMathlib.conwayEmbed_X_eq_norm {m n : ℕ} (p : ℕ) [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (hm : Hex.Conway.SupportedEntry p m) (hn : Hex.Conway.SupportedEntry p n) (hcompat : Hex.Conway.Compatible p m n hm hn) (hmn : m ∣ n) : (conwayEmbed p m n hm hn hcompat) (conwayX p m hm) = conwayX p n hn ^ ((p ^ n - 1) / (p ^ m - 1))

The Conway embedding sends the source class of X directly to the explicit finite-field norm power of the target class of X.