English
Let R be a commutative ring with the discrete topology and f a multivariate power series with coefficients in R. Then f is topologically nilpotent if and only if its constant coefficient is nilpotent in R.
Русский
Пусть R — коммутативное кольцо с дискретной топологией, и f — многочленовая по модулю векторная серия с коэффициентами в R. Тогда f топологически нильпотентна тогда и только тогда, когда её константный коэффициент нильпотентен в R.
LaTeX
$$$\text{IsTopologicallyNilpotent}(f) \iff \text{IsNilpotent}(\text{constantCoeff}(f))$$$
Lean4
/-- Assuming the base ring has a discrete topology, the powers of a `MvPowerSeries` converge to 0
iff its constant coefficient is nilpotent.
[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981]
See also `MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff`. -/
theorem isTopologicallyNilpotent_iff_constantCoeff_isNilpotent [CommRing R] [DiscreteTopology R]
(f : MvPowerSeries σ R) : IsTopologicallyNilpotent f ↔ IsNilpotent (constantCoeff f) :=
by
refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff_isNilpotent⟩
replace H := H.map (continuous_constantCoeff R)
simp_rw [IsTopologicallyNilpotent, nhds_discrete, tendsto_pure] at H
exact H.exists
