Closed-place splitting formula for an exact extension of constants

This file supplies the exhaustive presentation equivalences needed to sum the local constant-extension splitting laws over all closed places.

The finite branch is recorded first, then the reciprocal-infinity branch is transported to actual places. Their exact sum-branch fiber equivalence gives the global gcd splitting law and the closed-place degree-extension identity.

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingFormulaBaseConstantAlgebra (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 closed place splitting formula construction.

Equations

• BGS.HasseWeil.splittingFormulaBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.splittingFormulaBaseConstantTower (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.splittingFormulaTargetPolynomialAlgebra (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 algebra structure from S[X] to (ExactConstantExtension C N S) used in the constant extension closed place splitting formula construction.

Equations

• BGS.HasseWeil.splittingFormulaTargetPolynomialAlgebra C S N = BGS.HasseWeil.bridgeTargetPolynomialAlgebra C S N

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedUpstairsFinitePlaceEquiv (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 = ⊥) : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S)) ≃ CorvajaZannier.FiniteExtensionFinitePlace S (ExactConstantExtension C N S)

The explicit S[X]-normalization presentation exhausts the actual finite places over the enlarged rational function field S(X).

The first equivalence presents the same primes as places over C(X); the second is the finite-normalization base-change equivalence from C to S.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionPresentedUpstairsFinitePlaceEquiv_apply (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 ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) : (exactConstantExtensionPresentedUpstairsFinitePlaceEquiv C S N hExact) q = exactConstantExtensionUpstairsFinitePlace C S N hExact q

The exhaustive finite-place equivalence is definitionally the existing upstairs finite-place construction on presented primes.

theorem BGS.HasseWeil.exactConstantExtensionPresentedFinitePlaceFiber_natCard_eq_gcd_of_downstairs (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 = ⊥) (P : CorvajaZannier.FiniteExtensionFinitePlace C N) : Nat.card { q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S)) // exactConstantExtensionDownstairsFinitePlace C S N hExact q = P } = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inl P))

Every downstairs finite place has the standard gcd number of presented finite places above it. Unlike the selected-prime form of the splitting theorem, this statement is indexed by an arbitrary downstairs place and is therefore ready for fiberwise summation.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.splittingFormulaBaseRatFuncDecidableEq C = BGS.HasseWeil.closedPlaceRatFuncBaseDecidableEq C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.splittingFormulaTargetRatFuncDecidableEq S = BGS.HasseWeil.closedPlaceRatFuncConstantsDecidableEq S

@[instance_reducible]

noncomputable def BGS.HasseWeil.splittingFormulaInfinityBaseConstantAlgebra (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 closed place splitting formula construction.

Equations

• BGS.HasseWeil.splittingFormulaInfinityBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.splittingFormulaInfinityBaseConstantTower (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.splittingFormulaBaseReciprocalPolynomialAlgebra (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 closed place splitting formula construction.

Equations

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

theorem BGS.HasseWeil.splittingFormulaBaseReciprocalConstantTower (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.splittingFormulaOldNormalizationConstantAlgebra (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 closed place splitting formula construction.

Equations

• BGS.HasseWeil.splittingFormulaOldNormalizationConstantAlgebra C N = BGS.HasseWeil.infinityBridgeOldNormalizationConstantAlgebra C N

theorem BGS.HasseWeil.splittingFormulaOldNormalizationConstantTower (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.splittingFormulaTensorReciprocalPolynomialAlgebra (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 closed place splitting formula construction.

Equations

• BGS.HasseWeil.splittingFormulaTensorReciprocalPolynomialAlgebra C S N = BGS.HasseWeil.infinityBridgeTensorPolynomialAlgebra C S N

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

The reciprocal-normalization presentation exhausts the actual infinity places of the exact constant extension over the enlarged constant field S. The equivalence first transports the reciprocal affine prime to the S[X]-normalization, then localizes at the reciprocal origin.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionPresentedUpstairsInfinityPlaceEquiv_apply (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq 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) : (exactConstantExtensionPresentedUpstairsInfinityPlaceEquiv C S N hExact) q = exactConstantExtensionUpstairsInfinityPlace C S N hExact ↑q ⋯

On a reciprocal affine prime, the exhaustive equivalence is exactly the existing upstairs infinity-place construction.

theorem BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlaceFiber_natCard_eq_gcd_of_downstairs (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] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace C N)) : Nat.card { q : ExactConstantExtensionPresentedInfinityPlace C S N // exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯ = P } = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr P))

Every downstairs infinity place has the standard gcd number of presented reciprocal-normalization places above it. This removes the selected-prime index from the infinity splitting theorem and makes it ready for global fiberwise summation.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.globalPresentationBaseRatFuncDecidableEq C = BGS.HasseWeil.closedPlaceRatFuncBaseDecidableEq C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.globalPresentationTargetRatFuncDecidableEq S = BGS.HasseWeil.closedPlaceRatFuncConstantsDecidableEq S

@[instance_reducible]

noncomputable def BGS.HasseWeil.globalPresentationBaseConstantAlgebra (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 closed place splitting formula construction.

Equations

• BGS.HasseWeil.globalPresentationBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.globalPresentationBaseConstantTower (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.globalPresentationTargetPolynomialAlgebra (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 algebra structure from S[X] to (ExactConstantExtension C N S) used in the constant extension closed place splitting formula construction.

Equations

• BGS.HasseWeil.globalPresentationTargetPolynomialAlgebra C S N = BGS.HasseWeil.bridgeTargetPolynomialAlgebra C S N

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

The finite-normalization and reciprocal-normalization presentations together exhaust all actual closed places of the exact constant extension over S.

Equations

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

@[simp]

theorem BGS.HasseWeil.exactConstantExtensionPresentedUpstairsPlaceEquiv_apply (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq 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 : ExactConstantExtensionPresentedPlace C S N) : (exactConstantExtensionPresentedUpstairsPlaceEquiv C S N hExact) q = exactConstantExtensionPresentedUpstairsPlace C S N hExact q

The global exhaustive equivalence agrees branchwise with the existing presented-upstairs-place construction.

theorem BGS.HasseWeil.exactConstantExtensionPresentedPlaceFiber_natCard_eq_gcd_of_downstairs (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 = ⊥) (P : CorvajaZannier.FiniteExtensionPlace C N) : Nat.card { q : ExactConstantExtensionPresentedPlace C S N // exactConstantExtensionPresentedDownstairsPlace C S N hExact q = P } = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N P)

The contraction fiber of the combined finite-plus-infinity presentation over an arbitrary downstairs closed place has the standard gcd cardinality. The proof is an exact branchwise fiber equivalence, so finite and infinity places cannot be mixed by the presentation map.

theorem BGS.HasseWeil.exactConstantExtensionClosedPlaceExtensionCount_eq (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 = ⊥) (level : ℕ) : finiteExtensionClosedPlaceExtensionCount S (ExactConstantExtension C N S) level = finiteExtensionClosedPlaceExtensionCount C N (Module.finrank C S * level)

Exact closed-place count identity for an extension of constants. At level n, the exhaustive closed-place count over S is the original count at level [S : C] * n. The proof transfers the bounded upstairs family through the exhaustive presentation equivalence and sums the degree and gcd fiber formulas.