Plane monomial spaces for the Stepanov construction

This file packages the finite rectangular spaces spanned by the monomials x ^ i * y ^ j. It proves their dimension from linear independence, gives a plane-curve independence criterion from the degree in one coordinate, and records the mixed-radix exponent map occurring when an ordinary grid is multiplied by a grid in the powered coordinates.

The final tower lemma is the algebraic form needed by Stepanov: if the ordinary (digit) grid is independent over a subfield containing x ^ s and y ^ s, and the powered grid is independent over the constant field, then the twisted products

x ^ (i + s * i') * y ^ (j + s * j')

are independent over the constant field. No Frobenius endomorphism is introduced or assumed.

def BGS.HasseWeil.planeMonomialGrid {L : Type u_1} [Monoid L] (x y : L) (a b : ℕ) : Fin a × Fin b → L

The rectangular family of plane monomials with i < a and j < b.

Equations

• BGS.HasseWeil.planeMonomialGrid x y a b ij = x ^ ↑ij.1 * y ^ ↑ij.2

def BGS.HasseWeil.planeMonomialSpace (K : Type u_1) {L : Type u_2} [Field K] [CommRing L] [Algebra K L] (x y : L) (a b : ℕ) : Submodule K L

The finite K-subspace spanned by a rectangular plane-monomial grid.

Equations

• BGS.HasseWeil.planeMonomialSpace K x y a b = Submodule.span K (Set.range (BGS.HasseWeil.planeMonomialGrid x y a b))

theorem BGS.HasseWeil.planeMonomialGrid_mem_space {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] (x y : L) (a b : ℕ) (ij : Fin a × Fin b) : planeMonomialGrid x y a b ij ∈ planeMonomialSpace K x y a b

theorem BGS.HasseWeil.moduleFinite_planeMonomialSpace (K : Type u_1) {L : Type u_2} [Field K] [CommRing L] [Algebra K L] (x y : L) (a b : ℕ) : Module.Finite K ↥(planeMonomialSpace K x y a b)

A rectangular monomial space is finite, independently of any linear-independence hypothesis.

theorem BGS.HasseWeil.finrank_planeMonomialSpace_eq_mul {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] (x y : L) (a b : ℕ) (hLI : LinearIndependent K (planeMonomialGrid x y a b)) : Module.finrank K ↥(planeMonomialSpace K x y a b) = a * b

Linear independence identifies the finrank of a rectangular monomial space with the number of grid points.

