Splitting multiplicity at infinity in an exact extension of constants

This file identifies the reciprocal-normalization presentation of the places at infinity with the actual places over the original constant field. It then proves that an exact extension of constants is unramified at those places.

The comparison is noncircular: reciprocal affine normalizations are first compared over C[X], and only then localized to the valuation ring at infinity.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinitySplittingDecidableEqBase C = BGS.HasseWeil.infinityBridgeDecidableEqConstants C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinitySplittingDecidableEqRatFuncBase C = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinitySplittingDecidableEqConstants S = BGS.HasseWeil.infinityBridgeDecidableEqConstants S

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinitySplittingDecidableEqRatFuncConstants S = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants S

@[reducible]

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

The constant-field algebra on the original function field for the infinity splitting calculation.

Equations

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

@[reducible]

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

The algebra of reciprocal polynomials on the original function field.

Equations

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

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingOldNormalizationConstantAlgebra (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 splitting multiplicity construction.

Equations

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

theorem BGS.HasseWeil.infinitySplittingOldNormalizationConstantPolynomialTower (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.infinitySplittingCoefficientPolynomialAlgebra (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 constant extension infinity place splitting multiplicity construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingCoefficientPolynomialSMul (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 constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingCoefficientPolynomialSMul C S = (BGS.HasseWeil.infinitySplittingCoefficientPolynomialAlgebra C S).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingCoefficientPolynomialModule (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 constant extension infinity place splitting multiplicity construction.

Equations

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

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

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

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionCReciprocalPolynomialAlgebra (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 C) (ExactConstantExtension C N S)

The reciprocal C[X]-action on the exact constant extension.

Equations

• BGS.HasseWeil.exactConstantExtensionCReciprocalPolynomialAlgebra C S N = (Algebra.TensorProduct.includeRight.comp (algebraMap (Polynomial C) N)).toAlgebra

@[reducible]

noncomputable def BGS.HasseWeil.infinitySplittingExactCPolynomialAlgebra (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 C) (ExactConstantExtension C N S)

The polynomial algebra over the original constants on the exact constant extension.

Equations

• BGS.HasseWeil.infinitySplittingExactCPolynomialAlgebra C S N = BGS.HasseWeil.exactConstantExtensionCReciprocalPolynomialAlgebra C S N

@[reducible]

noncomputable def BGS.HasseWeil.infinitySplittingExactSPolynomialAlgebra (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) (ExactConstantExtension C N S)

The polynomial algebra over the enlarged constants on the exact constant extension.

Equations

• BGS.HasseWeil.infinitySplittingExactSPolynomialAlgebra C S N = BGS.HasseWeil.polynomialTensorCancelTargetPolynomialExtensionAlgebra C S N

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingExactCPolynomialSMul (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] : SMul (Polynomial C) (ExactConstantExtension C N S)

The scalar action of C[X] on (ExactConstantExtension C N S) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingExactCPolynomialSMul C S N = (BGS.HasseWeil.infinitySplittingExactCPolynomialAlgebra C S N).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingExactCPolynomialModule (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] : Module (Polynomial C) (ExactConstantExtension C N S)

The module structure of (ExactConstantExtension C N S) over C[X] used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingExactCPolynomialModule C S N = Algebra.toModule

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingExactSPolynomialSMul (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] : SMul (Polynomial S) (ExactConstantExtension C N S)

The scalar action of S[X] on (ExactConstantExtension C N S) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingExactSPolynomialSMul C S N = (BGS.HasseWeil.infinitySplittingExactSPolynomialAlgebra C S N).toSMul

@[reducible]

noncomputable def BGS.HasseWeil.infinitySplittingPresentedSPolynomialAlgebra (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 enlarged-constant polynomial algebra on the presented extension field.

Equations

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

@[reducible]

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

The original-constant polynomial algebra on the presented extension field.

Equations

• BGS.HasseWeil.infinitySplittingPresentedCPolynomialAlgebra C S N = (Algebra.TensorProduct.includeRight.comp (algebraMap (Polynomial C) ↥(integralClosure (Polynomial C) N))).toAlgebra

@[instance_reducible]

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

The scalar action of S[X] on (TensorProduct C S (integralClosure C[X] N)) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingPresentedSPolynomialSMul C S N = (BGS.HasseWeil.infinitySplittingPresentedSPolynomialAlgebra C S N).toSMul

@[instance_reducible]

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

The scalar action of C[X] on (TensorProduct C S (integralClosure C[X] N)) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingPresentedCPolynomialSMul C S N = (BGS.HasseWeil.infinitySplittingPresentedCPolynomialAlgebra C S N).toSMul

theorem BGS.HasseWeil.exactConstantExtensionReciprocalPolynomialTower (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] : IsScalarTower (Polynomial C) (Polynomial S) (ExactConstantExtension C N S)

The reciprocal polynomial actions on the exact constant extension form the expected scalar tower.

noncomputable def BGS.HasseWeil.exactConstantExtensionReciprocalIntegralClosureTowerEquiv (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] [IsGalois C S] : ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)) ≃+* ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))

Integral closure is unchanged when the integral coefficient extension C[X] -> S[X] is inserted into the reciprocal normalization.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedToCReciprocalNormalizationRingEquiv (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] [IsGalois C S] : TensorProduct C S ↥(integralClosure (Polynomial C) N) ≃+* ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S))

