Finite principal parts

This file assembles the one-place calculation in LocalPoleFiltration over a finite family of discrete valuation rings. At one place the principal parts of order at most n are the genuine quotient

localPoleSpace π n / localPoleSpace π 0.

The filtration by pole order proves that its dimension is n times the residue-field degree. Taking a finite product therefore has dimension the weighted degree of the chosen pole bounds.

The last section constructs the diagonal principal-parts map on any global subspace satisfying those pole bounds. Its kernel is exactly the subspace regular at every chosen place. Thus, once the all-place function-field layer identifies that regular subspace with the constants, the quotient by constants embeds in this finite-dimensional principal-parts space.

theorem BGS.HasseWeil.localPoleSpace_mono_of_le {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) {m n : ℕ} (hmn : m ≤ n) : localPoleSpace π m ≤ localPoleSpace π n

Monotonicity of the local pole filtration for an arbitrary increase in the allowed pole order.

@[reducible, inline]

abbrev BGS.HasseWeil.localPrincipalPartSpace {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 : ℕ) : Type u_3

Principal parts of order at most n at one DVR.

Equations

• BGS.HasseWeil.localPrincipalPartSpace π n = (↥(BGS.HasseWeil.localPoleSpace π n) ⧸ BGS.HasseWeil.relativeSubmodule (BGS.HasseWeil.localPoleSpace π 0) (BGS.HasseWeil.localPoleSpace π n))

@[reducible, inline]

abbrev BGS.HasseWeil.localPrincipalPartLayer {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 : ℕ) : Type u_3

The last graded layer in the local pole filtration.

Equations

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

def BGS.HasseWeil.localPrincipalPartInclusion {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 : ℕ) : localPrincipalPartSpace π n →ₗ[K] localPrincipalPartSpace π (n + 1)

Enlarging the pole bound by one gives an inclusion of principal-part spaces.

Equations

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

def BGS.HasseWeil.localPrincipalPartLayerMap {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 : ℕ) : localPrincipalPartSpace π (n + 1) →ₗ[K] localPrincipalPartLayer π n

Forgetting the top pole layer maps principal parts of order n + 1 onto the last local quotient.

Equations

• BGS.HasseWeil.localPrincipalPartLayerMap π n = Submodule.factor ⋯

theorem BGS.HasseWeil.localPrincipalPartInclusion_injective {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 : ℕ) : Function.Injective ⇑(localPrincipalPartInclusion π n)

theorem BGS.HasseWeil.range_localPrincipalPartInclusion_eq_ker_layerMap {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 : ℕ) : (localPrincipalPartInclusion π n).range = (localPrincipalPartLayerMap π n).ker

theorem BGS.HasseWeil.localPrincipalPartSpace_finite {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.Finite K (IsLocalRing.ResidueField R)] : Module.Finite K (localPrincipalPartSpace π n)

Every local principal-part space is finite-dimensional.

theorem BGS.HasseWeil.localPrincipalPartSpace_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.Finite K (IsLocalRing.ResidueField R)] : Module.finrank K (localPrincipalPartSpace π n) = n * Module.finrank K (IsLocalRing.ResidueField R)

The dimension of the genuine local principal-part quotient is the pole order times the residue-field degree.

