Infinity places in an exact constant extension

This file localizes the reciprocal affine normalizations used by the exact constant-extension model. A height-one prime of

S ⊗[C] integralClosure C[X] N

above the reciprocal origin gives actual places above infinity in both the extended function field and the original function field. Their residue degrees satisfy the usual division-by-gcd formula.

@[instance_reducible]

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

The algebra structure from K[X] to (RatFunc K) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.reciprocalRatFuncPolynomialAlgebra K = BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra K (RatFunc K)

@[instance_reducible]

noncomputable def BGS.HasseWeil.reciprocalRatFuncPolynomialSMul (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : SMul (Polynomial K) (RatFunc K)

The scalar action of K[X] on (RatFunc K) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.reciprocalRatFuncPolynomialSMul K = (BGS.HasseWeil.reciprocalRatFuncPolynomialAlgebra K).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.reciprocalRatFuncPolynomialModule (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Module (Polynomial K) (RatFunc K)

The module structure of (RatFunc K) over K[X] used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.reciprocalRatFuncPolynomialModule K = Algebra.toModule

theorem BGS.HasseWeil.reciprocalRatFuncPolynomialFaithful (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : FaithfulSMul (Polynomial K) (RatFunc K)

theorem BGS.HasseWeil.ratFunc_isFractionRing_reciprocalPolynomial (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsFractionRing (Polynomial K) (RatFunc K)

The reciprocal polynomial embedding K[X] → K(X), sending the polynomial variable to X⁻¹, still has K(X) as its fraction field.

noncomputable def BGS.HasseWeil.heightOneResidueFieldRingEquiv {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (e : A ≃+* B) (q : IsDedekindDomain.HeightOneSpectrum A) : q.asIdeal.ResidueField ≃+* ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) q).asIdeal.ResidueField

A ring equivalence transports the residue field of a height-one prime.

Equations

• BGS.HasseWeil.heightOneResidueFieldRingEquiv e q = q.asIdeal.residueFieldRingEquiv ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) q).asIdeal e ⋯

theorem BGS.HasseWeil.mappedPrimeCompl_disjoint_of_under_eq (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] (p : Ideal R) [p.IsPrime] (q : Ideal A) (hq : Ideal.under R q = p) : Disjoint ↑(Algebra.algebraMapSubmonoid A p.primeCompl) ↑q

A prime is disjoint from the image of the complement of its contracted prime.

theorem BGS.HasseWeil.localizationMap_liesOver_maximalIdeal (R : Type u_1) (V : Type u_2) (A : Type u_3) (B : Type u_4) [CommRing R] [CommRing V] [CommRing A] [CommRing B] [Algebra R V] [Algebra R A] [Algebra R B] [Algebra V B] [Algebra A B] [IsScalarTower R V B] [IsScalarTower R A B] (p : Ideal R) [p.IsPrime] [IsLocalization p.primeCompl V] [IsLocalRing V] (q : Ideal A) (hqPrime : q.IsPrime) (hqUnder : Ideal.under R q = p) [IsLocalization (Algebra.algebraMapSubmonoid A p.primeCompl) B] : (Ideal.map (algebraMap A B) q).LiesOver (IsLocalRing.maximalIdeal V)

Localizing a prime over the base prime gives a prime over the local maximal ideal.

noncomputable def BGS.HasseWeil.localizationResidueFieldAlgEquiv (K : Type u_1) (A : Type u_2) (B : Type u_3) [Field K] [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] [Algebra A B] [IsScalarTower K A B] (M : Submonoid A) [IsLocalization M B] (q : Ideal A) [q.IsPrime] (hdisj : Disjoint ↑M ↑q) : let Q := Ideal.map (algebraMap A B) q; q.ResidueField ≃ₐ[K] Q.ResidueField

Localizing away from a prime preserves its residue field as an algebra over the base field.

Equations

• BGS.HasseWeil.localizationResidueFieldAlgEquiv K A B M q hdisj = AlgEquiv.ofBijective (Ideal.ResidueField.mapₐ q (Ideal.map (algebraMap A B) q) (IsScalarTower.toAlgHom K A B) ⋯) ⋯

noncomputable def BGS.HasseWeil.localizationResidueFieldRingEquiv (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [Algebra A B] (M : Submonoid A) [IsLocalization M B] (q : Ideal A) [q.IsPrime] (hdisj : Disjoint ↑M ↑q) : let Q := Ideal.map (algebraMap A B) q; q.ResidueField ≃+* Q.ResidueField

Localizing away from a prime preserves its residue field as a ring.

Equations

• BGS.HasseWeil.localizationResidueFieldRingEquiv A B M q hdisj = RingEquiv.ofBijective (Ideal.ResidueField.map q (Ideal.map (algebraMap A B) q) (algebraMap A B) ⋯) ⋯

theorem BGS.HasseWeil.coefficientPolynomial_under_span_X (C : Type u_1) (S : Type u_2) [Field C] [Field S] [Algebra C S] : Ideal.under (Polynomial C) (Ideal.span {Polynomial.X}) = Ideal.span {Polynomial.X}

Extending polynomial coefficients carries the reciprocal origin back to the reciprocal origin.

theorem BGS.HasseWeil.polynomialTensorCancel_algebraMap_coefficient (C : Type u_1) (S : Type u_2) (A : Type u_3) [Field C] [Field S] [CommRing A] [Algebra C S] [Algebra (Polynomial C) A] [Algebra C A] [IsScalarTower C (Polynomial C) A] (p : Polynomial C) : (algebraMap (Polynomial S) (TensorProduct C S A)) ((algebraMap (Polynomial C) (Polynomial S)) p) = 1 ⊗ₜ[C] (algebraMap (Polynomial C) A) p

In the polynomial-cancellation model, coefficient extension of a polynomial acts as the right pure tensor of its old action.

@[instance_reducible]

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

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

Equations

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

@[instance_reducible]

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

Decidable equality on S used in the constant extension infinity place bridge construction.

Equations

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

@[instance_reducible]

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

Decidable equality on (RatFunc C) used in the constant extension infinity place bridge construction.

Equations

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

@[instance_reducible]

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

Decidable equality on (RatFunc S) used in the constant extension infinity place bridge construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeBaseConstantAlgebra (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 constant extension infinity place bridge construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeBaseReciprocalPolynomialAlgebra (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 constant extension infinity place bridge construction.

Equations

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

theorem BGS.HasseWeil.infinityBridgeBaseConstantPolynomialTower (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.infinityBridgeOldNormalizationConstantAlgebra (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 constant extension infinity place bridge construction.

Equations

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

theorem BGS.HasseWeil.infinityBridgeOldNormalizationConstantPolynomialTower (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.infinityBridgeTensorPolynomialAlgebra (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] : Algebra (Polynomial S) (TensorProduct C S ↥(integralClosure (Polynomial C) N))

The algebra structure from S[X] to (S ⊗[C] integralClosure C[X] N) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeTensorPolynomialAlgebra C S N = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S ↥(integralClosure (Polynomial C) N)

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeTensorConstantAlgebra (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] : Algebra S (TensorProduct C S ↥(integralClosure (Polynomial C) N))

The algebra structure from S to (S ⊗[C] integralClosure C[X] N) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeTensorConstantAlgebra C S N = Algebra.TensorProduct.leftAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeTensorOldNormalizationAlgebra (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] : Algebra (↥(integralClosure (Polynomial C) N)) (TensorProduct C S ↥(integralClosure (Polynomial C) N))

The algebra structure from (integralClosure C[X] N) to (S ⊗[C] integralClosure C[X] N) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeTensorOldNormalizationAlgebra C S N = Algebra.TensorProduct.rightAlgebra

noncomputable def BGS.HasseWeil.exactConstantExtensionInfinityDownstairsIdeal (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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) : Ideal ↥(integralClosure (Polynomial C) N)

Contract a reciprocal tensor-normalization prime to the old reciprocal normalization.

Equations

• BGS.HasseWeil.exactConstantExtensionInfinityDownstairsIdeal C S N q = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q.asIdeal

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionInfinityDownstairsIdeal_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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) : exactConstantExtensionInfinityDownstairsIdeal C S N q = Ideal.comap Algebra.TensorProduct.includeRight.toRingHom q.asIdeal

theorem BGS.HasseWeil.exactConstantExtensionInfinityDownstairsIdeal_under (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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : Ideal.under (Polynomial C) (exactConstantExtensionInfinityDownstairsIdeal C S N q) = Ideal.span {Polynomial.X}

A tensor-normalization prime above the reciprocal origin contracts to a prime above the reciprocal origin in the old normalization.

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeBaseInfinityPolynomialAlgebra (C : Type u_1) [Field C] : Algebra (Polynomial C) ↥(CorvajaZannier.RatFuncInfinityIntegers C)

The algebra structure from C[X] to (RatFuncInfinityIntegers C) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeBaseInfinityPolynomialAlgebra C = BGS.HasseWeil.ratFuncInfinityReciprocalPolynomialAlgebra C

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeBaseInfinityConstantAlgebra (C : Type u_1) [Field C] : Algebra C ↥(CorvajaZannier.RatFuncInfinityIntegers C)

The algebra structure from C to (RatFuncInfinityIntegers C) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeBaseInfinityConstantAlgebra C = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom C).toAlgebra

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

theorem BGS.HasseWeil.infinityBridgeBaseInfinityLocalization (C : Type u_1) [Field C] : IsLocalization (Ideal.span {Polynomial.X}).primeCompl ↥(CorvajaZannier.RatFuncInfinityIntegers C)

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityBridgeOldNormalizationInfinityAlgebra C N = BGS.HasseWeil.ratFuncInfinityReciprocalIntegralClosureAlgebra C N

@[instance_reducible]

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

The scalar action of (integralClosure C[X] N) on (RatFuncInfinityIntegralClosure C N) used in the constant extension infinity place bridge construction.

Equations

• BGS.HasseWeil.infinityBridgeOldNormalizationInfinitySMul C N = (BGS.HasseWeil.infinityBridgeOldNormalizationInfinityAlgebra C N).toSMul

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

@[instance_reducible]

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

The algebra structure from C[X] to (RatFuncInfinityIntegralClosure C N) used in the constant extension infinity place bridge construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinityBridgeInfinityConstantAlgebra (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N)

The algebra structure from C to (RatFuncInfinityIntegralClosure C N) used in the constant extension infinity place bridge construction.

Equations

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

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

theorem BGS.HasseWeil.infinityBridgeBasePolynomialInfinityTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower (Polynomial C) ↥(CorvajaZannier.RatFuncInfinityIntegers C) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N)

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

noncomputable def BGS.HasseWeil.exactConstantExtensionDownstairsInfinityPlace (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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : ↑(CorvajaZannier.FiniteExtensionInfinityPlace C N)

The contraction of a reciprocal tensor prime, localized at the old reciprocal origin, is an actual place of N above infinity.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionDownstairsInfinityPlace_asIdeal (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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : ↑(exactConstantExtensionDownstairsInfinityPlace C S N q hqOrigin) = Ideal.map (algebraMap ↥(integralClosure (Polynomial C) N) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C N)) (exactConstantExtensionInfinityDownstairsIdeal C S N q)

noncomputable def BGS.HasseWeil.exactConstantExtensionDownstairsResidueFieldAlgEquiv (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] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : let i := Algebra.TensorProduct.includeRight.toRingHom; let p := exactConstantExtensionInfinityDownstairsIdeal C S N q; p.ResidueField ≃ₐ[C] (↑(exactConstantExtensionDownstairsInfinityPlace C S N q hqOrigin)).ResidueField

Localization at the reciprocal origin does not change the residue field of the contracted downstairs prime.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionUpstairsInfinityPlace (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : ↑(CorvajaZannier.FiniteExtensionInfinityPlace S (ExactConstantExtension C N S))

Localizing the corresponding prime in the reciprocal affine normalization of the exact constant extension produces an actual upstairs place above infinity.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionUpstairsResidueFieldRingEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : q.asIdeal.ResidueField ≃+* (↑(exactConstantExtensionUpstairsInfinityPlace C S N hExact q hqOrigin)).ResidueField

The reciprocal affine prime and the corresponding actual upstairs infinity place have canonically ring-equivalent residue fields.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionUpstairsInfinityResidueField_finite (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : Finite (↑(exactConstantExtensionUpstairsInfinityPlace C S N hExact q hqOrigin)).ResidueField

The residue field of the actual upstairs infinity place is finite.

theorem BGS.HasseWeil.exactConstantExtensionInfinityTensorResidueField_finite (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Finite C] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : Finite q.asIdeal.ResidueField

The residue field of the reciprocal tensor-normalization prime is finite.

theorem BGS.HasseWeil.exactConstantExtensionInfinityTensorIdeal_isMaximal (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Finite C] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : q.asIdeal.IsMaximal

A reciprocal tensor-normalization height-one prime above the origin is maximal; no maximality hypothesis is left to the residue calculation.

theorem BGS.HasseWeil.exactConstantExtensionInfinityDownstairsResidueField_finite (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] [Finite C] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : let p := exactConstantExtensionInfinityDownstairsIdeal C S N q; let i := Algebra.TensorProduct.includeRight.toRingHom; Finite p.ResidueField

The residue field of the contracted downstairs reciprocal prime is finite.

theorem BGS.HasseWeil.exactConstantExtensionInfinityPlace_degree_eq_div_gcd (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (Sum.inr (exactConstantExtensionUpstairsInfinityPlace C S N hExact q hqOrigin)) = CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr (exactConstantExtensionDownstairsInfinityPlace C S N q hqOrigin)) / (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr (exactConstantExtensionDownstairsInfinityPlace C S N q hqOrigin)))

Exact extension of constants changes the degree of an actual infinity place by the standard division-by-gcd formula.

theorem BGS.HasseWeil.exactConstantExtensionInfinityPlace_degree_eq_one_of_dvd (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) (hqOrigin : Ideal.under (Polynomial S) q.asIdeal = Ideal.span {Polynomial.X}) (hdiv : CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr (exactConstantExtensionDownstairsInfinityPlace C S N q hqOrigin)) ∣ Module.finrank C S) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (Sum.inr (exactConstantExtensionUpstairsInfinityPlace C S N hExact q hqOrigin)) = 1

If the downstairs infinity-place degree divides the extension degree of the constants, the corresponding upstairs infinity place has degree one.