Absolute irreducibility of the descended nonsplit trace curve

The descended coordinates are (z, u), whereas the split cover uses (u, w). We therefore keep u as the outer polynomial variable and treat the Cayley change w = (z-δ^p)/(z-δ) as an automorphism of the rational function coefficient field.

noncomputable def BGS.Markoff.finTwoSecondToIteratedPolynomial {K : Type u_1} [Field K] : MvPolynomial (Fin 2) K ≃+* Polynomial (Polynomial K)

View a bivariate polynomial as a polynomial in coordinate 1, with coefficients in coordinate 0. This is the coordinate order needed after the descended curve's (z,u) coordinates are compared with the split cover's (u,w) coordinates.

Equations

• BGS.Markoff.finTwoSecondToIteratedPolynomial = (MvPolynomial.renameEquiv K (Equiv.swap 0 1)).toRingEquiv.trans BGS.Markoff.finTwoToIteratedPolynomial.toRingEquiv

@[simp]

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_X_zero {K : Type u_1} [Field K] : finTwoSecondToIteratedPolynomial (MvPolynomial.X 0) = Polynomial.C Polynomial.X

@[simp]

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_X_one {K : Type u_1} [Field K] : finTwoSecondToIteratedPolynomial (MvPolynomial.X 1) = Polynomial.X

@[simp]

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_C {K : Type u_1} [Field K] (r : K) : finTwoSecondToIteratedPolynomial (MvPolynomial.C r) = Polynomial.C (Polynomial.C r)

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] (phi : K →+* L) (P : MvPolynomial (Fin 2) K) : finTwoSecondToIteratedPolynomial ((MvPolynomial.map phi) P) = Polynomial.map (Polynomial.mapRingHom phi) (finTwoSecondToIteratedPolynomial P)

The descended coordinate-order equivalence commutes with scalar extension.

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_splitTraceCoverPolynomial {K : Type u_1} [Field K] (alpha beta : K) (e d : ℕ) : finTwoSecondToIteratedPolynomial (splitTraceCoverPolynomial alpha beta e d) = Polynomial.C (Polynomial.C alpha * Polynomial.X ^ e) * Polynomial.X ^ (2 * d) + Polynomial.C (Polynomial.C beta * Polynomial.X ^ e) - Polynomial.C (Polynomial.X ^ (2 * e) + 1) * Polynomial.X ^ d

theorem BGS.Markoff.finTwoToIteratedPolynomial_splitTraceCoverPolynomial_general {K : Type u_1} [Field K] (alpha beta : K) (e d : ℕ) : finTwoToIteratedPolynomial (splitTraceCoverPolynomial alpha beta e d) = (Polynomial.monomial (2 * e)) (-Polynomial.X ^ d) + (Polynomial.monomial e) (Polynomial.C alpha * Polynomial.X ^ (2 * d) + Polynomial.C beta) + Polynomial.C (-Polynomial.X ^ d)

theorem BGS.Markoff.finTwoToIteratedPolynomial_splitTraceCoverPolynomial_general_natDegree {K : Type u_1} [Field K] (alpha beta : K) (e d : ℕ) (he : 0 < e) : (finTwoToIteratedPolynomial (splitTraceCoverPolynomial alpha beta e d)).natDegree = 2 * e

theorem BGS.Markoff.descendedIteratedPolynomial_isPrimitive_of_isCoprime {K : Type u_1} [Field K] (Q N : Polynomial K) (e : ℕ) (he : 0 < e) (hcoprime : IsCoprime Q N) : ((Polynomial.monomial (2 * e)) (-Q) + (Polynomial.monomial e) N + Polynomial.C (-Q)).IsPrimitive

noncomputable def BGS.Markoff.extendedCayleyNumeratorFactor (p : ℕ) [Fact (Nat.Prime p)] : Polynomial (quadraticFiniteField p)

The numerator factor in the extended Cayley parametrization.

Equations

• BGS.Markoff.extendedCayleyNumeratorFactor p = Polynomial.X - Polynomial.C (BGS.Markoff.quadraticNonbaseElement p ^ p)

noncomputable def BGS.Markoff.extendedCayleyDenominatorFactor (p : ℕ) [Fact (Nat.Prime p)] : Polynomial (quadraticFiniteField p)

The denominator factor in the extended Cayley parametrization.

Equations

• BGS.Markoff.extendedCayleyDenominatorFactor p = Polynomial.X - Polynomial.C (BGS.Markoff.quadraticNonbaseElement p)

