Transporting function-field places across algebra equivalences

An equivalence of finite extensions over K(X) identifies both normalization charts. This file packages the induced equivalences of finite, infinity, and exhaustive places and records preservation of absolute place degree. In particular, rational-place counts depend only on the K(X)-algebra up to equivalence, not on its chosen field presentation.

def BGS.HasseWeil.heightOneSpectrumFiberEquivPrimesOver (R : Type u_1) (A : Type u_2) [CommRing R] [IsDomain R] [CommRing A] [IsDomain A] [Algebra R A] [Algebra.IsIntegral R A] [Module.IsTorsionFree R A] (p : IsDedekindDomain.HeightOneSpectrum R) : { q : IsDedekindDomain.HeightOneSpectrum A // IsDedekindDomain.HeightOneSpectrum.under R q = p } ≃ ↑(p.asIdeal.primesOver A)

A height-one prime restriction fiber is the usual type of primes above the base prime.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivPolynomialAlgebraLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the finite extension place alg equiv construction.

Equations

• BGS.HasseWeil.finiteAlgEquivPolynomialAlgebraLeft K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivPolynomialAlgebraRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] : Algebra (Polynomial K) M

The algebra structure from K[X] to M used in the finite extension place alg equiv construction.

Equations

• BGS.HasseWeil.finiteAlgEquivPolynomialAlgebraRight K M = ((algebraMap (RatFunc K) M).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.finiteAlgEquivPolynomialTowerLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.HasseWeil.finiteAlgEquivPolynomialTowerRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] : IsScalarTower (Polynomial K) (RatFunc K) M

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivInfinityAlgebraLeft (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] : Algebra (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

The algebra structure from (RatFuncInfinityIntegers K) to L used in the finite extension place alg equiv construction.

Equations

• BGS.HasseWeil.finiteAlgEquivInfinityAlgebraLeft K L = ((algebraMap (RatFunc K) L).comp (algebraMap (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivInfinityAlgebraRight (K : Type u_1) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field M] [Algebra (RatFunc K) M] : Algebra (↥(CorvajaZannier.RatFuncInfinityIntegers K)) M

The algebra structure from (RatFuncInfinityIntegers K) to M used in the finite extension place alg equiv construction.

Equations

• BGS.HasseWeil.finiteAlgEquivInfinityAlgebraRight K M = ((algebraMap (RatFunc K) M).comp (algebraMap (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.finiteAlgEquivInfinityTowerLeft (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] : IsScalarTower (↥(CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K) L

theorem BGS.HasseWeil.finiteAlgEquivInfinityTowerRight (K : Type u_1) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field M] [Algebra (RatFunc K) M] : IsScalarTower (↥(CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K) M

@[instance_reducible]

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

The algebra structure from K to (RatFuncInfinityIntegers K) used in the finite extension place alg equiv construction.

Equations

• BGS.HasseWeil.finiteAlgEquivInfinityConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.HasseWeil.finiteAlgEquivInfinityConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : IsScalarTower K (↥(CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K)

theorem BGS.HasseWeil.finiteAlgEquivPolynomialTorsionFreeLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.finiteAlgEquivPolynomialTorsionFreeRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : Module.IsTorsionFree (Polynomial K) M

theorem BGS.HasseWeil.finiteAlgEquivFiniteClosureTorsionFreeLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteAlgEquivFiniteClosureTorsionFreeRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

theorem BGS.HasseWeil.finiteAlgEquivInfinityClosureTorsionFreeLeft (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.finiteAlgEquivInfinityClosureTorsionFreeRight (K : Type u_1) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field M] [Algebra (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivFiniteClosureConstantAlgebraLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the finite extension place alg equiv construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivFiniteClosureConstantAlgebraRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

The algebra structure from K to (RatFuncFiniteIntegralClosure K M) used in the finite extension place alg equiv construction.

Equations

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

theorem BGS.HasseWeil.finiteAlgEquivFiniteClosureConstantTowerLeft (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteAlgEquivFiniteClosureConstantTowerRight (K : Type u_1) (M : Type u_3) [Field K] [Field M] [Algebra (RatFunc K) M] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivInfinityClosureConstantAlgebraLeft (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the finite extension place alg equiv construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAlgEquivInfinityClosureConstantAlgebraRight (K : Type u_1) (M : Type u_3) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Algebra (RatFunc K) M] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

The algebra structure from K to (RatFuncInfinityIntegralClosure K M) used in the finite extension place alg equiv construction.

Equations

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

theorem BGS.HasseWeil.finiteAlgEquivInfinityClosureConstantTowerLeft (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.finiteAlgEquivInfinityClosureConstantTowerRight (K : Type u_1) (M : Type u_3) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Algebra (RatFunc K) M] : IsScalarTower K ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

noncomputable def BGS.HasseWeil.ratFuncFiniteIntegralClosureAlgEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L) ≃ₐ[Polynomial K] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

A K(X)-algebra equivalence restricts to the finite normalization charts.

Equations

• BGS.HasseWeil.ratFuncFiniteIntegralClosureAlgEquivOfAlgEquiv K L M e = (AlgEquiv.restrictScalars (Polynomial K) e).mapIntegralClosure

noncomputable def BGS.HasseWeil.ratFuncInfinityIntegralClosureAlgEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L) ≃ₐ[↥(CorvajaZannier.RatFuncInfinityIntegers K)] ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

A K(X)-algebra equivalence restricts to the infinity normalization charts.

Equations

• BGS.HasseWeil.ratFuncInfinityIntegralClosureAlgEquivOfAlgEquiv K L M e = id (AlgEquiv.restrictScalars (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) e).mapIntegralClosure

noncomputable def BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : CorvajaZannier.FiniteExtensionFinitePlace K L ≃ CorvajaZannier.FiniteExtensionFinitePlace K M

Finite places are invariant under an equivalence of the ambient K(X)-algebras.

Equations

• BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfAlgEquiv K L M e = BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv (BGS.HasseWeil.ratFuncFiniteIntegralClosureAlgEquivOfAlgEquiv K L M e)

noncomputable def BGS.HasseWeil.finiteExtensionFinitePlaceResidueFieldAlgEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : Q.asIdeal.ResidueField ≃ₐ[K] ((finiteExtensionFinitePlaceEquivOfAlgEquiv K L M e) Q).asIdeal.ResidueField

The residue fields of corresponding finite places are equivalent over the constant field.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionInfinityPlaceEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L) ≃ ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)

Infinity places are invariant under an equivalence of the ambient K(X)-algebras.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionPlaceEquivOfAlgEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : CorvajaZannier.FiniteExtensionPlace K L ≃ CorvajaZannier.FiniteExtensionPlace K M

Exhaustive places are invariant under an equivalence of the ambient K(X)-algebras.

Equations

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

theorem BGS.HasseWeil.finiteExtensionFinitePlace_degree_eq_residue_finrank (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = Module.finrank K Q.asIdeal.ResidueField

The absolute degree of a finite place is the dimension of its residue field over the constant field.

theorem BGS.HasseWeil.finiteExtensionInfinityPlace_degree_eq_residue_finrank (K : Type u_1) (L : Type u_2) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field L] [Algebra (RatFunc K) L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P) = Module.finrank K (↑P).ResidueField

The absolute degree of an infinity place is the dimension of its residue field over the constant field.

@[simp]

theorem BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfAlgEquiv_degree (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) (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K M (Sum.inl ((finiteExtensionFinitePlaceEquivOfAlgEquiv K L M e) Q)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q)

Corresponding finite places have the same absolute degree.

@[simp]

theorem BGS.HasseWeil.finiteExtensionInfinityPlaceEquivOfAlgEquiv_asIdeal (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [DecidableEq (RatFunc K)] [Field L] [Field M] [Algebra (RatFunc K) L] [Algebra (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ↑((finiteExtensionInfinityPlaceEquivOfAlgEquiv K L M e) P) = Ideal.comap (ratFuncInfinityIntegralClosureAlgEquivOfAlgEquiv K L M e).symm ↑P

noncomputable def BGS.HasseWeil.finiteExtensionInfinityPlaceResidueFieldAlgEquivOfAlgEquiv (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] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (↑P).ResidueField ≃ₐ[K] (↑((finiteExtensionInfinityPlaceEquivOfAlgEquiv K L M e) P)).ResidueField

The residue fields of corresponding infinity places are equivalent over the constant field.

Equations

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

@[simp]

theorem BGS.HasseWeil.finiteExtensionInfinityPlaceEquivOfAlgEquiv_degree (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] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : CorvajaZannier.finiteExtensionPlaceDegree K M (Sum.inr ((finiteExtensionInfinityPlaceEquivOfAlgEquiv K L M e) P)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P)

Corresponding infinity places have the same absolute degree.

@[simp]

theorem BGS.HasseWeil.finiteExtensionPlaceEquivOfAlgEquiv_degree (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) (P : CorvajaZannier.FiniteExtensionPlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K M ((finiteExtensionPlaceEquivOfAlgEquiv K L M e) P) = CorvajaZannier.finiteExtensionPlaceDegree K L P

The exhaustive place equivalence preserves absolute degree.

noncomputable def BGS.HasseWeil.finiteExtensionRationalFinitePlaceEquivOfAlgEquiv (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) : FiniteExtensionRationalFinitePlace K L ≃ FiniteExtensionRationalFinitePlace K M

Degree-one finite places are invariant under a K(X)-algebra equivalence.

Equations

• BGS.HasseWeil.finiteExtensionRationalFinitePlaceEquivOfAlgEquiv K L M e = (BGS.HasseWeil.finiteExtensionFinitePlaceEquivOfAlgEquiv K L M e).subtypeEquiv ⋯

noncomputable def BGS.HasseWeil.finiteExtensionRationalInfinityPlaceEquivOfAlgEquiv (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] [Algebra.IsSeparable (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) M] (e : L ≃ₐ[RatFunc K] M) : FiniteExtensionRationalInfinityPlace K L ≃ FiniteExtensionRationalInfinityPlace K M

Degree-one infinity places are invariant under a K(X)-algebra equivalence.

Equations

• BGS.HasseWeil.finiteExtensionRationalInfinityPlaceEquivOfAlgEquiv K L M e = (BGS.HasseWeil.finiteExtensionInfinityPlaceEquivOfAlgEquiv K L M e).subtypeEquiv ⋯

noncomputable def BGS.HasseWeil.finiteExtensionRationalPlaceEquivOfAlgEquiv (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) : FiniteExtensionRationalPlace K L ≃ FiniteExtensionRationalPlace K M

Complete degree-one place types are invariant under a K(X)-algebra equivalence.

Equations

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

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_eq_of_algEquiv (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) : finiteExtensionRationalPlaceCount K L = finiteExtensionRationalPlaceCount K M

Complete rational-place counts are invariant under an equivalence of finite K(X)-algebras.