The local pole filtration of a discrete valuation ring

This file isolates the exact local calculation behind principal parts. If R is a discrete valuation ring in its fraction field L and π is a uniformizer, the functions whose pole order is at most n form a K-submodule of L. Consecutive levels have quotient equal to the residue field of R.

Unlike the corresponding global Riemann-space increment, this calculation is an equality: locally every leading residue has a lift.

def BGS.HasseWeil.localPoleSpace {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] (π : R) (n : ℕ) : Submodule K L

The local functions whose denominator is bounded by π ^ n.

Equations

• BGS.HasseWeil.localPoleSpace π n = { carrier := {x : L | ∃ (r : R), (algebraMap R L) (π ^ n) * x = (algebraMap R L) r}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem BGS.HasseWeil.mem_localPoleSpace_iff {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] (π : R) (n : ℕ) (x : L) : x ∈ localPoleSpace π n ↔ ∃ (r : R), (algebraMap R L) (π ^ n) * x = (algebraMap R L) r

theorem BGS.HasseWeil.localPoleSpace_mono {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] (π : R) (n : ℕ) : localPoleSpace π n ≤ localPoleSpace π (n + 1)

Increasing the allowed pole order enlarges the local pole space.

noncomputable def BGS.HasseWeil.localPoleLeadingResidueMap {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] IsLocalRing.ResidueField R

The leading-residue map on the nth local pole space.

Equations

• BGS.HasseWeil.localPoleLeadingResidueMap π n = BGS.HasseWeil.localLeadingResidueLinearMap (BGS.HasseWeil.localPoleSpace π n) ((algebraMap R L) (π ^ n)) ⋯

theorem BGS.HasseWeil.localPoleLeadingResidueMap_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 ⇑(localPoleLeadingResidueMap π n)

Every residue class occurs as a leading coefficient.

theorem BGS.HasseWeil.localPoleLeadingResidueMap_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 : (IsDiscreteValuationRing.maximalIdeal R).asIdeal = Ideal.span {π}) (n : ℕ) : (localPoleLeadingResidueMap π (n + 1)).ker = Submodule.comap (localPoleSpace π (n + 1)).subtype (localPoleSpace π n)

The kernel of the leading-residue map is the preceding local pole space.

noncomputable def BGS.HasseWeil.localPoleQuotientEquivResidueField {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 : (IsDiscreteValuationRing.maximalIdeal R).asIdeal = Ideal.span {π}) (n : ℕ) : (↥(localPoleSpace π (n + 1)) ⧸ Submodule.comap (localPoleSpace π (n + 1)).subtype (localPoleSpace π n)) ≃ₗ[K] IsLocalRing.ResidueField R

Consecutive local pole spaces have quotient the residue field.

Equations

• BGS.HasseWeil.localPoleQuotientEquivResidueField π hπ hπIdeal n = ⋯.mpr ((BGS.HasseWeil.localPoleLeadingResidueMap π (n + 1)).quotKerEquivOfSurjective ⋯)

theorem BGS.HasseWeil.localPoleQuotient_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] (π : R) (hπ : π ≠ 0) (hπIdeal : (IsDiscreteValuationRing.maximalIdeal R).asIdeal = Ideal.span {π}) (n : ℕ) : Module.finrank K (↥(localPoleSpace π (n + 1)) ⧸ Submodule.comap (localPoleSpace π (n + 1)).subtype (localPoleSpace π n)) = Module.finrank K (IsLocalRing.ResidueField R)

The exact dimension of one local principal-part layer.