Documentation

LeanPool.MarkoffModP.BGS.Algebra.ClearedLinearFractionalSubstitution

Cleared linear-fractional substitution #

For a polynomial f of degree n, this file studies the polynomial obtained from f ((a * X + b) / (c * X + d)) by multiplying by (c * X + d) ^ n.

The degree assumption in the irreducibility theorem is essential: inversion sends the linear polynomial X to the unit polynomial 1 after clearing its denominator.

source
noncomputable def BGS.clearedLinearFractionalSubstitution {K : Type u_1} [Field K] (f : Polynomial K) (a b c d : K) :
Polynomial K

The denominator-cleared substitution (cX+d)^deg(f) f((aX+b)/(cX+d)), written without division.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGS.natDegree_clearedLinearFractionalSubstitution_le {K : Type u_1} [Field K] (f : Polynomial K) (a b c d : K) :
    (clearedLinearFractionalSubstitution f a b c d).natDegree ≤ f.natDegree
    source
    theorem BGS.aeval_clearedLinearFractionalSubstitution {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (f : Polynomial K) (a b c d : K) (x y : L) (hrelation : (algebraMap K L) a * x + (algebraMap K L) b = y * ((algebraMap K L) c * x + (algebraMap K L) d)) :
    (Polynomial.aeval x) (clearedLinearFractionalSubstitution f a b c d) = ((algebraMap K L) c * x + (algebraMap K L) d) ^ f.natDegree * (Polynomial.aeval y) f
    source
    theorem BGS.irreducible_clearedLinearFractionalSubstitution {K : Type u_1} [Field K] {f : Polynomial K} (hf : Irreducible f) (hfDegree : 2 ≤ f.natDegree) {a b c d : K} (hdet : a * d - b * c ≠ 0) :
    Irreducible (clearedLinearFractionalSubstitution f a b c d)

    An invertible linear-fractional change of variable preserves irreducibility after clearing denominators at the degree of the polynomial. Degree at least two is necessary: for the inversion matrix, the cleared transform of X is 1.