Normalization at infinity in an exact constant extension

The affine coordinate at infinity is the reciprocal variable X⁻¹. This file checks that the copy of S(X) in the exact constant extension S ⊗[C] N sends that reciprocal variable to the tensor extension of the reciprocal coordinate on N.

Smooth base change and polynomial tensor cancellation then identify the constant extension of the reciprocal affine normalization with the reciprocal affine normalization over S. Localizing away from the origin gives a ring equivalence with the actual infinity integral closure. Thus no comparison with the finite-place coordinate is used or assumed.

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityDecidableEqBase (C : Type u_1) : DecidableEq C

Decidable equality on C used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityDecidableEqBase C = Classical.decEq C

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityDecidableEqRatFuncBase (C : Type u_1) [Field C] : DecidableEq (RatFunc C)

Decidable equality on (RatFunc C) used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityDecidableEqRatFuncBase C = Classical.decEq (RatFunc C)

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityDecidableEqConstants (S : Type u_2) : DecidableEq S

Decidable equality on S used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityDecidableEqConstants S = Classical.decEq S

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityDecidableEqRatFuncConstants (S : Type u_2) [Field S] : DecidableEq (RatFunc S)

Decidable equality on (RatFunc S) used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityDecidableEqRatFuncConstants S = Classical.decEq (RatFunc S)

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityConstantAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap C (RatFunc C))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityReciprocalPolynomialAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra (Polynomial C) N

The algebra structure from C[X] to N used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityReciprocalPolynomialAlgebra C N = BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra C N

theorem BGS.HasseWeil.infinityReciprocalPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (Polynomial C) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityReciprocalNormalizationConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C ↥(integralClosure (Polynomial C) N)

The algebra structure from C to (integralClosure C[X] N) used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityReciprocalNormalizationConstantAlgebra C N = ((algebraMap (Polynomial C) ↥(integralClosure (Polynomial C) N)).comp (algebraMap C (Polynomial C))).toAlgebra

theorem BGS.HasseWeil.infinityReciprocalNormalizationPolynomialTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (Polynomial C) ↥(integralClosure (Polynomial C) N)

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityCoefficientPolynomialAlgebra (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Algebra (Polynomial C) (Polynomial S)

The algebra structure from C[X] to S[X] used in the exact constant extension infinity normalization construction.

Equations

• BGS.HasseWeil.infinityCoefficientPolynomialAlgebra C S = Polynomial.algebra C S

theorem BGS.HasseWeil.infinitySpanXPrime (S : Type u_2) [Field S] : (Ideal.span {Polynomial.X}).IsPrime

theorem BGS.HasseWeil.ratFuncToExactConstantExtension_reciprocal_X (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : (ratFuncToExactConstantExtension C S N hExact) (1 / RatFunc.X) = polynomialTensorCancelEvaluationPoint C S N

The reciprocal coordinate in the exact constant extension is the tensor extension of the reciprocal coordinate on N.

theorem BGS.HasseWeil.exactConstantExtensionReciprocalPolynomialAlgebra_eq (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : polynomialTensorCancelTargetPolynomialExtensionAlgebra C S N = ratFuncExtensionReciprocalPolynomialAlgebra S (ExactConstantExtension C N S)

The tensor-product polynomial action in the reciprocal coordinate is exactly the reciprocal polynomial action induced from S(X).

noncomputable def BGS.HasseWeil.finiteFieldReciprocalNormalizationAlgEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [Fintype C] [Finite S] : TensorProduct C S ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))

Smooth base change in the reciprocal coordinate, before identifying the target polynomial action with the one induced from S(X).

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionInfinityAffineNormalizationAlgEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Fintype C] [Finite S] : TensorProduct C S ↥(integralClosure (Polynomial C) N) ≃ₐ[Polynomial S] ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))

The constant extension of the reciprocal affine normalization is the actual reciprocal affine normalization of the exact constant extension.

Equations

• BGS.HasseWeil.exactConstantExtensionInfinityAffineNormalizationAlgEquiv C S N hExact = ⋯.mpr (BGS.HasseWeil.finiteFieldReciprocalNormalizationAlgEquiv C S N)

theorem BGS.HasseWeil.exactConstantExtensionInfinityAffineNormalization_map_primeCompl (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Fintype C] [Finite S] : have e := exactConstantExtensionInfinityAffineNormalizationAlgEquiv C S N hExact; Submonoid.map e (Algebra.algebraMapSubmonoid (TensorProduct C S ↥(integralClosure (Polynomial C) N)) (Ideal.span {Polynomial.X}).primeCompl) = Algebra.algebraMapSubmonoid (↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) (Ideal.span {Polynomial.X}).primeCompl

The reciprocal affine normalization equivalence carries the natural localization set away from X = 0 to the corresponding target set.

noncomputable def BGS.HasseWeil.exactConstantExtensionInfinityNormalizationLocalizationRingEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Fintype C] [Finite S] : Localization (Algebra.algebraMapSubmonoid (TensorProduct C S ↥(integralClosure (Polynomial C) N)) (Ideal.span {Polynomial.X}).primeCompl) ≃+* ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S (ExactConstantExtension C N S))

Localizing the constant extension of the reciprocal normalization gives the actual integral closure of the infinity valuation ring in the exact constant extension. As a ring equivalence, this directly transports prime ideals, local rings, and residue rings.

Equations

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