The p-adic numbers are a Tate ring

ℚ_[p] is a Tate ring, with (ℤ_[p], (p)) as a pair of definition and p as a pseudouniformiser. Together with TauCeti.Huber.PadicInt.not_isTateRing this is the roadmap's Layer-0 example separating the two notions: the same ideal of definition makes ℤ_[p] Huber but not Tate, and ℚ_[p] Tate, the difference being that p becomes a unit in ℚ_[p].

No Ideal.comap is needed here. Mathlib's ℤ_[p] is the subtype {x : ℚ_[p] // ‖x‖ ≤ 1} and PadicInt.subring p is a separate declaration cutting out the same set, so ℤ_[p] and ↥(PadicInt.subring p) are definitionally equal. That is why idealOfDefinition := maximalIdeal ℤ_[p] typechecks against the expected Ideal ↥(PadicInt.subring p) below.

Main definitions

• TauCeti.Huber.Padic.pairOfDefinition: the pair of definition (ℤ_[p], (p)) of ℚ_[p].

Main results

• TauCeti.Huber.Padic.pairOfDefinition_ringOfDefinition and TauCeti.Huber.Padic.mem_pairOfDefinition_idealOfDefinition: the two projections of the pair. The ring of definition is pinned down by an equation, the ideal of definition by the membership form ‖x‖ < 1 — see the note on that lemma for why.
• TauCeti.Huber.Padic.isPseudoUniformizer_p: p is a pseudouniformiser of ℚ_[p].
• TauCeti.Huber.Padic.isHuberRing and TauCeti.Huber.Padic.isTateRing: ℚ_[p] is a Huber ring, and a Tate ring.

References

• Wedhorn, Adic Spaces, §6, where Huber and Tate rings are introduced (Proposition and Definition 6.1) and ℚ_[p] is the standard example of a Tate ring.

theorem TauCeti.Huber.Padic.isPseudoUniformizer_p {p : ℕ} [Fact (Nat.Prime p)] : IsPseudoUniformizer ↑p

p is a pseudouniformiser of ℚ_[p]: it is a unit, and its powers have norm p⁻ⁿ → 0.

noncomputable def TauCeti.Huber.Padic.pairOfDefinition {p : ℕ} [Fact (Nat.Prime p)] : PairOfDefinition ℚ_[p]

The pair of definition (ℤ_[p], (p)) exhibiting ℚ_[p] as a Huber ring.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Huber.Padic.pairOfDefinition_ringOfDefinition {p : ℕ} [Fact (Nat.Prime p)] : pairOfDefinition.ringOfDefinition = PadicInt.subring p

The ring of definition of pairOfDefinition is ℤ_[p].

The companion projection, the ideal of definition, is characterised by TauCeti.Huber.Padic.mem_pairOfDefinition_idealOfDefinition in membership form rather than by an equation; that lemma's docstring gives the reason.

@[simp]

theorem TauCeti.Huber.Padic.mem_pairOfDefinition_idealOfDefinition {p : ℕ} [Fact (Nat.Prime p)] {x : ↥pairOfDefinition.ringOfDefinition} : x ∈ pairOfDefinition.idealOfDefinition ↔ ‖↑x‖ < 1

The ideal of definition of pairOfDefinition is (p), in membership form: an element belongs exactly when its norm is less than one.

The membership form is used because the equation pairOfDefinition.idealOfDefinition = maximalIdeal ℤ_[p] does not elaborate. The two sides are definitionally equal — marking pairOfDefinition @[expose] makes that very statement typecheck and closes it by rfl — but at the transparency the elaborator uses it will not unfold a definition whose body is unexposed, so checking Ideal ℤ_[p] against Ideal ↥pairOfDefinition.ringOfDefinition fails with the note that pairOfDefinition "was not unfolded because their definition is not exposed". This is a limit on elaboration, not a statement that the projection cannot reduce. Exposing the body is not worth it here, since it would force the proof-only isOpen_padicIntSubring public too; membership sidesteps the issue entirely, as x already inhabits the dependent type.

instance TauCeti.Huber.Padic.isHuberRing {p : ℕ} [Fact (Nat.Prime p)] : IsHuberRing ℚ_[p]

ℚ_[p] is a Huber ring, with (ℤ_[p], (p)) as a pair of definition.

instance TauCeti.Huber.Padic.isTateRing {p : ℕ} [Fact (Nat.Prime p)] : IsTateRing ℚ_[p]

ℚ_[p] is a Tate ring, with p as a pseudouniformiser.