Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Cont.DominatingUnit

Wedhorn Lemma 7.31 and Corollary 7.32: dominating a nonvanishing element by a unit #

Let A be a Tate ring, X a quasi-compact set of continuous points of Spv A, and f : A an element that vanishes at no point of X. Wedhorn Corollary 7.32 produces a unit of A whose valuation is everywhere on X strictly below that of f; Lemma 7.31 is the neighbourhood-of-zero form it is drawn from.

The cover both rest on #

Fix a topologically nilpotent t : A. A continuous point v with v f ≠ 0 opens the ball {a | v a < v f} around 0, so the powers of t eventually enter it — that is Valuation.exists_pow_lt_of_isTopologicallyNilpotent, and it places v in the basic open set Spv(A)(tⁿ/f) for some n. These basic opens increase in n on X, because v t < 1 there, so quasi-compactness collapses the cover to a single exponent: X ⊆ Spv(A)(tᵐ/f).

Lemma 7.31 spends that exponent at a pseudouniformiser ϖ. The set ϖᵐ · I is then a neighbourhood of zero — multiplication by the unit ϖᵐ is an open map, and the image of an ideal of definition is an open neighbourhood of zero — and every a = ϖᵐ y in it satisfies v a = v ϖᵐ · v y < v ϖᵐ ≤ v f, strictly because y is topologically nilpotent. Corollary 7.32 then reads off a unit inside that neighbourhood, which is what the Tate hypothesis is for.

The hypothesis is continuity, not the plus ring #

Wedhorn states both results for a quasi-compact subset of an adic spectrum Spa (A, A⁺). Neither proof uses the sub-unit condition on A⁺, only continuity of the points, so both are stated here over TauCeti.ValuationSpectrum.cont A. They apply verbatim in Wedhorn's setting through spa_def ▸ Set.inter_subset_left : spa Aplus ⊆ cont A.

Main results #

The Tate-ring input, that a neighbourhood of zero contains a unit, is TauCeti.HasZeroSequenceOfUnits.exists_unit_smul_mem at x = 1, available for a Tate ring through the instance TauCeti.Huber.IsTateRing.hasZeroSequenceOfUnits.

Provenance #

Adapted from AINTLIB (see References), file Cor732.lean: the cover-and-collapse argument, the construction of the neighbourhood as ϖᵐ · I, and the assembly of the corollary are that file's exists_pow_dominated_finset, exists_zero_nbhd_lt_on_qc and exists_dominating_unit_noHArch. The vocabulary is adapted to this repository's interfaces throughout: cont/Spv.valuation in place of that file's Spa/ValuativeRel.valuation pairing, basicOpen in place of its bespoke dominatedBy, and the per-point step delegated to Valuation.exists_pow_lt_of_isTopologicallyNilpotent rather than restated. That file's exists_dominating_unit, which assumes MulArchimedean value groups, is not Corollary 7.32 and is not ported; the route taken here is Wedhorn's own and carries no such hypothesis.

References #

source
theorem TauCeti.ValuationSpectrum.IsContinuous.exists_pow_vlt_of_isTopologicallyNilpotent {A : Type u_1} [CommRing A] [TopologicalSpace A] {v : ValuationSpectrum A} (hv : v.IsContinuous) {t : A} (ht : IsTopologicallyNilpotent t) {f : A} (hf : f ∉ v.supp) :
∃ (n : ℕ), t ^ n <ᵥ f

Topologically nilpotent elements are eventually dominated at a continuous point. If v is continuous, t is topologically nilpotent and v f ≠ 0, then v (tⁿ) < v f for some n.

source
theorem TauCeti.ValuationSpectrum.exists_subset_basicOpen_pow {A : Type u_1} [CommRing A] [TopologicalSpace A] {X : Set (ValuationSpectrum A)} (hXcont : X ⊆ cont A) (hX : IsCompact X) {f : A} (hf : ∀ v ∈ X, ¬f ≤ᵥ 0) {t : A} (ht : IsTopologicallyNilpotent t) :
∃ (m : ℕ), X ⊆ basicOpen (t ^ m) f

The cover behind Wedhorn Lemma 7.31, collapsed to one exponent. For X a quasi-compact set of continuous points at which f does not vanish and t topologically nilpotent, some power tᵐ is dominated by f at every point of X: X ⊆ Spv(A)(tᵐ/f).

Pointwise this is IsContinuous.exists_pow_vlt_of_isTopologicallyNilpotent: the ball of radius v f is open because v is continuous. The resulting basic opens increase in the exponent on X, so a finite subcover has a largest exponent that works for all.

source
theorem TauCeti.ValuationSpectrum.exists_mem_nhds_zero_forall_vlt {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] {X : Set (ValuationSpectrum A)} (hXcont : X ⊆ cont A) (hX : IsCompact X) {f : A} (hf : ∀ v ∈ X, ¬f ≤ᵥ 0) :
∃ I ∈ nhds 0, ∀ a ∈ I, ∀ v ∈ X, a <ᵥ f

Wedhorn Lemma 7.31. For X a quasi-compact set of continuous points of a Tate ring at which f does not vanish, some neighbourhood of zero is strictly dominated by f throughout X.

The neighbourhood is ϖᵐ · I for a pseudouniformiser ϖ, the exponent m supplied by exists_subset_basicOpen_pow, and I the image of an ideal of definition. Its elements a = ϖᵐ y have v a = v ϖᵐ · v y < v ϖᵐ ≤ v f, the strict step because y is topologically nilpotent and v ϖᵐ ≠ 0.

source
theorem TauCeti.ValuationSpectrum.exists_unit_forall_vlt {A : Type u_1} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] [Huber.IsTateRing A] {X : Set (ValuationSpectrum A)} (hXcont : X ⊆ cont A) (hX : IsCompact X) {f : A} (hf : ∀ v ∈ X, ¬f ≤ᵥ 0) :
∃ (ϖ : Aˣ), ∀ v ∈ X, ↑ϖ <ᵥ f

Wedhorn Corollary 7.32. For X a quasi-compact set of continuous points of a Tate ring at which f does not vanish, there is a unit of A strictly dominated by f throughout X.

Lemma 7.31 supplies a neighbourhood of zero dominated by f, and the Tate hypothesis puts a unit inside it (TauCeti.HasZeroSequenceOfUnits.exists_unit_smul_mem at x = 1).