Local place actions in a Frobenius fiber

This file supplies the local ideal-theoretic bridge used by the Frobenius-coset step of the Hasse--Weil argument.

First, if a maximal ideal has residue degree one over a constant field S, then the kernel of the constant restriction map on its decomposition group is exactly its inertia group. This is proved directly from the induced action on the residue field; it assumes no point-count estimate.

Second, relative Galois conjugation preserves absolute place degree, so it acts on places of any prescribed degree. On each finite or infinity restriction fiber, the stabilizer of a point is identified with the existing decomposition group.

theorem BGS.HasseWeil.stabilizerRestriction_ker_eq_inertia_of_residue_finrank_one {C : Type u_1} {S : Type u_2} {A : Type u_3} {G : Type u_4} [Field C] [Field S] [CommRing A] [Algebra C S] [Algebra S A] [Group G] [MulSemiringAction G A] (q : Ideal A) [q.IsMaximal] (π : G →* Gal(S/C)) (hcompat : ∀ (g : G) (s : S), g • (algebraMap S A) s = (algebraMap S A) ((π g) s)) (hdegree : Module.finrank S q.ResidueField = 1) : (π.comp (MulAction.stabilizer G q).subtype).ker = Ideal.inertia (↥(MulAction.stabilizer G q)) q

If a maximal ideal has residue degree one over S, and the action on the ambient ring restricts along π to the stated action on S, then the kernel of π on the decomposition group is exactly the inertia group.

theorem BGS.HasseWeil.finiteExtensionFinitePlace_degree_finitePlaceGalSmul (K : Type u_1) [Field K] [DecidableEq 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] [IsGalois M L] (g : Gal(L/M)) (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl (finitePlaceGalSmul K M L g P)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl P)

Relative Galois conjugation preserves the absolute degree of a finite place.

theorem BGS.HasseWeil.finiteExtensionInfinityPlace_degree_infinityPlaceGalSmul (K : Type u_1) [Field K] [DecidableEq 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] (g : Gal(L/M)) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr (infinityPlaceGalSmul K M L g P)) = CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P)

Relative Galois conjugation preserves the absolute degree of a place above infinity.

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionFinitePlaceOfDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] (d : ℕ) : Type u_3

Finite places of a prescribed absolute degree.

Equations

• BGS.HasseWeil.FiniteExtensionFinitePlaceOfDegree K L d = { P : BGS.CorvajaZannier.FiniteExtensionFinitePlace K L // BGS.CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl P) = d }

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionInfinityPlaceOfDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] (d : ℕ) : Type u_3

Places above infinity of a prescribed absolute degree.

Equations

• BGS.HasseWeil.FiniteExtensionInfinityPlaceOfDegree K L d = { P : ↑(BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L) // BGS.CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr P) = d }

@[implicit_reducible]

noncomputable def BGS.HasseWeil.finitePlaceOfDegreeGalAction (K : Type u_1) [Field K] [DecidableEq 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] [IsGalois M L] (d : ℕ) : MulAction Gal(L/M) (FiniteExtensionFinitePlaceOfDegree K L d)

The relative Galois action on finite places restricts to places of any prescribed absolute degree.

Equations

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

@[implicit_reducible]

noncomputable def BGS.HasseWeil.infinityPlaceOfDegreeGalAction (K : Type u_1) [Field K] [DecidableEq 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] (d : ℕ) : MulAction Gal(L/M) (FiniteExtensionInfinityPlaceOfDegree K L d)

The relative Galois action on places above infinity restricts to places of any prescribed absolute degree.

Equations

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

theorem BGS.HasseWeil.finitePlaceUnderFiber_stabilizer_eq_decompositionGroup (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) (Q : FinitePlaceUnderFiber K M L P) : MulAction.stabilizer Gal(L/M) Q = finitePlaceDecompositionGroup K M L ↑Q

On a finite-place restriction fiber, the point stabilizer is the usual decomposition group of the underlying place.

theorem BGS.HasseWeil.infinityPlaceUnderFiber_stabilizer_eq_decompositionGroup (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)) (Q : InfinityPlaceUnderFiber K M L P) : MulAction.stabilizer Gal(L/M) Q = infinityPlaceDecompositionGroup K M L ↑Q

On an infinity-place restriction fiber, the point stabilizer is the usual decomposition group of the underlying place.