Weighted restricted power series A⟨X⟩_T

For a commutative nonarchimedean ring A and a family T of subsets of A indexed by the variables, Wedhorn defines the weighted restricted power series ring

A⟨X⟩_T := { ∑ aν Xν ∈ A[[X]] | aν ∈ Tν · U for every open subgroup U of A and almost all ν },

with the subgroups U⟨X⟩ := { ∑ aν Xν ∈ A⟨X⟩_T | aν ∈ Tν · U for all ν } as a fundamental system of neighbourhoods of zero. Here Tν := T₁^ν₁ ⋯ Tₖ^νₖ. Taking every Tᵢ = {1} recovers the ordinary restricted series A⟨X⟩.

Both of those claims need Wedhorn's standing hypothesis TauCeti.Huber.IsWeightFamily T, fixed at the start of his §5.6: without it A⟨X⟩_T is not multiplicatively closed and the U⟨X⟩ are not neighbourhoods of zero. The subring and topology constructions (weightedRestrictedSubring, weightedNhd, weightedTopology and the maps into them) therefore take it as an argument; the underlying weight operations weightPow and weightMul and the predicate IsWeightedRestricted do not, since they are defined for any family. The counterexample in IsWeightFamily's docstring shows the hypothesis is not automatic.

Main definitions

• TauCeti.Huber.weightPow: the subset Tν = T₁^ν₁ ⋯ Tₖ^νₖ of A.
• TauCeti.Huber.weightMul: the additive subgroup Tν · U.
• TauCeti.Huber.IsWeightFamily: Wedhorn's standing hypothesis on T — for every variable i, every m and every neighbourhood U of zero, the subgroup Tᵢ^m · U is again one. The subring and the topology below are defined only under it.
• TauCeti.Huber.IsWeightedRestricted: Wedhorn's condition (5.6.1) on a power series.
• TauCeti.Huber.weightedRestrictedSubring: A⟨X⟩_T as a subring of A[[X]].
• TauCeti.Huber.weightedNhd: the subgroup U⟨X⟩ of A⟨X⟩_T.
• TauCeti.Huber.weightedTopology: the ring topology they generate. A⟨X⟩_T also carries the group uniformity of that topology, with its IsUniformAddGroup and UniformContinuousConstSMul instances, so that its separated completion can be formed.
• TauCeti.Huber.weightedC and TauCeti.Huber.weightedX: the constant series and the variables. TauCeti.Huber.weightedC_injective, with its simp form TauCeti.Huber.weightedC_inj, reads a constant series off its coefficient in degree 0; TauCeti.Huber.algebraMap_weightedRestrictedSubring_injective and its product counterpart state the resulting injectivity for the canonical algebra maps.
• TauCeti.Huber.weightedMap: the morphism A⟨X⟩_T → B⟨X⟩_S induced by a continuous ring map carrying each weight into the corresponding one; continuous_weightedMap makes it a morphism of topological rings, and weightedMap_id with weightedMap_comp are the functor laws.

Main results

• TauCeti.Huber.IsWeightFamily.of_exists_isOpenMap_mul, with TauCeti.Huber.IsWeightFamily.of_exists_isUnit and TauCeti.Huber.IsWeightFamily.of_forall_openAddSubgroup: the three ways to supply the standing hypothesis. The first assumes multiplication by an element of Tᵢ is an open map.
• TauCeti.Huber.IsWeightedRestricted.mul: A⟨X⟩_T is closed under multiplication, the point Wedhorn flags as not entirely clear; with the additive closure lemmas this gives the subring. TauCeti.Huber.IsWeightedRestricted.finite_coeff_notMem restates the predicate as finiteness of the exceptional set of coefficients.
• TauCeti.Huber.weightedNhd_subgroups_basis: the U⟨X⟩ are a fundamental system of neighbourhoods of zero for a ring topology, with its contract (hasBasis_nhds_zero_weightedTopology, isTopologicalRing_weightedTopology, nonarchimedeanRing_weightedTopology, continuous_weightedC). TauCeti.Huber.weightedC_mem_weightedNhd records that a constant series meets the U bound exactly when its value does, and TauCeti.Huber.isOpen_weightedNhd that U⟨X⟩ is open whenever U is.
• TauCeti.Huber.weightedRestrictedSubring_one_weight: for the trivial weight this is the ordinary ring of restricted power series (Wedhorn Example 5.54), with TauCeti.Huber.subringCongr_one_weight_weightedX and TauCeti.Huber.subringCongr_one_weight_weightedC saying where that identification sends the generators — to restrictedX and to the algebra map.
• TauCeti.Huber.weightedPolynomials, the polynomials as a subring of A⟨X⟩_T, with mem_weightedPolynomials_iff identifying it with finite support and the generators weightedC/weightedX in it; TauCeti.Huber.dense_weightedPolynomials is Wedhorn 5.49(1), read off the predicate-level exists_mvPolynomial_forall_coeff_sub_mem.
• TauCeti.Huber.weightedPolynomialEquiv, with discreteTopology_weightedRestrictedSubring and weightedPolynomials_eq_top: over a discrete ring the weighted topology is discrete and A⟨X⟩_T is exactly the polynomial ring.
• TauCeti.Huber.weightedRestrictedSubring_fin_zero and TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv, with continuous_weightedRestrictedSubringFinZeroEquiv and its _symm: in no variables every series is restricted, so A⟨X⟩_T is A — and topologically so, since the index Fin 0 →₀ ℕ is a singleton and the basic neighbourhood is cut out by that one coefficient. All of them are stated for an arbitrary T : Fin 0 → Set A and take no weight-family hypothesis: TauCeti.Huber.isWeightFamily_fin_zero supplies it, the condition being a statement about each index and there being none.
• TauCeti.Huber.IsWeightedRestricted.map, with RingHom.weightMul_map_le and image_weightPow: restrictedness is preserved by a continuous ring map carrying each T i into S i. This is what weightedMap is built from; weightedMap_weightedX says it fixes the variables, while weightedMap_weightedC says it acts as φ on constants — the constants are moved, not fixed. weightedMap_id and weightedMap_comp are the functor laws.
• TauCeti.Huber.IsWeightFamily.image: a continuous open ring map carries a weight family to a weight family.

Scope

Wedhorn states (5.6.1) for an arbitrary index set I. This file formalises the finite-variable case I = Fin k. The product defining the weight therefore runs over all variables.

Implementation notes

Tν · U is read as the additive subgroup generated by the products t * u, not as the pointwise product set. Wedhorn's own statement forces this: he asserts that the U⟨X⟩ are a fundamental system of neighbourhoods of zero for a ring topology, so each must be an additive subgroup, and the pointwise set {t * u} is not closed under addition.

The predicate carries no nonarchimedean hypothesis, matching (5.6.1), but it only means coefficient convergence when the open additive subgroups are a neighbourhood basis of zero — the setting Wedhorn works in throughout §5.6. Without that it can be vacuous: over ℝ with its usual topology the only open additive subgroup is ℝ itself, so every power series is T-restricted for the trivial weight. TauCeti.Huber.isWeightedRestricted_one_weight_iff therefore assumes NonarchimedeanAddGroup — the additive condition is what rules that vacuity out, and no multiplicative structure of the topology enters its proof.

