Riemann-space increments from a local residue map

A local scaling order determines regularity and the residue kernel. Finite and infinite places supply their local rings and order identities to this common dimension argument.

noncomputable def BGS.HasseWeil.localNormalizedLift {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra R L] [Algebra K L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (x : ↥T) : R

A normalized lift of a finite-place residue class into the local ring.

Equations

• BGS.HasseWeil.localNormalizedLift T a hregular x = Classical.choose ⋯

theorem BGS.HasseWeil.localNormalizedLift_spec {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra R L] [Algebra K L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (x : ↥T) : a * ↑x = (algebraMap R L) (localNormalizedLift T a hregular x)

theorem BGS.HasseWeil.localNormalizedLift_add {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [Field L] [Algebra R L] [Algebra K L] [IsFractionRing R L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (x y : ↥T) : localNormalizedLift T a hregular (x + y) = localNormalizedLift T a hregular x + localNormalizedLift T a hregular y

theorem BGS.HasseWeil.localNormalizedLift_smul {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] [IsFractionRing R L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (c : K) (x : ↥T) : localNormalizedLift T a hregular (c • x) = c • localNormalizedLift T a hregular x

noncomputable def BGS.HasseWeil.localNormalizedLiftLinearMap {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] [IsFractionRing R L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) : ↥T →ₗ[K] R

The linear map sending a residue class to its normalized local lift.

Equations

• BGS.HasseWeil.localNormalizedLiftLinearMap T a hregular = { toFun := BGS.HasseWeil.localNormalizedLift T a hregular, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def BGS.HasseWeil.localLeadingResidueLinearMap {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] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) : ↥T →ₗ[K] IsLocalRing.ResidueField R

The linear map extracting the leading residue of a local element.

Equations

• BGS.HasseWeil.localLeadingResidueLinearMap T a hregular = (Ideal.Quotient.mkₐ K (IsLocalRing.maximalIdeal R)).toLinearMap ∘ₗ BGS.HasseWeil.localNormalizedLiftLinearMap T a hregular

theorem BGS.HasseWeil.localLeadingResidueLinearMap_eq_zero_iff {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] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (x : ↥T) : (localLeadingResidueLinearMap T a hregular) x = 0 ↔ localNormalizedLift T a hregular x ∈ IsLocalRing.maximalIdeal R

theorem BGS.HasseWeil.mem_heightOneSpectrum_of_one_le_finitePlaceOrder_algebraMap {R : Type u_2} {L : Type u_3} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [IsFractionRing R L] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (horder : 1 ≤ CorvajaZannier.finitePlaceOrder v ((algebraMap R L) r)) : r ∈ v.asIdeal

theorem BGS.HasseWeil.localNormalizedLift_mem_maximalIdeal_iff {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra R L] [Algebra K L] [IsFractionRing R L] (T : Submodule K L) (a : L) (hregular : ∀ (x : ↥T), ∃ (r : R), a * ↑x = (algebraMap R L) r) (x : ↥T) : localNormalizedLift T a hregular x ∈ IsLocalRing.maximalIdeal R ↔ 1 ≤ CorvajaZannier.finitePlaceOrderTop (IsDiscreteValuationRing.maximalIdeal R) (a * ↑x)

A normalized lift has zero residue exactly when its local order is positive.

theorem BGS.HasseWeil.riemannSpace_finite_and_finrank_le_of_residue_map {k : Type u_1} {E : Type u_2} {F : Type u_3} [Field k] [AddCommGroup E] [Module k E] [AddCommGroup F] [Module k F] [Module.Finite k F] (S T : Submodule k E) [Module.Finite k ↥S] (hST : S ≤ T) (f : ↥T →ₗ[k] F) (hker : f.ker = Submodule.comap T.subtype S) : Module.Finite k ↥T ∧ Module.finrank k ↥T ≤ Module.finrank k ↥S + Module.finrank k F

A residue map with the prescribed kernel bounds a finite Riemann-space extension.

@[instance_reducible]

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

The constant-field algebra induced by the canonical maps from K through RatFunc K.

Equations

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

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_increment_of_local_order (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {R : Type u_3} [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Algebra K R] [Algebra R L] [IsScalarTower K R L] [IsFractionRing R L] [Module.Finite K (IsLocalRing.ResidueField R)] (D : CorvajaZannier.FiniteExtensionDivisor K L) (Q : CorvajaZannier.FiniteExtensionPlace K L) (a : L) [Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)] (hscaleOrder : ∀ (x : L), x ≠ 0 → CorvajaZannier.finitePlaceOrderTop (IsDiscreteValuationRing.maximalIdeal R) (a * x) = ↑(D Q + 1 + (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) Q)) : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single Q 1)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single Q 1)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) + Module.finrank K (IsLocalRing.ResidueField R)

A scaling order at a local DVR determines the one-place residue kernel and rank bound.