English
The basis for the topology on MvPowerSeries is given by two-sided ideals encoded by pairs (J, d) with the sub-basis condition controlling coefficients: f ∈ basis iff ∀ e ≤ d, coeff e f ∈ J.
Русский
Базис линейной топологии на MvPowerSeries задаётся парами (J, d), где условие принадлежности элемента f к базису означает, что для всех e ≤ d коэффициент φ при e принадлежит J.
LaTeX
$$$f \in \mathrm{basis}(\sigma,R)\; Jd \iff \forall e \le Jd.2,\; \operatorname{coeff} e f \in Jd.1$$$
Lean4
/-- The underlying family for the basis of ideals in a multivariate power series ring. -/
def basis (σ : Type*) (R : Type*) [Ring R] (Jd : TwoSidedIdeal R × (σ →₀ ℕ)) : TwoSidedIdeal (MvPowerSeries σ R) :=
TwoSidedIdeal.mk' {f | ∀ e ≤ Jd.2, coeff e f ∈ Jd.1} (by simp [coeff_zero])
(fun hf hg e he ↦ by rw [map_add]; exact add_mem (hf e he) (hg e he))
(fun {f} hf e he ↦ by simp only [map_neg, neg_mem, hf e he])
(fun {f g} hg e he ↦ by
classical
rw [coeff_mul]
apply sum_mem
rintro uv huv
exact TwoSidedIdeal.mul_mem_left _ _ _ (hg _ (le_trans (Finset.antidiagonal.snd_le huv) he)))
(fun {f g} hf e he ↦ by
classical
rw [coeff_mul]
apply sum_mem
rintro uv huv
exact TwoSidedIdeal.mul_mem_right _ _ _ (hf _ (le_trans (Finset.antidiagonal.fst_le huv) he)))
