English
The evaluation maps between multivariate polynomials, power series, and ring homomorphisms are uniformly continuous under their respective Pi-topologies and uniform structures.
Русский
Оценочная карта между многочленами, рядaми степеней и гомоморфизмами сохраняет равномерную непрерывность в рамках соответствующих топологий и униформных структур.
LaTeX
$$Uniform continuity statements for eval₂Hom and related maps$$
Lean4
theorem _root_.MvPolynomial.toMvPowerSeries_uniformContinuous [IsUniformAddGroup R] [IsUniformAddGroup S]
[IsLinearTopology S S] (hφ : Continuous φ) (ha : HasEval a) : UniformContinuous (MvPolynomial.eval₂Hom φ a) := by
classical
apply uniformContinuous_of_continuousAt_zero
rw [ContinuousAt, map_zero, IsLinearTopology.hasBasis_ideal.tendsto_right_iff]
intro I hI
let n : σ → ℕ := fun s ↦ sInf {n : ℕ | (a s) ^ n.succ ∈ I}
have hn_ne : ∀ s, Set.Nonempty {n : ℕ | (a s) ^ n.succ ∈ I} := fun s ↦
by
rcases ha.hpow s |>.eventually_mem hI |>.exists_forall_of_atTop with ⟨n, hn⟩
use n
simpa using hn n.succ n.le_succ
have hn : Set.Finite (n.support) := by
change n =ᶠ[cofinite] 0
filter_upwards [ha.tendsto_zero.eventually_mem hI] with s has
simpa [n, Pi.zero_apply, Nat.sInf_eq_zero, or_iff_left (hn_ne s).ne_empty] using has
let n₀ : σ →₀ ℕ := .ofSupportFinite n hn
let D := Iic n₀
have hD : Set.Finite D := finite_Iic _
have : ∀ d ∈ D, ∀ᶠ (p : MvPolynomial σ R) in 𝓝 0, φ (p.coeff d) ∈ I := fun d hd ↦
by
have : Tendsto (φ ∘ coeff d ∘ toMvPowerSeries) (𝓝 0) (𝓝 0) :=
hφ.comp (continuous_coeff R d) |>.comp continuous_induced_dom |>.tendsto' 0 0 (map_zero _)
filter_upwards [this.eventually_mem hI] with f hf
simpa using hf
rw [← hD.eventually_all] at this
filter_upwards [this] with p hp
rw [coe_eval₂Hom, SetLike.mem_coe, eval₂_eq]
apply Ideal.sum_mem
intro d _
by_cases hd : d ∈ D
· exact Ideal.mul_mem_right _ _ (hp d hd)
· apply Ideal.mul_mem_left
simp only [mem_Iic, D, Finsupp.le_iff] at hd
push_neg at hd
rcases hd with ⟨s, hs', hs⟩
exact I.prod_mem hs' (I.pow_mem_of_pow_mem (Nat.sInf_mem (hn_ne s)) hs)
