Projectivized Riemann-space counts

For a finite constant field, nonzero vectors in a finite-dimensional vector space modulo multiplication by nonzero scalars form its projectivization. This file records the three equivalent cardinality formulas needed in the function-field zeta argument:

• the quotient by the scalar action;
• the set of one-dimensional subspaces; and
• the geometric sum 1 + q + ... + q^(l - 1).

The final statements specialize these formulas to every effective exhaustive divisor, using the already proved finite-dimensionality of its Riemann space.

theorem BGS.HasseWeil.finiteVectorSpace_oneDimensionalSubspace_card_eq_geomSum (K : Type u_1) [Field K] (V : Type u_2) [AddCommGroup V] [Module K V] [Finite K] : Nat.card { W : Submodule K V // Module.finrank K ↥W = 1 } = ∑ i ∈ Finset.range (Module.finrank K V), Nat.card K ^ i

One-dimensional subspaces of a finite vector space over K are counted by the geometric sum in the dimension.

theorem BGS.HasseWeil.finiteVectorSpace_nonzeroScalarOrbitQuotient_card_eq_geomSum (K : Type u_1) [Field K] (V : Type u_2) [AddCommGroup V] [Module K V] [Finite K] : Nat.card (Quotient (MulAction.orbitRel Kˣ { v : V // v ≠ 0 })) = ∑ i ∈ Finset.range (Module.finrank K V), Nat.card K ^ i

The orbit quotient of nonzero vectors by nonzero scalar multiplication is counted by the same geometric sum.

theorem BGS.HasseWeil.finiteVectorSpace_nonzeroScalarOrbitQuotient_card_eq_div (K : Type u_1) [Field K] (V : Type u_2) [AddCommGroup V] [Module K V] [Module.Finite K V] [Finite K] : Nat.card (Quotient (MulAction.orbitRel Kˣ { v : V // v ≠ 0 })) = (Nat.card K ^ Module.finrank K V - 1) / (Nat.card K - 1)

Division form of the projective-space cardinality formula.

@[instance_reducible]

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

The algebra structure from K to L used in the finite extension riemann space projectivization construction.

Equations

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

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

def BGS.HasseWeil.EffectiveDivisorInPrincipalClass (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) : Type u_3

Effective exhaustive divisors in the principal-divisor class represented by D. The sign convention matches the Riemann-space definition: x \in L(D) gives the effective divisor div(x) + D.

Equations

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

noncomputable def BGS.HasseWeil.effectiveDivisorInPrincipalClassOfNonzeroSection (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (x : { x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) // x ≠ 0 }) : EffectiveDivisorInPrincipalClass K L D

A nonzero Riemann-space section determines an effective divisor in the principal class represented by D.

Equations

• BGS.HasseWeil.effectiveDivisorInPrincipalClassOfNonzeroSection K L D x = ⟨BGS.CorvajaZannier.finiteExtensionPrincipalDivisor K L ↑↑x + D, ⋯⟩

theorem BGS.HasseWeil.effectiveDivisorInPrincipalClassOfNonzeroSection_smul (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (a b : { x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) // x ≠ 0 }) (c : K) (hab : ↑a = c • ↑b) : effectiveDivisorInPrincipalClassOfNonzeroSection K L D a = effectiveDivisorInPrincipalClassOfNonzeroSection K L D b

Multiplying a nonzero section by a nonzero base-field scalar does not change its associated effective divisor.

noncomputable def BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) : Projectivization K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) → EffectiveDivisorInPrincipalClass K L D

Projectivizing the nonzero sections makes the associated effective divisor independent of the chosen representative.

Equations

• BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass K L D = Projectivization.lift (BGS.HasseWeil.effectiveDivisorInPrincipalClassOfNonzeroSection K L D) ⋯

@[simp]

theorem BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass_mk (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)) (hx : x ≠ 0) : projectiveRiemannSectionToEffectiveDivisorInPrincipalClass K L D (Projectivization.mk K x hx) = effectiveDivisorInPrincipalClassOfNonzeroSection K L D ⟨x, hx⟩

theorem BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass_surjective (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) : Function.Surjective (projectiveRiemannSectionToEffectiveDivisorInPrincipalClass K L D)

Every effective divisor in the represented principal class arises from a projective nonzero section.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_eq_zero_iff_isBaseConstant (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (hconstants : algebraicClosure K L = ⊥) (x : L) (hx0 : x ≠ 0) : CorvajaZannier.finiteExtensionPrincipalDivisor K L x = 0 ↔ ∃ (c : K), c ≠ 0 ∧ (algebraMap K L) c = x

Under exact constants, a nonzero function has zero exhaustive principal divisor exactly when it is a nonzero base-field constant.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_eq_iff_exists_smul (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (hconstants : algebraicClosure K L = ⊥) (x y : L) (hx0 : x ≠ 0) (hy0 : y ≠ 0) : CorvajaZannier.finiteExtensionPrincipalDivisor K L x = CorvajaZannier.finiteExtensionPrincipalDivisor K L y ↔ ∃ (c : K), c • y = x

With exact constants, two nonzero functions have the same exhaustive principal divisor exactly when they differ by a base-field scalar.

theorem BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass_injective (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hconstants : algebraicClosure K L = ⊥) : Function.Injective (projectiveRiemannSectionToEffectiveDivisorInPrincipalClass K L D)

Exact constants make the projective-section map injective.

noncomputable def BGS.HasseWeil.projectiveRiemannSectionEquivEffectiveDivisorInPrincipalClass (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hconstants : algebraicClosure K L = ⊥) : Projectivization K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ≃ EffectiveDivisorInPrincipalClass K L D

With exact constants, projective nonzero sections are equivalent to the effective divisors in the represented principal class.

Equations

• BGS.HasseWeil.projectiveRiemannSectionEquivEffectiveDivisorInPrincipalClass K L D hconstants = Equiv.ofBijective (BGS.HasseWeil.projectiveRiemannSectionToEffectiveDivisorInPrincipalClass K L D) ⋯

theorem BGS.HasseWeil.effectiveRiemannSpace_nonzeroScalarOrbitQuotient_card_eq_geomSum (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) : Nat.card (Quotient (MulAction.orbitRel Kˣ { x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) // x ≠ 0 })) = ∑ i ∈ Finset.range (Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)), Nat.card K ^ i

Nonzero sections of L(D) modulo nonzero constant scalars satisfy the projective-space Nat.card identity. The following finiteness theorem turns this into an ordinary finite count when D is effective.

theorem BGS.HasseWeil.effectiveRiemannSpace_nonzeroScalarOrbitQuotient_finite (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) : Finite (Quotient (MulAction.orbitRel Kˣ { x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) // x ≠ 0 }))

For effective D, the scalar-orbit quotient of nonzero sections is a finite type.

theorem BGS.HasseWeil.effectiveRiemannSpace_nonzeroScalarOrbitQuotient_card_eq_div (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) : Nat.card (Quotient (MulAction.orbitRel Kˣ { x : ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) // x ≠ 0 })) = (Nat.card K ^ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) - 1) / (Nat.card K - 1)

Division form of the projectivized effective Riemann-space count.

theorem BGS.HasseWeil.effectiveDivisorInPrincipalClass_finite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (hconstants : algebraicClosure K L = ⊥) : Finite (EffectiveDivisorInPrincipalClass K L D)

Under exact constants, an effective divisor class represented by an effective D is finite.

theorem BGS.HasseWeil.effectiveDivisorInPrincipalClass_card_eq_geomSum (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hconstants : algebraicClosure K L = ⊥) : Nat.card (EffectiveDivisorInPrincipalClass K L D) = ∑ i ∈ Finset.range (Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)), Nat.card K ^ i

Cardinality of the effective divisors in a fixed principal class under the exact-constants hypothesis.

theorem BGS.HasseWeil.effectiveDivisorInPrincipalClass_card_eq_div (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (hconstants : algebraicClosure K L = ⊥) : Nat.card (EffectiveDivisorInPrincipalClass K L D) = (Nat.card K ^ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) - 1) / (Nat.card K - 1)

Division form of the fixed-principal-class count.