Cayley coordinates on the nonsplit norm-one torus

This file gives the rational coordinate needed to descend the nonsplit end-game cover from the quadratic finite field to ZMod p. A point delta outside the base field identifies the affine line with the norm-one torus minus its identity by

z |-> (z - delta ^ p) / (z - delta).

The inverse is (w * delta - delta ^ p) / (w - 1). The proof records the Frobenius identities explicitly; these are the identities used when the pulled-back trace equation is cleared of denominators over the base field.

@[instance_reducible]

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

Finiteness of the quadratic extension field used in the nonsplit parametrization.

Equations

• BGS.Markoff.instFintypeQuadraticFiniteField p = Fintype.ofFinite (BGS.Markoff.quadraticFiniteField p)

@[instance_reducible]

noncomputable def BGS.Markoff.instFintypeSubtypeUnitsQuadraticFiniteFieldMemSubgroupQuadraticNormOneTorusNeOfNat (p : ℕ) [Fact (Nat.Prime p)] : Fintype { w : ↥(quadraticNormOneTorus p) // w ≠ 1 }

A finite enumeration of nonidentity points of the norm-one torus.

Equations

• BGS.Markoff.instFintypeSubtypeUnitsQuadraticFiniteFieldMemSubgroupQuadraticNormOneTorusNeOfNat p = Fintype.ofFinite { w : ↥(BGS.Markoff.quadraticNormOneTorus p) // w ≠ 1 }

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

A chosen element of the quadratic finite field which is not defined over the base field.

Equations

• BGS.Markoff.quadraticNonbaseElement p = Classical.choose ⋯

theorem BGS.Markoff.quadraticNonbaseElement_not_mem_range (p : ℕ) [Fact (Nat.Prime p)] : quadraticNonbaseElement p ∉ Set.range ⇑(algebraMap (ZMod p) (quadraticFiniteField p))

theorem BGS.Markoff.quadraticNonbaseElement_frobenius_ne_self (p : ℕ) [Fact (Nat.Prime p)] : quadraticNonbaseElement p ^ p ≠ quadraticNonbaseElement p

theorem BGS.Markoff.quadraticNonbaseElement_frobenius_not_mem_range (p : ℕ) [Fact (Nat.Prime p)] : quadraticNonbaseElement p ^ p ∉ Set.range ⇑(algebraMap (ZMod p) (quadraticFiniteField p))

noncomputable def BGS.Markoff.quadraticCayleyValue (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : quadraticFiniteField p

The Cayley fraction before it is packaged as a norm-one unit.

Equations

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

theorem BGS.Markoff.quadraticCayleyValue_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : quadraticCayleyValue p z ≠ 0

theorem BGS.Markoff.quadraticNonbaseElement_frobenius_frobenius (p : ℕ) [Fact (Nat.Prime p)] : (quadraticNonbaseElement p ^ p) ^ p = quadraticNonbaseElement p

theorem BGS.Markoff.quadraticCayleyValue_frobenius (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : quadraticCayleyValue p z ^ p = (quadraticCayleyValue p z)⁻¹

theorem BGS.Markoff.quadraticCayleyBaseFactor_frobenius (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p) ^ p = (algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p

Frobenius exchanges the two linear factors occurring in the Cayley coordinate.

theorem BGS.Markoff.quadraticCayleyConjugateFactor_frobenius (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) ^ p = (algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p

Applying Frobenius again returns the other Cayley linear factor.

theorem BGS.Markoff.quadraticCayleyFactorProduct_frobenius (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p)) ^ p = ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p)

The product of the conjugate Cayley factors is Frobenius-fixed, hence is a base-field coefficient in the descended equation.

theorem BGS.Markoff.quadraticCayleyValue_pow_add_inv_pow (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) (d : ℕ) : quadraticCayleyValue p z ^ d + (quadraticCayleyValue p z ^ d)⁻¹ = (((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) ^ (2 * d) + ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p) ^ (2 * d)) / (((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p)) ^ d

Clearing the Cayley denominator gives the symmetric numerator used for powers of a norm-one parameter.

theorem BGS.Markoff.quadraticCayleyValue_ne_one (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : quadraticCayleyValue p z ≠ 1

noncomputable def BGS.Markoff.quadraticCayleyUnit (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (quadraticFiniteField p)ˣ

The Cayley coordinate as a unit of the quadratic finite field.

Equations

• BGS.Markoff.quadraticCayleyUnit p z = Units.mk0 (BGS.Markoff.quadraticCayleyValue p z) ⋯

theorem BGS.Markoff.quadraticCayleyUnit_norm (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (Algebra.norm (ZMod p)) ↑(quadraticCayleyUnit p z) = 1

noncomputable def BGS.Markoff.quadraticCayleyPoint (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : ↥(quadraticNormOneTorus p)

The Cayley coordinate, regarded as a point of the norm-one torus.

Equations

• BGS.Markoff.quadraticCayleyPoint p z = ⟨BGS.Markoff.quadraticCayleyUnit p z, ⋯⟩

theorem BGS.Markoff.quadraticCayleyPoint_ne_one (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : quadraticCayleyPoint p z ≠ 1

theorem BGS.Markoff.algebraMap_quadraticNormOneTrace_quadraticCayleyPoint_pow (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) (d : ℕ) : (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticNormOneTrace p (quadraticCayleyPoint p z ^ d)) = (((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) ^ (2 * d) + ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p) ^ (2 * d)) / (((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p)) ^ d

The base-field trace of a powered Cayley point is the cleared symmetric Cayley fraction.

theorem BGS.Markoff.quadraticCayleyInverseFormula_point (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (quadraticCayleyValue p z * quadraticNonbaseElement p - quadraticNonbaseElement p ^ p) / (quadraticCayleyValue p z - 1) = (algebraMap (ZMod p) (quadraticFiniteField p)) z

Solving the Cayley fraction for its base-field coordinate gives the expected inverse fraction.

noncomputable def BGS.Markoff.quadraticCayleyParameterEquiv (p : ℕ) [Fact (Nat.Prime p)] : ZMod p ≃ { w : ↥(quadraticNormOneTorus p) // w ≠ 1 }

Cayley coordinates identify the affine line with the norm-one torus minus its identity.

Equations

• BGS.Markoff.quadraticCayleyParameterEquiv p = Equiv.ofBijective (fun (z : ZMod p) => ⟨BGS.Markoff.quadraticCayleyPoint p z, ⋯⟩) ⋯

@[simp]

theorem BGS.Markoff.quadraticCayleyParameterEquiv_apply (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (quadraticCayleyParameterEquiv p) z = ⟨quadraticCayleyPoint p z, ⋯⟩

theorem BGS.Markoff.algebraMap_quadraticCayleyParameterEquiv_symm (p : ℕ) [Fact (Nat.Prime p)] (w : { w : ↥(quadraticNormOneTorus p) // w ≠ 1 }) : (algebraMap (ZMod p) (quadraticFiniteField p)) ((quadraticCayleyParameterEquiv p).symm w) = (↑↑↑w * quadraticNonbaseElement p - quadraticNonbaseElement p ^ p) / (↑↑↑w - 1)

The inverse coordinate has the explicit fraction used in the descent calculation.