theorem BGS.HasseWeil.linearIndependent_fin_powers_of_transcendental {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [Algebra K A] (z : A) (hz : Transcendental K z) (n : ℕ) : LinearIndependent K fun (i : Fin n) => z ^ ↑i

Finite initial segments of the powers of a transcendental element are linearly independent.

theorem BGS.HasseWeil.planeMonomialGrid_linearIndependent_of_transcendental_minpoly {K : Type u_1} {F : Type u_2} {L : Type u_3} [Field K] [Field F] [Field L] [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L] (x : F) (y : L) (a b : ℕ) (hx : Transcendental K x) (hb : b ≤ (minpoly F y).natDegree) : LinearIndependent K (planeMonomialGrid ((algebraMap F L) x) y a b)

A tower criterion for a rectangular monomial grid. Powers of the transcendental lower coordinate supply one independent family, and powers of the upper element below its minimal-polynomial degree supply the other.

theorem BGS.HasseWeil.planeMonomialGrid_linearIndependent_of_auxiliaryFamily {C : Type u_1} {L : Type u_2} [Field C] [Field L] [Algebra C L] (u v : L) (h k : ℕ) (haux : LinearIndependent C (CorvajaZannier.auxiliaryFamily u v h k)) : LinearIndependent C (planeMonomialGrid u v (k + 1) h)

The grid part of the Corvaja--Zannier auxiliary family is a linearly independent rectangular monomial family.

theorem BGS.HasseWeil.planeCurve_monomialGrid_linearIndependent {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (a b : ℕ) (hb : b ≤ MvPolynomial.degreeOf 1 f) : LinearIndependent K (planeMonomialGrid (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) a b)

On an irreducible plane curve, monomials with arbitrary first exponent and second exponent below the second-coordinate degree are independent.

theorem BGS.HasseWeil.finrank_planeCurve_monomialSpace_eq_mul {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (a b : ℕ) (hb : b ≤ MvPolynomial.degreeOf 1 f) : Module.finrank K ↥(planeMonomialSpace K (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) a b) = a * b

The bidegree criterion gives the exact dimension of the corresponding plane-curve monomial space.

def BGS.HasseWeil.digitExponent {a a' : ℕ} (s : ℕ) (ii' : Fin a × Fin a') : ℕ

The mixed-radix exponent attached to a low digit and a high digit.

Equations

• BGS.HasseWeil.digitExponent s ii' = ↑ii'.1 + s * ↑ii'.2

theorem BGS.HasseWeil.digitExponent_injective {s a a' : ℕ} (ha : a ≤ s) : Function.Injective (digitExponent s)

Low digits bounded by the radix make the mixed-radix exponent map injective.

def BGS.HasseWeil.twistedExponentGrid (s a b a' b' : ℕ) : (Fin a × Fin b) × Fin a' × Fin b' → ℕ × ℕ

The pair of mixed-radix exponents used by the twisted monomial grid.

Equations

• BGS.HasseWeil.twistedExponentGrid s a b a' b' z = (↑z.1.1 + s * ↑z.2.1, ↑z.1.2 + s * ↑z.2.2)

theorem BGS.HasseWeil.twistedExponentGrid_injective {s a b a' b' : ℕ} (ha : a ≤ s) (hb : b ≤ s) : Function.Injective (twistedExponentGrid s a b a' b')

Digit bounds in both coordinates make the exponent-pair map injective.

def BGS.HasseWeil.twistedPlaneMonomialGrid {L : Type u_1} [Monoid L] (x y : L) (s a b a' b' : ℕ) : (Fin a × Fin b) × Fin a' × Fin b' → L

The products of an ordinary monomial grid and its s-powered copy.

Equations

• BGS.HasseWeil.twistedPlaneMonomialGrid x y s a b a' b' z = x ^ (↑z.1.1 + s * ↑z.2.1) * y ^ (↑z.1.2 + s * ↑z.2.2)

def BGS.HasseWeil.twistedGridToGrid (s a b a' b' : ℕ) : (Fin a × Fin b) × Fin a' × Fin b' → Fin (a + s * a') × Fin (b + s * b')

Send a pair of low and high digits to the encompassing rectangular grid.

Equations

• BGS.HasseWeil.twistedGridToGrid s a b a' b' z = (⟨↑z.1.1 + s * ↑z.2.1, ⋯⟩, ⟨↑z.1.2 + s * ↑z.2.2, ⋯⟩)

theorem BGS.HasseWeil.twistedGridToGrid_injective {s a b a' b' : ℕ} (ha : a ≤ s) (hb : b ≤ s) : Function.Injective (twistedGridToGrid s a b a' b')

theorem BGS.HasseWeil.planeCurve_twistedMonomialGrid_linearIndependent {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (s a b a' b' : ℕ) (ha : a ≤ s) (hb : b ≤ s) (hdegree : b + s * b' ≤ MvPolynomial.degreeOf 1 f) : LinearIndependent K (twistedPlaneMonomialGrid (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) s a b a' b')

Direct bidegree criterion for the twisted family. The digit bounds make the exponent encoding injective, while the final second-exponent range stays below the curve's second-coordinate degree.

theorem BGS.HasseWeil.planeCurve_twistedMonomialGrid_injective {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (s a b a' b' : ℕ) (ha : a ≤ s) (hb : b ≤ s) (hdegree : b + s * b' ≤ MvPolynomial.degreeOf 1 f) : Function.Injective (twistedPlaneMonomialGrid (CorvajaZannier.planeCurveFunction f 0) (CorvajaZannier.planeCurveFunction f 1) s a b a' b')

In particular, under the direct bidegree criterion the twisted grid is an injective family of functions.

theorem BGS.HasseWeil.twistedPlaneMonomialGrid_linearIndependent_of_subfield {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (F : Subfield L) [Algebra K ↥F] [IsScalarTower K (↥F) L] (x y : L) (s a b a' b' : ℕ) (hxs : x ^ s ∈ F) (hys : y ^ s ∈ F) (hdigit : LinearIndependent (↥F) (planeMonomialGrid x y a b)) (hpowered : LinearIndependent K (planeMonomialGrid ⟨x ^ s, hxs⟩ ⟨y ^ s, hys⟩ a' b')) : LinearIndependent K (twistedPlaneMonomialGrid x y s a b a' b')

Tower composition for Stepanov's twisted grid. The ordinary grid is independent over F; the powered grid, regarded inside F, is independent over K. Multiplication combines the two independent families.

theorem BGS.HasseWeil.planeCurve_poweredMonomialGrid_linearIndependent {K : Type u_1} [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ℕ) (hm : 0 < m) (n a b : ℕ) (hb : b ≤ (CorvajaZannier.poweredCoordinateImageRelation hf hpartialSecond m hm n).natDegree) : LinearIndependent K (planeMonomialGrid (CorvajaZannier.planeCurveFunction f 0 ^ m) (CorvajaZannier.planeCurveFunction f 1 ^ n) a b)

The powered-image relation supplies the bidegree needed for a monomial grid in the powered coordinates.

@[instance_reducible]

noncomputable def BGS.HasseWeil.planeMonomialSpaceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the plane monomial space construction.

Equations

• BGS.HasseWeil.planeMonomialSpaceConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.planeMonomialSpaceConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.planeMonomialSpace_le_poleDivisorBudget (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (n b : ℕ) : planeMonomialSpace K x y (n + 1) b ≤ CorvajaZannier.finiteExtensionRiemannSpace K L (n • finiteExtensionPoleDivisor K L x + (b - 1) • finiteExtensionPoleDivisor K L y)

Every monomial with x-exponent at most n and y-exponent below b lies in the Riemann space with pole budget n · pole(x) + (b - 1) · pole(y).

theorem BGS.HasseWeil.rank_planeMonomialSpace_le_rank_poleDivisorBudget (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (n b : ℕ) : Module.rank K ↥(planeMonomialSpace K x y (n + 1) b) ≤ Module.rank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (n • finiteExtensionPoleDivisor K L x + (b - 1) • finiteExtensionPoleDivisor K L y))

Pole-budget containment is already useful before finite-dimensionality of the ambient Riemann space has been established: it gives monotonicity of the corresponding module ranks.

theorem BGS.HasseWeil.add_one_mul_le_finrank_poleDivisorBudget (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (n b : ℕ) (hLI : LinearIndependent K (planeMonomialGrid x y (n + 1) b)) (hfinite : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (n • finiteExtensionPoleDivisor K L x + (b - 1) • finiteExtensionPoleDivisor K L y))) : (n + 1) * b ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (n • finiteExtensionPoleDivisor K L x + (b - 1) • finiteExtensionPoleDivisor K L y))

Once finite-dimensionality of the ambient Riemann space is available, the same containment yields the numerical lower bound (n + 1) * b.