The formal Laurent series field is a Tate ring

For a field K the formal Laurent series K⸨X⸩, with the X-adic topology of Mathlib's LaurentSeries.valued instance, are a Tate ring: the power series are an open subring, the ideal (X) is a finitely generated ideal of definition, and X itself is a pseudouniformiser.

K⸨X⸩ is the equal-characteristic Tate example of the roadmap's Layer-0 Examples row.

Main definitions

• TauCeti.Huber.LaurentSeries.idealOfDefinition: the ideal (X) of K⟦X⟧ ⊆ K⸨X⸩.
• TauCeti.Huber.LaurentSeries.pairOfDefinition: the pair of definition (K⟦X⟧, (X)).

Main results

• TauCeti.Huber.LaurentSeries.mem_idealOfDefinition_pow_iff: membership of (X)ⁿ is the valuation bound v f ≤ exp (-n). isAdic_idealOfDefinition and mem_pairOfDefinition_idealImage are read off it; the openness of the ring of definition and the topological nilpotence of X come from Mathlib's valuation API instead.
• TauCeti.Huber.LaurentSeries.isPseudoUniformizer_X: X is a pseudouniformiser.
• TauCeti.Huber.LaurentSeries.isHuberRing and TauCeti.Huber.LaurentSeries.isTateRing.

Implementation notes

The ring of definition is not built by hand: LaurentSeries.val_le_one_iff_eq_coe says that a Laurent series has valuation at most one exactly when it is a power series, so Mathlib's LaurentSeries.powerSeries_as_subring is the valuation subring and is open by Valued.isOpen_integer.

The neighbourhood API of a Valued ring is phrased in the value group ValueGroup₀ v rather than in Γ₀, so the two private lemmas below convert once, in each direction, between that form and the ℤᵐ⁰ bounds the rest of the file uses.

Provenance

New work; the roadmap names no source for this row.

References

• Wedhorn, Adic Spaces, §6, where Huber and Tate rings are introduced (Proposition and Definition 6.1) and F⸨t⸩ is the standard equal-characteristic example of a Tate ring.

theorem TauCeti.Huber.LaurentSeries.coe_powerSeries_as_subring (K : Type u_1) [Field K] : ↑(LaurentSeries.powerSeries_as_subring K) = ↑Valued.v.integer

The power series inside K⸨X⸩ are exactly the elements of valuation at most one.

theorem TauCeti.Huber.LaurentSeries.isOpen_powerSeries_as_subring (K : Type u_1) [Field K] : IsOpen ↑(LaurentSeries.powerSeries_as_subring K)

The ring of definition is open, being the valuation subring.

theorem TauCeti.Huber.LaurentSeries.powerSeries_as_subring_eq_integer (K : Type u_1) [Field K] : LaurentSeries.powerSeries_as_subring K = Valued.v.integer

The power series are the valuation subring of K⸨X⸩, as subrings.

theorem TauCeti.Huber.LaurentSeries.integers_powerSeries_as_subring (K : Type u_1) [Field K] : Valued.v.Integers ↥(LaurentSeries.powerSeries_as_subring K)

The power series are the valuation integers of K⸨X⸩, packaged as Valuation.Integers. This is Mathlib's Valuation.integer.integers transported along TauCeti.Huber.LaurentSeries.powerSeries_as_subring_eq_integer, and is what lets the divisibility/valuation dictionary Valuation.Integers.dvd_iff_le apply to (X)ⁿ directly.

noncomputable def TauCeti.Huber.LaurentSeries.subringX (K : Type u_1) [Field K] : ↥(LaurentSeries.powerSeries_as_subring K)

The variable X, viewed inside the ring of definition K⟦X⟧ ⊆ K⸨X⸩.

Equations

• TauCeti.Huber.LaurentSeries.subringX K = (LaurentSeries.powerSeriesEquivSubring K) PowerSeries.X

@[simp]

theorem TauCeti.Huber.LaurentSeries.coe_subringX (K : Type u_1) [Field K] : ↑(subringX K) = (HahnSeries.ofPowerSeries ℤ K) PowerSeries.X

noncomputable def TauCeti.Huber.LaurentSeries.idealOfDefinition (K : Type u_1) [Field K] : Ideal ↥(LaurentSeries.powerSeries_as_subring K)

