Substituting polynomials into Tate algebras

Let R be an ultrametric normed commutative ring with ‖1‖ = 1, and let a s be polynomials in the variables τ, indexed by finitely many s : σ, without constant term and with all coefficients of norm at most 1. Mathlib's formal substitution MvPowerSeries.subst, which sends X s to a s, then carries unit-radius restricted series in σ to unit-radius restricted series in τ without increasing the Gauss norm. It therefore restricts to an R-algebra homomorphism of Tate algebras, and two mutually inverse substitutions give an isometric R-algebra isomorphism.

Renamings of the variables are the simplest examples. The triangular substitutions Xᵢ ↦ Xᵢ + Yᵅⁱ used to make a restricted series distinguished in one variable are the examples this file is written for.

The constant terms are required to vanish because the formal substitution is only defined for such families. Evaluating a Tate algebra at arbitrary elements of norm at most 1 requires the completeness of the target and is not treated here.

Main results

• MvPowerSeries.hasSubst_coe: polynomials without constant term in finitely many variables form a substitutable family, and MvPolynomial.coe_finsuppProd_pow: the coercion to power series commutes with the products of powers that appear in the coefficients of a substitution.
• MvPowerSeries.norm_coeff_subst_le: each coefficient of a substitution is bounded by the supremum of the terms contributing to it, in any ultrametric normed commutative ring.
• MvPowerSeries.norm_coeff_subst_coe_le and MvPowerSeries.norm_coeff_subst_coe_sub_le: for a substitution of unit-ball polynomials, a coefficient is controlled by the coefficients of the substituted series at the exponents contributing to it, possibly after isolating one of them.
• MvPowerSeries.IsRestricted.subst: substitution of unit-ball polynomials without constant term preserves unit-radius restrictedness.
• MvPowerSeries.restrictedSubst: the resulting R-algebra homomorphism of Tate algebras, and MvPowerSeries.norm_restrictedSubst_le: it does not increase the Gauss norm.
• MvPowerSeries.restrictedSubstEquiv: two mutually inverse substitutions give an R-algebra isomorphism of Tate algebras, which is an isometry (MvPowerSeries.norm_restrictedSubstEquiv).

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.3 and §5.2.4.

theorem MvPolynomial.coe_finsuppProd_pow {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] (a : σ → MvPolynomial τ R) (d : σ →₀ ℕ) : ↑(d.prod fun (s : σ) (n : ℕ) => a s ^ n) = d.prod fun (s : σ) (n : ℕ) => ↑(a s) ^ n

The coercion of polynomials to power series commutes with products of powers.

theorem MvPowerSeries.hasSubst_coe {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommRing R] [Finite σ] {a : σ → MvPolynomial τ R} (ha : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) : HasSubst fun (s : σ) => ↑(a s)

Polynomials without constant term form a substitutable family over finitely many variables.

theorem MvPowerSeries.norm_coeff_subst_le {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] {a : σ → MvPowerSeries τ R} (ha : HasSubst a) (f : MvPowerSeries σ R) (e : τ →₀ ℕ) {r : ℝ} (hr : 0 ≤ r) (h : ∀ (d : σ →₀ ℕ), ‖(coeff d) f * (coeff e) (d.prod fun (s : σ) (n : ℕ) => a s ^ n)‖ ≤ r) : ‖(coeff e) (subst a f)‖ ≤ r

Ultrametric bound for the coefficients of a substitution. The coefficient of a substitution is a finite sum of the products coeff d f * coeff e (∏ₛ (a s) ^ (d s)), so it is bounded by any common bound on these products.

theorem MvPowerSeries.isRestricted_one_iff {σ : Type u_1} {R : Type u_3} [NormedCommRing R] {f : MvPowerSeries σ R} : IsRestricted (fun (x : σ) => 1) f ↔ Filter.Tendsto (fun (t : σ →₀ ℕ) => ‖(coeff t) f‖) Filter.cofinite (nhds 0)

Restrictedness at the unit radius is convergence of the coefficient norms to zero.

theorem MvPowerSeries.norm_coeff_subst_coe_le {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] {a : σ → MvPolynomial τ R} (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : MvPowerSeries σ R) (e : τ →₀ ℕ) {r : ℝ} (hr : 0 ≤ r) (h : ∀ (d : σ →₀ ℕ), (d.prod fun (s : σ) (n : ℕ) => a s ^ n).coeff e ≠ 0 → ‖(coeff d) f‖ ≤ r) : ‖(coeff e) (subst (fun (s : σ) => ↑(a s)) f)‖ ≤ r

Coefficients of a substitution of unit-ball polynomials. A coefficient of the substitution is bounded by any common bound on the coefficients of f at the exponents d whose polynomial ∏ₛ (a s) ^ (d s) contributes to it.

