Geometric integrality of the incidence auxiliary coordinate ring

This module proves the missing coordinate-ring algebra by an explicit base change and rank-four biquadratic normal form. Every declaration is proved; there are no placeholder axioms.

noncomputable def BGS.Markoff.incidenceAuxBaseChangeIdeal (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (a b : K) : Ideal (MvPolynomial (Fin 3) L)

The explicit two-equation ideal after extending coefficients from K to L.

Equations

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

theorem BGS.Markoff.incidenceAuxBaseChangeIdeal_eq_map (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (a b : K) : incidenceAuxBaseChangeIdeal K L a b = Ideal.map (MvPolynomial.map (algebraMap K L)) (incidenceAuxIdeal a b)

theorem BGS.Markoff.incidenceAuxBaseChangeIdeal_eq_incidenceAuxIdeal (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (a b : K) : incidenceAuxBaseChangeIdeal K L a b = incidenceAuxIdeal ((algebraMap K L) a) ((algebraMap K L) b)

theorem BGS.Markoff.algebraTensorAlgEquiv_comp_includeRight (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] : (MvPolynomial.algebraTensorAlgEquiv K L).toRingEquiv.toRingHom.comp Algebra.TensorProduct.includeRight.toRingHom = MvPolynomial.map (algebraMap K L)

noncomputable def BGS.Markoff.incidenceAuxCoordinateRingBaseChangeEquiv (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (a b : K) : TensorProduct K L (IncidenceAuxCoordinateRing K a b) ≃ₐ[L] MvPolynomial (Fin 3) L ⧸ incidenceAuxBaseChangeIdeal K L a b

Base change commutes with the explicit presentation of the incidence auxiliary curve.

Equations

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

noncomputable def BGS.Markoff.incidenceAuxCoordinateRingBaseChangeExplicitEquiv (K : Type u) [Field K] (L : Type v) [Field L] [Algebra K L] (a b : K) : TensorProduct K L (IncidenceAuxCoordinateRing K a b) ≃ₐ[L] IncidenceAuxCoordinateRing L ((algebraMap K L) a) ((algebraMap K L) b)

Base change identifies the original coordinate ring with the same two equations over the larger coefficient field.

Equations

• BGS.Markoff.incidenceAuxCoordinateRingBaseChangeExplicitEquiv K L a b = (BGS.Markoff.incidenceAuxCoordinateRingBaseChangeEquiv K L a b).trans (Ideal.quotientEquivAlgOfEq L ⋯)

noncomputable def BGS.Markoff.adjoinSquarePolynomial {R : Type u_1} [CommRing R] (f : R) : Polynomial R

The monic quadratic used to adjoin a square root of an element.

Equations

• BGS.Markoff.adjoinSquarePolynomial f = Polynomial.X ^ 2 - Polynomial.C f

theorem BGS.Markoff.adjoinSquarePolynomial_monic {R : Type u_1} [CommRing R] (f : R) : (adjoinSquarePolynomial f).Monic

theorem BGS.Markoff.adjoinSquarePolynomial_natDegree {R : Type u_1} [Nontrivial R] [CommRing R] (f : R) : (adjoinSquarePolynomial f).natDegree = 2

theorem BGS.Markoff.adjoinSquareRoot_sq {R : Type u_1} [CommRing R] (f : R) : AdjoinRoot.root (adjoinSquarePolynomial f) ^ 2 = (algebraMap R (AdjoinRoot (adjoinSquarePolynomial f))) f

theorem BGS.Markoff.adjoinSquarePolynomial_irreducible_of_not_isSquare {F : Type u_1} [Field F] {f : F} (hf : ¬IsSquare f) : Irreducible (adjoinSquarePolynomial f)

theorem BGS.Markoff.not_isSquare_algebraMap_adjoinSquare_of_independent {F : Type u_1} [Field F] (h2 : 2 ≠ 0) {f g : F} (hf : ¬IsSquare f) (hg : ¬IsSquare g) (hfg : ¬IsSquare (f * g)) : ¬IsSquare ((algebraMap F (AdjoinRoot (adjoinSquarePolynomial f))) g)

In a quadratic extension generated by sqrt f, a base-field element g can become a square only if g or f * g was already a square.

noncomputable def BGS.Markoff.adjoinSquareMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (φ : R →+* S) (f : R) : AdjoinRoot (adjoinSquarePolynomial f) →+* AdjoinRoot (adjoinSquarePolynomial (φ f))

Extend coefficients in a quadratic AdjoinRoot presentation.

Equations

• BGS.Markoff.adjoinSquareMap φ f = AdjoinRoot.map φ (BGS.Markoff.adjoinSquarePolynomial f) (BGS.Markoff.adjoinSquarePolynomial (φ f)) ⋯

theorem BGS.Markoff.adjoinSquareMap_injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial R] [Nontrivial S] (φ : R →+* S) (hφ : Function.Injective ⇑φ) (f : R) : Function.Injective ⇑(adjoinSquareMap φ f)

Extending coefficients in a monic quadratic presentation preserves injectivity.

@[reducible, inline]

abbrev BGS.Markoff.IncidenceFirstQuadraticRing (L : Type v) [Field L] (a : L) : Type v

Adjoin the first branch square root over the polynomial ring in the y-coordinate.

Equations

• BGS.Markoff.IncidenceFirstQuadraticRing L a = AdjoinRoot (BGS.Markoff.adjoinSquarePolynomial (BGS.Markoff.incidenceBranchPolynomial a))

theorem BGS.Markoff.incidenceFirstQuadraticRing_nontrivial (L : Type v) [Field L] (a : L) : Nontrivial (IncidenceFirstQuadraticRing L a)

noncomputable def BGS.Markoff.incidenceSecondQuadraticPolynomial (L : Type v) [Field L] (a b : L) : Polynomial (IncidenceFirstQuadraticRing L a)

Over the first quadratic cover, adjoin the second branch square root.

Equations

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

@[reducible, inline]

abbrev BGS.Markoff.IncidenceBiquadraticRing (L : Type v) [Field L] (a b : L) : Type v

The iterated quadratic algebra with generators satisfying the two incidence equations.

Equations

• BGS.Markoff.IncidenceBiquadraticRing L a b = AdjoinRoot (BGS.Markoff.incidenceSecondQuadraticPolynomial L a b)

@[reducible, inline]

abbrev BGS.Markoff.IncidenceFirstQuadraticRatFuncRing (L : Type v) [Field L] (a : L) : Type v

The first quadratic extension after passing from L[y] to its rational function field.

Equations

• BGS.Markoff.IncidenceFirstQuadraticRatFuncRing L a = AdjoinRoot (BGS.Markoff.adjoinSquarePolynomial ((algebraMap (Polynomial L) (RatFunc L)) (BGS.Markoff.incidenceBranchPolynomial a)))

theorem BGS.Markoff.incidenceFirstQuadraticRatFuncRing_nontrivial (L : Type v) [Field L] (a : L) : Nontrivial (IncidenceFirstQuadraticRatFuncRing L a)

noncomputable def BGS.Markoff.incidenceFirstQuadraticToRatFunc (L : Type v) [Field L] (a : L) : IncidenceFirstQuadraticRing L a →+* IncidenceFirstQuadraticRatFuncRing L a

Extend the first quadratic cover from L[y] to L(y).

Equations

• BGS.Markoff.incidenceFirstQuadraticToRatFunc L a = BGS.Markoff.adjoinSquareMap (algebraMap (Polynomial L) (RatFunc L)) (BGS.Markoff.incidenceBranchPolynomial a)

theorem BGS.Markoff.incidenceFirstQuadraticToRatFunc_algebraMap (L : Type v) [Field L] (a : L) (r : Polynomial L) : (incidenceFirstQuadraticToRatFunc L a) ((algebraMap (Polynomial L) (IncidenceFirstQuadraticRing L a)) r) = (algebraMap (RatFunc L) (IncidenceFirstQuadraticRatFuncRing L a)) ((algebraMap (Polynomial L) (RatFunc L)) r)

noncomputable def BGS.Markoff.incidenceSecondQuadraticRatFuncPolynomial (L : Type v) [Field L] (a b : L) : Polynomial (IncidenceFirstQuadraticRatFuncRing L a)

The second quadratic polynomial over the first rational-function-field extension.

Equations

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

@[reducible, inline]

abbrev BGS.Markoff.IncidenceBiquadraticRatFuncRing (L : Type v) [Field L] (a b : L) : Type v

The biquadratic field presentation over L(y). Field instances are installed below from the two irreducibility proofs.

Equations

• BGS.Markoff.IncidenceBiquadraticRatFuncRing L a b = AdjoinRoot (BGS.Markoff.incidenceSecondQuadraticRatFuncPolynomial L a b)

noncomputable def BGS.Markoff.incidenceBiquadraticToRatFunc (L : Type v) [Field L] (a b : L) : IncidenceBiquadraticRing L a b →+* IncidenceBiquadraticRatFuncRing L a b

Extend both successive quadratic presentations from L[y] to L(y).

Equations

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

theorem BGS.Markoff.incidenceFirstQuadraticToRatFunc_injective (L : Type v) [Field L] (a : L) : Function.Injective ⇑(incidenceFirstQuadraticToRatFunc L a)

theorem BGS.Markoff.incidenceBiquadraticToRatFunc_injective (L : Type v) [Field L] (a b : L) : Function.Injective ⇑(incidenceBiquadraticToRatFunc L a b)

theorem BGS.Markoff.incidenceBiquadraticRatFuncRing_isDomain (L : Type v) [Field L] (h2 : 2 ≠ 0) {a b : L} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : IsDomain (IncidenceBiquadraticRatFuncRing L a b)

The rational-function-field biquadratic presentation is a domain when the three square classes supplied by the branch-polynomial calculation are nontrivial.

theorem BGS.Markoff.incidenceBiquadraticRing_isDomain (L : Type v) [Field L] (h2 : 2 ≠ 0) {a b : L} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : IsDomain (IncidenceBiquadraticRing L a b)

The rank-four algebra over L[y] is a domain because it injects into the preceding biquadratic field presentation.

theorem BGS.Markoff.incidenceSecondQuadraticPolynomial_monic (L : Type v) [Field L] (a b : L) : (incidenceSecondQuadraticPolynomial L a b).Monic

theorem BGS.Markoff.incidenceSecondQuadraticPolynomial_natDegree (L : Type v) [Field L] (a b : L) : (incidenceSecondQuadraticPolynomial L a b).natDegree = 2

noncomputable def BGS.Markoff.incidenceBiquadraticTowerBasis (L : Type v) [Field L] (a b : L) : Module.Basis (Fin (adjoinSquarePolynomial (incidenceBranchPolynomial a)).natDegree × Fin (incidenceSecondQuadraticPolynomial L a b).natDegree) (Polynomial L) (IncidenceBiquadraticRing L a b)

The canonical product basis of the two successive monic quadratic extensions.

Equations

• BGS.Markoff.incidenceBiquadraticTowerBasis L a b = (AdjoinRoot.powerBasis' ⋯).basis.smulTower (AdjoinRoot.powerBasis' ⋯).basis

theorem BGS.Markoff.incidenceBiquadraticRing_finrank (L : Type v) [Field L] (a b : L) : Module.finrank (Polynomial L) (IncidenceBiquadraticRing L a b) = 4

The unreduced two-equation algebra has the expected rank four over L[y].

theorem BGS.Markoff.incidenceFirstQuadraticRoot_sq (L : Type v) [Field L] (a : L) : AdjoinRoot.root (adjoinSquarePolynomial (incidenceBranchPolynomial a)) ^ 2 = (algebraMap (Polynomial L) (IncidenceFirstQuadraticRing L a)) (incidenceBranchPolynomial a)

theorem BGS.Markoff.incidenceSecondQuadraticRoot_sq (L : Type v) [Field L] (a b : L) : AdjoinRoot.root (incidenceSecondQuadraticPolynomial L a b) ^ 2 = (algebraMap (IncidenceFirstQuadraticRing L a) (IncidenceBiquadraticRing L a b)) ((algebraMap (Polynomial L) (IncidenceFirstQuadraticRing L a)) (incidenceBranchPolynomial b))

noncomputable def BGS.Markoff.incidenceBiquadraticY (L : Type v) [Field L] (a b : L) : IncidenceBiquadraticRing L a b

The y-coordinate in the iterated quadratic presentation.

Equations

• BGS.Markoff.incidenceBiquadraticY L a b = (algebraMap (Polynomial L) (BGS.Markoff.IncidenceBiquadraticRing L a b)) Polynomial.X

noncomputable def BGS.Markoff.incidenceBiquadraticLambda (L : Type v) [Field L] (a b : L) : IncidenceBiquadraticRing L a b

The first square-root coordinate in the iterated quadratic presentation.

Equations

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

noncomputable def BGS.Markoff.incidenceBiquadraticMu (L : Type v) [Field L] (a b : L) : IncidenceBiquadraticRing L a b

The second square-root coordinate in the iterated quadratic presentation.

Equations

• BGS.Markoff.incidenceBiquadraticMu L a b = AdjoinRoot.root (BGS.Markoff.incidenceSecondQuadraticPolynomial L a b)

noncomputable def BGS.Markoff.incidenceAuxAevalToBiquadratic (L : Type v) [Field L] (a b : L) : MvPolynomial (Fin 3) L →ₐ[L] IncidenceBiquadraticRing L a b

Evaluate the three-variable incidence presentation in the iterated quadratic algebra.

Equations

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

theorem BGS.Markoff.incidenceAuxAevalToBiquadratic_polynomial1 (L : Type v) [Field L] (a b : L) : (incidenceAuxAevalToBiquadratic L a b) (incidenceAuxPolynomial1 a) = 0

theorem BGS.Markoff.incidenceAuxAevalToBiquadratic_polynomial2 (L : Type v) [Field L] (a b : L) : (incidenceAuxAevalToBiquadratic L a b) (incidenceAuxPolynomial2 b) = 0

theorem BGS.Markoff.incidenceAuxIdeal_le_aevalToBiquadratic_ker (L : Type v) [Field L] (a b : L) : incidenceAuxIdeal a b ≤ RingHom.ker (incidenceAuxAevalToBiquadratic L a b).toRingHom

noncomputable def BGS.Markoff.incidenceAuxCoordinateRingToBiquadratic (L : Type v) [Field L] (a b : L) : IncidenceAuxCoordinateRing L a b →ₐ[L] IncidenceBiquadraticRing L a b

The canonical map from the explicit coordinate-ring quotient to the iterated quadratic normal form.

Equations

• BGS.Markoff.incidenceAuxCoordinateRingToBiquadratic L a b = Ideal.Quotient.liftₐ (BGS.Markoff.incidenceAuxIdeal a b) (BGS.Markoff.incidenceAuxAevalToBiquadratic L a b) ⋯

theorem BGS.Markoff.incidenceBiquadraticY_mem_aeval_range (L : Type v) [Field L] (a b : L) : incidenceBiquadraticY L a b ∈ (incidenceAuxAevalToBiquadratic L a b).range

theorem BGS.Markoff.incidenceBiquadraticLambda_mem_aeval_range (L : Type v) [Field L] (a b : L) : incidenceBiquadraticLambda L a b ∈ (incidenceAuxAevalToBiquadratic L a b).range

theorem BGS.Markoff.incidenceBiquadraticMu_mem_aeval_range (L : Type v) [Field L] (a b : L) : incidenceBiquadraticMu L a b ∈ (incidenceAuxAevalToBiquadratic L a b).range

theorem BGS.Markoff.polynomialAlgebraMap_mem_incidenceAevalRange (L : Type v) [Field L] (a b : L) (r : Polynomial L) : (algebraMap (Polynomial L) (IncidenceBiquadraticRing L a b)) r ∈ (incidenceAuxAevalToBiquadratic L a b).range

theorem BGS.Markoff.firstQuadraticAlgebraMap_mem_incidenceAevalRange (L : Type v) [Field L] (a b : L) (s : IncidenceFirstQuadraticRing L a) : (algebraMap (IncidenceFirstQuadraticRing L a) (IncidenceBiquadraticRing L a b)) s ∈ (incidenceAuxAevalToBiquadratic L a b).range

theorem BGS.Markoff.incidenceAuxAevalToBiquadratic_surjective (L : Type v) [Field L] (a b : L) : Function.Surjective ⇑(incidenceAuxAevalToBiquadratic L a b)

theorem BGS.Markoff.incidenceAuxCoordinateRingToBiquadratic_surjective (L : Type v) [Field L] (a b : L) : Function.Surjective ⇑(incidenceAuxCoordinateRingToBiquadratic L a b)

noncomputable def BGS.Markoff.incidenceAuxCoordinateClass (L : Type v) [Field L] (a b : L) (i : Fin 3) : IncidenceAuxCoordinateRing L a b

The class of one of the three coordinate variables in the auxiliary coordinate ring.

Equations

• BGS.Markoff.incidenceAuxCoordinateClass L a b i = (Ideal.Quotient.mk (BGS.Markoff.incidenceAuxIdeal a b)) (MvPolynomial.X i)

noncomputable def BGS.Markoff.incidenceAuxPolynomialAlgebraMap (L : Type v) [Field L] (a b : L) : Polynomial L →ₐ[L] IncidenceAuxCoordinateRing L a b

The polynomial algebra in y maps to the auxiliary coordinate ring by sending X to the class of the y-coordinate.

Equations

• BGS.Markoff.incidenceAuxPolynomialAlgebraMap L a b = Polynomial.aeval (BGS.Markoff.incidenceAuxCoordinateClass L a b 0)

theorem BGS.Markoff.incidenceAuxPolynomial1_class_eq_zero (L : Type v) [Field L] (a b : L) : (Ideal.Quotient.mk (incidenceAuxIdeal a b)) (incidenceAuxPolynomial1 a) = 0

theorem BGS.Markoff.incidenceAuxPolynomial2_class_eq_zero (L : Type v) [Field L] (a b : L) : (Ideal.Quotient.mk (incidenceAuxIdeal a b)) (incidenceAuxPolynomial2 b) = 0

theorem BGS.Markoff.incidenceAuxLambdaClass_sq (L : Type v) [Field L] (a b : L) : incidenceAuxCoordinateClass L a b 1 ^ 2 = (incidenceAuxPolynomialAlgebraMap L a b) (incidenceBranchPolynomial a)

theorem BGS.Markoff.incidenceAuxMuClass_sq (L : Type v) [Field L] (a b : L) : incidenceAuxCoordinateClass L a b 2 ^ 2 = (incidenceAuxPolynomialAlgebraMap L a b) (incidenceBranchPolynomial b)

noncomputable def BGS.Markoff.incidenceFirstQuadraticToAuxCoordinateRing (L : Type v) [Field L] (a b : L) : IncidenceFirstQuadraticRing L a →ₐ[L] IncidenceAuxCoordinateRing L a b

Map the first quadratic extension back to the explicit coordinate ring.

Equations

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

noncomputable def BGS.Markoff.incidenceBiquadraticToAuxCoordinateRing (L : Type v) [Field L] (a b : L) : IncidenceBiquadraticRing L a b →ₐ[L] IncidenceAuxCoordinateRing L a b

Map the iterated quadratic normal form back to the explicit coordinate ring.

Equations

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

@[simp]

theorem BGS.Markoff.incidenceAuxCoordinateRingToBiquadratic_coordinateClass (L : Type v) [Field L] (a b : L) (i : Fin 3) : (incidenceAuxCoordinateRingToBiquadratic L a b) (incidenceAuxCoordinateClass L a b i) = ![incidenceBiquadraticY L a b, incidenceBiquadraticLambda L a b, incidenceBiquadraticMu L a b] i

@[simp]

theorem BGS.Markoff.incidenceBiquadraticToAuxCoordinateRing_y (L : Type v) [Field L] (a b : L) : (incidenceBiquadraticToAuxCoordinateRing L a b) (incidenceBiquadraticY L a b) = incidenceAuxCoordinateClass L a b 0

@[simp]

theorem BGS.Markoff.incidenceBiquadraticToAuxCoordinateRing_lambda (L : Type v) [Field L] (a b : L) : (incidenceBiquadraticToAuxCoordinateRing L a b) (incidenceBiquadraticLambda L a b) = incidenceAuxCoordinateClass L a b 1

@[simp]

theorem BGS.Markoff.incidenceBiquadraticToAuxCoordinateRing_mu (L : Type v) [Field L] (a b : L) : (incidenceBiquadraticToAuxCoordinateRing L a b) (incidenceBiquadraticMu L a b) = incidenceAuxCoordinateClass L a b 2

theorem BGS.Markoff.incidenceBiquadraticToAux_comp_auxToBiquadratic (L : Type v) [Field L] (a b : L) : (incidenceBiquadraticToAuxCoordinateRing L a b).comp (incidenceAuxCoordinateRingToBiquadratic L a b) = AlgHom.id L (IncidenceAuxCoordinateRing L a b)

theorem BGS.Markoff.incidenceAuxToBiquadratic_comp_biquadraticToAux (L : Type v) [Field L] (a b : L) : (incidenceAuxCoordinateRingToBiquadratic L a b).comp (incidenceBiquadraticToAuxCoordinateRing L a b) = AlgHom.id L (IncidenceBiquadraticRing L a b)

noncomputable def BGS.Markoff.incidenceAuxCoordinateRingEquivBiquadratic (L : Type v) [Field L] (a b : L) : IncidenceAuxCoordinateRing L a b ≃ₐ[L] IncidenceBiquadraticRing L a b

The two-equation coordinate quotient is exactly the rank-four iterated quadratic algebra.

Equations

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

theorem BGS.Markoff.incidenceAuxCoordinateRing_isDomain (L : Type v) [Field L] (h2 : 2 ≠ 0) {a b : L} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : IsDomain (IncidenceAuxCoordinateRing L a b)

The explicit two-equation coordinate quotient is a domain under the off-diagonal nondegeneracy hypotheses.

theorem BGS.Markoff.incidenceAuxGeometricallyIntegral_of_nondegenerate {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) : IncidenceAuxGeometricallyIntegral a b

The actual geometric-integrality statement follows after explicit scalar extension to the algebraic closure; no irreducibility assertion is hidden in a structure field.

theorem BGS.Markoff.incidenceAux_offDiagonal_geometricallyIntegral : ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → IncidenceAuxOffDiagonalGeometryAt p hp

Specialization to the paper's admissible off-diagonal coordinates. The threshold 3 only excludes characteristic two; no large-prime estimate is used in this geometric step.