Local pole spaces and valuation order

The denominator presentation of localPoleSpace agrees with the usual valuation-order condition when its denominator is a power of a uniformizer. This is the bridge from the exact DVR quotient to exhaustive function-field places.

theorem BGS.HasseWeil.mem_localPoleSpace_iff_finitePlaceOrder {K : Type u_1} {R : Type u_2} {L : Type u_3} [Field K] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Field L] [Algebra K R] [Algebra R L] [Algebra K L] [IsScalarTower K R L] [IsFractionRing R L] (π : R) (hπ : Irreducible π) (hπIdeal : (IsDiscreteValuationRing.maximalIdeal R).asIdeal = Ideal.span {π}) (n : ℕ) (x : L) : x ∈ localPoleSpace π n ↔ x = 0 ∨ x ≠ 0 ∧ -↑n ≤ CorvajaZannier.finitePlaceOrder (IsDiscreteValuationRing.maximalIdeal R) x

Membership in the local denominator filtration is exactly the expected lower bound on the discrete valuation.