def BGS.HasseWeil.quotientLinearMapOfKerEq {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (f : V →ₗ[K] W) (P : Submodule K V) (hker : f.ker = P) : V ⧸ P →ₗ[K] W

A linear map descends injectively after quotienting by a submodule known to be its kernel.

Equations

• BGS.HasseWeil.quotientLinearMapOfKerEq f P hker = P.liftQ f ⋯

theorem BGS.HasseWeil.quotientLinearMapOfKerEq_injective {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (f : V →ₗ[K] W) (P : Submodule K V) (hker : f.ker = P) : Function.Injective ⇑(quotientLinearMapOfKerEq f P hker)

theorem BGS.HasseWeil.finrank_quotient_le_of_ker_eq {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (f : V →ₗ[K] W) (P : Submodule K V) (hker : f.ker = P) [Module.Finite K W] : Module.finrank K (V ⧸ P) ≤ Module.finrank K W

The quotient by the kernel of a map into a finite-dimensional space has dimension at most that of the target.

@[reducible, inline]

abbrev BGS.HasseWeil.finitePrincipalPartsSpace {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] {R : I → Type u_4} [(i : I) → CommRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] (π : (i : I) → R i) (n : I → ℕ) : Type (max u_3 u_2)

A finite family of local principal-part spaces.

Equations

• BGS.HasseWeil.finitePrincipalPartsSpace π n = ((i : I) → BGS.HasseWeil.localPrincipalPartSpace (π i) (n i))

noncomputable def BGS.HasseWeil.finitePrincipalPartsDegree {K : Type u_1} {I : Type u_3} [Field K] [Fintype I] {R : I → Type u_4} [(i : I) → CommRing (R i)] [∀ (i : I), IsDedekindDomain (R i)] [∀ (i : I), IsDiscreteValuationRing (R i)] [(i : I) → Algebra K (R i)] (n : I → ℕ) : ℕ

The weighted degree of a finite family of pole bounds.

Equations

• BGS.HasseWeil.finitePrincipalPartsDegree n = ∑ i : I, n i * Module.finrank K (IsLocalRing.ResidueField (R i))

theorem BGS.HasseWeil.finitePrincipalPartsSpace_finrank {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] [Fintype I] {R : I → Type u_4} [(i : I) → CommRing (R i)] [∀ (i : I), IsDedekindDomain (R i)] [∀ (i : I), IsDiscreteValuationRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] [∀ (i : I), IsFractionRing (R i) L] (π : (i : I) → R i) (hπ : ∀ (i : I), π i ≠ 0) (hπIdeal : ∀ (i : I), (IsDiscreteValuationRing.maximalIdeal (R i)).asIdeal = Ideal.span {π i}) (n : I → ℕ) [∀ (i : I), Module.Finite K (IsLocalRing.ResidueField (R i))] : Module.finrank K (finitePrincipalPartsSpace π n) = finitePrincipalPartsDegree n

Finite principal parts have dimension equal to the weighted pole degree.

def BGS.HasseWeil.finitePrincipalPartsDiagonalMap {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] {R : I → Type u_4} [(i : I) → CommRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] (π : (i : I) → R i) (n : I → ℕ) (S : Submodule K L) (hS : ∀ (i : I), S ≤ localPoleSpace (π i) (n i)) : ↥S →ₗ[K] finitePrincipalPartsSpace π n

A global subspace with the prescribed local pole bounds maps diagonally to its finite family of principal parts.

Equations

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

def BGS.HasseWeil.regularAtFiniteFamily {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] {R : I → Type u_4} [(i : I) → CommRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] (π : (i : I) → R i) (S : Submodule K L) : Submodule K ↥S

The elements of a global subspace that are regular at every chosen place.

Equations

• BGS.HasseWeil.regularAtFiniteFamily π S = ⨅ (i : I), Submodule.comap S.subtype (BGS.HasseWeil.localPoleSpace (π i) 0)

theorem BGS.HasseWeil.finitePrincipalPartsDiagonalMap_ker {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] {R : I → Type u_4} [(i : I) → CommRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] (π : (i : I) → R i) (n : I → ℕ) (S : Submodule K L) (hS : ∀ (i : I), S ≤ localPoleSpace (π i) (n i)) : (finitePrincipalPartsDiagonalMap π n S hS).ker = regularAtFiniteFamily π S

The kernel of the diagonal principal-parts map is exactly simultaneous regularity at the chosen places.

theorem BGS.HasseWeil.finrank_quotient_regularAtFiniteFamily_le_degree {K : Type u_1} {L : Type u_2} {I : Type u_3} [Field K] [Field L] [Fintype I] {R : I → Type u_4} [(i : I) → CommRing (R i)] [∀ (i : I), IsDedekindDomain (R i)] [∀ (i : I), IsDiscreteValuationRing (R i)] [(i : I) → Algebra K (R i)] [(i : I) → Algebra (R i) L] [Algebra K L] [∀ (i : I), IsScalarTower K (R i) L] [∀ (i : I), IsFractionRing (R i) L] (π : (i : I) → R i) (hπ : ∀ (i : I), π i ≠ 0) (hπIdeal : ∀ (i : I), (IsDiscreteValuationRing.maximalIdeal (R i)).asIdeal = Ideal.span {π i}) (n : I → ℕ) (S : Submodule K L) (hS : ∀ (i : I), S ≤ localPoleSpace (π i) (n i)) [∀ (i : I), Module.Finite K (IsLocalRing.ResidueField (R i))] : Module.finrank K (↥S ⧸ regularAtFiniteFamily π S) ≤ finitePrincipalPartsDegree n

Consequently, the global quotient by simultaneous regularity has dimension at most the weighted pole degree.