Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionLocalPoleSpace

Local and away-regular subspaces of a function field #

For an exhaustive place P, the one-point Riemann space is the intersection of two elementary subspaces: functions with a bounded pole at P, and functions regular at every place away from P. This is the two-open-cover decomposition used by the Cech form of Riemann's inequality.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.localPoleConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
Algebra K L

The algebra structure from K to L used in the finite extension local pole space construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.localPoleConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    def BGS.HasseWeil.finiteExtensionLocalPoleSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) :
    Submodule K L

    Functions whose pole at P has order at most n, with no condition at the other places.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem BGS.HasseWeil.mem_finiteExtensionLocalPoleSpace_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (x : L) :
      x ∈ finiteExtensionLocalPoleSpace K L P n ↔ x = 0 ∨ x ≠ 0 ∧ -↑n ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) P
      source
      def BGS.HasseWeil.finiteExtensionAwayRegularSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) :
      Submodule K L

      Functions regular at every exhaustive place other than P.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem BGS.HasseWeil.mem_finiteExtensionAwayRegularSpace_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (x : L) :
        x ∈ finiteExtensionAwayRegularSpace K L P ↔ x = 0 ∨ x ≠ 0 ∧ ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), v ≠ P → 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v
        source
        theorem BGS.HasseWeil.finiteExtensionLocalPoleSpace_mono (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) {m n : ℕ} (hmn : m ≤ n) :
        finiteExtensionLocalPoleSpace K L P m ≤ finiteExtensionLocalPoleSpace K L P n

        The local pole filtration is increasing.

        source
        theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_eq_inf (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) :
        CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n = finiteExtensionLocalPoleSpace K L P n ⊓ finiteExtensionAwayRegularSpace K L P

        The one-point Riemann space is the intersection of its local pole bound and its away-regular condition.

        source
        theorem BGS.HasseWeil.finiteExtensionRiemannSpace_zero_eq_local_inf_away (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) :
        CorvajaZannier.finiteExtensionRiemannSpace K L 0 = finiteExtensionLocalPoleSpace K L P 0 ⊓ finiteExtensionAwayRegularSpace K L P

        At level zero the same intersection is the all-place regular space.