Absolute degrees of constant-extension places at infinity

This file compares the degree of an infinity place in the original constant field presentation with its degree after extending the constants. Both degrees are computed from the same reciprocal-normalization residue field, so the comparison is just the residue-field dimension tower.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityDegreeTowerDecidableEqBase C = BGS.HasseWeil.infinityBridgeDecidableEqConstants C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityDegreeTowerDecidableEqRatFuncBase C = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityDegreeTowerDecidableEqConstants S = BGS.HasseWeil.infinityBridgeDecidableEqConstants S

@[instance_reducible]

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

Classical equality on rational functions over the extended constants for the infinity-place tower.

Equations

• BGS.HasseWeil.infinityDegreeTowerDecidableEqRatFuncConstants S = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants S

@[reducible]

noncomputable def BGS.HasseWeil.infinityDegreeTowerBaseConstantAlgebra (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 base rational function field in the infinity-place tower.

Equations

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

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

theorem BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlace_degree_baseChange (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) : CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inr ((exactConstantExtensionPresentedInfinityPlaceEquiv C S N hExact) q)) = Module.finrank C S * CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (Sum.inr (exactConstantExtensionUpstairsInfinityPlace C S N hExact ↑q ⋯))

The degree over the original constants of a presented infinity place is the constant-field degree times the degree of its upstairs S-place.

theorem BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlace_relativeInertiaDeg_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 : ExactConstantExtensionPresentedInfinityPlace C S N) : infinityPlaceRelativeInertiaDeg C N (ExactConstantExtension C N S) ((exactConstantExtensionPresentedInfinityPlaceEquiv C S N hExact) q) = Module.finrank C S / (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr (exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯)))

The relative residue degree over the original function field is the constant extension degree divided by the same gcd that controls splitting.

theorem BGS.HasseWeil.exactConstantExtensionInfinityPlace_fiber_card_eq_gcd (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 : ExactConstantExtensionPresentedInfinityPlace C S N) : Fintype.card (InfinityPlaceUnderFiber C N (ExactConstantExtension C N S) (exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯)) = (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (Sum.inr (exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯)))

A downstairs infinity place of degree d has exactly gcd([S : C], d) places above it in an exact extension of constants.

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedInfinityPlaceFiberEquiv (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.FiniteExtensionInfinityPlace C N)) : { q : ExactConstantExtensionPresentedInfinityPlace C S N // exactConstantExtensionDownstairsInfinityPlace C S N ↑q ⋯ = P } ≃ InfinityPlaceUnderFiber C N (ExactConstantExtension C N S) P

Restricting the global reciprocal presentation equivalence to a fixed downstairs infinity place identifies the presented contraction fiber with the entire actual place-restriction fiber.

Equations

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

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

The presented reciprocal infinity fiber itself has the standard gcd cardinality. This is the presentation-level exhaustiveness form of the constant-extension splitting law at infinity.