Restriction of function-field places in a finite tower

Stichtenoth's fixed-field proof of the Hasse--Weil lower bound compares rational places in several intermediate fields of one Galois tower. This file starts that tower API for the repository's exhaustive place type. It restricts both finite places and places above infinity by contracting the corresponding height-one prime through the integral closures.

The construction is intrinsic to the field tower. It assumes no point-count bound, zeta theorem, or Hasse--Weil statement.

@[instance_reducible]

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

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

Equations

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

@[instance_reducible]

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

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

Equations

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

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

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

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

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

The field inclusion maps the finite integral closure in an intermediate field into the finite integral closure in the top field.

Equations

• BGS.HasseWeil.finiteIntegralClosureMap K M L = (IsScalarTower.toAlgHom (Polynomial K) M L).mapIntegralClosure

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.finitePlaceTowerIntegralClosureAlgebra K M L = (BGS.HasseWeil.finiteIntegralClosureMap K M L).toAlgebra

theorem BGS.HasseWeil.finitePlaceTowerIntermediateIntegral (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

theorem BGS.HasseWeil.finitePlaceTowerIntermediateModuleFinite (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

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

theorem BGS.HasseWeil.finitePlaceTowerIntermediateClosureTorsionFree (K : Type u_1) [Field K] (M : Type u_2) [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.finitePlaceTowerIntermediateDedekind (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)

theorem BGS.HasseWeil.finitePlaceTowerBaseIntegral (K : Type u_1) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finitePlaceTowerTopModuleFinite (K : Type u_1) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

theorem BGS.HasseWeil.finitePlaceTowerTopClosureTorsionFree (K : Type u_1) [Field K] (L : Type u_3) [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.finitePlaceTowerTopDedekind (K : Type u_1) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

theorem BGS.HasseWeil.finitePlaceTowerTopIntegral (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finitePlaceTowerFaithful (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : FaithfulSMul ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finitePlaceTowerRelativeModuleFinite (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Module.Finite ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finitePlaceTowerIntermediateFractionRing (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] : IsFractionRing (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)) M

theorem BGS.HasseWeil.finitePlaceTowerTopFractionRing (K : Type u_1) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) L

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

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

theorem BGS.HasseWeil.finitePlaceTowerRelativeIsIntegralClosure (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : IsIntegralClosure (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)) L

noncomputable def BGS.HasseWeil.finitePlaceUnder (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.FiniteExtensionFinitePlace K M

Restriction of a finite place contracts its height-one prime to the intermediate finite integral closure.

Equations

• BGS.HasseWeil.finitePlaceUnder K M L P = IsDedekindDomain.HeightOneSpectrum.under (↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K M)) P

@[simp]

theorem BGS.HasseWeil.finitePlaceUnder_asIdeal (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : (finitePlaceUnder K M L P).asIdeal = Ideal.under (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M)) P.asIdeal

@[simp]

theorem BGS.HasseWeil.finitePlaceUnder_under (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) (finitePlaceUnder K M L P) = IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) P

Restricting a finite place through the intermediate field preserves the place below it in the rational function field.

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

The field inclusion maps the integral closure of the infinity valuation ring in an intermediate field into the corresponding top integral closure.

Equations

• BGS.HasseWeil.infinityIntegralClosureMap K M L = (IsScalarTower.toAlgHom (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) M L).mapIntegralClosure

@[instance_reducible]

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

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

Equations

• BGS.HasseWeil.infinityPlaceTowerIntegralClosureAlgebra K M L = (BGS.HasseWeil.infinityIntegralClosureMap K M L).toAlgebra

theorem BGS.HasseWeil.infinityPlaceTowerIntermediateIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

theorem BGS.HasseWeil.infinityPlaceTowerIntermediateModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

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

theorem BGS.HasseWeil.infinityPlaceTowerIntermediateDedekind (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)

theorem BGS.HasseWeil.infinityPlaceTowerBaseIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.infinityPlaceTowerTopModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

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

theorem BGS.HasseWeil.infinityPlaceTowerTopDedekind (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

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

theorem BGS.HasseWeil.infinityPlaceTowerTopIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.infinityPlaceTowerFaithful (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : FaithfulSMul ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.infinityPlaceTowerRelativeModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.infinityPlaceTowerIntermediateFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)) M

theorem BGS.HasseWeil.infinityPlaceTowerTopFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) L

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

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

theorem BGS.HasseWeil.infinityPlaceTowerRelativeIsIntegralClosure (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : IsIntegralClosure (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) (↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M)) L

noncomputable def BGS.HasseWeil.infinityPlaceUnder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)

Restriction of a place above infinity contracts its prime to the intermediate integral closure. The tower law for ideals proves that the contracted prime still lies above the distinguished infinity place.

Equations

• BGS.HasseWeil.infinityPlaceUnder K M L P = ⟨Ideal.under ↥(BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↑P, ⋯⟩

@[simp]

theorem BGS.HasseWeil.infinityPlaceUnder_asIdeal (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ↑(infinityPlaceUnder K M L P) = Ideal.under ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↑P

noncomputable def BGS.HasseWeil.placeUnder (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : CorvajaZannier.FiniteExtensionPlace K L → CorvajaZannier.FiniteExtensionPlace K M

Restriction on the exhaustive sum of finite and above-infinity places.

Equations

• BGS.HasseWeil.placeUnder K M L (Sum.inl P) = Sum.inl (BGS.HasseWeil.finitePlaceUnder K M L P)
• BGS.HasseWeil.placeUnder K M L (Sum.inr P) = Sum.inr (BGS.HasseWeil.infinityPlaceUnder K M L P)

@[simp]

theorem BGS.HasseWeil.placeUnder_inl (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : placeUnder K M L (Sum.inl P) = Sum.inl (finitePlaceUnder K M L P)

@[simp]

theorem BGS.HasseWeil.placeUnder_inr (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : placeUnder K M L (Sum.inr P) = Sum.inr (infinityPlaceUnder K M L P)

theorem BGS.HasseWeil.finitePlaceUnder_surjective (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Function.Surjective (finitePlaceUnder K M L)

Every finite place of the intermediate field has a finite place above it in the top field. This is lying-over for the induced integral-closure map.

theorem BGS.HasseWeil.infinityPlaceUnder_surjective (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Function.Surjective (infinityPlaceUnder K M L)

Every place above infinity in the intermediate field has a place above it in the top field.

theorem BGS.HasseWeil.placeUnder_surjective (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Function.Surjective (placeUnder K M L)

Restriction from the top field is surjective on the exhaustive place type.

@[reducible, inline]

abbrev BGS.HasseWeil.FinitePlaceUnderFiber (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : Type u_3

The finite places of the top field above a fixed intermediate finite place.

Equations

• BGS.HasseWeil.FinitePlaceUnderFiber K M L P = { Q : BGS.CorvajaZannier.FiniteExtensionFinitePlace K L // BGS.HasseWeil.finitePlaceUnder K M L Q = P }

noncomputable def BGS.HasseWeil.finitePlaceUnderFiberEquivPrimesOver (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : FinitePlaceUnderFiber K M L P ≃ ↑(P.asIdeal.primesOver ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))

A restriction fiber is the usual finite set of primes lying over the contracted prime ideal.

Equations

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

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finitePlaceUnderFiberFintype (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : Fintype (FinitePlaceUnderFiber K M L P)

Equations

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

@[reducible, inline]

abbrev BGS.HasseWeil.InfinityPlaceUnderFiber (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : Type u_3

The places of the top field above a fixed intermediate place at infinity.

Equations

• BGS.HasseWeil.InfinityPlaceUnderFiber K M L P = { Q : ↑(BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L) // BGS.HasseWeil.infinityPlaceUnder K M L Q = P }

def BGS.HasseWeil.infinityPlaceUnderFiberEquivPrimesOver (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : InfinityPlaceUnderFiber K M L P ≃ ↑((↑P).primesOver ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L))

The restriction fiber above infinity is likewise the finite set of primes over the corresponding intermediate prime.

Equations

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

@[instance_reducible]

noncomputable instance BGS.HasseWeil.infinityPlaceUnderFiberFintype (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : Fintype (InfinityPlaceUnderFiber K M L P)

Equations

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

theorem BGS.HasseWeil.finiteIntegralClosure_relative_finrank_eq_field_finrank (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Module.finrank ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L) = Module.finrank M L

The rank of the relative finite integral-closure extension is the field degree of the top function field over the intermediate field.

theorem BGS.HasseWeil.infinityIntegralClosure_relative_finrank_eq_field_finrank (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] : Module.finrank ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L) = Module.finrank M L

The infinity integral-closure model has the same relative rank, namely the degree of the field extension.

noncomputable def BGS.HasseWeil.finitePlaceRelativeRamificationIdx (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : ℕ

Ramification index of a top finite place over the intermediate finite integral closure.

Equations

• BGS.HasseWeil.finitePlaceRelativeRamificationIdx K M L Q = Q.asIdeal.ramificationIdx ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K M)

noncomputable def BGS.HasseWeil.finitePlaceRelativeInertiaDeg (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : ℕ

Inertia degree of a top finite place over the intermediate finite integral closure.

Equations

• BGS.HasseWeil.finitePlaceRelativeInertiaDeg K M L Q = Q.asIdeal.inertiaDeg ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K M)

theorem BGS.HasseWeil.sum_finitePlaceUnderFiber_ramification_inertia_eq_finrank (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : ∑ Q : FinitePlaceUnderFiber K M L P, finitePlaceRelativeRamificationIdx K M L ↑Q * finitePlaceRelativeInertiaDeg K M L ↑Q = Module.finrank ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The fundamental equality for the finite-place restriction fiber.

theorem BGS.HasseWeil.sum_finitePlaceUnderFiber_ramification_inertia_eq_field_finrank (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : ∑ Q : FinitePlaceUnderFiber K M L P, finitePlaceRelativeRamificationIdx K M L ↑Q * finitePlaceRelativeInertiaDeg K M L ↑Q = Module.finrank M L

Field-degree form of the finite-place fundamental equality.

noncomputable def BGS.HasseWeil.infinityPlaceRelativeRamificationIdx (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ℕ

Ramification index of a top place above infinity over the intermediate infinity integral closure.

Equations

• BGS.HasseWeil.infinityPlaceRelativeRamificationIdx K M L Q = (↑Q).ramificationIdx ↥(BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K M)

noncomputable def BGS.HasseWeil.infinityPlaceRelativeInertiaDeg (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ℕ

Inertia degree of a top place above infinity over the intermediate infinity integral closure.

Equations

• BGS.HasseWeil.infinityPlaceRelativeInertiaDeg K M L Q = (↑Q).inertiaDeg ↥(BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K M)

theorem BGS.HasseWeil.sum_infinityPlaceUnderFiber_ramification_inertia_eq_finrank (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : ∑ Q : InfinityPlaceUnderFiber K M L P, infinityPlaceRelativeRamificationIdx K M L ↑Q * infinityPlaceRelativeInertiaDeg K M L ↑Q = Module.finrank ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The fundamental equality for the restriction fiber above infinity.

theorem BGS.HasseWeil.sum_infinityPlaceUnderFiber_ramification_inertia_eq_field_finrank (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : ∑ Q : InfinityPlaceUnderFiber K M L P, infinityPlaceRelativeRamificationIdx K M L ↑Q * infinityPlaceRelativeInertiaDeg K M L ↑Q = Module.finrank M L

Field-degree form of the fundamental equality above infinity.

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_inl_eq_mul_relativeInertiaDeg (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = CorvajaZannier.finiteExtensionPlaceDegree K M (Sum.inl (finitePlaceUnder K M L Q)) * finitePlaceRelativeInertiaDeg K M L Q

Place degree is multiplicative when a finite place is restricted through an intermediate function field. The second factor is the residue-field degree in the relative extension.

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_inr_eq_mul_relativeInertiaDeg (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr Q) = CorvajaZannier.finiteExtensionPlaceDegree K M (Sum.inr (infinityPlaceUnder K M L Q)) * infinityPlaceRelativeInertiaDeg K M L Q

The analogous degree-tower formula for places above infinity.

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_eq_under_mul_relativeInertiaDeg (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : CorvajaZannier.FiniteExtensionPlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L Q = CorvajaZannier.finiteExtensionPlaceDegree K M (placeUnder K M L Q) * match Q with | Sum.inl q => finitePlaceRelativeInertiaDeg K M L q | Sum.inr q => infinityPlaceRelativeInertiaDeg K M L q

Exhaustive place degree is multiplicative under restriction through an intermediate function field.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.finiteIntegralClosureGalAction (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : MulSemiringAction Gal(L/M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The field Galois group acts on the finite integral closure in the top field, relative to the intermediate finite integral closure.

Equations

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

theorem BGS.HasseWeil.finiteIntegralClosureGalSmulComm (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : SMulCommClass Gal(L/M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K M) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The relative Galois action fixes the intermediate finite integral closure.

noncomputable def BGS.HasseWeil.finitePlaceGalSmul (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (g : Gal(L/M)) (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.FiniteExtensionFinitePlace K L

The relative Galois action on a finite place, obtained by acting on its height-one prime ideal.

Equations

• BGS.HasseWeil.finitePlaceGalSmul K M L g P = { asIdeal := g • P.asIdeal, isPrime := ⋯, ne_bot := ⋯ }

@[implicit_reducible]

noncomputable def BGS.HasseWeil.finitePlaceGalAction (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : MulAction Gal(L/M) (CorvajaZannier.FiniteExtensionFinitePlace K L)

The relative Galois group acts on finite places of the top function field.

Equations

• BGS.HasseWeil.finitePlaceGalAction K M L = { smul := BGS.HasseWeil.finitePlaceGalSmul K M L, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem BGS.HasseWeil.finitePlaceUnder_finitePlaceGalSmul (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (g : Gal(L/M)) (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : finitePlaceUnder K M L (finitePlaceGalSmul K M L g P) = finitePlaceUnder K M L P

Relative Galois conjugation does not change the restricted finite place.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.finitePlaceUnderFiberGalAction (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : MulAction Gal(L/M) (FinitePlaceUnderFiber K M L P)

The relative Galois action restricts to every finite-place fiber.

Equations

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

def BGS.HasseWeil.FinitePlacesGaloisConjugate (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : Prop

Galois conjugacy of finite places, expressed on their prime ideals.

Equations

• BGS.HasseWeil.FinitePlacesGaloisConjugate K M L P Q = ∃ (g : Gal(L/M)), Q.asIdeal = g • P.asIdeal

theorem BGS.HasseWeil.exists_gal_smul_finitePlace_asIdeal_of_same_under (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : CorvajaZannier.FiniteExtensionFinitePlace K L) (hPQ : finitePlaceUnder K M L P = finitePlaceUnder K M L Q) : FinitePlacesGaloisConjugate K M L P Q

Two finite places above the same intermediate place are conjugate under the relative field Galois group.

theorem BGS.HasseWeil.finitePlaceUnderFiberGalAction_isPretransitive (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : MulAction.IsPretransitive Gal(L/M) (FinitePlaceUnderFiber K M L P)

Each finite-place restriction fiber is a transitive relative Galois set.

noncomputable def BGS.HasseWeil.finitePlaceUnderFiberFixedBy (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) (g : Gal(L/M)) : Type u_3

Finite places in a restriction fiber fixed by one relative Galois automorphism.

Equations

• BGS.HasseWeil.finitePlaceUnderFiberFixedBy K M L P g = ↑(MulAction.fixedBy (BGS.HasseWeil.FinitePlaceUnderFiber K M L P) g)

theorem BGS.HasseWeil.sum_card_finitePlaceUnderFiberFixedBy_eq_card_galoisGroup (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) : ∑ g : Gal(L/M), Nat.card (finitePlaceUnderFiberFixedBy K M L P g) = Nat.card Gal(L/M)

The exact local fixed-point trace identity for a finite-place restriction fiber.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.infinityIntegralClosureGalAction (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : MulSemiringAction Gal(L/M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The same relative Galois group acts on the integral closure of the infinity valuation ring.

Equations

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

theorem BGS.HasseWeil.infinityIntegralClosureGalSmulComm (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : SMulCommClass Gal(L/M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K M) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The relative Galois action fixes the intermediate infinity integral closure.

theorem BGS.HasseWeil.ratFuncInfinityIntegersGalSmulComm (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : SMulCommClass Gal(L/M) ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The relative Galois action also commutes with scalars from the base infinity valuation ring.

noncomputable def BGS.HasseWeil.infinityPlaceGalSmul (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (g : Gal(L/M)) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)

The relative Galois action on a place above infinity, obtained by acting on its prime ideal.

Equations

• BGS.HasseWeil.infinityPlaceGalSmul K M L g P = ⟨g • ↑P, ⋯⟩

@[implicit_reducible]

noncomputable def BGS.HasseWeil.infinityPlaceGalAction (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] : MulAction Gal(L/M) ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)

The relative Galois group acts on places above infinity of the top function field.

Equations

• BGS.HasseWeil.infinityPlaceGalAction K M L = { smul := BGS.HasseWeil.infinityPlaceGalSmul K M L, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem BGS.HasseWeil.infinityPlaceUnder_infinityPlaceGalSmul (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (g : Gal(L/M)) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : infinityPlaceUnder K M L (infinityPlaceGalSmul K M L g P) = infinityPlaceUnder K M L P

Relative Galois conjugation does not change the restricted infinity place.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.infinityPlaceUnderFiberGalAction (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : MulAction Gal(L/M) (InfinityPlaceUnderFiber K M L P)

The relative Galois action restricts to every infinity-place fiber.

Equations

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

def BGS.HasseWeil.InfinityPlacesGaloisConjugate (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : Prop

Galois conjugacy of places above infinity, expressed on their prime ideals.

Equations

• BGS.HasseWeil.InfinityPlacesGaloisConjugate K M L P Q = ∃ (g : Gal(L/M)), ↑Q = g • ↑P

theorem BGS.HasseWeil.exists_gal_smul_infinityPlace_asIdeal_of_same_under (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) (hPQ : infinityPlaceUnder K M L P = infinityPlaceUnder K M L Q) : InfinityPlacesGaloisConjugate K M L P Q

Two places above infinity with the same intermediate restriction are conjugate under the relative field Galois group.

theorem BGS.HasseWeil.infinityPlaceUnderFiberGalAction_isPretransitive (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : MulAction.IsPretransitive Gal(L/M) (InfinityPlaceUnderFiber K M L P)

Each infinity-place restriction fiber is a transitive relative Galois set.

noncomputable def BGS.HasseWeil.infinityPlaceUnderFiberFixedBy (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) (g : Gal(L/M)) : Type u_3

Places above infinity in a restriction fiber fixed by one relative Galois automorphism.

Equations

• BGS.HasseWeil.infinityPlaceUnderFiberFixedBy K M L P g = ↑(MulAction.fixedBy (BGS.HasseWeil.InfinityPlaceUnderFiber K M L P) g)

theorem BGS.HasseWeil.sum_card_infinityPlaceUnderFiberFixedBy_eq_card_galoisGroup (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) : ∑ g : Gal(L/M), Nat.card (infinityPlaceUnderFiberFixedBy K M L P g) = Nat.card Gal(L/M)

The exact local fixed-point trace identity for an infinity-place restriction fiber.

theorem BGS.HasseWeil.finitePlaceRelative_ramificationIdx_inertiaDeg_eq_of_same_under (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : CorvajaZannier.FiniteExtensionFinitePlace K L) (hPQ : finitePlaceUnder K M L P = finitePlaceUnder K M L Q) : finitePlaceRelativeRamificationIdx K M L P = finitePlaceRelativeRamificationIdx K M L Q ∧ finitePlaceRelativeInertiaDeg K M L P = finitePlaceRelativeInertiaDeg K M L Q

Ramification index and inertia degree are constant on each finite-place restriction fiber in a Galois tower.

theorem BGS.HasseWeil.infinityPlaceRelative_ramificationIdx_inertiaDeg_eq_of_same_under (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P Q : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) (hPQ : infinityPlaceUnder K M L P = infinityPlaceUnder K M L Q) : infinityPlaceRelativeRamificationIdx K M L P = infinityPlaceRelativeRamificationIdx K M L Q ∧ infinityPlaceRelativeInertiaDeg K M L P = infinityPlaceRelativeInertiaDeg K M L Q

Ramification index and inertia degree are constant on each restriction fiber above infinity in a Galois tower.

theorem BGS.HasseWeil.finitePlaceUnderFiber_card_mul_ramificationIdx_mul_inertiaDeg_eq_field_finrank (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K M) (Q₀ : FinitePlaceUnderFiber K M L P) : Fintype.card (FinitePlaceUnderFiber K M L P) * finitePlaceRelativeRamificationIdx K M L ↑Q₀ * finitePlaceRelativeInertiaDeg K M L ↑Q₀ = Module.finrank M L

In a Galois tower, the number of finite places in a restriction fiber times their common ramification index and inertia degree is the relative field degree.

theorem BGS.HasseWeil.infinityPlaceUnderFiber_card_mul_ramificationIdx_mul_inertiaDeg_eq_field_finrank (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K M)) (Q₀ : InfinityPlaceUnderFiber K M L P) : Fintype.card (InfinityPlaceUnderFiber K M L P) * infinityPlaceRelativeRamificationIdx K M L ↑Q₀ * infinityPlaceRelativeInertiaDeg K M L ↑Q₀ = Module.finrank M L

The analogous Galois decomposition formula for a restriction fiber above infinity.

noncomputable def BGS.HasseWeil.finitePlaceDecompositionGroup (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : Subgroup Gal(L/M)

The decomposition group of a finite place in the relative Galois group.

Equations

• BGS.HasseWeil.finitePlaceDecompositionGroup K M L P = MulAction.stabilizer Gal(L/M) P.asIdeal

noncomputable def BGS.HasseWeil.finitePlaceInertiaGroup (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : Subgroup Gal(L/M)

The inertia group of a finite place in the relative Galois group.

Equations

• BGS.HasseWeil.finitePlaceInertiaGroup K M L P = Ideal.inertia Gal(L/M) P.asIdeal

noncomputable def BGS.HasseWeil.infinityPlaceDecompositionGroup (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : Subgroup Gal(L/M)

The decomposition group of a place above infinity in the relative Galois group.

Equations

• BGS.HasseWeil.infinityPlaceDecompositionGroup K M L P = MulAction.stabilizer Gal(L/M) ↑P

noncomputable def BGS.HasseWeil.infinityPlaceInertiaGroup (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : Subgroup Gal(L/M)

The inertia group of a place above infinity in the relative Galois group.

Equations

• BGS.HasseWeil.infinityPlaceInertiaGroup K M L P = Ideal.inertia Gal(L/M) ↑P

theorem BGS.HasseWeil.finitePlaceInertiaGroup_card_eq_ramificationIdx (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] [Finite K] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : Nat.card ↥(finitePlaceInertiaGroup K M L P) = finitePlaceRelativeRamificationIdx K M L P

The inertia-group cardinality is the ramification index at a finite place.

theorem BGS.HasseWeil.finitePlaceDecompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg (K : Type u_1) [Field K] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] [Finite K] (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : Nat.card ↥(finitePlaceDecompositionGroup K M L P) = finitePlaceRelativeRamificationIdx K M L P * finitePlaceRelativeInertiaDeg K M L P

The decomposition-group cardinality is ramification index times inertia degree at a finite place.

theorem BGS.HasseWeil.infinityPlaceInertiaGroup_card_eq_ramificationIdx (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] [Finite K] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : Nat.card ↥(infinityPlaceInertiaGroup K M L P) = infinityPlaceRelativeRamificationIdx K M L P

The inertia-group cardinality is the ramification index above infinity.

theorem BGS.HasseWeil.infinityPlaceDecompositionGroup_card_eq_ramificationIdx_mul_inertiaDeg (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] [Finite K] (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : Nat.card ↥(infinityPlaceDecompositionGroup K M L P) = infinityPlaceRelativeRamificationIdx K M L P * infinityPlaceRelativeInertiaDeg K M L P

The decomposition-group cardinality is ramification index times inertia degree above infinity.