Prime-to-characteristic torsion exponents for Corvaja--Zannier

Corvaja--Zannier, Theorem 2, assumes that the two rational functions have nonzero differentials. In Corollary 2 those functions are coordinate powers whose exponents are the orders of the two root-of-unity groups. The source suppresses the resulting prime-to-characteristic check.

For the actual Markoff application, both exponents are cardinalities of subgroups of the multiplicative group of a finite field. This file proves that they are prime to the characteristic, that the associated root-of-unity polynomials are separable, and that raising a nonzero coordinate with nonzero differential to either exponent preserves a nonzero differential. Thus inseparability is not part of the remaining Corvaja--Zannier wall.

theorem BGS.Markoff.characteristic_not_dvd_multiplicativeSubgroup_natCard {E : Type u_1} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] (H : Subgroup Eˣ) : ¬p ∣ Nat.card ↥H

The order of a multiplicative subgroup of a finite field is prime to the field characteristic. This is the hidden separability check in the passage from Corvaja--Zannier Theorem 2 to Corollary 2.

theorem BGS.Markoff.weightedTraceCurveTorsionIntersection_orders_primeToCharacteristic {E : Type u_1} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] (H₁ H₂ : Subgroup Eˣ) : ¬p ∣ Nat.card ↥H₁ ∧ ¬p ∣ Nat.card ↥H₂

Both exponents occurring in the exact weighted torsion intersection are prime to the characteristic.

theorem BGS.Markoff.multiplicativeSubgroup_torsionPolynomial_separable {E : Type u_1} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] (H : Subgroup Eˣ) : (Polynomial.X ^ Nat.card ↥H - 1).Separable

The root-of-unity polynomial attached to an actual finite-field subgroup has no inseparable multiplicity.

theorem BGS.Markoff.weightedTraceCurveTorsionIntersection_torsionPolynomials_separable {E : Type u_1} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] (H₁ H₂ : Subgroup Eˣ) : (Polynomial.X ^ Nat.card ↥H₁ - 1).Separable ∧ (Polynomial.X ^ Nat.card ↥H₂ - 1).Separable

The two torsion equations defining the exact geometric intersection are reduced.

theorem BGS.Markoff.derivation_pow_ne_zero {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing k] [Field L] [AddCommGroup M] [Module L M] [Algebra k L] [Module k M] (D : Derivation k L M) (x : L) (n : ℕ) (hn : ↑n ≠ 0) (hx : x ≠ 0) (hDx : D x ≠ 0) : D (x ^ n) ≠ 0

A prime-to-characteristic power of a nonzero function with nonzero differential again has nonzero differential. This is the exact derivation calculation used when Corvaja--Zannier Theorem 2 is specialized to root-of-unity exponents.

theorem BGS.Markoff.multiplicativeSubgroup_order_pow_has_nonzeroDifferential {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing k] [Field L] [AddCommGroup M] [Module L M] [Algebra k L] [Module k M] {E : Type u_4} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] [CharP L p] (H : Subgroup Eˣ) (D : Derivation k L M) (x : L) (hx : x ≠ 0) (hDx : D x ≠ 0) : D (x ^ Nat.card ↥H) ≠ 0

Actual finite-field subgroup orders satisfy the nonzero-differential condition after transport to any function field of the same characteristic.

theorem BGS.Markoff.weightedTraceCurveTorsionIntersection_coordinatePowers_haveNonzeroDifferentials {k : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing k] [Field L] [AddCommGroup M] [Module L M] [Algebra k L] [Module k M] {E : Type u_4} [Field E] [Finite E] (p : ℕ) [Fact (Nat.Prime p)] [CharP E p] [CharP L p] (H₁ H₂ : Subgroup Eˣ) (D : Derivation k L M) (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (hDx : D x ≠ 0) (hDy : D y ≠ 0) : D (x ^ Nat.card ↥H₁) ≠ 0 ∧ D (y ^ Nat.card ↥H₂) ≠ 0

The two coordinate powers in Corvaja--Zannier Corollary 2 retain nonzero differentials for the exact pair of subgroup orders used in the Markoff middle game.