theorem MvPowerSeries.norm_coeff_subst_coe_sub_le {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] {a : σ → MvPolynomial τ R} (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : MvPowerSeries σ R) (ν : σ →₀ ℕ) (e : τ →₀ ℕ) {r : ℝ} (hr : 0 ≤ r) (h : ∀ (d : σ →₀ ℕ), d ≠ ν → (d.prod fun (s : σ) (n : ℕ) => a s ^ n).coeff e ≠ 0 → ‖(coeff d) f‖ ≤ r) : ‖(coeff e) (subst (fun (s : σ) => ↑(a s)) f) - (coeff ν) f * (ν.prod fun (s : σ) (n : ℕ) => a s ^ n).coeff e‖ ≤ r

Isolating one term of a substitution. Up to the contribution coeff ν f * coeff e (∏ₛ (a s) ^ (ν s)) of a single exponent ν, a coefficient of a substitution of unit-ball polynomials is bounded by the coefficients of f at the other exponents whose polynomials contribute to it.

theorem MvPowerSeries.IsRestricted.subst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] {a : σ → MvPolynomial τ R} (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) {f : MvPowerSeries σ R} (hf : IsRestricted (fun (x : σ) => 1) f) : IsRestricted (fun (x : τ) => 1) (MvPowerSeries.subst (fun (s : σ) => ↑(a s)) f)

Substitution of unit-ball polynomials preserves restrictedness. If finitely many polynomials without constant term have all coefficients of norm at most 1, then substituting them into a unit-radius restricted series gives a unit-radius restricted series.

noncomputable def MvPowerSeries.restrictedSubst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) : ↥(IsRestricted.subring fun (x : σ) => 1) →ₐ[R] ↥(IsRestricted.subring fun (x : τ) => 1)

Substitution of unit-ball polynomials as a map of Tate algebras. Substituting polynomials without constant term whose coefficients have norm at most 1 is an R-algebra homomorphism between the unit-radius Tate algebras.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MvPowerSeries.coe_restrictedSubst {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : ↥(IsRestricted.subring fun (x : σ) => 1)) : ↑((restrictedSubst a ha₀ ha₁) f) = subst (fun (s : σ) => ↑(a s)) ↑f

The map of Tate algebras is Mathlib's formal substitution.

theorem MvPowerSeries.norm_restrictedSubst_le {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) (f : ↥(IsRestricted.subring fun (x : σ) => 1)) : ‖(restrictedSubst a ha₀ ha₁) f‖ ≤ ‖f‖

Substitution of unit-ball polynomials does not increase the Gauss norm.

noncomputable def MvPowerSeries.restrictedSubstEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) : ↥(IsRestricted.subring fun (x : σ) => 1) ≃ₐ[R] ↥(IsRestricted.subring fun (x : τ) => 1)

Isomorphisms of Tate algebras from inverse substitutions. If two families of unit-ball polynomials without constant term are inverse to each other under substitution, the substitutions are mutually inverse R-algebra isomorphisms of the unit-radius Tate algebras.

Equations

• MvPowerSeries.restrictedSubstEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba = AlgEquiv.ofAlgHom (MvPowerSeries.restrictedSubst a ha₀ ha₁) (MvPowerSeries.restrictedSubst b hb₀ hb₁) ⋯ ⋯

@[simp]

theorem MvPowerSeries.coe_restrictedSubstEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(IsRestricted.subring fun (x : σ) => 1)) : ↑((restrictedSubstEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) f) = subst (fun (s : σ) => ↑(a s)) ↑f

The isomorphism of Tate algebras is the substitution of a.

@[simp]

theorem MvPowerSeries.coe_restrictedSubstEquiv_symm {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(IsRestricted.subring fun (x : τ) => 1)) : ↑((restrictedSubstEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba).symm f) = subst (fun (t : τ) => ↑(b t)) ↑f

The inverse isomorphism of Tate algebras is the substitution of b.

@[simp]

theorem MvPowerSeries.norm_restrictedSubstEquiv {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [Finite σ] (a : σ → MvPolynomial τ R) (ha₀ : ∀ (s : σ), MvPolynomial.constantCoeff (a s) = 0) (ha₁ : ∀ (s : σ) (t : τ →₀ ℕ), ‖(a s).coeff t‖ ≤ 1) [Finite τ] (b : τ → MvPolynomial σ R) (hb₀ : ∀ (t : τ), MvPolynomial.constantCoeff (b t) = 0) (hb₁ : ∀ (t : τ) (u : σ →₀ ℕ), ‖(b t).coeff u‖ ≤ 1) (hab : ∀ (s : σ), (MvPolynomial.aeval b) (a s) = MvPolynomial.X s) (hba : ∀ (t : τ), (MvPolynomial.aeval a) (b t) = MvPolynomial.X t) (f : ↥(IsRestricted.subring fun (x : σ) => 1)) : ‖(restrictedSubstEquiv a ha₀ ha₁ b hb₀ hb₁ hab hba) f‖ = ‖f‖

An isomorphism of Tate algebras given by inverse substitutions preserves the Gauss norm.