Linear topology on the ring of multivariate power series #

MvPowerSeries.LinearTopology.basis: the ideals of the ring of multivariate power series all coefficients the exponent of which is smaller than some bound vanish.
MvPowerSeries.LinearTopology.hasBasis_nhds_zero : the two-sided ideals from MvPowerSeries.LinearTopology.basis form a basis of neighborhoods of 0 if the topology of R is (left and right) linear.

Instances : #

If R has a linear topology, then the product topology on MvPowerSeries σ R is a linear topology.

This applies in particular when R has the discrete topology.

Note #

If we had an analogue of PolynomialModule for power series, meaning that we could consider the R⟦X⟧-module M⟦X⟧ when M is an R-module, then one could prove that M⟦X⟧ is linearly topologized over R⟦X⟧ whenever M is linearly topologized over R. To recover the ring case, it would remain to show that the isomorphism between Rᵐᵒᵖ⟦X⟧ and R⟦X⟧ᵐᵒᵖ identifies their respective actions on R⟦X⟧. (And likewise in the multivariate case.)

source

def MvPowerSeries.LinearTopology.basis (σ : Type u_1) (R : Type u_2) [Ring R] (Jd : TwoSidedIdeal R × (σ →₀ ℕ)) :

TwoSidedIdeal (MvPowerSeries σ R)

The underlying family for the basis of ideals in a multivariate power series ring.

Equations

MvPowerSeries.LinearTopology.basis σ R Jd = TwoSidedIdeal.mk' {f : MvPowerSeries σ R | ∀ e ≤ Jd.2, (MvPowerSeries.coeff R e) f ∈ Jd.1} ⋯ ⋯ ⋯ ⋯ ⋯

Instances For

source

theorem MvPowerSeries.LinearTopology.mem_basis_iff {σ : Type u_1} {R : Type u_2} [Ring R] {f : MvPowerSeries σ R} {Jd : TwoSidedIdeal R × (σ →₀ ℕ)} :

f ∈ basis σ R Jd ↔ ∀ e ≤ Jd.2, (coeff R e) f ∈ Jd.1

A power series f belongs to the twosided ideal basis σ R ⟨J, d⟩ if and only if coeff R e f ∈ J for all e ≤ d.

source

theorem MvPowerSeries.LinearTopology.basis_le {σ : Type u_1} {R : Type u_2} [Ring R] {Jd Ke : TwoSidedIdeal R × (σ →₀ ℕ)} (hJK : Jd.1 ≤ Ke.1) (hed : Ke.2 ≤ Jd.2) :

basis σ R Jd ≤ basis σ R Ke

If J ≤ K and e ≤ d, then we have the inclusion of twosided ideals basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e,>.

source

theorem MvPowerSeries.LinearTopology.basis_le_iff {σ : Type u_1} {R : Type u_2} [Ring R] {J K : TwoSidedIdeal R} {d e : σ →₀ ℕ} (hK : K ≠ ⊤) :

basis σ R (J, d) ≤ basis σ R (K, e) ↔ J ≤ K ∧ e ≤ d

basis σ R ⟨J, d⟩ ≤ basis σ R ⟨K, e⟩ if and only if J ≤ K and e ≤ d.

source

theorem MvPowerSeries.LinearTopology.hasBasis_nhds_zero {σ : Type u_1} {R : Type u_2} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :

(nhds 0).HasBasis (fun (Id : TwoSidedIdeal R × (σ →₀ ℕ)) => ↑Id.1 ∈ nhds 0) fun (Id : TwoSidedIdeal R × (σ →₀ ℕ)) => ↑(basis σ R Id)

If the ring R is endowed with a linear topology, then the sets ↑basis σ R (J, d), for J : TwoSidedIdeal R which are neighborhoods of 0 : R and d : σ →₀ ℕ, constitute a basis of neighborhoods of 0 : MvPowerSeries σ R for the product topology.

source