Actual finite-place auxiliary orders in the exhaustive divisor model

This file keeps the local DVR construction independent of the heavier exhaustive-place infrastructure, then identifies its normalized order with the coefficient used by the global principal divisor.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.auxiliaryFinitePlaceBridgePolynomialAlgebra (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 plane curve auxiliary finite place principal divisor construction.

Equations

• BGS.CorvajaZannier.auxiliaryFinitePlaceBridgePolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.auxiliaryFinitePlaceBridgePolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.CorvajaZannier.auxiliaryFinitePlaceBridgeIntegralClosureIsDedekindDomain (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] : IsDedekindDomain ↥(FunctionField.ringOfIntegers K L)

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrder_eq_principalDivisor (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] (q : PlaneCurveExtensionFinitePlace K L) (x : L) : finiteExtensionFinitePlaceLocalOrder q x = (finiteExtensionFinitePrincipalDivisor K L x) q

The actual localized finite-place order is exactly the coefficient in the exhaustive finite principal divisor.

theorem BGS.CorvajaZannier.finiteExtensionFinitePlaceLocalOrderTop_eq_principalDivisor (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] (q : PlaneCurveExtensionFinitePlace K L) (x : L) (hx : x ≠ 0) : finiteExtensionFinitePlaceLocalOrderTop q x = ↑((finiteExtensionFinitePrincipalDivisor K L x) q)

For a nonzero element, the WithTop order appearing in the local Wronskian inequality is the exhaustive principal-divisor coefficient.