Closed places and rational places after extension of constants

For an exact extension of constants S / C, the existing finite and infinity normalization bridges both prove the residue-degree formula

deg_S(Q) = deg_C(P) / gcd([S : C], deg_C(P)).

This file combines the two branches into one presented-place type and proves that an upstairs presented place is rational exactly when its downstairs degree divides [S : C]. Thus it identifies, place by place, the support of the closed-place extension coefficient with rationality after constant extension.

The global cardinality identity needs one further splitting theorem: the fiber over a downstairs place of degree d must have cardinality gcd([S : C], d). That multiplicity is not supplied by the current finite/infinity bridge APIs, so no global count equality is asserted here.

theorem BGS.HasseWeil.div_gcd_eq_one_iff_dvd (r d : ℕ) (hd : 0 < d) : d / r.gcd d = 1 ↔ d ∣ r

Elementary arithmetic behind rationality after extension of constants.

theorem BGS.HasseWeil.div_gcd_dvd_iff_dvd_mul (extensionDegree placeDegree level : ℕ) (hextension : 0 < extensionDegree) : placeDegree / extensionDegree.gcd placeDegree ∣ level ↔ placeDegree ∣ extensionDegree * level

The degree after extending constants divides an extension level exactly when the original closed-place degree divides the multiplied level.

theorem BGS.HasseWeil.sum_degree_eq_sum_degree_of_div_gcd_and_fiber_card {Base : Type u_1} {Up : Type u_2} [Fintype Base] [Fintype Up] (down : Up → Base) (baseDegree : Base → ℕ) (upDegree : Up → ℕ) (extensionDegree : ℕ) (hdegree : ∀ (Q : Up), upDegree Q = baseDegree (down Q) / extensionDegree.gcd (baseDegree (down Q))) (hfiber : ∀ (P : Base), Nat.card { Q : Up // down Q = P } = extensionDegree.gcd (baseDegree P)) : ∑ Q : Up, upDegree Q = ∑ P : Base, baseDegree P

Abstract finite-fiber form of the constant-extension contribution identity. If every object above P has degree deg(P) / gcd(r, deg(P)) and there are exactly gcd(r, deg(P)) such objects, then the total degrees in the two finite families agree.

theorem BGS.HasseWeil.sum_degree_dvd_eq_sum_degree_dvd_of_div_gcd_fibers {Base : Type u_1} {Up : Type u_2} (down : Up → Base) (baseDegree : Base → ℕ) (upDegree : Up → ℕ) (extensionDegree level : ℕ) (hextension : 0 < extensionDegree) (hlevel : 0 < level) [Fintype { P : Base // baseDegree P ≤ extensionDegree * level }] [Fintype { Q : Up // upDegree Q ≤ level }] (hdegree : ∀ (Q : Up), upDegree Q = baseDegree (down Q) / extensionDegree.gcd (baseDegree (down Q))) (hfiber : ∀ (P : Base), Nat.card { Q : Up // down Q = P } = extensionDegree.gcd (baseDegree P)) : ∑ Q : { Q : { Q : Up // upDegree Q ≤ level } // upDegree ↑Q ∣ level }, upDegree ↑↑Q = ∑ P : { P : { P : Base // baseDegree P ≤ extensionDegree * level } // baseDegree ↑P ∣ extensionDegree * level }, baseDegree ↑↑P

Bounded divisor-support form of the preceding fiber identity. It is the exact combinatorial interface used by closed-place extension counts: the map between all places need not have finite domain, because the two degree-bounded families are supplied as finite types.

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.closedPlaceRatFuncBaseDecidableEq C = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants C

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.closedPlaceRatFuncConstantsDecidableEq S = BGS.HasseWeil.infinityBridgeDecidableEqRatFuncConstants S

@[instance_reducible]

noncomputable def BGS.HasseWeil.closedPlaceBaseConstantAlgebra (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 count construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.closedPlaceTargetPolynomialAlgebra (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 count construction.

Equations

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

@[reducible, inline]

abbrev BGS.HasseWeil.ExactConstantExtensionPresentedInfinityPlace (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] : Type (max 0 u_2 u_3)

Reciprocal-affine primes used to present places above infinity. The local algebra structure sends the polynomial variable to X⁻¹, exactly as in ConstantExtensionInfinityPlaceBridge.

Equations

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

@[reducible, inline]

abbrev BGS.HasseWeil.ExactConstantExtensionPresentedPlace (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] : Type (max (max u_2 u_3) u_3 u_2)

A common presentation of finite and infinity places in the explicit normalizations used by the two constant-extension bridge files.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedUpstairsPlace (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 : ExactConstantExtensionPresentedPlace C S N) : CorvajaZannier.FiniteExtensionPlace S (ExactConstantExtension C N S)

The actual upstairs exhaustive place represented by a finite or reciprocal-infinity normalization prime.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionPresentedDownstairsPlace (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 : ExactConstantExtensionPresentedPlace C S N) : CorvajaZannier.FiniteExtensionPlace C N

The actual downstairs exhaustive place obtained by contraction.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionPresentedPlace_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] [DecidableEq C] [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) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (exactConstantExtensionPresentedUpstairsPlace C S N hExact q) = CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) / (Module.finrank C S).gcd (CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q))

The finite and infinity residue-degree formulas combine into one formula on presented exhaustive places.

theorem BGS.HasseWeil.exactConstantExtensionPresentedPlace_degree_eq_one_iff_dvd (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 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) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (exactConstantExtensionPresentedUpstairsPlace C S N hExact q) = 1 ↔ CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) ∣ Module.finrank C S

A presented upstairs place is rational over S exactly when its downstairs degree divides the constant-extension degree.

def BGS.HasseWeil.exactConstantExtensionPresentedRationalPlaceEquivDegreeDvd (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 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 // CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (exactConstantExtensionPresentedUpstairsPlace C S N hExact q) = 1 } ≃ { q : ExactConstantExtensionPresentedPlace C S N // CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) ∣ Module.finrank C S }

Presented rational places are the same subtype as presented places whose downstairs degree contributes to the closed-place extension coefficient.

Equations

• BGS.HasseWeil.exactConstantExtensionPresentedRationalPlaceEquivDegreeDvd C S N hExact = Equiv.subtypeEquivRight ⋯

theorem BGS.HasseWeil.exactConstantExtensionPresentedPlace_closedContribution_eq (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 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) : (if CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (exactConstantExtensionPresentedUpstairsPlace C S N hExact q) = 1 then CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) else 0) = if CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) ∣ Module.finrank C S then CorvajaZannier.finiteExtensionPlaceDegree C N (exactConstantExtensionPresentedDownstairsPlace C S N hExact q) else 0

Pointwise equality between the closed-place contribution and the rational-presented-place indicator.

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_eq_degreeDvdSum (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Fintype C] [DecidableEq C] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (r : ℕ) : finiteExtensionClosedPlaceExtensionCount C N r = ∑ P : { P : CorvajaZannier.FiniteExtensionPlace C N // CorvajaZannier.finiteExtensionPlaceDegree C N P ≤ r }, if CorvajaZannier.finiteExtensionPlaceDegree C N ↑P ∣ r then CorvajaZannier.finiteExtensionPlaceDegree C N ↑P else 0

Public unfolding of the closed-place extension coefficient.