Square classes for the incidence auxiliary curve

This file proves the polynomial and rational-function-field algebra behind geometric integrality of the off-diagonal incidence curve. The remaining coordinate-ring normal-form argument is stated separately in BGS.Markoff.Incidence.

theorem BGS.Markoff.not_isSquare_algebraMap_of_squarefree_not_isUnit {R : Type u_2} {Q : Type u_3} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] [Field Q] [Algebra R Q] [IsFractionRing R Q] {f : R} (hsq : Squarefree f) (hf : ¬IsUnit f) : ¬IsSquare ((algebraMap R Q) f)

A nonunit squarefree element of a UFD does not become a square in its fraction field.

noncomputable def BGS.Markoff.incidenceBranchPolynomial {K : Type u_1} [Field K] (a : K) : Polynomial K

The twofold-cover polynomial whose square root is the auxiliary lambda coordinate.

Equations

• BGS.Markoff.incidenceBranchPolynomial a = Polynomial.C (9 * a ^ 2 - 4) * Polynomial.X ^ 2 - Polynomial.C (4 * a ^ 2)

theorem BGS.Markoff.incidenceBranchPolynomial_natDegree {K : Type u_1} [Field K] {a : K} (hA : 9 * a ^ 2 - 4 ≠ 0) : (incidenceBranchPolynomial a).natDegree = 2

theorem BGS.Markoff.incidenceBranchPolynomial_not_isUnit {K : Type u_1} [Field K] {a : K} (hA : 9 * a ^ 2 - 4 ≠ 0) : ¬IsUnit (incidenceBranchPolynomial a)

theorem BGS.Markoff.incidenceBranchPolynomial_linearCombination {K : Type u_1} [Field K] (a b : K) : Polynomial.C (9 * b ^ 2 - 4) * incidenceBranchPolynomial a - Polynomial.C (9 * a ^ 2 - 4) * incidenceBranchPolynomial b = Polynomial.C (16 * (a ^ 2 - b ^ 2))

The branch polynomials for two parameters have an explicit constant Bezout combination.

theorem BGS.Markoff.incidenceBranchPolynomial_isCoprime {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {a b : K} (hab : a ^ 2 ≠ b ^ 2) : IsCoprime (incidenceBranchPolynomial a) (incidenceBranchPolynomial b)

Away from characteristic two, distinct parameter squares give coprime branch polynomials.

theorem BGS.Markoff.incidenceBranchPolynomial_separable {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {a : K} (ha : a ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) : (incidenceBranchPolynomial a).Separable

Each branch polynomial is separable under exactly the nondegeneracy hypotheses used in the incidence graph.

theorem BGS.Markoff.incidenceBranchPolynomial_product_squarefree {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : Squarefree (incidenceBranchPolynomial a * incidenceBranchPolynomial b)

The product has no repeated irreducible factor. This is the polynomial shadow of the independence of the two quadratic square classes.

theorem BGS.Markoff.incidenceBranchSquareClasses_independent_ratFunc {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial a)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial b)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial a * incidenceBranchPolynomial b))

The three nonzero elements of the span of the two branch square classes are nonsquares in the rational function field. Equivalently, the two classes are linearly independent over ZMod 2.

theorem BGS.Markoff.incidenceBranchLocation_injective {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {a b : K} (h : a ^ 2 * (9 * b ^ 2 - 4) = b ^ 2 * (9 * a ^ 2 - 4)) : a ^ 2 = b ^ 2

Equality of the squared branch locations forces equality of the parameter squares.