The presented reciprocal normalization is the normalization of the exact constant extension over the original reciprocal polynomial ring C[X].

Equations

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

theorem BGS.HasseWeil.ratFuncExtensionReciprocalPolynomialAlgebra_map (K : Type u_4) (L : Type u_5) [Field K] [Field L] [DecidableEq K] [DecidableEq (RatFunc K)] [Algebra (RatFunc K) L] (p : Polynomial K) : (algebraMap (Polynomial K) L) p = (algebraMap (RatFunc K) L) ↑((reciprocalPolynomialRingHom K) p)

The reciprocal polynomial algebra map is the composite through the rational-function field.

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

The transported reciprocal C[X]-action is the actual action induced by the canonical embedding of C(X) into the exact constant extension.

noncomputable def BGS.HasseWeil.exactConstantExtensionCReciprocalNormalizationRingEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)) ≃+* ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S))

Replace the transported reciprocal polynomial action by the definitionally actual action induced from C(X).

Equations

• BGS.HasseWeil.exactConstantExtensionCReciprocalNormalizationRingEquiv C S N hExact = ⋯.mpr (RingEquiv.refl ↥(integralClosure (Polynomial C) (BGS.HasseWeil.ExactConstantExtension C N S)))

noncomputable def BGS.HasseWeil.exactConstantExtensionCReciprocalPrimesEquivInfinityPlace (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) : ↑((Ideal.span {Polynomial.X}).primesOver ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S))) ≃ ↑(CorvajaZannier.FiniteExtensionInfinityPlace C (ExactConstantExtension C N S))

Localization at the reciprocal origin identifies affine primes with the actual places of the exact constant extension above C-infinity.

Equations

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

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

The reciprocal origin is the unique prime of S[X] above the reciprocal origin of C[X].

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedToCReciprocalNormalizationHeightOneEquiv (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] [IsGalois C S] : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N)) ≃ IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S))

The reciprocal normalization equivalence transports height-one primes.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionPresentedToCReciprocalNormalizationHeightOneEquiv_under (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] [IsGalois C S] (q : IsDedekindDomain.HeightOneSpectrum (TensorProduct C S ↥(integralClosure (Polynomial C) N))) : Ideal.under (Polynomial C) ((exactConstantExtensionPresentedToCReciprocalNormalizationHeightOneEquiv C S N) q).asIdeal = Ideal.under (Polynomial C) q.asIdeal

The reciprocal normalization equivalence preserves contraction to C[X].

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedInfinityHeightOneEquiv (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] [IsGalois C S] : ExactConstantExtensionPresentedInfinityPlace C S N ≃ { q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)) // Ideal.under (Polynomial C) q.asIdeal = Ideal.span {Polynomial.X} }

Presented infinity places correspond to height-one primes above the reciprocal origin.

Equations

• BGS.HasseWeil.exactConstantExtensionPresentedInfinityHeightOneEquiv C S N = (BGS.HasseWeil.exactConstantExtensionPresentedToCReciprocalNormalizationHeightOneEquiv C S N).subtypeEquiv ⋯

noncomputable def BGS.HasseWeil.exactConstantExtensionCReciprocalHeightOneEquivPrimesOver (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 ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)) // Ideal.under (Polynomial C) q.asIdeal = Ideal.span {Polynomial.X} } ≃ ↑((Ideal.span {Polynomial.X}).primesOver ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)))

