Cumulative local principal parts

For a DVR uniformizer π, the quotient of functions with pole order at most n by the regular functions is the quotient of the DVR by the nth power of its maximal ideal. Over a finite constant field its dimension is therefore n times the residue-field degree.

noncomputable def BGS.HasseWeil.localPolePrincipalPartMap {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] (π : R) (n : ℕ) : ↥(localPoleSpace π n) →ₗ[K] R ⧸ IsLocalRing.maximalIdeal R ^ n

The normalized numerator modulo the nth power of the maximal ideal.

Equations

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

theorem BGS.HasseWeil.localPolePrincipalPartMap_surjective {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] (π : R) (hπ : π ≠ 0) (n : ℕ) : Function.Surjective ⇑(localPolePrincipalPartMap π n)

theorem BGS.HasseWeil.localPolePrincipalPartMap_ker {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] (π : R) (hπ : π ≠ 0) (hπIdeal : IsLocalRing.maximalIdeal R = Ideal.span {π}) (n : ℕ) : (localPolePrincipalPartMap π n).ker = Submodule.comap (localPoleSpace π n).subtype (localPoleSpace π 0)

noncomputable def BGS.HasseWeil.localPoleCumulativeQuotientEquiv {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] (π : R) (hπ : π ≠ 0) (hπIdeal : IsLocalRing.maximalIdeal R = Ideal.span {π}) (n : ℕ) : (↥(localPoleSpace π n) ⧸ Submodule.comap (localPoleSpace π n).subtype (localPoleSpace π 0)) ≃ₗ[K] R ⧸ IsLocalRing.maximalIdeal R ^ n

Cumulative local principal parts are the quotient by the corresponding power of the maximal ideal.

Equations

• BGS.HasseWeil.localPoleCumulativeQuotientEquiv π hπ hπIdeal n = ⋯.mpr ((BGS.HasseWeil.localPolePrincipalPartMap π n).quotKerEquivOfSurjective ⋯)

theorem BGS.HasseWeil.localPoleCumulativeQuotient_finrank {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] [Finite K] (π : R) (hπ : π ≠ 0) (hπIdeal : IsLocalRing.maximalIdeal R = Ideal.span {π}) (n : ℕ) [Finite (IsLocalRing.ResidueField R)] : Module.finrank K (↥(localPoleSpace π n) ⧸ Submodule.comap (localPoleSpace π n).subtype (localPoleSpace π 0)) = n * Module.finrank K (IsLocalRing.ResidueField R)

Over a finite constant field, allowing poles through order n creates exactly n copies of the local residue field.