Closed-place counts across function-field equivalences

The closed-place extension-count sequence is a weighted sum depending only on absolute place degrees. Hence the degree-preserving place equivalence induced by a K(X)-algebra equivalence preserves the entire sequence.

noncomputable def BGS.HasseWeil.finiteExtensionPlaceDegreeLEEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) L] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (r : ℕ) : { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ r } ≃ { P : CorvajaZannier.FiniteExtensionPlace K M // CorvajaZannier.finiteExtensionPlaceDegree K M P ≤ r }

Places of degree at most r are preserved by a function-field equivalence.

Equations

• BGS.HasseWeil.finiteExtensionPlaceDegreeLEEquivOfAlgEquiv K L M e r = (BGS.HasseWeil.finiteExtensionPlaceEquivOfAlgEquiv K L M e).subtypeEquiv ⋯

noncomputable def BGS.HasseWeil.finiteExtensionPlaceDegreeDvdEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) L] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (r : ℕ) : { P : { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ r } // CorvajaZannier.finiteExtensionPlaceDegree K L ↑P ∣ r } ≃ { P : { P : CorvajaZannier.FiniteExtensionPlace K M // CorvajaZannier.finiteExtensionPlaceDegree K M P ≤ r } // CorvajaZannier.finiteExtensionPlaceDegree K M ↑P ∣ r }

Within a bounded family, the places whose degrees divide r are also preserved.

Equations

• BGS.HasseWeil.finiteExtensionPlaceDegreeDvdEquivOfAlgEquiv K L M e r = (BGS.HasseWeil.finiteExtensionPlaceDegreeLEEquivOfAlgEquiv K L M e r).subtypeEquiv ⋯

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_eq_of_algEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) L] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (r : ℕ) : finiteExtensionClosedPlaceExtensionCount K L r = finiteExtensionClosedPlaceExtensionCount K M r

Every closed-place extension count is invariant under an equivalence of finite K(X)-algebras.