Affine ideal degrees in a finite function field

The finite class group of the normalization of K[X] controls ideal classes, but an affine ideal zeta series also needs finite coefficient sets. This file provides that missing finiteness layer for a finite separable extension of K(X) over a finite field K.

First, every nonzero quotient of K[X] is finite: a nonzero ideal contains a monic polynomial up to multiplication by a unit, and its quotient maps onto the original quotient. Module finiteness transfers this property to the normalization of K[X] in the function field. For a nonzero ideal I, its affine degree is then the K-dimension of the quotient by I. Consequently

cardQuot I = |K| ^ degree(I),

and Mathlib's bounded-quotient-cardinality theorem makes the ideals of each fixed degree into a finite type. No Riemann--Roch or Hasse--Weil input is used.

theorem BGS.HasseWeil.ratFuncPolynomial_hasFiniteQuotients (K : Type u_1) [Field K] [Finite K] : Ring.HasFiniteQuotients (Polynomial K)

The polynomial ring over a finite field has finite quotients.

@[instance_reducible]

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

The algebra structure from K[X] to L used in the finite extension affine ideal degree construction.

Equations

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

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

theorem BGS.HasseWeil.affineIdealClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

@[instance_reducible]

noncomputable def BGS.HasseWeil.affineIdealClosureConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension affine ideal degree construction.

Equations

• BGS.HasseWeil.affineIdealClosureConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.HasseWeil.affineIdealClosureConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.ratFuncFiniteIntegralClosure_hasFiniteQuotients (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] : Ring.HasFiniteQuotients ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The normalization of K[X] in a finite separable extension of K(X) has finite quotients.

theorem BGS.HasseWeil.finiteExtensionAffineClassGroup_finite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] : Finite (ClassGroup ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))

The affine ideal class group is finite. This is the function-field class number theorem from Mathlib, stated at the normalization used by BGS.

@[reducible, inline]

noncomputable abbrev BGS.HasseWeil.FiniteExtensionAffineIdeal (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Submonoid (Ideal ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))

Nonzero affine ideals in the normalization of K[X] in L.

Equations

• BGS.HasseWeil.FiniteExtensionAffineIdeal K L = nonZeroDivisors (Ideal ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L))

noncomputable def BGS.HasseWeil.finiteExtensionAffineIdealDegree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (I : ↥(FiniteExtensionAffineIdeal K L)) : ℕ

The degree of a nonzero affine ideal is the K-dimension of its quotient.

Equations

• BGS.HasseWeil.finiteExtensionAffineIdealDegree K L I = Module.finrank K (↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L) ⧸ ↑I)

theorem BGS.HasseWeil.finiteExtensionAffineIdeal_cardQuot_eq_card_pow_degree (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (I : ↥(FiniteExtensionAffineIdeal K L)) : Submodule.cardQuot ↑I = Fintype.card K ^ finiteExtensionAffineIdealDegree K L I

Quotient cardinality is the cardinality of the constant field raised to the affine ideal degree.

theorem BGS.HasseWeil.finiteExtensionAffineIdealDegree_eq_zero_iff (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (I : ↥(FiniteExtensionAffineIdeal K L)) : finiteExtensionAffineIdealDegree K L I = 0 ↔ ↑I = ⊤

An affine ideal has degree zero exactly when it is the unit ideal.

theorem BGS.HasseWeil.finite_setOf_finiteExtensionAffineIdealDegree_eq (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (n : ℕ) : {I : ↥(FiniteExtensionAffineIdeal K L) | finiteExtensionAffineIdealDegree K L I = n}.Finite

There are only finitely many nonzero affine ideals of any prescribed degree.

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finiteExtensionAffineIdealsOfDegreeFintype (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : Fintype { I : ↥(FiniteExtensionAffineIdeal K L) // finiteExtensionAffineIdealDegree K L I = n }

A finite indexing type for nonzero affine ideals of degree n.

Equations

• BGS.HasseWeil.finiteExtensionAffineIdealsOfDegreeFintype K L n = ⋯.fintype

noncomputable def BGS.HasseWeil.finiteExtensionAffineIdealCount (K : Type u_1) [Field K] [Fintype K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (n : ℕ) : ℕ

The number of nonzero affine ideals of degree n; this is the natural coefficient sequence for the affine ideal zeta series.

Equations

• BGS.HasseWeil.finiteExtensionAffineIdealCount K L n = Fintype.card { I : ↥(BGS.HasseWeil.FiniteExtensionAffineIdeal K L) // BGS.HasseWeil.finiteExtensionAffineIdealDegree K L I = n }