Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionHasseWeil

Hasse--Weil for finite separable function-field extensions #

The normal closure supplies one finite enlargement of the constant field over which the extension is geometric. At every sufficiently divisible even constant-field degree, a quadratic subfield and an auxiliary extension of factorial degree put the fixed-tower Frobenius-twist estimate into a uniform form. Exact constant-extension splitting and the spectral argument then transport that estimate back to the original function field.

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

The constant-field algebra on N used in the genus bridge.

Equations
Instances For
    source
    theorem BGS.HasseWeil.instIsScalarTowerRatFunc_leanPool_2 (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.finiteExtensionHasseBaseConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] :
    Algebra K F

    The algebra structure from K to F used in the finite extension hasse weil construction.

    Equations
    Instances For
      source
      theorem BGS.HasseWeil.finiteExtensionHasseBaseConstantTower (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] :
      IsScalarTower K (RatFunc K) F
      source
      @[instance_reducible]
      noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantFintype (K : Type u_1) (F : Type u_2) [Field K] [Fintype K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
      Fintype ↥(FunctionFieldNormalClosureConstantField K F)

      A finite enumeration of (FunctionFieldNormalClosureConstantField K F) used in the finite extension hasse weil construction.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
        Algebra K ↥(FunctionFieldNormalClosureConstantField K F)

        The algebra structure from K to (FunctionFieldNormalClosureConstantField K F) used in the finite extension hasse weil construction.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantSmul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
          SMul K ↥(FunctionFieldNormalClosureConstantField K F)

          The scalar action of K on (FunctionFieldNormalClosureConstantField K F) used in the finite extension hasse weil construction.

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
            Module K ↥(FunctionFieldNormalClosureConstantField K F)

            The module structure of (FunctionFieldNormalClosureConstantField K F) over K used in the finite extension hasse weil construction.

            Equations
            Instances For
              source
              theorem BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantFiniteDimensional (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] [Finite K] :
              FiniteDimensional K ↥(FunctionFieldNormalClosureConstantField K F)
              source
              theorem BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantIsGalois (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] [Finite K] :
              IsGalois K ↥(FunctionFieldNormalClosureConstantField K F)
              source
              @[instance_reducible]
              noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureConstantDecidableEq (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
              DecidableEq ↥(FunctionFieldNormalClosureConstantField K F)

              Decidable equality on (FunctionFieldNormalClosureConstantField K F) used in the finite extension hasse weil construction.

              Equations
              Instances For
                source
                @[instance_reducible]
                noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureRatFuncDecidableEq (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                DecidableEq (RatFunc ↥(FunctionFieldNormalClosureConstantField K F))

                Decidable equality on (RatFunc (FunctionFieldNormalClosureConstantField K F)) used in the finite extension hasse weil construction.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureRatFuncSmul (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                  SMul (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)

                  The scalar action of (RatFunc (FunctionFieldNormalClosureConstantField K F)) on (FunctionFieldNormalClosure K F) used in the finite extension hasse weil construction.

                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureRatFuncModule (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                    Module (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)

                    The module structure of (FunctionFieldNormalClosure K F) over (RatFunc (FunctionFieldNormalClosureConstantField K F)) used in the finite extension hasse weil construction.

                    Equations
                    Instances For
                      source
                      theorem BGS.HasseWeil.finiteExtensionHasseNormalClosureRatFuncTorsionFree (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                      Module.IsTorsionFree (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)
                      source
                      theorem BGS.HasseWeil.finiteExtensionHasseNormalClosureFiniteDimensional (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                      FiniteDimensional (RatFunc ↥(FunctionFieldNormalClosureConstantField K F)) ↥(FunctionFieldNormalClosure K F)
                      source
                      @[instance_reducible]
                      noncomputable def BGS.HasseWeil.finiteExtensionHasseNormalClosureCanonicalConstantAlgebra (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                      Algebra ↥(FunctionFieldNormalClosureConstantField K F) ↥(FunctionFieldNormalClosure K F)

                      The algebra structure from (FunctionFieldNormalClosureConstantField K F) to (FunctionFieldNormalClosure K F) used in the finite extension hasse weil construction.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def BGS.HasseWeil.functionFieldNormalClosureGenus (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                        ℕ

                        The genus of the chosen normal closure over its full constant field.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          noncomputable def BGS.HasseWeil.functionFieldNormalClosureRatFuncDegree (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                          ℕ

                          The degree of the chosen normal closure over the canonical rational function field of its full constant field.

                          Equations
                          Instances For
                            source
                            noncomputable def BGS.HasseWeil.functionFieldNormalClosureStepanovThreshold (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                            ℕ

                            The Stepanov threshold attached to the chosen normal closure.

                            Equations
                            Instances For
                              source
                              theorem BGS.HasseWeil.functionFieldNormalClosureRatFuncDegree_pos (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                              0 < functionFieldNormalClosureRatFuncDegree K F
                              source
                              theorem BGS.HasseWeil.functionFieldNormalClosureStepanovThreshold_pos (K : Type u_1) (F : Type u_2) [Field K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] :
                              0 < functionFieldNormalClosureStepanovThreshold K F
                              source
                              @[instance_reducible]
                              noncomputable def BGS.HasseWeil.genericGaloisTowerConstantAlgebraM (C : Type u_3) (M : Type u_4) [Field C] [Field M] [Algebra (RatFunc C) M] :
                              Algebra C M

                              Restrict the intermediate rational-function-field algebra to the constants.

                              Equations
                              Instances For
                                source
                                @[instance_reducible]
                                noncomputable def BGS.HasseWeil.genericGaloisTowerConstantAlgebraN (C : Type u_3) (N : Type u_5) [Field C] [Field N] [Algebra (RatFunc C) N] :
                                Algebra C N

                                Restrict the top rational-function-field algebra to the constants.

                                Equations
                                Instances For
                                  source
                                  theorem BGS.HasseWeil.exactConstantExtensionClosedPlaceError_le_normalClosureConstants (K : Type u_1) (F : Type u_2) [Field K] [Fintype K] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) (n : ℕ) :
                                  0 < n → |↑(exactConstantExtensionClosedPlaceExtensionCount K (↥(FunctionFieldNormalClosureConstantField K F)) F hExact (2 * functionFieldNormalClosureStepanovThreshold K F * n)) - ↑(Nat.card ↥(FunctionFieldNormalClosureConstantField K F)) ^ (2 * functionFieldNormalClosureStepanovThreshold K F * n) - 1| ≤ 2 * ↑(functionFieldNormalClosureRatFuncDegree K F) ^ 2 + 2 * ↑(functionFieldNormalClosureRatFuncDegree K F) ^ 3 + ↑(functionFieldNormalClosureRatFuncDegree K F) ^ 2 * (2 * ↑(functionFieldNormalClosureGenus K F) + 1) * ↑(Nat.card ↥(FunctionFieldNormalClosureConstantField K F)) ^ (functionFieldNormalClosureStepanovThreshold K F * n)

                                  The normal-closure constant field gives a uniform square-root-scale bound for the packaged exact constant extensions of the original function field.

                                  Here H = (g + 1)(g + 2) is the Stepanov threshold for the genus g of the geometric normal closure, while D is its degree over the rational function field of its full constant field.

                                  source
                                  theorem BGS.HasseWeil.finiteExtensionClosedPlaceHasseWeil (K : Type u_1) (F : Type u_2) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] [Field F] [Algebra (RatFunc K) F] [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F] (hExact : algebraicClosure K F = ⊥) :
                                  |↑(finiteExtensionClosedPlaceExtensionCount K F 1) - ↑(Nat.card K) - 1| ≤ (2 * ↑(MarkoffRiemannRoch.FunctionField.genus K F) + 1) * √↑(Nat.card K)

                                  The closed Hasse--Weil bound for a finite separable extension of K(X) with exact constant field K.