Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionPrincipalParts

Principal parts of an effective exhaustive divisor #

For an effective divisor D on the exhaustive places of a finite extension of K(X), this file forms the product of the local principal-part spaces over the finite support of D. The local cumulative quotient calculation gives this product dimension equal to deg D.

The Riemann space L(D) maps diagonally to those principal parts. Its kernel is exactly L(0): vanishing of the principal part gives regularity on the support, while membership in L(D) already gives regularity off the support. Consequently L(D) / L(0) is finite-dimensional and has dimension at most deg D. Under the exact-constant-field hypothesis, the denominator is the space of constants.

source
@[instance_reducible]
noncomputable def BGS.HasseWeil.finitePrincipalPartsConstantAlgebra (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 principal parts construction.

Equations
Instances For
    source
    theorem BGS.HasseWeil.finitePrincipalPartsConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower K (RatFunc K) L
    source
    @[reducible, inline]
    abbrev BGS.HasseWeil.finiteExtensionPrincipalPartAt (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : ↥D.support) :
    Type u_2

    Principal parts at a place in the support of an effective exhaustive divisor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      abbrev BGS.HasseWeil.finiteExtensionPrincipalPartsSpace (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) :
      Type u_2

      The finite product of local principal parts supported by D.

      Equations
      Instances For
        source
        noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorNatDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) :
        ℕ

        The natural-number weighted degree of an effective exhaustive divisor.

        Equations
        Instances For
          source
          theorem BGS.HasseWeil.finiteExtensionDivisor_toNat_pos_of_mem_support (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) (P : ↥D.support) :
          0 < (D ↑P).toNat

          A nonzero effective coefficient has positive natural part.

          source
          theorem BGS.HasseWeil.finiteExtensionPrincipalPartAt_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) (P : ↥D.support) :
          Module.Finite K (finiteExtensionPrincipalPartAt K L D P)

          Each supported local principal-part quotient is finite-dimensional.

          source
          theorem BGS.HasseWeil.finiteExtensionPrincipalPartsSpace_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
          Module.Finite K (finiteExtensionPrincipalPartsSpace K L D)

          The supported product of local principal parts is finite-dimensional.

          source
          theorem BGS.HasseWeil.finiteExtensionPrincipalPartsSpace_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
          Module.finrank K (finiteExtensionPrincipalPartsSpace K L D) = finiteExtensionEffectiveDivisorNatDegree K L D

          The supported product has dimension equal to the natural weighted degree of D.

          source
          theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorNatDegree_cast (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
          ↑(finiteExtensionEffectiveDivisorNatDegree K L D) = CorvajaZannier.finiteExtensionDivisorDegree K L D

          For an effective divisor, the natural weighted degree casts to the usual integer-valued divisor degree.

          source
          theorem BGS.HasseWeil.finiteExtensionRiemannSpace_le_localPoleSpace (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) (P : CorvajaZannier.FiniteExtensionPlace K L) :
          CorvajaZannier.finiteExtensionRiemannSpace K L D ≤ finiteExtensionLocalPoleSpace K L P (D P).toNat

          Membership in L(D) supplies the local pole bound at every place.

          source
          noncomputable def BGS.HasseWeil.finiteExtensionRiemannPrincipalPartsDiagonalMap (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
          ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) →ₗ[K] finiteExtensionPrincipalPartsSpace K L D

          The diagonal principal-parts map from L(D).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem BGS.HasseWeil.finiteExtensionRiemannPrincipalPartsDiagonalMap_ker (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
            (finiteExtensionRiemannPrincipalPartsDiagonalMap K L D hD).ker = relativeSubmodule (CorvajaZannier.finiteExtensionRiemannSpace K L 0) (CorvajaZannier.finiteExtensionRiemannSpace K L D)

            The kernel of the diagonal map is the copy of L(0) inside L(D).

            source
            noncomputable def BGS.HasseWeil.finiteExtensionRiemannPrincipalPartsQuotientMap (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
            ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ⧸ relativeSubmodule (CorvajaZannier.finiteExtensionRiemannSpace K L 0) (CorvajaZannier.finiteExtensionRiemannSpace K L D) →ₗ[K] finiteExtensionPrincipalPartsSpace K L D

            The diagonal map descends injectively from L(D) / L(0).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem BGS.HasseWeil.finiteExtensionRiemannPrincipalPartsQuotientMap_injective (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
              Function.Injective ⇑(finiteExtensionRiemannPrincipalPartsQuotientMap K L D hD)

              The descended principal-parts map is injective.

              source
              theorem BGS.HasseWeil.finiteExtensionRiemannSpace_quotient_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
              Module.Finite K (↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ⧸ relativeSubmodule (CorvajaZannier.finiteExtensionRiemannSpace K L 0) (CorvajaZannier.finiteExtensionRiemannSpace K L D))

              For an effective divisor, L(D) / L(0) is finite-dimensional.

              source
              theorem BGS.HasseWeil.finiteExtensionRiemannSpace_quotient_zero_finrank_le (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
              Module.finrank K (↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ⧸ relativeSubmodule (CorvajaZannier.finiteExtensionRiemannSpace K L 0) (CorvajaZannier.finiteExtensionRiemannSpace K L D)) ≤ finiteExtensionEffectiveDivisorNatDegree K L D

              Riemann's elementary principal-parts upper bound for an effective exhaustive divisor.

              source
              theorem BGS.HasseWeil.finiteExtensionRiemannSpace_quotient_zero_finrank_cast_le_degree (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) :
              ↑(Module.finrank K (↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ⧸ relativeSubmodule (CorvajaZannier.finiteExtensionRiemannSpace K L 0) (CorvajaZannier.finiteExtensionRiemannSpace K L D))) ≤ CorvajaZannier.finiteExtensionDivisorDegree K L D

              Integer-valued form of the principal-parts upper bound.

              source
              theorem BGS.HasseWeil.finiteExtensionRiemannSpace_mod_constants_finrank_cast_le_degree (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P) (hconstants : algebraicClosure K L = ⊥) :
              ↑(Module.finrank K (↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ⧸ relativeSubmodule (Algebra.linearMap K L).range (CorvajaZannier.finiteExtensionRiemannSpace K L D))) ≤ CorvajaZannier.finiteExtensionDivisorDegree K L D

              With exact constants, the preceding quotient is literally L(D) modulo the constant functions.