The canonical divisor -2∞ on the rational function field

This module constructs an actual infinity place of the identity extension K(X) / K(X), proves that its residue degree is one, and identifies the divisor supported there with coefficient -2 as canonical. The proof uses the in-repository Riemann--Roch theorem and the proved genus-zero theorem for RatFunc K; it does not assume a base canonical divisor.

theorem BGS.HasseWeil.ratFuncIdentityInfinityClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K (RatFunc K))

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

theorem BGS.HasseWeil.ratFuncIdentityInfinityClosureIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K (RatFunc K))

theorem BGS.HasseWeil.ratFuncIdentityInfinityClosureNoZeroSMulDivisors (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : NoZeroSMulDivisors ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K (RatFunc K))

theorem BGS.HasseWeil.ratFuncIdentityInfinityClosureIsDedekind (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K (RatFunc K))

theorem BGS.HasseWeil.ratFuncIdentityInfinityClosureIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K (RatFunc K))) (RatFunc K)

noncomputable def BGS.HasseWeil.ratFuncIdentityInfinityPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K (RatFunc K))

A place above infinity in the identity extension K(X) / K(X).

Equations

• BGS.HasseWeil.ratFuncIdentityInfinityPlace K = Classical.choice ⋯

theorem BGS.HasseWeil.ratFuncIdentityInfinityPlace_degree_eq_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : CorvajaZannier.finiteExtensionPlaceDegree K (RatFunc K) (Sum.inr (ratFuncIdentityInfinityPlace K)) = 1

The chosen identity-extension infinity place has residue degree one.

noncomputable def BGS.HasseWeil.ratFuncInfinityChartPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : MarkoffRiemannRoch.FunctionField.Chart.PlaceA K (RatFunc K)

The chosen infinity place in the Riemann--Roch two-chart place model.

Equations

• BGS.HasseWeil.ratFuncInfinityChartPlace K = (BGS.HasseWeil.finiteExtensionPlaceEquivChart K (RatFunc K)) (Sum.inr (BGS.HasseWeil.ratFuncIdentityInfinityPlace K))

noncomputable def BGS.HasseWeil.ratFuncCanonicalInfinityDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : MarkoffRiemannRoch.FunctionField.Chart.DivisorA K (RatFunc K)

The explicit divisor -2∞ on K(X).

Equations

• BGS.HasseWeil.ratFuncCanonicalInfinityDivisor K = Finsupp.single (BGS.HasseWeil.ratFuncInfinityChartPlace K) (-2)

theorem BGS.HasseWeil.ratFuncCanonicalInfinityDivisor_degree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : MarkoffRiemannRoch.FunctionField.Chart.deg K (RatFunc K) (ratFuncCanonicalInfinityDivisor K) = -2

The explicit divisor -2∞ has degree -2.

theorem BGS.HasseWeil.ratFuncCanonicalInfinityDivisor_isCanonical (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : MarkoffRiemannRoch.FunctionField.Chart.IsCanonical K (RatFunc K) (ratFuncCanonicalInfinityDivisor K)

The explicit divisor -2∞ is canonical on K(X).