Documentation

CompPoly.Fields.Extension.Bridge

Bridging Ext P to AdjoinRoot P.poly #

The computable coefficient-vector arithmetic of CompPoly/Fields/Extension/Defs.lean is related to its specification AdjoinRoot f by

toQuot x = ∑ i, algebraMap F _ (x.coeff i) * root ^ i,

which is shown to be an injective ring homomorphism. The ring axioms on Ext P are then discharged by pushing through toQuot rather than proved on coordinates.

The load-bearing lemma is toQuot_shiftReduce: shiftReduce is "multiply by X, reduce mod f", and correspondingly toQuot (shiftReduce e) = rt * toQuot e. Everything about multiplication follows from it: monomialMod k = X^k mod f satisfies toQuot (monomialMod k) = rt ^ k by a one-line induction, and toQuot_mul is then a direct double sum with no case analysis on wrap-around.

Main definitions and statements #

Bijectivity, cardinality and the Field structure are in CompPoly/Fields/Extension/Field.lean.

source
def CompPoly.Extension.Ext.«termQuot[_]» :
Lean.ParserDescr

The specification of the extension: the quotient ring F[X] / f.

Instances For
    source
    noncomputable def CompPoly.Extension.Ext.rt {F : Type u_1} [Field F] (P : ExtensionParams F) :
    AdjoinRoot P.poly

    The image of X in the quotient, i.e. the adjoined root of f.

    Instances For
      source
      theorem CompPoly.Extension.Ext.degree_poly {F : Type u_1} [Field F] {P : ExtensionParams F} :
      P.poly.degree = ↑P.d

      The degree of the defining polynomial, as a WithBot ℕ.

      source
      noncomputable def CompPoly.Extension.Ext.toQuot {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) :
      AdjoinRoot P.poly

      The map from coefficient vectors to the quotient ring.

      Instances For

        toQuot is additive #

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_zero {F : Type u_1} [Field F] {P : ExtensionParams F} :
        toQuot 0 = 0
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_add {F : Type u_1} [Field F] {P : ExtensionParams F} (x y : Ext P) :
        (x + y).toQuot = x.toQuot + y.toQuot
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_neg {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) :
        (-x).toQuot = -x.toQuot
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_sub {F : Type u_1} [Field F] {P : ExtensionParams F} (x y : Ext P) :
        (x - y).toQuot = x.toQuot - y.toQuot
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_smul {F : Type u_1} [Field F] {P : ExtensionParams F} (c : F) (x : Ext P) :
        (c • x).toQuot = (algebraMap F (AdjoinRoot P.poly)) c * x.toQuot
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_one {F : Type u_1} [Field F] {P : ExtensionParams F} :
        toQuot 1 = 1

        Only the constant coefficient of 1 is nonzero, so toQuot 1 collapses to 1.

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_natCast {F : Type u_1} [Field F] {P : ExtensionParams F} (n : ℕ) :
        (↑n).toQuot = ↑n
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_intCast {F : Type u_1} [Field F] {P : ExtensionParams F} (n : ℤ) :
        (↑n).toQuot = ↑n

        Injectivity #

        source
        theorem CompPoly.Extension.Ext.toQuot_eq_mk {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) :
        x.toQuot = (AdjoinRoot.mk P.poly) (∑ i : Fin P.d, Polynomial.C (x.coeff i) * Polynomial.X ^ ↑i)

        toQuot as the class of an explicit degree-< d polynomial representative.

        source
        theorem CompPoly.Extension.Ext.toQuot_injective {F : Type u_1} [Field F] {P : ExtensionParams F} :
        Function.Injective toQuot
        source
        theorem CompPoly.Extension.Ext.toQuot_inj {F : Type u_1} [Field F] {P : ExtensionParams F} {x y : Ext P} :
        x.toQuot = y.toQuot ↔ x = y

        The defining relation and the multiply-by-X homomorphism law #

        source
        theorem CompPoly.Extension.Ext.toQuot_rangeForm {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) :
        x.toQuot = ∑ k ∈ Finset.range P.d, (algebraMap F (AdjoinRoot P.poly)) (x.coeffNat k) * rt P ^ k

        toQuot as a sum over Finset.range, using the total coeffNat. Convenient for the shift reindexing in toQuot_shiftReduce.

        source
        theorem CompPoly.Extension.Ext.rt_relation {F : Type u_1} [Field F] {P : ExtensionParams F} :
        rt P ^ P.d + ∑ i : Fin P.d, (algebraMap F (AdjoinRoot P.poly)) (P.lowerCoeff i) * rt P ^ ↑i = 0

        The defining relation, from AdjoinRoot.mk_self: the adjoined root rt satisfies rt ^ d + ∑ lowerᵢ · rt ^ i = 0.

        source
        theorem CompPoly.Extension.Ext.sum_lower_rangeForm {F : Type u_1} [Field F] {P : ExtensionParams F} :
        ∑ m ∈ Finset.range P.d, (algebraMap F (AdjoinRoot P.poly)) (P.lowerCoeffNat m) * rt P ^ m = -rt P ^ P.d

        In range form: ∑_{m < d} lowerₘ · rt ^ m = -rt ^ d.

        source
        theorem CompPoly.Extension.Ext.coeffNat_shiftReduce {F : Type u_1} [Field F] {P : ExtensionParams F} (e : Ext P) {m : ℕ} (h : m < P.d) :
        e.shiftReduce.coeffNat m = (if m = 0 then 0 else e.coeffNat (m - 1)) - e.coeffNat (P.d - 1) * P.lowerCoeffNat m

        The coefficient formula for shiftReduce, in coeffNat form.

        source
        theorem CompPoly.Extension.Ext.toQuot_shiftReduce {F : Type u_1} [Field F] {P : ExtensionParams F} (e : Ext P) :
        e.shiftReduce.toQuot = rt P * e.toQuot

        The multiply-by-X homomorphism law. shiftReduce is multiplication by X in the quotient, so toQuot (shiftReduce e) = rt * toQuot e. This is the one place rt_relation is consumed, and everything about multiplication reduces to it.

        Reduced monomials #

        source
        @[simp]
        theorem CompPoly.Extension.Ext.monomialMod_zero {F : Type u_1} [Field F] {P : ExtensionParams F} :
        monomialMod 0 = 1
        source
        theorem CompPoly.Extension.Ext.monomialMod_succ {F : Type u_1} [Field F] {P : ExtensionParams F} (k : ℕ) :
        monomialMod (k + 1) = (monomialMod k).shiftReduce
        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_monomialMod {F : Type u_1} [Field F] {P : ExtensionParams F} (k : ℕ) :
        (monomialMod k).toQuot = rt P ^ k

        monomialMod k really is X^k reduced: its image under toQuot is rt ^ k.

        toQuot is multiplicative #

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_mul {F : Type u_1} [Field F] {P : ExtensionParams F} (x y : Ext P) :
        (x * y).toQuot = x.toQuot * y.toQuot

        Exponentiation #

        x ^ n on Ext P is npowBinRec, i.e. repeated squaring, so it costs O(log n) multiplications. npowBinRec_succ needs only Semigroup, and associativity is already available from toQuot_mul plus injectivity — so exponentiation can be handled before the full ring structure is transported.

        source
        theorem CompPoly.Extension.Ext.mul_assoc' {F : Type u_1} [Field F] {P : ExtensionParams F} (x y z : Ext P) :
        x * y * z = x * (y * z)

        Associativity. Kept out of the instance graph as a plain theorem to avoid a Semigroup diamond with the CommRing instance below.

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_pow {F : Type u_1} [Field F] {P : ExtensionParams F} (x : Ext P) (n : ℕ) :
        (x ^ n).toQuot = x.toQuot ^ n

        Algebraic structure #

        The axioms are all discharged by pushing through the injective toQuot, but the instances are built field-by-field with where rather than via Function.Injective.commRing. That transport takes toQuot as data, which would make the resulting instance noncomputable and — because Monoid.toNatPow then outranks Ext.instPow — would silently break compiled x ^ n. Building by hand keeps every operation computable, matching how CPolynomial assembles its instances in CompPoly/Univariate/Basic.lean.

        source
        @[instance_reducible]
        instance CompPoly.Extension.Ext.instAddCommGroup {F : Type u_1} [Field F] {P : ExtensionParams F} :
        AddCommGroup (Ext P)
        source
        @[instance_reducible]
        instance CompPoly.Extension.Ext.instCommRing {F : Type u_1} [Field F] {P : ExtensionParams F} :
        CommRing (Ext P)

        The base field and the adjoined root #

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_ofBase {F : Type u_1} [Field F] {P : ExtensionParams F} (c : F) :
        (ofBase c).toQuot = (algebraMap F (AdjoinRoot P.poly)) c

        ofBase lands on the constant coefficient, so it agrees with algebraMap into the quotient.

        source
        @[simp]
        theorem CompPoly.Extension.Ext.toQuot_gen {F : Type u_1} [Field F] {P : ExtensionParams F} :
        gen.toQuot = rt P

        gen is the class of X, i.e. the adjoined root.

        source
        def CompPoly.Extension.Ext.ofBaseRingHom {F : Type u_1} [Field F] (P : ExtensionParams F) :
        F →+* Ext P

        The base-field embedding, as a ring homomorphism.

        Instances For
          source
          @[simp]
          theorem CompPoly.Extension.Ext.ofBaseRingHom_apply {F : Type u_1} [Field F] {P : ExtensionParams F} (c : F) :
          (ofBaseRingHom P) c = ofBase c
          source
          @[instance_reducible]
          instance CompPoly.Extension.Ext.instAlgebra {F : Type u_1} [Field F] {P : ExtensionParams F} :
          Algebra F (Ext P)

          The extension is an F-algebra.

          source
          @[simp]
          theorem CompPoly.Extension.Ext.algebraMap_eq_ofBase {F : Type u_1} [Field F] {P : ExtensionParams F} (c : F) :
          (algebraMap F (Ext P)) c = ofBase c
          source
          theorem CompPoly.Extension.Ext.toQuot_sum {F : Type u_1} [Field F] {P : ExtensionParams F} {ι : Type u_2} (s : Finset ι) (f : ι → Ext P) :
          (∑ i ∈ s, f i).toQuot = ∑ i ∈ s, (f i).toQuot
          source
          theorem CompPoly.Extension.Ext.gen_pow_d {F : Type u_1} [Field F] {P : ExtensionParams F} :
          gen ^ P.d = monomialMod P.d

          The defining relation at the level of Ext: gen ^ d equals the reduced monomial monomialMod d.

          source
          theorem CompPoly.Extension.Ext.aeval_gen_poly {F : Type u_1} [Field F] {P : ExtensionParams F} :
          (Polynomial.aeval gen) P.poly = 0

          gen is a root of the defining polynomial, in the form Mathlib's aeval expects.

          source
          noncomputable def CompPoly.Extension.Ext.toQuotRingHom {F : Type u_1} [Field F] (P : ExtensionParams F) :
          Ext P →+* AdjoinRoot P.poly

          toQuot packaged as a ring homomorphism.

          Instances For

            Binomial compatibility #

            For a binomial modulus X^d - W, the general defining relation rt ^ d = -∑ lowerᵢ rt ^ i collapses (the only nonzero lower coefficient is lower₀ = -W) to rt ^ d = W, recovering the gen ^ d = ofBase W law the degree-4 extensions rely on.

            source
            theorem CompPoly.Extension.Ext.rt_pow_d_binomial {F : Type u_1} [Field F] (P : BinomialParams F) :
            rt P.toExtensionParams ^ P.d = (algebraMap F (AdjoinRoot P.toExtensionParams.poly)) P.W

            The collapsed defining relation for a binomial modulus: rt ^ d = W.

            source
            theorem CompPoly.Extension.Ext.gen_pow_d_binomial {F : Type u_1} [Field F] (P : BinomialParams F) :
            gen ^ P.d = ofBase P.W

            The binomial defining relation at the level of Ext: gen ^ d = ofBase W.