Units on a Laurent piece #
In Wedhorn's reduction of a standard rational cover to Laurent covers, one first chooses a unit
ϖ smaller than some member of the covering family at every point. On a Laurent piece generated
by the ratios ϖ⁻¹ t, each generator on the ≥ 1 side is invertible in the coordinate ring of
that piece. The pointwise nonvanishing inequality is
not_vle_zero_of_mem_laurentPiece_inv_mul; the result here promotes it to invertibility in
any rational presentation of the piece.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 8.34(ii).
theorem
TauCeti.ValuationSpectrum.isUnit_toCompletionLoc_of_laurentPiece_inv_mul
{A : Type u_1}
[CommRing A]
[TopologicalSpace A]
[IsTopologicalRing A]
(P : Huber.PairOfDefinition A)
(Aplus : Subring A)
(hP : P.ringOfDefinition ≤ Aplus)
(hAplus : ∀ ⦃a : A⦄, a ∈ Aplus → Huber.IsPowerBounded a)
{T : Finset A}
(ϖ : Aˣ)
{J : Set ↥T}
{t : ↥T}
(ht : t ∈ J)
(U : Finset A)
(s : A)
(S : Type u_2)
[CommRing S]
[Algebra A S]
[IsLocalization.Away s S]
(hden : P.HasDenominatorPower U s S)
(hU : rationalSubset Aplus U s ⊆ laurentPiece Aplus (fun (t : ↥T) => ↑ϖ⁻¹ * ↑t) J)
:
IsUnit ((P.toCompletionLoc U s S hden) ↑t)
A generator with sign ≥ 1 is a unit on a Laurent piece generated by ϖ⁻¹ t.
The rational presentation may be any one whose rational subset lies in that piece; in
particular this applies to any presentation of the whole piece.