The infinity valuation ring as a reciprocal localization

Writing Y = X⁻¹, a rational function is regular at infinity exactly when it belongs to the local ring K[Y]_(Y). This file proves that statement for the repository's valuation-ring model RatFuncInfinityIntegers K.

The proof is explicit: a function of nonpositive integer degree is written using the reversed numerator and denominator. This localization model is the bridge needed to transport polynomial normalization under finite constant extension to places above infinity.

@[instance_reducible]

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

The constant-field algebra on the infinity valuation ring of rational functions.

Equations

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

noncomputable def BGS.HasseWeil.reciprocalPolynomialRingHom (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Polynomial K →+* ↥(CorvajaZannier.RatFuncInfinityIntegers K)

Evaluate a polynomial in the reciprocal coordinate X⁻¹.

Equations

• BGS.HasseWeil.reciprocalPolynomialRingHom K = Polynomial.eval₂RingHom (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K) (BGS.CorvajaZannier.ratFuncInfinityUniformizer K)

@[reducible]

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

The polynomial algebra structure on the infinity valuation ring in the reciprocal coordinate. Its variable is the uniformizer X⁻¹.

Equations

• BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra K = (BGS.HasseWeil.reciprocalPolynomialRingHom K).toAlgebra

@[instance_reducible]

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

The algebra structure from K[X] to (RatFuncInfinityIntegers K) used in the rat func infinity localization construction.

Equations

• BGS.HasseWeil.reciprocalPolynomialAlgebra K = BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra K

theorem BGS.HasseWeil.reciprocalSpanXPrime (K : Type u_1) [Field K] : (Ideal.span {Polynomial.X}).IsPrime

@[simp]

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_X (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : (reciprocalPolynomialRingHom K) Polynomial.X = CorvajaZannier.ratFuncInfinityUniformizer K

@[simp]

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_C (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (c : K) : (reciprocalPolynomialRingHom K) (Polynomial.C c) = (algebraMap K ↥(CorvajaZannier.RatFuncInfinityIntegers K)) c

@[simp]

theorem BGS.HasseWeil.reciprocalPolynomialAlgebraMap_eq (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (p : Polynomial K) : (algebraMap (Polynomial K) ↥(CorvajaZannier.RatFuncInfinityIntegers K)) p = (reciprocalPolynomialRingHom K) p

@[simp]

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_coe (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (p : Polynomial K) : ↑((reciprocalPolynomialRingHom K) p) = Polynomial.eval₂ RatFunc.C (1 / RatFunc.X) p

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_isUnit_of_coeff_zero_ne_zero (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (p : Polynomial K) (hp : p.coeff 0 ≠ 0) : IsUnit ((reciprocalPolynomialRingHom K) p)

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_injective (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Function.Injective ⇑(reciprocalPolynomialRingHom K)

@[simp]

theorem BGS.HasseWeil.polynomialEvalRatFuncX_eq_algebraMap (K : Type u_1) [Field K] (p : Polynomial K) : Polynomial.eval₂ RatFunc.C RatFunc.X p = (algebraMap (Polynomial K) (RatFunc K)) p

theorem BGS.HasseWeil.eval_reciprocal_reverse_mul_X_pow (K : Type u_1) [Field K] (p : Polynomial K) : Polynomial.eval₂ RatFunc.C (1 / RatFunc.X) p.reverse * RatFunc.X ^ p.natDegree = (algebraMap (Polynomial K) (RatFunc K)) p

theorem BGS.HasseWeil.reciprocalPolynomialRingHom_surj (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (z : ↥(CorvajaZannier.RatFuncInfinityIntegers K)) : ∃ (x : Polynomial K × ↥(Ideal.span {Polynomial.X}).primeCompl), z * (algebraMap (Polynomial K) ↥(CorvajaZannier.RatFuncInfinityIntegers K)) ↑x.2 = (algebraMap (Polynomial K) ↥(CorvajaZannier.RatFuncInfinityIntegers K)) x.1

theorem BGS.HasseWeil.ratFuncInfinityIntegers_isLocalization_reciprocal (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsLocalization (Ideal.span {Polynomial.X}).primeCompl ↥(CorvajaZannier.RatFuncInfinityIntegers K)

The infinity valuation ring is the localization of the reciprocal polynomial coordinate ring at the origin.

theorem BGS.HasseWeil.ratFuncInfinityIntegersReciprocalLocalization (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsLocalization (Ideal.span {Polynomial.X}).primeCompl ↥(CorvajaZannier.RatFuncInfinityIntegers K)

noncomputable def BGS.HasseWeil.reciprocalPolynomialAtOriginAlgEquivInfinityIntegers (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Localization.AtPrime (Ideal.span {Polynomial.X}) ≃ₐ[Polynomial K] ↥(CorvajaZannier.RatFuncInfinityIntegers K)

Canonical localization model for the infinity valuation ring, with the polynomial variable corresponding to X⁻¹.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityLocalizationConstantAlgebra (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 rat func infinity localization construction.

Equations

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

@[instance_reducible]

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

The algebra structure from K[X] to (RatFuncInfinityIntegers K) used in the rat func infinity localization construction.

Equations

• BGS.HasseWeil.infinityLocalizationReciprocalPolynomialAlgebra K = BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra K

theorem BGS.HasseWeil.infinityLocalizationSpanXPrime (K : Type u_1) [Field K] : (Ideal.span {Polynomial.X}).IsPrime

@[reducible]

noncomputable def BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : Algebra (Polynomial K) N

Reciprocal polynomial structure on an extension of K(X). The variable acts as the image of X⁻¹.

Equations

• BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra K N = ((algebraMap (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) N).comp (BGS.HasseWeil.reciprocalPolynomialRingHom K)).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityLocalizationExtensionPolynomialAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : Algebra (Polynomial K) N

The algebra structure from K[X] to N used in the rat func infinity localization construction.

Equations

• BGS.HasseWeil.infinityLocalizationExtensionPolynomialAlgebra K N = BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra K N

theorem BGS.HasseWeil.infinityLocalizationPolynomialTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : IsScalarTower (Polynomial K) (↥(CorvajaZannier.RatFuncInfinityIntegers K)) N

theorem BGS.HasseWeil.infinityLocalizationBase (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsLocalization (Ideal.span {Polynomial.X}).primeCompl ↥(CorvajaZannier.RatFuncInfinityIntegers K)

theorem BGS.HasseWeil.infinityLocalizationExtensionPolynomialFaithful (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : FaithfulSMul (Polynomial K) N

theorem BGS.HasseWeil.infinityLocalizationExtensionSelf (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : IsLocalization (Algebra.algebraMapSubmonoid N (Ideal.span {Polynomial.X}).primeCompl) N

@[instance_reducible]

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

The algebra structure from K[X] to (RatFuncInfinityIntegralClosure K N) used in the rat func infinity localization construction.

Equations

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

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

noncomputable def BGS.HasseWeil.reciprocalIntegralClosureToInfinityAlgHom (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : ↥(integralClosure (Polynomial K) N) →ₐ[Polynomial K] ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)

Inclusion of the reciprocal affine normalization into its localization at infinity.

Equations

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

@[reducible]

noncomputable def BGS.HasseWeil.ratFuncInfinityReciprocalIntegralClosureAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : Algebra ↥(integralClosure (Polynomial K) N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)

Algebra structure on the infinity normalization induced by localizing the reciprocal affine normalization.

Equations

• BGS.HasseWeil.ratFuncInfinityReciprocalIntegralClosureAlgebra K N = (BGS.HasseWeil.reciprocalIntegralClosureToInfinityAlgHom K N).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.reciprocalIntegralClosureInfinityAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : Algebra ↥(integralClosure (Polynomial K) N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)

The algebra structure from (integralClosure K[X] N) to (RatFuncInfinityIntegralClosure K N) used in the rat func infinity localization construction.

Equations

• BGS.HasseWeil.reciprocalIntegralClosureInfinityAlgebra K N = BGS.HasseWeil.ratFuncInfinityReciprocalIntegralClosureAlgebra K N

theorem BGS.HasseWeil.reciprocalIntegralClosureInfinityAmbientTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : IsScalarTower (↥(integralClosure (Polynomial K) N)) (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)) N

theorem BGS.HasseWeil.reciprocalPolynomialIntegralClosuresTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : IsScalarTower (Polynomial K) ↥(integralClosure (Polynomial K) N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)

theorem BGS.HasseWeil.ratFuncInfinityIntegralClosure_isLocalization_reciprocal (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (N : Type u_2) [Field N] [Algebra (RatFunc K) N] : IsLocalization (Algebra.algebraMapSubmonoid (↥(integralClosure (Polynomial K) N)) (Ideal.span {Polynomial.X}).primeCompl) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K N)

The infinity integral closure is the localization of the reciprocal affine normalization away from the origin.