10.2. Quotient types🔗

The two primitive notions are Hex.GFqRing.reduceMod (canonical remainder modulo f) and Hex.GFqRing.PolyQuotient (the subtype of reduced representatives).

def

Hex.GFqRing.reduceMod {p : Nat} [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) : Hex.FpPoly p → Hex.FpPoly p
Hex.GFqRing.reduceMod {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f : Hex.FpPoly p) :
  Hex.FpPoly p → Hex.FpPoly p

Canonical remainder reduction modulo f, using the existing division surface.

def

Hex.GFqRing.IsReduced {p : Nat} [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) : Prop
Hex.GFqRing.IsReduced {p : Nat}
  [Hex.ZMod64.Bounds p]
  (f g : Hex.FpPoly p) : Prop

Polynomials already known to be canonical representatives modulo f.

def

Hex.GFqRing.PolyQuotient {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (_hf : 0 < f.degree) :
  Type
Hex.GFqRing.PolyQuotient {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.FpPoly p)
  (_hf : 0 < f.degree) : Type

Executable quotient elements, carrying the reducedness invariant in the type.

A value of this type is a polynomial together with a proof that it lies in the image of reduceMod f, so a raw FpPoly p cannot be supplied where one of these is expected.

The modulus is required to be prime, which guarantees the representative is canonical for every nonconstant f: reduceMod is a genuine remainder only when the leading coefficient it divides by is a unit, and over a prime modulus every nonzero coefficient is. Drop the hypothesis and canonicality can fail. At p = 4 with f = 2X the division step subtracts zero and leaves the remainder untouched, so f and 0 are congruent yet both reduced and distinct. isReduced_iff_degree_lt states the contract this hypothesis buys.

Primality is sufficient, not necessary: a monic f needs no coefficient inversion and would be canonical over any modulus. The uniform prime hypothesis is the deliberate choice here, since every modulus this library serves is over a prime field anyway.

reduceMod itself, and its degree-short-circuit lemmas above, stay general; it is the quotient type that is restricted, because that is what carries the canonicality claim.

Two further definitions are the main entry points: the smart constructor Hex.GFqRing.ofPoly and the projection Hex.GFqRing.repr. Callers never manage reduction by hand: Hex.GFqRing.ofPoly runs the canonical reduction and Hex.GFqRing.repr reads back the stored representative.

def

Hex.GFqRing.ofPoly {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] (f : Hex.FpPoly p) (hf : 0 < f.degree)
  (g : Hex.FpPoly p) : Hex.GFqRing.PolyQuotient f hf
Hex.GFqRing.ofPoly {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (f : Hex.FpPoly p) (hf : 0 < f.degree)
  (g : Hex.FpPoly p) :
  Hex.GFqRing.PolyQuotient f hf

Inject a polynomial into the quotient by reducing it modulo f.

def

Hex.GFqRing.repr {p : Nat} [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p] {f : Hex.FpPoly p} {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) : Hex.FpPoly p
Hex.GFqRing.repr {p : Nat}
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  {f : Hex.FpPoly p} {hf : 0 < f.degree}
  (x : Hex.GFqRing.PolyQuotient f hf) :
  Hex.FpPoly p

Project a quotient element to its canonical polynomial representative.