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.)

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} ⋯ ⋯ ⋯ ⋯ ⋯

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.

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,>.

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.

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.

instance MvPowerSeries.LinearTopology.instIsLinearTopologyOfMulOpposite {σ : Type u_1} {R : Type u_2} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] : IsLinearTopology (MvPowerSeries σ R) (MvPowerSeries σ R)

The topology on MvPowerSeries is a left linear topology when the ring of coefficients has a linar topology.

instance MvPowerSeries.LinearTopology.instIsLinearTopologyMulOpposite {σ : Type u_1} {R : Type u_2} [Ring R] [TopologicalSpace R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] : IsLinearTopology (MvPowerSeries σ R)ᵐᵒᵖ (MvPowerSeries σ R)

The topology on MvPowerSeries is a right linear topology when the ring of coefficients has a linear topology.