If some Tᵢ is empty and νᵢ > 0 then Tν is empty and Tν · U = ⊥, so all but finitely many such coefficients must vanish; the closure lemmas below need no nonemptiness hypothesis.

This construction is not the same as retopologising the ordinary A⟨X⟩ by transporting along a substitution X ↦ f X: there the weight multiplies the coefficient rather than the neighbourhood, and the carrier does not vary with T. Here the carrier itself depends on T.

Nor is it Mathlib's MvPowerSeries.IsRestricted, despite that also being a weighted condition. Mathlib weights by a polyradius c : σ → ℝ over a normed ring, asking that ‖coeff t f‖ * ∏ i, c i ^ t i tend to 0 along the cofinite filter. A Huber ring's topology is nonarchimedean but in general carries no norm, so no polyradius is available to state that condition, and the weight family here is a family of subsets Tᵢ ⊆ A acting on neighbourhood subgroups rather than a family of reals scaling coefficient norms. The two do agree at the trivial weight when the norm is ultrametric: the balls {a | ‖a‖ < r} are then additive subgroups, and every open subgroup contains one, so quantifying over all open subgroups is the same as quantifying over the balls and the condition becomes ‖coeff ν f‖ → 0 along the cofinite filter. Over a general normed ring they do not agree: over ℝ, as above, the condition here is vacuous while Mathlib's still asks for ‖coeff ν f‖ → 0. The unweighted predicate of TauCeti/RingTheory/Huber/Restricted/PowerSeries.lean is a topological limit rather than a condition on subgroups, and that file remarks on the comparison for it — in prose, not as a proved declaration. Neither notion is a special case of the other in general.

The finite-family absorption fact the multiplicative arguments run on — finitely many fixed elements are absorbed into their own targets by a single open subgroup — mentions no weight, so it lives in TauCeti/Topology/Algebra/Nonarchimedean/Absorption.lean, built on Mathlib's single-element NonarchimedeanRing.left_mul_subset.

Closure of A⟨X⟩_T under multiplication is the one non-obvious point of the construction — Wedhorn writes "note that it is not entirely clear that A⟨X⟩_T is multiplicatively closed" — and is TauCeti.Huber.IsWeightedRestricted.mul here. It is exactly what the standing hypothesis is for.

Provenance

The construction differs from AINTLIB's TateAlgebraWedhorn, which retopologises the ordinary A⟨X⟩ by transporting along a substitution rather than letting the carrier depend on T.