The ideal of definition (X) of K⟦X⟧ ⊆ K⸨X⸩.

Equations

• TauCeti.Huber.LaurentSeries.idealOfDefinition K = Ideal.span {TauCeti.Huber.LaurentSeries.subringX K}

theorem TauCeti.Huber.LaurentSeries.idealOfDefinition_def (K : Type u_1) [Field K] : idealOfDefinition K = Ideal.span {subringX K}

Unfolding lemma for TauCeti.Huber.LaurentSeries.idealOfDefinition.

@[simp]

theorem TauCeti.Huber.LaurentSeries.mem_idealOfDefinition_pow_iff {K : Type u_1} [Field K] (n : ℕ) (f : ↥(LaurentSeries.powerSeries_as_subring K)) : f ∈ idealOfDefinition K ^ n ↔ Valued.v ↑f ≤ WithZero.exp (-↑n)

The bridge to the valuation: a power series lies in (X)ⁿ exactly when its valuation is at most exp (-n).

theorem TauCeti.Huber.LaurentSeries.isAdic_idealOfDefinition (K : Type u_1) [Field K] : IsAdic (idealOfDefinition K)

The subspace topology on K⟦X⟧ ⊆ K⸨X⸩ is the X-adic topology.

noncomputable def TauCeti.Huber.LaurentSeries.pairOfDefinition (K : Type u_1) [Field K] : PairOfDefinition (LaurentSeries K)

The pair of definition (K⟦X⟧, (X)) of K⸨X⸩.

Equations

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

@[simp]

theorem TauCeti.Huber.LaurentSeries.pairOfDefinition_ringOfDefinition (K : Type u_1) [Field K] : (pairOfDefinition K).ringOfDefinition = LaurentSeries.powerSeries_as_subring K

The ring of definition of TauCeti.Huber.LaurentSeries.pairOfDefinition is the power series.

The ideal is characterised in membership form by TauCeti.Huber.LaurentSeries.mem_pairOfDefinition_idealOfDefinition_pow_iff. An equation is avoided rather than impossible: idealOfDefinition's type depends on ringOfDefinition, so an equation would be between two Ideal types that the elaborator identifies only through that projection.

@[simp]

theorem TauCeti.Huber.LaurentSeries.mem_pairOfDefinition_idealOfDefinition_pow_iff (K : Type u_1) [Field K] {n : ℕ} {f : ↥(pairOfDefinition K).ringOfDefinition} : f ∈ (pairOfDefinition K).idealOfDefinition ^ n ↔ Valued.v ↑f ≤ WithZero.exp (-↑n)

The ideal of definition of pairOfDefinition is (X), in membership form.

The membership form is used because idealOfDefinition's type depends on the pair's ringOfDefinition; f is already taken in that dependent type, so nothing has to be transported.

theorem TauCeti.Huber.LaurentSeries.mem_pairOfDefinition_idealImage (K : Type u_1) [Field K] (n : ℕ) (f : LaurentSeries K) : f ∈ (pairOfDefinition K).idealImage n ↔ Valued.v f ≤ WithZero.exp (-↑n)

The pair of definition is (K⟦X⟧, (X)), said without touching the dependent field: PairOfDefinition.idealImage n is the image of (X)ⁿ in K⸨X⸩, so it can be compared with a valuation bound directly.

Deliberately not @[simp]: PairOfDefinition.mem_idealImage is itself a simp lemma, so simp rewrites this left-hand side further, to an existential over the subring, and the simpNF linter rejects the attribute. Rewrite with this lemma explicitly.

theorem TauCeti.Huber.LaurentSeries.isPseudoUniformizer_X (K : Type u_1) [Field K] : IsPseudoUniformizer ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X)

X is a pseudouniformiser of K⸨X⸩: it is a unit, since K⸨X⸩ is a field, and v (Xⁿ) = exp (-n) tends to zero.

instance TauCeti.Huber.LaurentSeries.isHuberRing (K : Type u_1) [Field K] : IsHuberRing (LaurentSeries K)

K⸨X⸩ is a Huber ring, with (K⟦X⟧, (X)) as a pair of definition.

instance TauCeti.Huber.LaurentSeries.isTateRing (K : Type u_1) [Field K] : IsTateRing (LaurentSeries K)

K⸨X⸩ is a Tate ring: X is a pseudouniformiser.