Analytic substitution into restricted power series #
Let R be a complete ultrametric normed commutative ring, let r be positive radii for the
variables X₁, …, X_k, and let g₁, …, g_k be series restricted at positive polyradii s in
variables Y, with Gauss norms ‖gᵢ‖_s ≤ rᵢ. The target algebra R{Y/s} is a complete
ultrametric normed ring, so a series f ∈ R{X/r} can be evaluated at g:
f(g) = ∑ₜ fₜ g₁^t₁ ⋯ g_k^t_k,
the convergent sum of MvPowerSeries.restrictedEval₂. This is the analytic substitution
R{X/r} → R{Y/s}. It is an R-algebra homomorphism that does not increase Gauss norms, and it
is the only continuous one sending Xᵢ to gᵢ. Unlike Mathlib's formal substitution
MvPowerSeries.subst, it allows the gᵢ to have nonzero, even non-nilpotent, constant terms,
paying for this with the norm bounds; where both are defined they agree.
The universal property gives the identity and composition laws and the compatibility with
evaluation. Translation Xᵢ ↦ Xᵢ + aᵢ by constants with ‖aᵢ‖ ≤ rᵢ is an example in which the
constant terms do not vanish: it is an isometric R-algebra automorphism of R{X/r}, with
inverse the translation by -a. Such substitutions are the changes of disc coordinates on closed
polydiscs of arbitrary real radii. Translation of unit-radius topological restricted series by
power-bounded constants is TauCeti.ValuationSpectrum.taylorHom. The Gauss-normed construction
here allows radii that are not norms of elements of R, which no weight family can encode.
Main definitions #
TauCeti.MvPowerSeries.restrictedAnalyticSubst: the substitutionf ↦ f(g)as anR-algebra homomorphismR{X/r} →ₐ[R] R{Y/s}.TauCeti.MvPowerSeries.restrictedTranslateandTauCeti.MvPowerSeries.restrictedTranslateEquiv: translation bya, as an algebra homomorphism and as an algebra automorphism.
Main results #
TauCeti.MvPowerSeries.coeff_restrictedAnalyticSubst: the coefficients off(g)are the convergent sums∑' t, fₜ · coeff e (g₁^t₁ ⋯ g_k^t_k).TauCeti.MvPowerSeries.norm_restrictedAnalyticSubst_le: substitution is contractive.TauCeti.MvPowerSeries.eq_restrictedAnalyticSubst: uniqueness among continuous algebra homomorphisms.TauCeti.MvPowerSeries.restrictedAnalyticSubst_zero_apply: substituting zero gives the constant coefficient.TauCeti.MvPowerSeries.restrictedAnalyticSubst_selfandTauCeti.MvPowerSeries.restrictedAnalyticSubst_comp: the identity and composition laws.TauCeti.MvPowerSeries.restrictedEval₂_restrictedAnalyticSubst: evaluatingf(g)atbis evaluatingfatg(b).TauCeti.MvPowerSeries.restrictedMap_restrictedAnalyticSubst: compatibility with bounded coefficient maps.TauCeti.MvPowerSeries.coe_restrictedAnalyticSubst_eq_subst: agreement with Mathlib's formal substitution whenever the latter is defined.TauCeti.MvPowerSeries.norm_restrictedTranslate: translation preserves the Gauss norm.
References #
- S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, Grundlehren 261, §5.1, for Tate algebras and their homomorphisms.
Analytic substitution. For series gᵢ ∈ R{Y/s} with ‖gᵢ‖ ≤ rᵢ, the R-algebra
homomorphism R{X/r} → R{Y/s} sending f = ∑ₜ fₜ Xᵗ to the convergent sum ∑ₜ fₜ gᵗ. The gᵢ
may have nonzero constant terms.
Instances For
Analytic substitution is evaluation at g in the complete ring R{Y/s}.
The substitution f(g) is the sum of the substituted monomials fₜ gᵗ.
The coefficient of Yᵉ in f(g) is the sum of the coefficients of Yᵉ in the substituted
monomials fₜ gᵗ.
The coefficient formula for analytic substitution: the coefficient of Yᵉ in f(g) is
the convergent sum ∑' t, fₜ · coeff e (g₁^t₁ ⋯ g_k^t_k).
Substitution sends the variable Xᵢ to gᵢ.
Coefficient maps commute with analytic substitution. For a bounded ring homomorphism
φ : R →+* S such that the mapped series φ(gᵢ) still satisfy ‖φ(gᵢ)‖ ≤ rᵢ, mapping the
coefficients of f(g) gives φ(f)(φ(g)).
Comparison with formal substitution. When Mathlib's formal substitution of the gᵢ is
defined, for instance when their constant coefficients are nilpotent, it agrees with analytic
substitution.
Substituting zero evaluates at the origin: f(0) is the constant coefficient of f.
Analytic substitution does not increase the Gauss norm: ‖f(g)‖_s ≤ ‖f‖_r.
Analytic substitution is continuous for the Gauss norms.
Uniqueness of analytic substitution: a continuous R-algebra homomorphism
R{X/r} → R{Y/s} sending each Xᵢ to gᵢ is the substitution f ↦ f(g).
Substituting the variables themselves is the identity.
Composition of analytic substitutions: substituting h into f(g) is substituting the
series g(h) into f.
Applying two analytic substitutions in turn is substituting the composite series.
Evaluation of a substitution: for b in a complete ultrametric ring with ‖bⱼ‖ ≤ s'ⱼ,
evaluating f(g) at b is evaluating f at the values gᵢ(b).
The translated variable Xᵢ + aᵢ has Gauss norm at most rᵢ when ‖aᵢ‖ ≤ rᵢ.
Translation Xᵢ ↦ Xᵢ + aᵢ of the polydisc of radii r, for constants with
‖aᵢ‖ ≤ rᵢ.
Instances For
Translation by a is the analytic substitution Xᵢ ↦ Xᵢ + aᵢ, so the substitution API
(coefficient formula, evaluation, coefficient maps) applies to it.
Translation sends Xᵢ to Xᵢ + aᵢ.
Translation is continuous for the Gauss norm.
Translation by 0 is the identity.
Translations compose additively: translating by a and then by b is translating by
a + b.
Translation is an automorphism: translation by a, with inverse the translation
by -a.
Instances For
The automorphism restrictedTranslateEquiv a is the translation by a.
The inverse of translation by a is translation by -a.
Translation is an isometry for the Gauss norm at the radii r.