Compatibility of infinity places with exact constant extension

The reciprocal affine normalization of an exact constant extension may be viewed either over the original constants or over the extended constants. This module proves that these two presentations commute with localization at infinity. Consequently, the explicit upstairs infinity prime contracts to the explicit downstairs infinity prime under the canonical algebra on infinity normalizations.

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityPlaceCompatibilityBaseConstantAlgebra (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 place compatibility construction.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityBaseConstantAlgebra C N = BGS.HasseWeil.infinityConstantAlgebra C N

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityPlaceCompatibilityBaseReciprocalPolynomialAlgebra (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 place compatibility construction.

Equations

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

theorem BGS.HasseWeil.infinityPlaceCompatibilityBaseConstantReciprocalTower (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.infinityPlaceCompatibilityOldNormalizationConstantAlgebra (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 place compatibility construction.

Equations

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

theorem BGS.HasseWeil.infinityPlaceCompatibilityOldNormalizationConstantPolynomialTower (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.infinityPlaceCompatibilityCoefficientPolynomialAlgebra (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 place compatibility construction.

Equations

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

@[instance_reducible]

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

The scalar action of C[X] on S[X] used in the exact constant extension infinity place compatibility construction.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityCoefficientPolynomialSMul C S = (BGS.HasseWeil.infinityPlaceCompatibilityCoefficientPolynomialAlgebra C S).toSMul

@[instance_reducible]

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

The module structure of S[X] over C[X] used in the exact constant extension infinity place compatibility construction.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityCoefficientPolynomialModule C S = Algebra.toModule

@[instance_reducible]

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

Classical equality on base rational functions in the infinity-place comparison.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityDecidableEqBaseRatFunc C = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants C

@[instance_reducible]

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

Classical equality on rational functions over the enlarged constants in that comparison.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityDecidableEqExtendedRatFunc S = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants S

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityDecidableEqBase C = BGS.HasseWeil.infinityBridgeDecidableEqConstants C

@[instance_reducible]

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

Classical equality on the enlarged constants in the infinity-place comparison.

Equations

• BGS.HasseWeil.infinityPlaceCompatibilityDecidableEqExtended S = BGS.HasseWeil.infinityBridgeDecidableEqConstants S

theorem BGS.HasseWeil.exactConstantExtensionUpstairsInfinityPlace_under (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Fintype C] [Finite S] (hExact : algebraicClosure C N = ⊥) (q : ExactConstantExtensionPresentedInfinityPlace C S N) : let E := ExactConstantExtension C N S; let R2 := CorvajaZannier.RatFuncInfinityIntegralClosure C N; have B := CorvajaZannier.RatFuncInfinityIntegralClosure S E; Ideal.under ↥R2 ↑(exactConstantExtensionUpstairsInfinityPlace C S N hExact ↑q ⋯) = ↑(exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯)

The explicit upstairs infinity prime of an exact constant extension contracts, through the canonical algebra on infinity normalizations, to its explicit downstairs infinity prime.