feat(MvPowerSeries/Substitution): substitution of power series inside power series (#15158)

Define substitution of power series other power series. This is an application of evaluation, where the ground ring is given the discrete topology. The condition for being defined is that the constant coefficient is nilpotent (and, for infinitely many variables, that the family tends to 0).

Co-authored-by: @mariainesdff

Author: AntoineChambert-Loir

Mathlib.lean

@@ -5053,6 +5053,7 @@ import Mathlib.RingTheory.MvPowerSeries.LinearTopology
 import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
 import Mathlib.RingTheory.MvPowerSeries.Order
 import Mathlib.RingTheory.MvPowerSeries.PiTopology
+import Mathlib.RingTheory.MvPowerSeries.Substitution
 import Mathlib.RingTheory.MvPowerSeries.Trunc
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Nilpotent.Basic

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -454,6 +454,11 @@ theorem constantCoeff_one : constantCoeff σ R 1 = 1 :=
 theorem constantCoeff_X (s : σ) : constantCoeff σ R (X s) = 0 :=
   coeff_zero_X s
 
+@[simp]
+theorem constantCoeff_smul {S : Type*} [Semiring S] [Module R S]
+    (φ : MvPowerSeries σ S) (a : R) :
+    constantCoeff σ S (a • φ) = a • constantCoeff σ S φ := rfl
+
 /-- If a multivariate formal power series is invertible,
  then so is its constant coefficient. -/
 theorem isUnit_constantCoeff (φ : MvPowerSeries σ R) (h : IsUnit φ) :
@@ -673,9 +678,9 @@ theorem coeff_pow [DecidableEq σ] (f : MvPowerSeries σ R) {n : ℕ} (d : σ 
 /-- Vanishing of coefficients of powers of multivariate power series
 when the constant coefficient is nilpotent
 [N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, proposition 3][bourbaki1981] -/
-theorem coeff_eq_zero_of_constantCoeff_nilpotent
-    {f : MvPowerSeries σ R} {m : ℕ} (hf : constantCoeff σ R f ^ m = 0)
-    {d : σ →₀ ℕ} {n : ℕ} (hn : m + degree d ≤ n) : coeff R d (f ^ n) = 0 := by
+theorem coeff_eq_zero_of_constantCoeff_nilpotent {f : MvPowerSeries σ R} {m : ℕ}
+    (hf : constantCoeff σ R f ^ m = 0) {d : σ →₀ ℕ} {n : ℕ} (hn : m + degree d ≤ n) :
+    coeff R d (f ^ n) = 0 := by
   classical
   rw [coeff_pow]
   apply sum_eq_zero

Mathlib/RingTheory/MvPowerSeries/Evaluation.lean

@@ -64,6 +64,12 @@ structure HasEval (a : σ → S) : Prop where
   hpow : ∀ s, IsTopologicallyNilpotent (a s)
   tendsto_zero : Tendsto a cofinite (𝓝 0)
 
+theorem HasEval.mono {S : Type*} [CommRing S] {a : σ → S}
+    {t u : TopologicalSpace S} (h : t ≤ u) (ha : @HasEval _ _ _ t a) :
+    @HasEval _ _ _ u a :=
+  ⟨fun s ↦ Filter.Tendsto.mono_right (@HasEval.hpow _ _ _ t a ha s) (nhds_mono h),
+   Filter.Tendsto.mono_right (@HasEval.tendsto_zero σ _ _ t a ha) (nhds_mono h)⟩
+
 theorem HasEval.zero : HasEval (0 : σ → S) where
   hpow _ := .zero
   tendsto_zero := tendsto_const_nhds

Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

@@ -66,6 +66,11 @@ variable (R) in
 scoped instance : TopologicalSpace (MvPowerSeries σ R) :=
   Pi.topologicalSpace
 
+theorem instTopologicalSpace_mono (σ : Type*) {R : Type*} {t u : TopologicalSpace R} (htu : t ≤ u) :
+    @instTopologicalSpace σ R t ≤ @instTopologicalSpace σ R u := by
+  simp only [instTopologicalSpace, Pi.topologicalSpace, ge_iff_le, le_iInf_iff]
+  exact fun i ↦ le_trans (iInf_le _ i) (induced_mono htu)
+
 /-- `MvPowerSeries` on a `T0Space` form a `T0Space` -/
 @[scoped instance]
 theorem instT0Space [T0Space R] : T0Space (MvPowerSeries σ R) := Pi.instT0Space
@@ -127,6 +132,12 @@ theorem continuous_C [Semiring R] :
   · exact tendsto_id
   · exact tendsto_const_nhds
 
+/-- Scalar multiplication on `MvPowerSeries` is continous -/
+instance {S : Type*} [Semiring S] [TopologicalSpace S]
+    [CommSemiring R] [Algebra R S] [ContinuousSMul R S] :
+    ContinuousSMul R (MvPowerSeries σ S) :=
+  instContinuousSMulForall
+
 theorem variables_tendsto_zero [Semiring R] :
     Tendsto (X · : σ → MvPowerSeries σ R) cofinite (nhds 0) := by
   classical