noncomputable def BGS.Markoff.extendedSeededCayleyNumerator (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) : Polynomial (quadraticFiniteField p)

The seeded numerator polynomial obtained from the extended Cayley factor.

Equations

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

noncomputable def BGS.Markoff.extendedCayleyNormFactor (p : ℕ) [Fact (Nat.Prime p)] : Polynomial (quadraticFiniteField p)

The norm factor in the extended Cayley parametrization.

Equations

• BGS.Markoff.extendedCayleyNormFactor p = BGS.Markoff.extendedCayleyNumeratorFactor p * BGS.Markoff.extendedCayleyDenominatorFactor p

theorem BGS.Markoff.extendedCayleyNormFactor_isCoprime_extendedSeededCayleyNumerator (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) (hd : 0 < d) : IsCoprime (extendedCayleyNormFactor p) (extendedSeededCayleyNumerator p s d)

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_map_univariateInFirstCoordinate {K : Type u_1} {L : Type u_2} [Field K] [Field L] (phi : K →+* L) (P : Polynomial K) : finTwoSecondToIteratedPolynomial ((MvPolynomial.map phi) (univariateInFirstCoordinate P)) = Polynomial.C (Polynomial.map phi P)

theorem BGS.Markoff.finTwoSecondToIteratedPolynomial_map_seededNonsplitDescendedPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : finTwoSecondToIteratedPolynomial ((MvPolynomial.map (algebraMap (ZMod p) (quadraticFiniteField p))) (seededNonsplitDescendedPolynomial p s d e)) = (Polynomial.monomial (2 * e)) (-extendedCayleyNormFactor p ^ d) + (Polynomial.monomial e) (extendedSeededCayleyNumerator p s d) + Polynomial.C (-extendedCayleyNormFactor p ^ d)

theorem BGS.Markoff.cayleyTransport_splitIteratedPolynomial {K : Type u_1} [Field K] (alpha beta r t : K) (e d : ℕ) (_hrt : r ≠ t) (hdet : 1 * -t - -r * 1 ≠ 0) : have phi := Algebra.ratFuncLinearFractionalEquiv 1 (-r) 1 (-t) hdet; have _A := RatFunc.X - RatFunc.C r; have B := RatFunc.X - RatFunc.C t; have Q := (Polynomial.X - Polynomial.C r) * (Polynomial.X - Polynomial.C t); have N := Polynomial.C alpha * (Polynomial.X - Polynomial.C r) ^ (2 * d) + Polynomial.C beta * (Polynomial.X - Polynomial.C t) ^ (2 * d); Polynomial.C (B ^ (2 * d)) * Polynomial.map phi.toRingEquiv.toRingHom (Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (finTwoToIteratedPolynomial (splitTraceCoverPolynomial alpha beta e d))) = Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) ((Polynomial.monomial (2 * e)) (-Q ^ d) + (Polynomial.monomial e) N + Polynomial.C (-Q ^ d))

theorem BGS.Markoff.map_seededNonsplitDescendedPolynomial_irreducible_of_map_splitCover (p : ℕ) [Fact (Nat.Prime p)] {L : Type u_1} [Field L] (ι : quadraticFiniteField p →+* L) (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hcover : Irreducible ((MvPolynomial.map ι) (splitTraceCoverPolynomial (↑s) (↑s ^ p) e d))) : Irreducible ((MvPolynomial.map (ι.comp (algebraMap (ZMod p) (quadraticFiniteField p)))) (seededNonsplitDescendedPolynomial p s d e))

Irreducibility descends through the nonsplit Cayley model after any field extension of the quadratic splitting field. This is the algebraic core used below with an algebraic closure as the target field.

theorem BGS.Markoff.seededNonsplitDescendedPolynomial_absolutelyIrreducible_of_splitCover (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (hd : 0 < d) (he : 0 < e) (hcover : Irreducible ((MvPolynomial.map (algebraMap (quadraticFiniteField p) (AlgebraicClosure (quadraticFiniteField p)))) (splitTraceCoverPolynomial (↑s) (↑s ^ p) e d))) : Irreducible ((MvPolynomial.map (algebraMap (ZMod p) (AlgebraicClosure (ZMod p)))) (seededNonsplitDescendedPolynomial p s d e))

Absolute irreducibility of the descended nonsplit trace curve follows from absolute irreducibility of its split cover. The proof applies the split-cover premise over the quadratic field's algebraic closure, performs the explicit Cayley descent there, and then uses uniqueness of algebraic closures over the base field.