Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistFinitePlaceBridge

Finite places of Frobenius-twist fields #

This file connects the fixed finite places occurring in Frobenius-coset averaging with finite places of the corresponding Frobenius-twist fixed field. The first step is the arithmetic core of that comparison: every rational finite place of a twist field has a unique finite place above it in the exact constant extension.

Indeed, the top residue field contains the enlarged constant field S, so its degree over C is divisible by [S : C]. Multiplicativity of place degree identifies that degree with the relative residue degree above a rational twist-field place. Since the entire extension has degree [S : C], the Galois decomposition formula forces both the number of places above the rational place and the ramification index to be one.

Only this rational-place-to-fixed-lift direction is asserted here. The reverse implication for an arbitrary twist-fixed top place additionally requires the unramified residue-field descent for the constant extension; that result is not hidden in the interface below.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.twistBridgeConstantAlgebra (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] :
Algebra C N

The algebra structure from C to N used in the exact constant extension frobenius twist finite place bridge construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.twistBridgeConstantTower (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] :
    IsScalarTower C (RatFunc C) N
    source
    theorem BGS.HasseWeil.rationalFinitePlace_fiber_card_eq_one_of_finrank_dvd_degree (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] [Algebra (RatFunc K) T] [FiniteDimensional (RatFunc K) T] [Algebra.IsSeparable (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] [FiniteDimensional M T] [IsGalois M T] (hdegree : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q)) (P : FiniteExtensionRationalFinitePlace K M) :
    Fintype.card (FinitePlaceUnderFiber K M T ↑P) = 1

    If every top finite-place degree is divisible by the relative field degree, then every rational finite place downstairs has a unique place above it. The proof uses only degree multiplicativity and the Galois decomposition formula.

    source
    theorem BGS.HasseWeil.finitePlaceGalSmul_eq_self_over_rationalFinitePlace_of_finrank_dvd_degree (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] [Algebra (RatFunc K) T] [FiniteDimensional (RatFunc K) T] [Algebra.IsSeparable (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] [FiniteDimensional M T] [IsGalois M T] (hdegree : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q)) (P : FiniteExtensionRationalFinitePlace K M) (Q : CorvajaZannier.FiniteExtensionFinitePlace K T) (hQ : finitePlaceUnder K M T Q = ↑P) (sigma : Gal(T/M)) :
    finitePlaceGalSmul K M T sigma Q = Q

    Under the same degree-divisibility hypothesis, every relative Galois automorphism fixes every finite place above a rational finite place. This is the action form of the singleton-fiber theorem.

    source
    theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_finrank_constants_dvd_degree (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) :
    Module.finrank C S ∣ CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q)

    Every finite place of the exact constant extension, viewed over the original constants C, has degree divisible by [S : C]. This is the degree-theoretic expression of the inclusion of S in every top residue field.

    source
    noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusTwistOverFixedField (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) :
    ExactConstantExtension C N S ≃ₐ[↥(exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g)] ExactConstantExtension C N S

    The Frobenius-twist generator, regarded as an automorphism over its own fixed field. Its underlying field automorphism is definitionally the same twist used in the Frobenius fiber over C(X).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem BGS.HasseWeil.exactConstantExtensionFrobeniusTwistOverFixedField_apply (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) (x : ExactConstantExtension C N S) :
      (exactConstantExtensionFrobeniusTwistOverFixedField C N S hExact g) x = (exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g) x
      source
      theorem BGS.HasseWeil.frobeniusTwistField_rationalFinitePlace_fiber_card_eq_one (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) :
      let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; ∀ (P : FiniteExtensionRationalFinitePlace C ↥F), Fintype.card (FinitePlaceUnderFiber C (↥F) (ExactConstantExtension C N S) ↑P) = 1

      A rational finite place of a Frobenius-twist field has exactly one finite place above it in the exact constant extension.

      source
      theorem BGS.HasseWeil.frobeniusTwistField_rationalFinitePlace_lift_fixed (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Field S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Finite S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) :
      let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; ∀ (P : FiniteExtensionRationalFinitePlace C ↥F) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)), finitePlaceUnder C (↥F) (ExactConstantExtension C N S) Q = ↑P → finitePlaceGalSmul C (↥F) (ExactConstantExtension C N S) (exactConstantExtensionFrobeniusTwistOverFixedField C N S hExact g) Q = Q

      Every finite-place lift of a rational Frobenius-twist-field place is fixed by the canonical twist generator over its fixed field.

      source
      @[reducible, inline]
      abbrev BGS.HasseWeil.RationalFinitePlaceLift (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [Algebra (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] :
      Type (max u_5 u_6)

      A rational finite place together with a finite place above it.

      Equations
      Instances For
        source
        noncomputable def BGS.HasseWeil.rationalFinitePlaceEquivLift (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] [Algebra (RatFunc K) T] [FiniteDimensional (RatFunc K) T] [Algebra.IsSeparable (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] [FiniteDimensional M T] [IsGalois M T] (hdegree : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q)) :
        FiniteExtensionRationalFinitePlace K M ≃ RationalFinitePlaceLift K M T

        If the relative degree divides every top place degree, projection from rational finite-place lifts is an equivalence. Equivalently, every rational finite place has exactly one top lift.

        Equations
        Instances For
          source
          theorem BGS.HasseWeil.rationalFinitePlaceLift_fixed (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] [Algebra (RatFunc K) T] [FiniteDimensional (RatFunc K) T] [Algebra.IsSeparable (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] [FiniteDimensional M T] [IsGalois M T] (hdegree : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q)) (sigma : Gal(T/M)) (x : RationalFinitePlaceLift K M T) :
          finitePlaceGalSmul K M T sigma ↑x.snd = ↑x.snd

          Every top lift of a rational finite place is fixed by every relative Galois automorphism under the degree-divisibility hypothesis.

          source
          theorem BGS.HasseWeil.natCard_rationalFinitePlaceLift_eq (K : Type u_4) (M : Type u_5) (T : Type u_6) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field M] [Field T] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] [Algebra (RatFunc K) T] [FiniteDimensional (RatFunc K) T] [Algebra.IsSeparable (RatFunc K) T] [Algebra M T] [IsScalarTower (RatFunc K) M T] [FiniteDimensional M T] [IsGalois M T] (hdegree : ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace K T), Module.finrank M T ∣ CorvajaZannier.finiteExtensionPlaceDegree K T (Sum.inl Q)) :
          Nat.card (RationalFinitePlaceLift K M T) = Nat.card (FiniteExtensionRationalFinitePlace K M)

          Cardinal form of the rational-place/unique-lift correspondence.