The proofs, however, follow TauCeti/RingTheory/Huber/Restricted/PowerSeries.lean (TauCetiProject/TauCeti#2348), which is itself AINTLIB-derived — and not only in API layout. In particular TauCeti.Huber.IsWeightedRestricted.mul follows the plan of IsRestricted.mul there: choose W with W · W ⊆ U; take the finite sets of coefficients of f and g that fail the W bound; find one open subgroup absorbing those finitely many bad coefficients into the target; rule out the exceptional index set (F + G_Z) ∪ (F_Z + G); and split each antidiagonal term by whether neither, or exactly one, of its factors is bad.

What is new there is the weighting, and it is not cosmetic: the target Tν · U varies with the index, so the absorbing subgroup has to work against a family of targets — which is what TauCeti.Huber.IsWeightFamily is for and what NonarchimedeanRing.exists_openAddSubgroup_forall_mul_subset was factored out to supply — and the trichotomy has to land in Tα · U and Tβ · U separately before mul_mem_weightMul_add recombines them at α + β. The unweighted proof needs none of that.

The API layout — the isWeightedRestricted_zero/one/add/neg/mul series, the subring with its mem_ lemma, and the algebra-map coercion — follows the same file.

References

• T. Wedhorn, Adic Spaces, Remark and Definition 5.48, equation (5.6.1), Proposition 5.49(1) for the density of the polynomials, and Example 5.54 for the case Tᵢ = {1}.

Weights and weighted subgroups

def TauCeti.Huber.weightPow {k : ℕ} {A : Type u_1} [CommMonoid A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) : Set A

The weight Tν = T₁^ν₁ ⋯ Tₖ^νₖ attached to a multi-index, as a subset of A.

Equations

• TauCeti.Huber.weightPow T ν = ∏ i : Fin k, T i ^ ν i

theorem TauCeti.Huber.weightPow_def {k : ℕ} {A : Type u_1} [CommMonoid A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) : weightPow T ν = ∏ i : Fin k, T i ^ ν i

Unfolding lemma for TauCeti.Huber.weightPow.

theorem TauCeti.Huber.weightPow_mono {k : ℕ} {A : Type u_1} [CommMonoid A] {T S : Fin k → Set A} (h : ∀ (i : Fin k), T i ⊆ S i) (ν : Fin k →₀ ℕ) : weightPow T ν ⊆ weightPow S ν

The weight is monotone in the family.

@[simp]

theorem TauCeti.Huber.weightPow_zero {k : ℕ} {A : Type u_1} [CommMonoid A] (T : Fin k → Set A) : weightPow T 0 = 1

At the zero multi-index every factor is T i ^ 0 = 1, so the weight is the trivial set 1 = {1}.

theorem TauCeti.Huber.weightPow_add {k : ℕ} {A : Type u_1} [CommMonoid A] (T : Fin k → Set A) (α β : Fin k →₀ ℕ) : weightPow T (α + β) = weightPow T α * weightPow T β

Weights are multiplicative in the multi-index: T^(α+β) = T^α · T^β.

theorem TauCeti.Huber.weightPow_single {k : ℕ} {A : Type u_1} [CommMonoid A] (T : Fin k → Set A) (i : Fin k) (m : ℕ) : weightPow T (Finsupp.single i m) = T i ^ m

At a single-variable multi-index the weight is the corresponding power: T^(single i m) is Tᵢ ^ m.

@[simp]

theorem TauCeti.Huber.weightPow_one_weight {k : ℕ} {A : Type u_1} [CommMonoid A] (ν : Fin k →₀ ℕ) : weightPow (fun (x : Fin k) => {1}) ν = {1}

With every weight equal to {1}, the weight of any multi-index is {1}.

theorem TauCeti.Huber.image_weightPow {k : ℕ} {A : Type u_1} [CommMonoid A] {F : Type u_2} {B : Type u_3} [CommMonoid B] [FunLike F A B] [MonoidHomClass F A B] (φ : F) (T : Fin k → Set A) (ν : Fin k →₀ ℕ) : ⇑φ '' weightPow T ν = weightPow (fun (i : Fin k) => ⇑φ '' T i) ν

A monoid homomorphism carries the weight Tν onto the weight of the image family.

def TauCeti.Huber.weightMul {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) (U : AddSubgroup A) : AddSubgroup A

The additive subgroup generated by the products t * u with t ∈ Tν and u ∈ U. See the module docstring: the subgroup, not the pointwise product set, is what Wedhorn's statement requires.

Equations

• TauCeti.Huber.weightMul T ν U = AddSubgroup.closure (TauCeti.Huber.weightPow T ν * ↑U)

theorem TauCeti.Huber.weightMul_def {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) (U : AddSubgroup A) : weightMul T ν U = AddSubgroup.closure (weightPow T ν * ↑U)

Tν · U is the subgroup generated by the products t * u.

theorem TauCeti.Huber.mul_mem_weightMul {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) (U : AddSubgroup A) {t u : A} (ht : t ∈ weightPow T ν) (hu : u ∈ U) : t * u ∈ weightMul T ν U

Introduction for weightMul: a product of a weight element and a U element lies in it.

theorem TauCeti.Huber.weightMul_le {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {ν : Fin k →₀ ℕ} {U V : AddSubgroup A} : weightMul T ν U ≤ V ↔ ∀ t ∈ weightPow T ν, ∀ u ∈ U, t * u ∈ V

Elimination for weightMul: it is the least subgroup containing those products.

theorem TauCeti.Huber.mul_mem_of_forall_mul_mul_mem {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {ν : Fin k →₀ ℕ} {U V : AddSubgroup A} {a x : A} (h : ∀ t ∈ weightPow T ν, ∀ u ∈ U, a * (t * u) ∈ V) (hx : x ∈ weightMul T ν U) : a * x ∈ V

Elimination through a multiplication. To land the whole of a * (Tν · U) inside a subgroup V it is enough to land the generators a * (t * u). This is TauCeti.Huber.weightMul_le read in V.comap (AddMonoidHom.mulLeft a).

@[simp]

theorem TauCeti.Huber.weightMul_zero {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (U : AddSubgroup A) : weightMul T 0 U = U

At the zero multi-index the weight is trivial, so T⁰ · U is just U; in particular it is a neighbourhood of zero whenever U is.

@[simp]

theorem TauCeti.Huber.weightMul_bot {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) : weightMul T ν ⊥ = ⊥

Weighting the zero subgroup gives the zero subgroup.

theorem TauCeti.Huber.weightMul_mono {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (ν : Fin k →₀ ℕ) {U V : AddSubgroup A} (h : U ≤ V) : weightMul T ν U ≤ weightMul T ν V

Tν · U is monotone in U.

theorem TauCeti.Huber.mul_mem_weightMul_add {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {α β : Fin k →₀ ℕ} {V W : AddSubgroup A} {x y : A} (hx : x ∈ weightMul T α V) (hy : y ∈ weightMul T β W) : x * y ∈ weightMul T (α + β) (AddSubgroup.closure (↑V * ↑W))

A product of an element of T^α · V with an element of T^β · W lies in T^(α+β) · (V · W).

theorem TauCeti.Huber.mul_mem_weightMul_of_mul_subset {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {α β ν : Fin k →₀ ℕ} (hν : α + β = ν) {W U : AddSubgroup A} (hWU : ↑W * ↑W ⊆ ↑U) {a b : A} (ha : a ∈ weightMul T α W) (hb : b ∈ weightMul T β W) : a * b ∈ weightMul T ν U

The unexceptional term of a convolution. If W · W ⊆ U, then a product of an element of Tα · W with an element of Tβ · W lies in Tν · U whenever α + β = ν.

theorem TauCeti.Huber.mul_mem_weightMul_add_of_mem_weightPow {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {α β : Fin k →₀ ℕ} {U : AddSubgroup A} {t x : A} (ht : t ∈ weightPow T β) (hx : x ∈ weightMul T α U) : t * x ∈ weightMul T (α + β) U

Multiplying by a weight element shifts the multi-index: T^β · (T^α · U) ⊆ T^(α+β) · U.

theorem TauCeti.Huber.weightMul_add_eq {k : ℕ} {A : Type u_1} [CommRing A] (T : Fin k → Set A) (α β : Fin k →₀ ℕ) (U : AddSubgroup A) : weightMul T (α + β) U = AddSubgroup.closure (weightPow T α * ↑(weightMul T β U))

Splitting a multi-index splits the weight subgroup: T^(α+β) · U is generated by T^α against T^β · U.

theorem TauCeti.Huber.mul_mem_weightMul_of_forall_mul_mem {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {α β : Fin k →₀ ℕ} {U Z : AddSubgroup A} {a b : A} (ha : ∀ z ∈ Z, a * z ∈ weightMul T α U) (hb : b ∈ weightMul T β Z) : a * b ∈ weightMul T (α + β) U

The absorption step. If multiplication by a carries the subgroup Z into T^α · U, then it carries all of T^β · Z into T^(α+β) · U.

@[simp]

theorem TauCeti.Huber.weightMul_one_weight {k : ℕ} {A : Type u_1} [CommRing A] (ν : Fin k →₀ ℕ) (U : AddSubgroup A) : weightMul (fun (x : Fin k) => {1}) ν U = U

With every weight equal to {1}, the subgroup Tν · U is U itself.

theorem TauCeti.Huber.coeff_mul_mem_weightMul {k : ℕ} {A : Type u_1} [CommRing A] {T : Fin k → Set A} {V W : AddSubgroup A} {f g : MvPowerSeries (Fin k) A} (hf : ∀ (α : Fin k →₀ ℕ), (MvPowerSeries.coeff α) f ∈ weightMul T α V) (hg : ∀ (β : Fin k →₀ ℕ), (MvPowerSeries.coeff β) g ∈ weightMul T β W) (ν : Fin k →₀ ℕ) : (MvPowerSeries.coeff ν) (f * g) ∈ weightMul T ν (AddSubgroup.closure (↑V * ↑W))

If every coefficient of f meets the V bound and every coefficient of g meets the W bound, then every coefficient of f * g meets the V · W bound. Unlike TauCeti.Huber.IsWeightedRestricted.mul there are no exceptional coefficients.

def TauCeti.Huber.IsWeightFamily {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) : Prop

Wedhorn's standing hypothesis on the weight family, fixed at the start of his §5.6: for every variable i, every m, and every neighbourhood U of zero, the subgroup Tᵢ^m · U is again a neighbourhood of zero.

Without it A⟨X⟩_T is not multiplicatively closed. Take A = ℚ_p⟨Y, Z⟩, T = {Y}, f = Z X and g = ∑ₙ Yⁿ pⁿ Xⁿ: both are T-restricted, but the Xᵏ coefficient of f * g is Z Yᵏ⁻¹ pᵏ⁻¹, which never lies in Tᵏ · A = Yᵏ A. Note that there A is complete, Tate and Huber and T is finite, bounded and power-bounded — so none of those conditions substitute for this one. What fails is exactly that Y A is not open.

Equations

• TauCeti.Huber.IsWeightFamily T = ∀ (i : Fin k) (m : ℕ), ∀ U ∈ nhds 0, ↑(AddSubgroup.closure (T i ^ m * U)) ∈ nhds 0

theorem TauCeti.Huber.isWeightFamily_iff {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} : IsWeightFamily T ↔ ∀ (i : Fin k) (m : ℕ), ∀ U ∈ nhds 0, ↑(AddSubgroup.closure (T i ^ m * U)) ∈ nhds 0

Unfolding lemma for TauCeti.Huber.IsWeightFamily.

theorem TauCeti.Huber.IsWeightFamily.of_exists_isOpenMap_mul {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} (h : ∀ (i : Fin k), ∃ t ∈ T i, IsOpenMap fun (x : A) => t * x) : IsWeightFamily T

The openness form of the standing hypothesis. If some element of each T i multiplies open sets to open sets, the family is a weight family.

Openness of the subgroup generated by Tᵢ · A alone does not supply the neighbourhood condition for arbitrarily small U. An open multiplication map supplies it directly, as does a unit acting continuously in TauCeti.Huber.IsWeightFamily.of_exists_isUnit.

theorem TauCeti.Huber.IsWeightFamily.of_exists_isUnit {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [ContinuousConstSMul Aˣ A] {T : Fin k → Set A} (hu : ∀ (i : Fin k), ∃ t ∈ T i, IsUnit t) : IsWeightFamily T

Wedhorn's automatic case: the standing hypothesis holds as soon as each weight contains a unit.

One unit per index suffices; no conditions are imposed on the other elements of T i.

Only multiplication by units needs to be continuous: each such multiplication is then a homeomorphism, with inverse multiplication by the inverse unit.

theorem TauCeti.Huber.isWeightFamily_one_weight {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] : IsWeightFamily fun (x : Fin k) => {1}

Wedhorn: the standing hypothesis is automatic when every Tᵢ is {1}, the important special case, since then Tᵢ^m · U is the subgroup generated by U.

def TauCeti.Huber.IsWeightedRestricted {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) (f : MvPowerSeries (Fin k) A) : Prop

Wedhorn (5.6.1): a power series is T-restricted if, for every open subgroup U of A, all but finitely many of its coefficients lie in Tν · U.

Equations

• TauCeti.Huber.IsWeightedRestricted T f = ∀ (U : OpenAddSubgroup A), ∀ᶠ (ν : Fin k →₀ ℕ) in Filter.cofinite, (MvPowerSeries.coeff ν) f ∈ TauCeti.Huber.weightMul T ν ↑U

theorem TauCeti.Huber.isWeightedRestricted_iff {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} {f : MvPowerSeries (Fin k) A} : IsWeightedRestricted T f ↔ ∀ (U : OpenAddSubgroup A), ∀ᶠ (ν : Fin k →₀ ℕ) in Filter.cofinite, (MvPowerSeries.coeff ν) f ∈ weightMul T ν ↑U

Unfolding lemma for TauCeti.Huber.IsWeightedRestricted.

@[simp]

theorem TauCeti.Huber.isWeightedRestricted_zero {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) : IsWeightedRestricted T 0

The zero series is T-restricted.

@[simp]

theorem TauCeti.Huber.isWeightedRestricted_one {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) : IsWeightedRestricted T 1

The one series is T-restricted: every coefficient but the constant one vanishes.

theorem TauCeti.Huber.IsWeightFamily.weightMul_mem_nhds {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} (hT : IsWeightFamily T) (ν : Fin k →₀ ℕ) {U : AddSubgroup A} (hU : ↑U ∈ nhds 0) : ↑(weightMul T ν U) ∈ nhds 0

Wedhorn's derived hypothesis: from the per-variable assumption that each Tᵢ^m · U is a neighbourhood of zero it follows that Tν · U is one for every multi-index ν. Wedhorn states this in a sentence: "Then Tν U is a neighborhood of 0 for all ν".

theorem TauCeti.Huber.IsWeightFamily.of_forall_openAddSubgroup {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {T : Fin k → Set A} (h : ∀ (i : Fin k) (m : ℕ) (V : OpenAddSubgroup A), ↑(weightMul T (Finsupp.single i m) ↑V) ∈ nhds 0) : IsWeightFamily T

Over a nonarchimedean ring the standing hypothesis need only be checked on open subgroups: those are cofinal in the neighbourhoods of zero, and Tᵢ^m · V ≤ Tᵢ^m · U for V ⊆ U.

theorem TauCeti.Huber.IsWeightFamily.isOpen_weightMul {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] {T : Fin k → Set A} (hT : IsWeightFamily T) (ν : Fin k →₀ ℕ) {U : AddSubgroup A} (hU : ↑U ∈ nhds 0) : IsOpen ↑(weightMul T ν U)

The subgroups Tν · U are themselves open, so they can be fed back into TauCeti.Huber.IsWeightedRestricted, which quantifies over OpenAddSubgroup A.

theorem TauCeti.Huber.IsWeightFamily.isOpen_weightMul_top {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [SeparatelyContinuousAdd A] {T : Fin k → Set A} (hT : IsWeightFamily T) (i : Fin k) (m : ℕ) : IsOpen ↑(weightMul T (Finsupp.single i m) ⊤)

Each Tᵢ^m · A is an open additive subgroup of A: the U = ⊤ case of TauCeti.Huber.IsWeightFamily.isOpen_weightMul.

theorem TauCeti.Huber.isWeightedRestricted_one_weight_iff {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanAddGroup A] {f : MvPowerSeries (Fin k) A} : IsWeightedRestricted (fun (x : Fin k) => {1}) f ↔ Filter.Tendsto (fun (ν : Fin k →₀ ℕ) => (MvPowerSeries.coeff ν) f) Filter.cofinite (nhds 0)

Wedhorn Example 5.54: for the trivial weight Tᵢ = {1} the condition is the ordinary restrictedness of A⟨X⟩, that the coefficients tend to zero along the cofinite filter. This is the nontrivial witness that TauCeti.Huber.IsWeightedRestricted is not vacuous.

theorem TauCeti.Huber.isWeightedRestricted_of_finite_support {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) {f : MvPowerSeries (Fin k) A} (h : {ν : Fin k →₀ ℕ | (MvPowerSeries.coeff ν) f ≠ 0}.Finite) : IsWeightedRestricted T f

Anything with only finitely many nonzero coefficients is T-restricted, whatever the weight: the zero coefficients meet every bound. This is the source of all the polynomial constructors below.

@[simp]

theorem TauCeti.Huber.isWeightedRestricted_monomial {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) (μ : Fin k →₀ ℕ) (a : A) : IsWeightedRestricted T ((MvPowerSeries.monomial μ) a)

A monomial is T-restricted.

@[simp]

theorem TauCeti.Huber.isWeightedRestricted_C {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) (a : A) : IsWeightedRestricted T (MvPowerSeries.C a)

A constant series is T-restricted.

@[simp]

theorem TauCeti.Huber.isWeightedRestricted_X {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) (i : Fin k) : IsWeightedRestricted T (MvPowerSeries.X i)

Each variable is T-restricted.

theorem TauCeti.Huber.IsWeightedRestricted.add {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : IsWeightedRestricted T (f + g)

A sum of T-restricted series is T-restricted.

theorem TauCeti.Huber.IsWeightedRestricted.finite_coeff_notMem {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (U : OpenAddSubgroup A) : {ν : Fin k →₀ ℕ | (MvPowerSeries.coeff ν) f ∉ weightMul T ν ↑U}.Finite

Weighted restrictedness, restated: for every open additive subgroup U, only finitely many coefficients fail to lie in Tν · U.

theorem TauCeti.Huber.IsWeightedRestricted.mul {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {f g : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (hg : IsWeightedRestricted T g) : IsWeightedRestricted T (f * g)

A⟨X⟩_T is closed under multiplication (Wedhorn 5.48, the point he flags as "not entirely clear").

This is the substantive use of the standing hypothesis TauCeti.Huber.IsWeightFamily — the neighbourhood half, TauCeti.Huber.exists_weightedNhd_mul_mem, uses it too — and the docstring of that definition records what goes wrong without it.

theorem TauCeti.Huber.IsWeightedRestricted.neg {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : IsWeightedRestricted T (-f)

The negation of a T-restricted series is T-restricted.

The ring A⟨X⟩_T

def TauCeti.Huber.weightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : Subring (MvPowerSeries (Fin k) A)

Wedhorn's A⟨X⟩_T: the weighted restricted power series form a subring of A[[X]].

The weight family must satisfy Wedhorn's standing hypothesis (TauCeti.Huber.IsWeightFamily); without it the carrier is not closed under multiplication, and the docstring of that definition records the counterexample.

Equations

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

@[simp]

theorem TauCeti.Huber.mem_weightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {f : MvPowerSeries (Fin k) A} : f ∈ weightedRestrictedSubring T hT ↔ IsWeightedRestricted T f

Membership in A⟨X⟩_T is T-restrictedness.

noncomputable def TauCeti.Huber.weightedC {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : A →+* ↥(weightedRestrictedSubring T hT)

The constant-series embedding A → A⟨X⟩_T.

Equations

• TauCeti.Huber.weightedC T hT = MvPowerSeries.C.codRestrict (TauCeti.Huber.weightedRestrictedSubring T hT) ⋯

@[simp]

theorem TauCeti.Huber.coe_weightedC {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (a : A) : ↑((weightedC T hT) a) = MvPowerSeries.C a

theorem TauCeti.Huber.weightedC_injective {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : Function.Injective ⇑(weightedC T hT)

The constant-series embedding is injective: a constant series is read off as its coefficient in degree 0.

@[simp]

theorem TauCeti.Huber.weightedC_inj {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {a b : A} : (weightedC T hT) a = (weightedC T hT) b ↔ a = b

Equality of constant series is equality of constants: the iff form of TauCeti.Huber.weightedC_injective.

noncomputable def TauCeti.Huber.weightedX {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) (i : Fin k) : ↥(weightedRestrictedSubring T hT)

The variable Xᵢ, as an element of A⟨X⟩_T.

Equations

• TauCeti.Huber.weightedX T hT i = ⟨MvPowerSeries.X i, ⋯⟩

@[simp]

theorem TauCeti.Huber.coe_weightedX {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (i : Fin k) : ↑(weightedX T hT i) = MvPowerSeries.X i

@[instance_reducible]

noncomputable instance TauCeti.Huber.weightedRestrictedSubring.instAlgebra {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : Algebra A ↥(weightedRestrictedSubring T hT)

A⟨X⟩_T is an A-algebra, via the constant series.

Equations

• TauCeti.Huber.weightedRestrictedSubring.instAlgebra T hT = (TauCeti.Huber.weightedC T hT).toAlgebra

@[simp]

theorem TauCeti.Huber.algebraMap_weightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : algebraMap A ↥(weightedRestrictedSubring T hT) = weightedC T hT

The structure map of the A-algebra A⟨X⟩_T is the constant-series embedding.

theorem TauCeti.Huber.algebraMap_weightedRestrictedSubring_injective {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : Function.Injective ⇑(algebraMap A ↥(weightedRestrictedSubring T hT))

The structure map into a weighted restricted-series ring is injective, since it is the constant-series embedding.

theorem TauCeti.Huber.algebraMap_prod_weightedRestrictedSubring_injective {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {m : ℕ} (T : Fin k → Set A) (S : Fin m → Set A) (hT : IsWeightFamily T) (hS : IsWeightFamily S) : Function.Injective ⇑(algebraMap A (↥(weightedRestrictedSubring T hT) × ↥(weightedRestrictedSubring S hS)))

The diagonal structure map into a product of weighted restricted-series rings is injective.

def TauCeti.Huber.weightedNhd {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) (U : AddSubgroup A) : AddSubgroup ↥(weightedRestrictedSubring T hT)

Wedhorn's neighbourhood subgroups U⟨X⟩: the series all of whose coefficients — not merely almost all — satisfy the U bound. These are the fundamental system of neighbourhoods of zero for the topology on A⟨X⟩_T.

Equations

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

@[simp]

theorem TauCeti.Huber.mem_weightedNhd {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {U : AddSubgroup A} {f : ↥(weightedRestrictedSubring T hT)} : f ∈ weightedNhd T hT U ↔ ∀ (ν : Fin k →₀ ℕ), (MvPowerSeries.coeff ν) ↑f ∈ weightMul T ν U

Membership in U⟨X⟩ is the U bound on every coefficient.

@[simp]

theorem TauCeti.Huber.weightedNhd_bot {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : weightedNhd T hT ⊥ = ⊥

The zero subgroup bounds exactly the zero series.

theorem TauCeti.Huber.weightedRestrictedSubring_one_weight {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] : weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯ = restrictedMvPowerSeriesSubring k A

Wedhorn Example 5.54, bundled: for the trivial weight, A⟨X⟩_T is the ordinary ring of restricted power series, not merely a predicate-level equivalent.

@[simp]

theorem TauCeti.Huber.subringCongr_one_weight_weightedX {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (i : Fin k) : (RingEquiv.subringCongr ⋯) (weightedX (fun (x : Fin k) => {1}) ⋯ i) = restrictedX i

The weighted variable is the restricted variable. Transporting weightedX along the identification above gives restrictedX.

weightedRestrictedSubring_one_weight is an equality of subrings, so it transports elements along RingEquiv.subringCongr; what it does not say is where the generators go. This and the companion below say it, so that a generator-level statement proved over one of the two subrings can be read over the other instead of being re-transported at each use site.

@[simp]

theorem TauCeti.Huber.subringCongr_one_weight_weightedC {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (a : A) : (RingEquiv.subringCongr ⋯) ((weightedC (fun (x : Fin k) => {1}) ⋯) a) = (algebraMap A ↥(restrictedMvPowerSeriesSubring k A)) a

The weighted constant is the algebra map. Transporting weightedC a along the same identification gives the image of a under the structure map of the restricted subring.

theorem TauCeti.Huber.weightedNhd_mono {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {U V : AddSubgroup A} (h : U ≤ V) : weightedNhd T hT U ≤ weightedNhd T hT V

The neighbourhood subgroups are monotone in U.

theorem TauCeti.Huber.mul_mem_weightedNhd {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {W U : AddSubgroup A} (hWU : ↑W * ↑W ⊆ ↑U) {f g : ↥(weightedRestrictedSubring T hT)} (hf : f ∈ weightedNhd T hT W) (hg : g ∈ weightedNhd T hT W) : f * g ∈ weightedNhd T hT U

The multiplicative half of the neighbourhood basis: if W · W ⊆ U then the product of two elements of W⟨X⟩ lies in U⟨X⟩. This is the condition RingSubgroupsBasis calls mul, and unlike multiplicative closure of the ring it needs no finiteness argument.

@[simp]

theorem TauCeti.Huber.weightedC_mem_weightedNhd {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {U : AddSubgroup A} {a : A} : (weightedC T hT) a ∈ weightedNhd T hT U ↔ a ∈ U

A constant series lies in U⟨X⟩ exactly when its value lies in U: the constant coefficient is unweighted, since T⁰ · U is U, and every other coefficient vanishes.

theorem TauCeti.Huber.exists_weightedNhd_mul_mem {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) (x : ↥(weightedRestrictedSubring T hT)) (U : OpenAddSubgroup A) : ∃ (V : OpenAddSubgroup A), ∀ g ∈ weightedNhd T hT ↑V, x * g ∈ weightedNhd T hT ↑U

The left-multiplication half of the neighbourhood basis: for a fixed x ∈ A⟨X⟩_T and an open subgroup U, some V⟨X⟩ is carried into U⟨X⟩ by multiplication by x. This is the condition RingSubgroupsBasis calls leftMul.

Unlike TauCeti.Huber.mul_mem_weightedNhd this does need the bad coefficients of x handled, since x is only restricted rather than uniformly bounded — but no exceptional set of ν survives, because the absorbing subgroup works for every β at once.

theorem TauCeti.Huber.weightedNhd_subgroups_basis {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : RingSubgroupsBasis fun (U : OpenAddSubgroup A) => weightedNhd T hT ↑U

The neighbourhood basis of A⟨X⟩_T: the subgroups U⟨X⟩, as U ranges over the open subgroups of A, are a RingSubgroupsBasis. This is Wedhorn's assertion that they form a fundamental system of neighbourhoods of zero for a ring topology.

@[instance_reducible]

noncomputable instance TauCeti.Huber.weightedTopology {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : TopologicalSpace ↥(weightedRestrictedSubring T hT)

Wedhorn's topology on A⟨X⟩_T (Remark and Definition 5.48): the ring topology whose neighbourhoods of zero are the U⟨X⟩.

Consumers should go through the contract lemmas below rather than unfolding this: the basis is hasBasis_nhds_zero_weightedTopology, and isTopologicalRing_weightedTopology / nonarchimedeanRing_weightedTopology give the structure.

It is an instance rather than a plain def so that a consumer of A⟨X⟩_T gets the topology, and the IsTopologicalRing and NonarchimedeanRing structures below, by inference. Both T and the standing hypothesis are implicit because they are read off the carrier's own type.

On diamonds. Mathlib does register a topology on MvPowerSeries σ R, but as a scoped instance in MvPowerSeries.WithPiTopology (Mathlib/RingTheory/MvPowerSeries/PiTopology.lean). It is therefore invisible here, and no file in this repository opens that scope; a downstream file that did would get the induced subtype topology on the carrier alongside this instance, and would have to say which it means.

Equations

• TauCeti.Huber.weightedTopology = ⋯.topology

theorem TauCeti.Huber.hasBasis_nhds_zero_weightedTopology {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : (nhds 0).HasBasis (fun (x : OpenAddSubgroup A) => True) fun (U : OpenAddSubgroup A) => ↑(weightedNhd T hT ↑U)

The U⟨X⟩ are a basis of neighbourhoods of zero for weightedTopology.

instance TauCeti.Huber.isTopologicalRing_weightedTopology {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : IsTopologicalRing ↥(weightedRestrictedSubring T hT)

A⟨X⟩_T is a topological ring.

instance TauCeti.Huber.nonarchimedeanRing_weightedTopology {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : NonarchimedeanRing ↥(weightedRestrictedSubring T hT)

A⟨X⟩_T is nonarchimedean: it inherits a basis of open additive subgroups at zero, as every ring built from a RingSubgroupsBasis does.

theorem TauCeti.Huber.isOpen_weightedNhd {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {U : AddSubgroup A} (hU : IsOpen ↑U) : IsOpen ↑(weightedNhd T hT U)

U⟨X⟩ is open in A⟨X⟩_T when U is open in A: it is one of the basic neighbourhoods of zero, and an additive subgroup that is a neighbourhood of zero is open.

theorem TauCeti.Huber.continuous_weightedC {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : Continuous ⇑(weightedC T hT)

The constant-series embedding A → A⟨X⟩_T is continuous.

A constant series has its only nonzero coefficient at ν = 0, where T⁰ · U is U itself, so the open subgroup U already witnesses continuity at zero.

Density of the polynomials

theorem TauCeti.Huber.isWeightedRestricted_toMvPowerSeries {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin k → Set A) (p : MvPolynomial (Fin k) A) : IsWeightedRestricted T ↑p

Every polynomial is T-restricted, for any family T.

theorem TauCeti.Huber.exists_mvPolynomial_forall_coeff_sub_mem {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] {T : Fin k → Set A} {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) (U : OpenAddSubgroup A) : ∃ (p : MvPolynomial (Fin k) A), ∀ (ν : Fin k →₀ ℕ), (MvPowerSeries.coeff ν) (f - ↑p) ∈ weightMul T ν ↑U

Wedhorn 5.49(1), the approximation step, at predicate level: a T-restricted series is approximated by a polynomial, coefficientwise inside Tν · U. Neither a nonarchimedean hypothesis on A nor IsWeightFamily T is needed — only the ambient [CommRing A] and [TopologicalSpace A] that OpenAddSubgroup A already asks for.

noncomputable def TauCeti.Huber.weightedPolynomialHom {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : MvPolynomial (Fin k) A →+* ↥(weightedRestrictedSubring T hT)

The coefficientwise inclusion of the polynomials into A⟨X⟩_T, as a ring homomorphism. Every polynomial is T-restricted, so it lands in A⟨X⟩_T and not merely in A[[X]]; its range is TauCeti.Huber.weightedPolynomials.

Equations

• TauCeti.Huber.weightedPolynomialHom T hT = MvPolynomial.coeToMvPowerSeries.ringHom.codRestrict (TauCeti.Huber.weightedRestrictedSubring T hT) ⋯

@[simp]

theorem TauCeti.Huber.coe_weightedPolynomialHom {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (p : MvPolynomial (Fin k) A) : ↑((weightedPolynomialHom T hT) p) = ↑p

@[simp]

theorem TauCeti.Huber.weightedPolynomialHom_C {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (a : A) : (weightedPolynomialHom T hT) (MvPolynomial.C a) = (weightedC T hT) a

The inclusion sends the polynomial constant C a to the constant series weightedC a.

@[simp]

theorem TauCeti.Huber.weightedPolynomialHom_X {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (i : Fin k) : (weightedPolynomialHom T hT) (MvPolynomial.X i) = weightedX T hT i

The inclusion sends the polynomial variable X i to the weighted variable weightedX i.

theorem TauCeti.Huber.weightedPolynomialHom_injective {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : Function.Injective ⇑(weightedPolynomialHom T hT)

The inclusion of the polynomials is injective: a polynomial is determined by its coefficients, and the inclusion changes none of them.

This is what makes TauCeti.Huber.weightedPolynomials a faithful copy of MvPolynomial (Fin k) A inside A⟨X⟩_T, so that a map defined on polynomials transfers to it.

noncomputable def TauCeti.Huber.weightedPolynomials {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] (T : Fin k → Set A) (hT : IsWeightFamily T) : Subring ↥(weightedRestrictedSubring T hT)

A[X] ⊆ A⟨X⟩_T, as a subring.

Equations

• TauCeti.Huber.weightedPolynomials T hT = (TauCeti.Huber.weightedPolynomialHom T hT).range

noncomputable def TauCeti.Huber.weightedPolynomialsEquiv {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : MvPolynomial (Fin k) A ≃+* ↥(weightedPolynomials T hT)

A[X] and its copy inside A⟨X⟩_T are the same ring. The inclusion is injective by TauCeti.Huber.weightedPolynomialHom_injective and surjective onto its range by construction.

This is what lets a homomorphism defined on MvPolynomial (Fin k) A — an evaluation, say — be read as one defined on the subring of A⟨X⟩_T, which is where the uniformity lives.

Equations

• TauCeti.Huber.weightedPolynomialsEquiv hT = RingEquiv.ofBijective (TauCeti.Huber.weightedPolynomialHom T hT).rangeRestrict ⋯

@[simp]

theorem TauCeti.Huber.coe_weightedPolynomialsEquiv {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (p : MvPolynomial (Fin k) A) : ↑((weightedPolynomialsEquiv hT) p) = (weightedPolynomialHom T hT) p

theorem TauCeti.Huber.mem_weightedPolynomials_iff {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {f : ↥(weightedRestrictedSubring T hT)} : f ∈ weightedPolynomials T hT ↔ {ν : Fin k →₀ ℕ | (MvPowerSeries.coeff ν) ↑f ≠ 0}.Finite

Membership in weightedPolynomials is exactly having finitely many nonzero coefficients.

@[simp]

theorem TauCeti.Huber.weightedC_mem_weightedPolynomials {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (a : A) : (weightedC T hT) a ∈ weightedPolynomials T hT

A constant series is a polynomial.

@[simp]

theorem TauCeti.Huber.weightedX_mem_weightedPolynomials {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} (i : Fin k) : weightedX T hT i ∈ weightedPolynomials T hT

A weighted variable is a polynomial.

theorem TauCeti.Huber.dense_weightedPolynomials {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : Dense ↑(weightedPolynomials T hT)

Wedhorn 5.49(1): the polynomials are dense in A⟨X⟩_T.

theorem TauCeti.Huber.eqOn_weightedPolynomials {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} {B : Type u_2} [Semiring B] {f g : ↥(weightedRestrictedSubring T hT) →+* B} (hC : ∀ (a : A), f ((weightedC T hT) a) = g ((weightedC T hT) a)) (hX : ∀ (i : Fin k), f (weightedX T hT i) = g (weightedX T hT i)) : Set.EqOn ⇑f ⇑g ↑(weightedPolynomials T hT)

Agreement on the generators propagates to the polynomials. Two ring homomorphisms out of A⟨X⟩_T that agree on every constant series and every variable agree on the whole polynomial subring. No topology is involved.

theorem TauCeti.Huber.weightedRestrictedSubring_ringHom_ext_of_continuous {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) {B : Type u_2} [Semiring B] [TopologicalSpace B] [T2Space B] {f g : ↥(weightedRestrictedSubring T hT) →+* B} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (hC : ∀ (a : A), f ((weightedC T hT) a) = g ((weightedC T hT) a)) (hX : ∀ (i : Fin k), f (weightedX T hT i) = g (weightedX T hT i)) : f = g

A continuous homomorphism out of A⟨X⟩_T is determined by its values on the generators. Two of them agreeing on every constant series and every variable are equal. This is the uniqueness half of Wedhorn 5.50: among continuous homomorphisms there is at most one extending a given map on constants and sending each Xᵢ to a prescribed value.

Equality on the polynomial subring is propagated to the whole ring by its density, and that is what continuity and the Hausdorff hypothesis are for. Whether uniqueness can fail without them is not addressed here.

The discrete case

Over a discrete ring the picture collapses: {0} is an open subgroup, so a restricted series has finitely many nonzero coefficients — A⟨X⟩_T is the polynomial ring — and the topology generated by U⟨X⟩ at U = ⊥ is discrete.

instance TauCeti.Huber.discreteTopology_weightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [DiscreteTopology A] {T : Fin k → Set A} {hT : IsWeightFamily T} : DiscreteTopology ↥(weightedRestrictedSubring T hT)

Over a discrete ring every weighted topology is discrete: ⊥⟨X⟩ = {0} is open.

theorem TauCeti.Huber.weightedPolynomials_eq_top {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [DiscreteTopology A] {T : Fin k → Set A} {hT : IsWeightFamily T} : weightedPolynomials T hT = ⊤

Over a discrete ring the restricted series are exactly the polynomials.

noncomputable def TauCeti.Huber.weightedPolynomialEquiv {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [DiscreteTopology A] (T : Fin k → Set A) (hT : IsWeightFamily T) : MvPolynomial (Fin k) A ≃+* ↥(weightedRestrictedSubring T hT)

Over a discrete ring, the coefficientwise inclusion of the polynomials into A⟨X⟩_T is a ring isomorphism.

Equations

• TauCeti.Huber.weightedPolynomialEquiv T hT = RingEquiv.ofBijective (TauCeti.Huber.weightedPolynomialHom T hT) ⋯

@[simp]

theorem TauCeti.Huber.weightedPolynomialEquiv_apply {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] [DiscreteTopology A] {T : Fin k → Set A} {hT : IsWeightFamily T} (p : MvPolynomial (Fin k) A) : (weightedPolynomialEquiv T hT) p = (weightedPolynomialHom T hT) p

The forward map of weightedPolynomialEquiv is the coefficientwise inclusion weightedPolynomialHom, so its coe_/_C/_X lemmas apply.

Zero variables

At k = 0 the coefficient index Fin 0 →₀ ℕ is a singleton: a series is its constant coefficient and nothing else. So restrictedness is vacuous, and the basic neighbourhood cut out by a subgroup U is exactly the series whose one coefficient lies in U, which is U.

Neither fact mentions the weight, so the whole section is stated for an arbitrary T : Fin 0 → Set A — at Fin 0 the only multi-index is 0, and weightMul T 0 U is U for every T. The weight-family hypothesis is not carried either: it quantifies over the index, so isWeightFamily_fin_zero discharges it outright.

theorem TauCeti.Huber.isWeightFamily_fin_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) : IsWeightFamily T

Every family of sets indexed by no variables is a weight family, the condition being a statement about each index and there being none. This is what lets the rest of this section drop the hypothesis.

@[simp]

theorem TauCeti.Huber.weightedRestrictedSubring_fin_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] : weightedRestrictedSubring T ⋯ = ⊤

At zero variables every power series is restricted, whatever the weight. There is only one monomial, so every series has finite support.

noncomputable def TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] : ↥(weightedRestrictedSubring T ⋯) ≃+* A

A⟨⟩ = A: the restricted power series in no variables are A itself, as a ring.

Equations

• TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv T = (RingEquiv.subringCongr ⋯).trans (Subring.topEquiv.trans (MvPowerSeries.isEmptyEquiv (Fin 0) A).toRingEquiv)

@[simp]

theorem TauCeti.Huber.weightedRestrictedSubringFinZeroEquiv_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] (f : ↥(weightedRestrictedSubring T ⋯)) : (weightedRestrictedSubringFinZeroEquiv T) f = MvPowerSeries.constantCoeff ↑f

The zero-variable comparison is the constant coefficient.

theorem TauCeti.Huber.continuous_weightedRestrictedSubringFinZeroEquiv {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] : Continuous ⇑(weightedRestrictedSubringFinZeroEquiv T)

The zero-variable comparison is continuous.

@[simp]

theorem TauCeti.Huber.coe_weightedRestrictedSubringFinZeroEquiv_symm_apply {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] (a : A) : ↑((weightedRestrictedSubringFinZeroEquiv T).symm a) = MvPowerSeries.C a

The inverse comparison sends a to the constant series.

theorem TauCeti.Huber.continuous_weightedRestrictedSubringFinZeroEquiv_symm {A : Type u_1} [CommRing A] [TopologicalSpace A] (T : Fin 0 → Set A) [NonarchimedeanRing A] : Continuous ⇑(weightedRestrictedSubringFinZeroEquiv T).symm

The inverse of the zero-variable comparison is continuous: it is the constant-series map weightedC, whose continuity is already known.

The uniform structure

A⟨X⟩_T carries the group uniformity of its additive topological group, so that its separated completion can be formed. As with weightedTopology there is no diamond to fear: Mathlib's uniformity on MvPowerSeries (like its topology) lives in the scoped MvPowerSeries.WithPiTopology, so nothing else registers a UniformSpace on this carrier.

@[instance_reducible]

noncomputable instance TauCeti.Huber.instUniformSpaceSubtypeMvPowerSeriesFinMemSubringWeightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : UniformSpace ↥(weightedRestrictedSubring T hT)

Equations

• TauCeti.Huber.instUniformSpaceSubtypeMvPowerSeriesFinMemSubringWeightedRestrictedSubring = IsTopologicalAddGroup.rightUniformSpace ↥(TauCeti.Huber.weightedRestrictedSubring T hT)

instance TauCeti.Huber.instIsUniformAddGroupSubtypeMvPowerSeriesFinMemSubringWeightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : IsUniformAddGroup ↥(weightedRestrictedSubring T hT)

instance TauCeti.Huber.instContinuousConstSMulSubtypeMvPowerSeriesFinMemSubringWeightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : ContinuousConstSMul A ↥(weightedRestrictedSubring T hT)

instance TauCeti.Huber.instUniformContinuousConstSMulSubtypeMvPowerSeriesFinMemSubringWeightedRestrictedSubring {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} {hT : IsWeightFamily T} : UniformContinuousConstSMul A ↥(weightedRestrictedSubring T hT)

Functoriality

theorem RingHom.weightMul_map_le {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] (φ : A →+* B) {T : Fin k → Set A} {S : Fin k → Set B} (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (ν : Fin k →₀ ℕ) {U : AddSubgroup A} {V : AddSubgroup B} (hUV : U ≤ AddSubgroup.comap (↑φ) V) : AddSubgroup.map (↑φ) (TauCeti.Huber.weightMul T ν U) ≤ TauCeti.Huber.weightMul S ν V

weightMul is functorial: a ring map carrying each T i into S i and U into V carries Tν · U into Sν · V.

theorem TauCeti.Huber.IsWeightFamily.image {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) (hφo : IsOpenMap ⇑φ) {T : Fin k → Set A} (hT : IsWeightFamily T) : IsWeightFamily fun (i : Fin k) => ⇑φ '' T i

A weight family pushes forward along a continuous open ring map: if φ : A → B is continuous and open, the images φ '' T i of a weight family form a weight family on B.

For a ring isomorphism continuous in both directions, IsOpenMap.of_inverse supplies the openness, so weight families transport along isomorphisms of topological rings.

theorem TauCeti.Huber.IsWeightedRestricted.map {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) {f : MvPowerSeries (Fin k) A} (hf : IsWeightedRestricted T f) : IsWeightedRestricted S ((MvPowerSeries.map φ) f)

Restrictedness is functorial: a continuous ring map carrying each T i into S i carries T-restricted series to S-restricted ones.

noncomputable def TauCeti.Huber.weightedMap {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) : ↥(weightedRestrictedSubring T hT) →+* ↥(weightedRestrictedSubring S hS)

The induced morphism A⟨X⟩_T → B⟨X⟩_S: a continuous ring map φ : A → B carrying each weight T i into S i induces one, acting coefficientwise.

The two weight families are given independently rather than taking S i := φ '' T i, because the image of a weight family need not be one.

Equations

• TauCeti.Huber.weightedMap hφ hT hS hTS = ((MvPowerSeries.map φ).comp (TauCeti.Huber.weightedRestrictedSubring T hT).subtype).codRestrict (TauCeti.Huber.weightedRestrictedSubring S hS) ⋯

@[simp]

theorem TauCeti.Huber.coe_weightedMap {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (f : ↥(weightedRestrictedSubring T hT)) : ↑((weightedMap hφ hT hS hTS) f) = (MvPowerSeries.map φ) ↑f

weightedMap is MvPowerSeries.map with its codomain cut down, so its values coerce back to the coefficientwise map.

@[simp]

theorem TauCeti.Huber.weightedMap_weightedC {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (a : A) : (weightedMap hφ hT hS hTS) ((weightedC T hT) a) = (weightedC S hS) (φ a)

weightedMap is compatible with the constant-series embeddings.

theorem TauCeti.Huber.continuous_weightedMap {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) : Continuous ⇑(weightedMap hφ hT hS hTS)

weightedMap is continuous, so the induced morphism is one of topological rings rather than of the underlying rings only.

@[simp]

theorem TauCeti.Huber.weightedMap_id {k : ℕ} {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {T : Fin k → Set A} (hT : IsWeightFamily T) : weightedMap ⋯ hT hT ⋯ = RingHom.id ↥(weightedRestrictedSubring T hT)

The identity law: the map induced by RingHom.id is the identity.

theorem TauCeti.Huber.weightedMap_comp {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {C : Type u_3} [CommRing C] [TopologicalSpace C] [NonarchimedeanRing C] {φ : A →+* B} {ψ : B →+* C} (hφ : Continuous ⇑φ) (hψ : Continuous ⇑ψ) {T : Fin k → Set A} {S : Fin k → Set B} {R : Fin k → Set C} (hT : IsWeightFamily T) (hS : IsWeightFamily S) (hR : IsWeightFamily R) (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (hSR : ∀ (i : Fin k), ⇑ψ '' S i ⊆ R i) : weightedMap ⋯ hT hR ⋯ = (weightedMap hψ hS hR hSR).comp (weightedMap hφ hT hS hTS)

The composition law: the map induced by a composite is the composite of the induced maps. With weightedMap_id this is what makes A⟨X⟩_T functorial in the pair (A, T).

@[simp]

theorem TauCeti.Huber.weightedMap_weightedX {k : ℕ} {A : Type u_1} [CommRing A] {B : Type u_2} [CommRing B] [TopologicalSpace A] [TopologicalSpace B] [NonarchimedeanRing A] [NonarchimedeanRing B] {φ : A →+* B} (hφ : Continuous ⇑φ) {T : Fin k → Set A} {S : Fin k → Set B} {hT : IsWeightFamily T} {hS : IsWeightFamily S} (hTS : ∀ (i : Fin k), ⇑φ '' T i ⊆ S i) (i : Fin k) : (weightedMap hφ hT hS hTS) (weightedX T hT i) = weightedX S hS i

weightedMap fixes the variables.