Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Condenser.Modulus.Binary.Extension.Internal

Flattening a binomial tower into one binary quotient #

Polynomial composition multiplies the power-of-three exponents. Mathlib's AdjoinRoot.compAlgEquiv then supplies the tower equivalence and its generator laws, with only equality transports on the two defining polynomials.

source
theorem Algebraic.Cutwidth.Extractor.Internal.binaryModulus_comp_pow_three (s v : ℕ) :
(binaryModulus s).comp (Polynomial.X ^ 3 ^ v) = binaryModulus (s + v)
source
theorem Algebraic.Cutwidth.Extractor.Internal.extensionModulus_monic (s v : ℕ) :
(extensionModulus s v).Monic
source
theorem Algebraic.Cutwidth.Extractor.Internal.extensionModulus_natDegree (s v : ℕ) :
(extensionModulus s v).natDegree = 3 ^ v
source
theorem Algebraic.Cutwidth.Extractor.Internal.extensionModulus_irreducible (s v : ℕ) :
Irreducible (extensionModulus s v)
source
noncomputable def Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv (s v : ℕ) :
AdjoinRoot (binaryModulus (s + v)) ≃ₐ[ZMod 2] AdjoinRoot (extensionModulus s v)

Transport Mathlib's composition equivalence along the two polynomial identities.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_root (s v : ℕ) :
    (binaryExtensionEquiv s v) (AdjoinRoot.root (binaryModulus (s + v))) = AdjoinRoot.root (extensionModulus s v)
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_symm_root (s v : ℕ) :
    (binaryExtensionEquiv s v).symm (AdjoinRoot.root (extensionModulus s v)) = AdjoinRoot.root (binaryModulus (s + v))
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.root_extensionModulus_pow (s v : ℕ) :
    AdjoinRoot.root (extensionModulus s v) ^ 3 ^ v = (AdjoinRoot.of (extensionModulus s v)) (AdjoinRoot.root (binaryModulus s))
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_symm_of_root (s v : ℕ) :
    (binaryExtensionEquiv s v).symm ((AdjoinRoot.of (extensionModulus s v)) (AdjoinRoot.root (binaryModulus s))) = AdjoinRoot.root (binaryModulus (s + v)) ^ 3 ^ v
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_mk (s v : ℕ) (p : Polynomial (ZMod 2)) :
    (binaryExtensionEquiv s v) ((AdjoinRoot.mk (binaryModulus (s + v))) p) = (Polynomial.aeval (AdjoinRoot.root (extensionModulus s v))) p
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_symm_of_mk (s v : ℕ) (p : Polynomial (ZMod 2)) :
    (binaryExtensionEquiv s v).symm ((AdjoinRoot.of (extensionModulus s v)) ((AdjoinRoot.mk (binaryModulus s)) p)) = (Polynomial.aeval (AdjoinRoot.root (binaryModulus (s + v)) ^ 3 ^ v)) p
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.binaryExtensionEquiv_symm_mk (s v : ℕ) (p : Polynomial (AdjoinRoot (binaryModulus s))) :
    (binaryExtensionEquiv s v).symm ((AdjoinRoot.mk (extensionModulus s v)) p) = Polynomial.eval₂ ((binaryExtensionEquiv s v).symm.toRingEquiv.toRingHom.comp (AdjoinRoot.of (extensionModulus s v))) (AdjoinRoot.root (binaryModulus (s + v))) p