Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.RiemannSpaceConstants

The zero-divisor Riemann space and the exact constant field #

The functions regular at every exhaustive place form a finite-dimensional subalgebra of the function field. Consequently every such function is algebraic over the constant field. When the relative algebraic closure of the constants is trivial, this identifies L(0) with the image of the constant field and gives its finrank exactly equal to one.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.regularConstantAlgebra (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 riemann space constants construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.regularConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    theorem BGS.HasseWeil.regularInfinityNonempty (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Nonempty ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)
    source
    theorem BGS.HasseWeil.regularPlaceNonempty (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Nonempty (CorvajaZannier.FiniteExtensionPlace K L)
    source
    def BGS.HasseWeil.finiteExtensionRegularSubalgebra (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] :
    Subalgebra K L

    The subalgebra of functions regular at every exhaustive place.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.HasseWeil.mem_finiteExtensionRegularSubalgebra (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] {x : L} :
      x ∈ finiteExtensionRegularSubalgebra K L ↔ x ∈ CorvajaZannier.finiteExtensionRiemannSpace K L 0
      source
      def BGS.HasseWeil.finiteExtensionRegularSubalgebraEquiv (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] :
      ↥(finiteExtensionRegularSubalgebra K L) ≃ₗ[K] ↥(CorvajaZannier.finiteExtensionRiemannSpace K L 0)

      The regular subalgebra and the zero-divisor Riemann space have the same underlying vector space.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem BGS.HasseWeil.finiteExtensionRiemannSpace_zero_moduleFinite (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] :
        Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L 0)

        The all-place zero-divisor Riemann space is finite-dimensional.

        source
        theorem BGS.HasseWeil.finiteExtensionRegularSubalgebra_moduleFinite (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] :
        Module.Finite K ↥(finiteExtensionRegularSubalgebra K L)

        The everywhere-regular subalgebra is finite-dimensional.

        source
        theorem BGS.HasseWeil.finiteExtensionRiemannSpace_zero_eq_range (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] (hconstants : algebraicClosure K L = ⊥) :
        CorvajaZannier.finiteExtensionRiemannSpace K L 0 = (Algebra.linearMap K L).range

        With exact constants, every everywhere-regular function is a constant.

        source
        theorem BGS.HasseWeil.finiteExtensionRiemannSpace_zero_finrank (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] (hconstants : algebraicClosure K L = ⊥) :
        Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L 0) = 1

        With exact constants, L(0) has dimension one.