Height-one primes above the reciprocal origin identify with its prime fiber.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlaceEquivCReciprocalPrimes (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] [IsGalois C S] : ExactConstantExtensionPresentedInfinityPlace C S N ≃ ↑((Ideal.span {Polynomial.X}).primesOver ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)))

Presented infinity places, before changing the transported reciprocal action to the actual one, are precisely the affine primes above (X).

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionCReciprocalPrimesEquivActual (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : ↑((Ideal.span {Polynomial.X}).primesOver ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S))) ≃ ↑((Ideal.span {Polynomial.X}).primesOver ↥(integralClosure (Polynomial C) (ExactConstantExtension C N S)))

The prime fiber over the reciprocal origin is preserved by identifying the two polynomial actions.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlaceEquiv (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [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 = ⊥) : ExactConstantExtensionPresentedInfinityPlace C S N ≃ ↑(CorvajaZannier.FiniteExtensionInfinityPlace C (ExactConstantExtension C N S))

The reciprocal-normalization presentation of infinity places is exactly the actual infinity-place type of the exact constant extension over C.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlaceEquiv_under (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 : ExactConstantExtensionPresentedInfinityPlace C S N) : infinityPlaceUnder C N (ExactConstantExtension C N S) ((exactConstantExtensionPresentedInfinityPlaceEquiv C S N hExact) q) = exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯

The reciprocal presentation equivalence respects restriction to the original function field.

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedInfinityResidueFieldRingEquiv (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 : ExactConstantExtensionPresentedInfinityPlace C S N) : (↑q).asIdeal.ResidueField ≃+* (↑((exactConstantExtensionPresentedInfinityPlaceEquiv C S N hExact) q)).ResidueField

The residue field of a presented reciprocal prime is the residue field of the corresponding actual C-infinity place.

Equations

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

@[reducible]

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

The rational function algebra over the reciprocal polynomial ring at infinity.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncAlgebra C = (SubringClass.subtype (RatFunc.inftyValuation C).integer).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncSMul (C : Type u_1) [Field C] [DecidableEq (RatFunc C)] : SMul (↥(CorvajaZannier.RatFuncInfinityIntegers C)) (RatFunc C)

The scalar action of (RatFuncInfinityIntegers C) on (RatFunc C) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncSMul C = (BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncAlgebra C).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncModule (C : Type u_1) [Field C] [DecidableEq (RatFunc C)] : Module (↥(CorvajaZannier.RatFuncInfinityIntegers C)) (RatFunc C)

The module structure of (RatFunc C) over (RatFuncInfinityIntegers C) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseRatFuncModule C = Algebra.toModule

@[reducible]

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

The extension-field algebra over the reciprocal polynomial ring at infinity.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseNAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers C)) (RatFunc C))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingInfinityBaseNSMul (C : Type u_1) (N : Type u_3) [Field C] [Field N] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] : SMul (↥(CorvajaZannier.RatFuncInfinityIntegers C)) N

The scalar action of (RatFuncInfinityIntegers C) on N used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseNSMul C N = (BGS.HasseWeil.infinitySplittingInfinityBaseNAlgebra C N).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.infinitySplittingInfinityBaseNModule (C : Type u_1) (N : Type u_3) [Field C] [Field N] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] : Module (↥(CorvajaZannier.RatFuncInfinityIntegers C)) N

The module structure of N over (RatFuncInfinityIntegers C) used in the constant extension infinity place splitting multiplicity construction.

Equations

• BGS.HasseWeil.infinitySplittingInfinityBaseNModule C N = Algebra.toModule

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

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_action_on_infinityNormalization (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : ExactConstantExtension C N S ≃ₐ[N] ExactConstantExtension C N S) (s : S) : g • (algebraMap S ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C (ExactConstantExtension C N S))) s = (algebraMap S ↥(CorvajaZannier.RatFuncInfinityIntegralClosure C (ExactConstantExtension C N S))) (((exactConstantExtensionConstantQuotient C N N S hExact) g) s)

Galois action on the infinity normalization restricts to the expected constant-field quotient action.

theorem BGS.HasseWeil.exactConstantExtensionInfinityPlace_ramificationIdx_eq_one (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [DecidableEq (RatFunc C)] [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 : ↑(CorvajaZannier.FiniteExtensionInfinityPlace C (ExactConstantExtension C N S))) : infinityPlaceRelativeRamificationIdx C N (ExactConstantExtension C N S) Q = 1

Every infinity place is unramified in an exact extension of constants.