ValuationSpectrum.HasLocLiftPowerBounded
Mathematical summary.
HasLocLiftPowerBounded A is an internal interface used to construct restriction maps between completed rational localisations. For R(Dโฒ) โ R(D), it records that the denominator of D becomes a unit in ๐ช(R(Dโฒ)) and that each fraction t/s, for t โ T, is power-bounded there. These facts make the localisation map continuous and allow it to extend to the completions. In the complete Tate setting of the paper this class is supplied automatically, so it is not an additional mathematical hypothesis. The status note in the original docstring below is stale: this snapshot already contains the instance used for complete Tate pairs.
Original Lean docstring
The adic Nullstellensatz hypothesis for the presheaf restriction maps: for any
rational containment R(D'.T/D'.s) โ R(D.T/D.s), each generator t/D.s
(for t โ D.T) maps to a power-bounded element in the D'-localization topology
under the canonical lift Localization.Away D.s โ+* Localization.Away D'.s.
This is a consequence of Wedhorn Prop 5.30(4) + 7.14 (adic Nullstellensatz):
the rational containment gives v(t) โค v(D.s) for all relevant continuous
valuations, hence t/D.s is integral over the ring of definition, hence
power-bounded.
Status: Will be proved as an instance for Tate rings (where the Nullstellensatz
is available). For now, carried as an explicit hypothesis via this class.
Used in the paper for: Appendix A (restriction-map hypothesis); Appendix: construction of rational restriction maps
class HasLocLiftPowerBounded (A : Type*) [CommRing A] [TopologicalSpace A] [PlusSubring A]
[IsHuberRing A] : Prop where
/-- **(Wedhorn-faithful, blocker-2 refactor 2026-05-17)** `D.s` is a unit
**in the completion** `presheafValue D'`, where `D'.canonicalMap : A โ+*
presheafValue D'` is the natural map.
This matches Wedhorn 7.52(2) (in a *complete* affinoid ring, `f` is a unit
iff `|f|(x) โ 0` for every `x โ Spa`) applied to the completion. The
previous algebraic-side field demanded unit-ness in `Localization.Away D'.s`,
which Wedhorn 7.52(2) cannot directly give (algebraic localizations are not
complete in general). -/
isUnit_canonicalMap_s : โ (D D' : RationalLocData A),
rationalOpen D'.T D'.s โ rationalOpen D.T D.s โ
IsUnit (D'.canonicalMap D.s)
/-- **(Wedhorn-faithful, blocker-2 refactor 2026-05-17)** Each
`IsLocalization.Away.lift D.s (...) (divByS t D.s)` (which lands in
`presheafValue D'`) is power-bounded in `presheafValue D'`.
Wedhorn-faithful: power-boundedness in the *completion*, derived from
Wedhorn 7.41 (analytic height-1 valuations + power-bounded continuity). -/
locLift_divByS_isPowerBounded : โ (D D' : RationalLocData A)
(h : rationalOpen D'.T D'.s โ rationalOpen D.T D.s) (t : A), t โ D.T โ
@TopologicalRing.IsPowerBounded (presheafValue D') _ inferInstance
(IsLocalization.Away.lift D.s (isUnit_canonicalMap_s D D' h) (divByS t D.s))