Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFinitePlaceFrobeniusAverage

Frobenius-coset averaging at finite places of an exact constant extension #

This file composes the actual constant-extension finite-place construction with the Frobenius-coset form of Burnside's lemma. A rational place below one explicit constant-extended finite place supplies the decomposition-group cardinality at that place. Transitivity of the relative Galois action and cyclicity of the finite-field Galois group propagate surjectivity of the constant quotient to every stabilizer in the same restriction fiber.

source
theorem BGS.HasseWeil.MonoidHom.stabilizer_surjective_of_isPretransitive_of_isCyclic {G : Type u_1} {A : Type u_2} {X : Type u_3} [Group G] [Group A] [IsCyclic A] [MulAction G X] [MulAction.IsPretransitive G X] (pi : G →* A) (x₀ : X) (h₀ : Function.Surjective ⇑(pi.comp (MulAction.stabilizer G x₀).subtype)) (x : X) :
Function.Surjective ⇑(pi.comp (MulAction.stabilizer G x).subtype)

In a transitive action, surjectivity of a homomorphism on one stabilizer propagates to every stabilizer when the target is cyclic. Stabilizers in the same orbit are conjugate, and conjugation disappears in a cyclic target.

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

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

Equations
Instances For
    source
    theorem BGS.HasseWeil.averageBaseConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] :
    IsScalarTower C (RatFunc C) N
    source
    @[instance_reducible]
    noncomputable def BGS.HasseWeil.averageTargetPolynomialAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] :
    Algebra (Polynomial S) (ExactConstantExtension C N S)

    The algebra structure from S[X] to (ExactConstantExtension C N S) used in the exact constant extension finite place frobenius average construction.

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.averageIntermediateConstantAlgebra (C : Type u_1) [Field C] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] :
      Algebra C L

      The algebra structure from C to L used in the exact constant extension finite place frobenius average construction.

      Equations
      Instances For
        source
        theorem BGS.HasseWeil.averageConstantIntermediateTopTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] :
        IsScalarTower C L N
        source
        theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_frobeniusFiber_fixedPoint_sum (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) (hBase : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl (finitePlaceUnder C L N (exactConstantExtensionDownstairsFinitePlace C S N hExact q))) = 1) (hDegreeDiv : Module.finrank L N ∣ Module.finrank C S) :
        have Q := exactConstantExtensionCompatibleBaseFinitePlace C S N hExact q; have P := finitePlaceUnder C L (ExactConstantExtension C N S) Q; have pi := exactConstantExtensionConstantQuotient C L N S hExact; ∑ g : ↑(⇑pi ⁻¹' {FiniteField.frobeniusAlgEquivOfAlgebraic C S}), Nat.card ↑(MulAction.fixedBy (FinitePlaceUnderFiber C L (ExactConstantExtension C N S) P) ↑g) = Nat.card Gal(N/L)

        Local Frobenius-coset Burnside identity for an actual finite place of an exact constant extension. The assumptions say only that its restriction to L is rational and that [N : L] divides the constant-extension degree. The exact decomposition-group cardinality, stabilizer surjectivity, and the fixed-point total are all derived internally.