Documentation

TauCeti.RingTheory.Huber.UnitGroup

The unit group of a complete Huber ring is open, and proper ideals stay proper #

This is the first half of Wedhorn's Proposition 7.51, whose statement is "then 𝔪 is closed and there exists v ∈ Spa A with supp v = 𝔪". Only the closedness conjunct is proved here; the existence conjunct needs nonemptiness of the adic spectrum (Wedhorn Proposition 7.49) and is carried out in TauCeti/AlgebraicGeometry/AdicSpace/Spa/Support.lean, which consumes the density statements below.

The argument is Wedhorn's. The topologically nilpotent elements of a Huber ring form an open set (TauCeti.Huber.isOpen_setOf_isTopologicallyNilpotent), and completeness makes 1 + A°° consist of units (IsTopologicallyNilpotent.isUnit_one_add). Around a unit u the set of x with u⁻¹x - 1 topologically nilpotent is then an open neighbourhood of u made of units, so the unit group is open. Closedness of maximal ideals is then immediate from Ideal.isClosed_of_isMaximal_of_isOpen_isUnit, which holds over any topological ring, and so is the fact that a proper ideal is never dense — a statement that survives the passage to A ⧸ J, where it says that the separated quotient of A ⧸ J is nonzero.

Why this does not assume a linear topology #

TauCeti.Topology.Algebra.Nonarchimedean.MaximalIdeals proves the openness of maximal ideals, and everything in it carries [IsLinearTopology A A] — a basis of neighbourhoods of zero consisting of ideals. That is not incidental. An open ideal of a Tate ring is the whole ring (TauCeti.Huber.IsTateRing.isOpen_iff_eq_top), so no proper ideal of a nonzero Tate ring is open and the results in that file are adic-only; over ℚ_p, IsTopologicallyNilpotent.mem_of_isMaximal would otherwise put p in the zero ideal.

Closedness carries no such hypothesis, so it is available for every complete Huber ring, Tate ones included. Getting there does take a different argument from the linear-topology one — see the Provenance section — but the resulting statements are hypothesis-free, which is what makes this the form of Proposition 7.51 that survives the Tate case.

Main results #

Provenance #

Adapted from AINTLIB (see References), section OpenUnits of the source file, where the statement is isOpen_units_of_isOpen_topologicallyNilpotent. (That file's other half, the closedness argument, is carried over in TauCeti.Topology.Algebra.Ring.MaximalIdeals.)

The openness argument is not taken over verbatim, and the difference is the point of this file. AINTLIB covers a unit u by the additive translate u + A°°, which forces it to rewrite u + a = u * (1 + u⁻¹a) and to know that u⁻¹a is again topologically nilpotent — that is IsTopologicallyNilpotent.mul_left, which Mathlib states only under [IsLinearTopology R R], so AINTLIB carries that hypothesis. It is not removable there: in a Tate ring A°° is not an ideal, and ℚ_p is a counterexample, with p topologically nilpotent but p⁻² * p = p⁻¹ not. The hypothesis is load bearing for that route, not an oversight.

The proof here covers u by the multiplicative neighbourhood {x : u⁻¹x - 1 ∈ A°°} instead. That needs only continuity of x ↦ u⁻¹x - 1 and the geometric series, never that A°° absorbs multiplication, so it holds with no linear-topology hypothesis at all and therefore applies to Tate rings. Separately, this repository already has TauCeti.Huber.isOpen_setOf_isTopologicallyNilpotent, so AINTLIB's A°°-openness hypothesis is discharged rather than carried, and the Huber-level statements need no side conditions.

References #

source
theorem TauCeti.Huber.isOpen_setOf_isUnit {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [IsHuberRing A] :
IsOpen {a : A | IsUnit a}

The unit group of a complete Huber ring is open.

source
theorem TauCeti.Huber.isClosed_of_isMaximal {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [IsHuberRing A] (𝔪 : Ideal A) [𝔪.IsMaximal] :
IsClosed ↑𝔪

Wedhorn Proposition 7.51, closedness half: every maximal ideal of a complete Huber ring is closed. Wedhorn states it for a complete affinoid ring; the affinoid A⁺ plays no part in the argument, so the plus subring is absent here.

source
theorem TauCeti.Huber.one_notMem_closure_zero_quotient_of_ne_top {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsTopologicalRing A] [IsUniformAddGroup A] [IsHuberRing A] {J : Ideal A} (hJ : J ≠ ⊤) :
1 ∉ closure {0}

The separated quotient of A ⧸ J is nonzero for every proper ideal J of a complete Huber ring.