Documentation

LeanPool.MarkoffModP.BGS.CorvajaZannier.FiniteExtensionOneSubGcdHeight

The gcd height of a function and its complement #

Control the common divisor of a function and one minus that function using local orders, exceptional places, and outside height.

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

The algebra structure from K[X] to L used in the finite extension one sub gcd height construction.

Equations
Instances For
    source
    theorem BGS.CorvajaZannier.oneSubGcdPolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    IsScalarTower (Polynomial K) (RatFunc K) L
    source
    theorem BGS.CorvajaZannier.oneSubGcdFiniteIntegralClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.Finite (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdFiniteIntegralClosureIsIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    Algebra.IsIntegral (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdPolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.IsTorsionFree (Polynomial K) L
    source
    theorem BGS.CorvajaZannier.oneSubGcdFiniteIntegralClosureIsTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] :
    Module.IsTorsionFree (Polynomial K) ↥(RatFuncFiniteIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdInfinityIntegralClosureModuleFinite (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] :
    Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdInfinityIntegralClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :
    Algebra.IsIntegral ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdInfinityTorsionFreeTop (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] :
    Module.IsTorsionFree (↥(RatFuncInfinityIntegers K)) L
    source
    theorem BGS.CorvajaZannier.oneSubGcdInfinityIntegralClosureIsTorsionFree (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] :
    Module.IsTorsionFree ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.oneSubGcdInfinityIntegralClosureIsDedekindDomain (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] :
    IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)
    source
    theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_add_ge_min (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] (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (hxy : x + y ≠ 0) (w : FiniteExtensionPlace K L) :
    min ((finiteExtensionPrincipalDivisor K L x) w) ((finiteExtensionPrincipalDivisor K L y) w) ≤ (finiteExtensionPrincipalDivisor K L (x + y)) w
    source
    theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_neg_apply (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] (x : L) (hx : x ≠ 0) (w : FiniteExtensionPlace K L) :
    (finiteExtensionPrincipalDivisor K L (-x)) w = (finiteExtensionPrincipalDivisor K L x) w
    source
    theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_one_sub_nonnegative_of_eq_zero (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] (x : L) (hxone : x ≠ 1) (w : FiniteExtensionPlace K L) (hzero : (finiteExtensionPrincipalDivisor K L x) w = 0) :
    0 ≤ (finiteExtensionPrincipalDivisor K L (1 - x)) w
    source
    theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_eq_zero_of_one_sub_pos (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] (x : L) (hx : x ≠ 0) (hxone : x ≠ 1) (w : FiniteExtensionPlace K L) (hpos : 0 < (finiteExtensionPrincipalDivisor K L (1 - x)) w) :
    (finiteExtensionPrincipalDivisor K L x) w = 0
    source
    noncomputable def BGS.CorvajaZannier.propositionTwoExceptionalPlaces (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] (u v : L) :
    Finset (FiniteExtensionPlace K L)

    The exceptional places used in Proposition 2: exactly the zeroes and poles of the two coordinates.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.CorvajaZannier.finiteExtensionOneSubGcd_add_outsideHeight_le_positiveDegree (K : Type u_1) [Field 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] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) :
      finiteExtensionGcdWeightedDegree K L (1 - u) (1 - v) + finiteExtensionOutsideHeight K L ((1 - u) / (1 - v)) (propositionTwoExceptionalPlaces K L u v) ≤ finiteExtensionPositiveDegree K L (1 - v)

      The divisor-theoretic gcd comparison used in Proposition 2, now on the actual exhaustive place type used by the canonical Wronskian sum.

      source
      theorem BGS.CorvajaZannier.finiteExtensionOneSubGcd_add_outsideHeight_le_positiveDegree_coordinate (K : Type u_1) [Field 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] (u v : L) (hu : u ≠ 0) (hv : v ≠ 0) (huone : u ≠ 1) (hvone : v ≠ 1) :
      finiteExtensionGcdWeightedDegree K L (1 - u) (1 - v) + finiteExtensionOutsideHeight K L ((1 - u) / (1 - v)) (propositionTwoExceptionalPlaces K L u v) ≤ finiteExtensionPositiveDegree K L v

      In the gcd comparison, the positive degree of 1-v is exactly the coordinate height, hence the positive degree of v.