Riemann-space increments at infinity

Identify the kernel of the leading-residue map and bound the dimension increase by the degree of an infinite place.

@[instance_reducible]

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

The algebra structure from K to L used in the riemann space infinity place increment construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.upperInfinityConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the riemann space infinity place increment construction.

Equations

• BGS.HasseWeil.upperInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.upperInfinityClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the riemann space infinity place increment construction.

Equations

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

theorem BGS.HasseWeil.upperInfinityClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.upperInfinityClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.upperInfinityClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.upperInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.HasseWeil.upperInfinityClosureTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.upperInfinityClosureDedekind (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.upperInfinityClosureFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.HasseWeil.upperInfinityClosureConstantTowerToField (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_infinityPlace_increment (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) [Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)] : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single (Sum.inr P) 1)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single (Sum.inr P) 1)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) + CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P)

Adding one infinity place to an effective divisor preserves finite dimensionality. The dimension jump is at most the degree of that place.