Multivariate restricted power series #

In this file we introduce the theory of restricted multivariate power series (historically called Tate algebras when c = 1).

Specifically we define the predicate:

IsRestricted : a multivariate power series over a normed ring R is restricted for a tuple c if ‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0 under the cofinite filter.

And then promote it to a type:

Restricted: the set of restricted multivariate power series over a normed ring R for a tuple c.

When R is an ultrametric (non-archimedean) normed ring we have the following key properties:

MvPowerSeries.instRingRestricted: Restricted R c is a ring
MvPowerSeries.instModuleRestricted: Restricted R c is an R-module
MvPowerSeries.instAlgebraRestricted: Restricted R c is an R-algebra

source

def MvPowerSeries.IsRestricted {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R) :

Prop

A multivariate power series over a normed ring R is restricted for a tuple c if ‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0 under the cofinite filter.

Equations

MvPowerSeries.IsRestricted c f = Filter.Tendsto (fun (t : σ →₀ ℕ) => ‖(MvPowerSeries.coeff t) f‖ * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) Filter.cofinite (nhds 0)

Instances For

source

@[simp]

theorem MvPowerSeries.isRestricted_abs_iff {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (f : MvPowerSeries σ R) :

IsRestricted |c| f ↔ IsRestricted c f

source

theorem MvPowerSeries.isRestricted_zero {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) :

IsRestricted c 0

source

theorem MvPowerSeries.isRestricted_monomial {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) :

IsRestricted c ((monomial n) a)

source

theorem MvPowerSeries.isRestricted_one {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) :

IsRestricted c 1

source

theorem MvPowerSeries.isRestricted_C {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (a : R) :

IsRestricted c (C a)

source

theorem MvPowerSeries.isRestricted_X {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) (s : σ) :

IsRestricted c (X s)

source

theorem MvPowerSeries.isRestricted_of_finite_support {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f : MvPowerSeries σ R} (hf : (Function.support fun (t : σ →₀ ℕ) => (coeff t) f).Finite) :

IsRestricted c f

source

theorem MvPowerSeries.tendsto_antidiagonal {M : Type u_3} {S : Type u_4} [AddMonoid M] [Finset.HasAntidiagonal M] [NormedRing S] [IsUltrametricDist S] {C : M → ℝ} (hC : ∀ (a b : M), C (a + b) = C a * C b) {f g : M → S} (hf : Filter.Tendsto (fun (i : M) => ‖f i‖ * C i) Filter.cofinite (nhds 0)) (hg : Filter.Tendsto (fun (i : M) => ‖g i‖ * C i) Filter.cofinite (nhds 0)) :

Filter.Tendsto (fun (a : M) => ‖∑ p ∈ Finset.antidiagonal a, f p.1 * g p.2‖ * C a) Filter.cofinite (nhds 0)

source

theorem MvPowerSeries.isRestricted_map {R : Type u_1} [NormedRing R] {σ : Type u_2} {S : Type u_3} [NormedRing S] (c : σ → ℝ) (π : R → S) {C : ℝ} (hCπ : ∀ (x : R), ‖π x‖ ≤ C * ‖x‖) {f : MvPowerSeries σ R} (hf : IsRestricted c f) :

IsRestricted c fun (t : σ →₀ ℕ) => π ((coeff t) f)

source

theorem MvPowerSeries.IsRestricted.add {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) :

IsRestricted c (f + g)

source

theorem MvPowerSeries.IsRestricted.neg {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} {f : MvPowerSeries σ R} (hf : IsRestricted c f) :

IsRestricted c (-f)

source

theorem MvPowerSeries.IsRestricted.smul {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} (r : R) {f : MvPowerSeries σ R} (hf : IsRestricted c f) :

IsRestricted c (r • f)

source

theorem MvPowerSeries.IsRestricted.mul {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] {c : σ → ℝ} {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) :

IsRestricted c (f * g)

source

def MvPowerSeries.IsRestricted.addSubgroup {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) :

AddSubgroup (MvPowerSeries σ R)

Restricted power series as an additive subgroup of MvPowerSeries σ R.

Equations

MvPowerSeries.IsRestricted.addSubgroup c = { carrier := {f : MvPowerSeries σ R | MvPowerSeries.IsRestricted c f}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source

@[simp]

theorem MvPowerSeries.IsRestricted.mem_addSubgroup {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} {f : MvPowerSeries σ R} :

f ∈ IsRestricted.addSubgroup c ↔ IsRestricted c f

source

theorem MvPowerSeries.IsRestricted.sub {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) :

IsRestricted c (f - g)

source

theorem MvPowerSeries.IsRestricted.sum {R : Type u_1} [NormedRing R] {σ : Type u_2} {c : σ → ℝ} {ι : Type u_3} {s : Finset ι} {f : ι → MvPowerSeries σ R} (hf : ∀ i ∈ s, IsRestricted c (f i)) :

IsRestricted c (∑ i ∈ s, f i)

source

def MvPowerSeries.IsRestricted.subring {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

Subring (MvPowerSeries σ R)

Restricted power series as a subring of MvPowerSeries σ R.

Equations

MvPowerSeries.IsRestricted.subring c = { carrier := (MvPowerSeries.IsRestricted.addSubgroup c).carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

Instances For

source

@[simp]

theorem MvPowerSeries.IsRestricted.mem_subring {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] {c : σ → ℝ} {f : MvPowerSeries σ R} :

f ∈ IsRestricted.subring c ↔ IsRestricted c f

source

theorem MvPowerSeries.IsRestricted.pow {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] {c : σ → ℝ} {f : MvPowerSeries σ R} (hf : IsRestricted c f) (n : ℕ) :

IsRestricted c (f ^ n)

source

@[deprecated MvPowerSeries.IsRestricted.add (since := "2026-09-23")]

theorem MvPowerSeries.isRestricted.add {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) :

IsRestricted c (f + g)

source

@[deprecated MvPowerSeries.IsRestricted.neg (since := "2026-09-23")]

theorem MvPowerSeries.isRestricted.neg {R : Type u_1} [NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f : MvPowerSeries σ R} (hf : IsRestricted c f) :

IsRestricted c (-f)

source

@[deprecated MvPowerSeries.IsRestricted.mul (since := "2026-09-23")]

theorem MvPowerSeries.isRestricted.mul {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {f g : MvPowerSeries σ R} (hf : IsRestricted c f) (hg : IsRestricted c g) :

IsRestricted c (f * g)

source

def MvPowerSeries.Restricted (R : Type u_1) [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

Type (max u_1 u_2)

The type of restricted MvPowerSeries σ R.

Equations

MvPowerSeries.Restricted R c = ↥(MvPowerSeries.IsRestricted.subring c)

Instances For

source

@[instance_reducible]

noncomputable instance MvPowerSeries.instRingRestricted {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

Ring (Restricted R c)

Ring structure on Restricted R c.

Equations

MvPowerSeries.instRingRestricted c = (MvPowerSeries.IsRestricted.subring c).toRing

source

@[instance_reducible]

instance MvPowerSeries.instModuleRestricted {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

Module R (Restricted R c)

R-module structure on Restricted R c.

Equations

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

source

@[instance_reducible]

noncomputable instance MvPowerSeries.instCommRingRestricted {σ : Type u_2} {S : Type u_3} [NormedCommRing S] [IsUltrametricDist S] (c : σ → ℝ) :

CommRing (Restricted S c)

Commutative ring structure on Restricted S c when S is commutative.

Equations

MvPowerSeries.instCommRingRestricted c = { toRing := inferInstance, mul_comm := ⋯ }

source

@[instance_reducible]

noncomputable instance MvPowerSeries.instAlgebraRestricted {σ : Type u_2} {S : Type u_3} [NormedCommRing S] [IsUltrametricDist S] (c : σ → ℝ) :

Algebra S (Restricted S c)

Algebra structure on Restricted S c when S is commutative.

Equations

MvPowerSeries.instAlgebraRestricted c = Algebra.ofModule ⋯ ⋯

source

theorem MvPowerSeries.Restricted.ext {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] {c : σ → ℝ} {f g : Restricted R c} (h : ↑f = ↑g) :

f = g

source

theorem MvPowerSeries.Restricted.ext_iff {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] {c : σ → ℝ} {f g : Restricted R c} :

f = g ↔ ↑f = ↑g

source

@[simp]

theorem MvPowerSeries.Restricted.val_zero {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

↑0 = 0

source

@[simp]

theorem MvPowerSeries.Restricted.val_one {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

↑1 = 1

source

@[simp]

theorem MvPowerSeries.Restricted.val_add {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (f g : Restricted R c) :

↑(f + g) = ↑f + ↑g

source

@[simp]

theorem MvPowerSeries.Restricted.val_neg {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (f : Restricted R c) :

↑(-f) = -↑f

source

@[simp]

theorem MvPowerSeries.Restricted.val_sub {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (f g : Restricted R c) :

↑(f - g) = ↑f - ↑g

source

@[simp]

theorem MvPowerSeries.Restricted.val_smul {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (r : R) (f : Restricted R c) :

↑(r • f) = r • ↑f

source

@[simp]

theorem MvPowerSeries.Restricted.val_mul {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (f g : Restricted R c) :

↑(f * g) = ↑f * ↑g

source

@[simp]

theorem MvPowerSeries.Restricted.val_pow {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (f : Restricted R c) (n : ℕ) :

↑(f ^ n) = ↑f ^ n

source

@[simp]

theorem MvPowerSeries.Restricted.val_sum {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {ι : Type u_3} (s : Finset ι) (g : ι → Restricted R c) :

↑(∑ i ∈ s, g i) = ∑ i ∈ s, ↑(g i)

source

noncomputable def MvPowerSeries.Restricted.monomial {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) :

Restricted R c

MvPowerSeries.monomial n a as an element of Restricted R c.

Equations

MvPowerSeries.Restricted.monomial c n a = ⟨(MvPowerSeries.monomial n) a, ⋯⟩

Instances For

source

@[simp]

theorem MvPowerSeries.Restricted.val_monomial {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) :

↑(monomial c n a) = (MvPowerSeries.monomial n) a

source

noncomputable def MvPowerSeries.Restricted.X (R : Type u_1) [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (s : σ) :

Restricted R c

MvPowerSeries.X s as an element of Restricted R c.

Equations

MvPowerSeries.Restricted.X R c s = ⟨MvPowerSeries.X s, ⋯⟩

Instances For

source

@[simp]

theorem MvPowerSeries.Restricted.val_X {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (s : σ) :

↑(X R c s) = MvPowerSeries.X s

source

noncomputable def MvPowerSeries.Restricted.C {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

R →+* Restricted R c

The constant MvPowerSeries.C a as an element of Restricted R c, bundled as a ring homomorphism.

Equations

MvPowerSeries.Restricted.C c = MvPowerSeries.C.codRestrict (MvPowerSeries.IsRestricted.subring c) ⋯

Instances For

source

@[simp]

theorem MvPowerSeries.Restricted.val_C {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (a : R) :

↑((C c) a) = MvPowerSeries.C a

source

theorem MvPowerSeries.Restricted.algebraMap_apply {σ : Type u_2} (c : σ → ℝ) {S : Type u_3} [NormedCommRing S] [IsUltrametricDist S] (a : S) :

(algebraMap S (Restricted S c)) a = (C c) a

source

noncomputable def MvPowerSeries.Restricted.map {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] {φ : R →+* S} {K : ℝ} (hφ : ∀ (x : R), ‖φ x‖ ≤ K * ‖x‖) :

Restricted R c →+* Restricted S c

The map between restricted power series induced by a map on the coefficients.

Equations

MvPowerSeries.Restricted.map c hφ = ((MvPowerSeries.map φ).comp (MvPowerSeries.IsRestricted.subring c).subtype).codRestrict (MvPowerSeries.IsRestricted.subring c) ⋯

Instances For

source

@[simp]

theorem MvPowerSeries.Restricted.val_map {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] {φ : R →+* S} {K : ℝ} (hφ : ∀ (x : R), ‖φ x‖ ≤ K * ‖x‖) (f : Restricted R c) :

↑((map c hφ) f) = (MvPowerSeries.map φ) ↑f

source

theorem MvPowerSeries.Restricted.map_injective {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] {φ : R →+* S} {K : ℝ} (hφ : ∀ (x : R), ‖φ x‖ ≤ K * ‖x‖) (hφinj : Function.Injective ⇑φ) :

Function.Injective ⇑(map c hφ)

source

noncomputable def MvPowerSeries.Restricted.mapAdditive {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] (π : S →+ R) {K : ℝ} (hK : ∀ (x : S), ‖π x‖ ≤ K * ‖x‖) :

Restricted S c →+ Restricted R c

A version of MvPowerSeries.Restricted.map where we take π only being additive (not necessarily multiplicative), this gives an additive map between restricted power series.

Equations

MvPowerSeries.Restricted.mapAdditive c π hK = { toFun := fun (A : MvPowerSeries.Restricted S c) => ⟨fun (t : σ →₀ ℕ) => π ((MvPowerSeries.coeff t) ↑A), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MvPowerSeries.Restricted.coeff_val_mapAdditive {R : Type u_1} [NormedRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] (π : S →+ R) {K : ℝ} (hK : ∀ (x : S), ‖π x‖ ≤ K * ‖x‖) (A : Restricted S c) (t : σ →₀ ℕ) :

(coeff t) ↑((mapAdditive c π hK) A) = π ((coeff t) ↑A)

source

theorem MvPolynomial.isRestricted {R : Type u_1} [NormedCommRing R] {σ : Type u_2} (c : σ → ℝ) (p : MvPolynomial σ R) :

MvPowerSeries.IsRestricted c ↑p

source

noncomputable def MvPolynomial.toRestricted {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

MvPolynomial σ R →+* MvPowerSeries.Restricted R c

The map from multivariate polynomials to restricted power series.

Equations

MvPolynomial.toRestricted c = MvPolynomial.coeToMvPowerSeries.ringHom.codRestrict (MvPowerSeries.IsRestricted.subring c) ⋯

Instances For

source

@[simp]

theorem MvPolynomial.val_toRestricted {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (p : MvPolynomial σ R) :

↑((toRestricted c) p) = ↑p

source

@[simp]

theorem MvPolynomial.toRestricted_monomial {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (n : σ →₀ ℕ) (a : R) :

(toRestricted c) ((monomial n) a) = MvPowerSeries.Restricted.monomial c n a

source

@[simp]

theorem MvPolynomial.toRestricted_X {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (s : σ) :

(toRestricted c) (X s) = MvPowerSeries.Restricted.X R c s

source

@[simp]

theorem MvPolynomial.toRestricted_C {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) (a : R) :

(toRestricted c) (C a) = (MvPowerSeries.Restricted.C c) a

source

theorem MvPolynomial.toRestricted_injective {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) :

Function.Injective ⇑(toRestricted c)

source

@[simp]

theorem MvPolynomial.toRestricted_inj {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {p q : MvPolynomial σ R} :

(toRestricted c) p = (toRestricted c) q ↔ p = q

source

@[simp]

theorem MvPolynomial.toRestricted_eq_zero_iff {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {p : MvPolynomial σ R} :

(toRestricted c) p = 0 ↔ p = 0

source

@[simp]

theorem MvPolynomial.toRestricted_eq_one_iff {R : Type u_1} [NormedCommRing R] {σ : Type u_2} [IsUltrametricDist R] (c : σ → ℝ) {p : MvPolynomial σ R} :

(toRestricted c) p = 1 ↔ p = 1

Documentation

Mathlib.RingTheory.MvPowerSeries.Restricted

Multivariate restricted power series #