Restriction to smaller polyradii

A series restricted at polyradii s is restricted at any nonnegative polyradii r ≤ s. The resulting ring homomorphism leaves the coefficients unchanged. At positive polyradii it is injective, contractive for the Gauss norms, and has dense image: every polynomial extends to the larger polydisc. No finiteness of the variable set or completeness of the coefficient ring is required.

The restriction maps compose and commute with bounded coefficient maps and variable renaming. For commutative coefficients they are coefficient-algebra homomorphisms and, at positive polyradii, continuous linear maps. These maps compare algebras of functions on nested closed polydiscs.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.1.1.

theorem TauCeti.MvPowerSeries.isRestricted_of_le {σ : Type u_1} {R : Type u_2} [NormedRing R] {r s : σ → ℝ} {f : MvPowerSeries σ R} (hf : MvPowerSeries.IsRestricted s f) (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) : MvPowerSeries.IsRestricted r f

Restrictedness passes to smaller nonnegative polyradii.

noncomputable def TauCeti.MvPowerSeries.restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) : ↥(MvPowerSeries.IsRestricted.subring s) →+* ↥(MvPowerSeries.IsRestricted.subring r)

Restrict a series to smaller nonnegative polyradii, leaving its coefficients unchanged.

@[simp]

theorem TauCeti.MvPowerSeries.coe_restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) (f : ↥(MvPowerSeries.IsRestricted.subring s)) : ↑((restrictedRadiusHom hr hrs) f) = ↑f

Radius restriction leaves the underlying formal series unchanged.

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_injective {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) : Function.Injective ⇑(restrictedRadiusHom hr hrs)

Radius restriction is injective.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_refl {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) : restrictedRadiusHom hr ⋯ = RingHom.id ↥(MvPowerSeries.IsRestricted.subring r)

Restriction to the same radii is the identity.

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_comp {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s t : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) (hs : ∀ (i : σ), 0 ≤ s i) (hst : s ≤ t) : (restrictedRadiusHom hr hrs).comp (restrictedRadiusHom hs hst) = restrictedRadiusHom hr ⋯

Restriction along nested polyradii is the composite of the two restrictions.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s t : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) (hs : ∀ (i : σ), 0 ≤ s i) (hst : s ≤ t) (f : ↥(MvPowerSeries.IsRestricted.subring t)) : (restrictedRadiusHom hr hrs) ((restrictedRadiusHom hs hst) f) = (restrictedRadiusHom hr ⋯) f

Restricting twice agrees with direct restriction.

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_restrictedMap {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) {S : Type u_3} [NormedRing S] [IsUltrametricDist S] (φ : R →+* S) {C : ℝ} (hφ : ∀ (a : R), ‖φ a‖ ≤ C * ‖a‖) (f : ↥(MvPowerSeries.IsRestricted.subring s)) : (restrictedRadiusHom hr hrs) ((restrictedMap φ hφ) f) = (restrictedMap φ hφ) ((restrictedRadiusHom hr hrs) f)

Radius restriction commutes with bounded maps of coefficients.

theorem TauCeti.MvPowerSeries.norm_restrictedRadiusHom_le {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) [∀ (i : σ), Fact (0 < r i)] [∀ (i : σ), Fact (0 < s i)] (f : ↥(MvPowerSeries.IsRestricted.subring s)) : ‖(restrictedRadiusHom hr hrs) f‖ ≤ ‖f‖

Radius restriction is contractive for the Gauss norms.

theorem TauCeti.MvPowerSeries.lipschitzWith_restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) [∀ (i : σ), Fact (0 < r i)] [∀ (i : σ), Fact (0 < s i)] : LipschitzWith 1 ⇑(restrictedRadiusHom hr hrs)

Radius restriction is a Lipschitz map with constant one.

theorem TauCeti.MvPowerSeries.continuous_restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) [∀ (i : σ), Fact (0 < r i)] [∀ (i : σ), Fact (0 < s i)] : Continuous ⇑(restrictedRadiusHom hr hrs)

Radius restriction is continuous in the Gauss norm topologies.

theorem TauCeti.MvPowerSeries.denseRange_restrictedRadiusHom {σ : Type u_1} {R : Type u_2} [NormedRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) [∀ (i : σ), Fact (0 < r i)] : DenseRange ⇑(restrictedRadiusHom hr hrs)

Radius restriction has dense image, since every restricted monomial extends to any radii.

noncomputable def TauCeti.MvPowerSeries.restrictedRadiusAlgHom {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) : ↥(MvPowerSeries.IsRestricted.subring s) →ₐ[R] ↥(MvPowerSeries.IsRestricted.subring r)

Radius restriction as a homomorphism of coefficient algebras.

@[simp]

theorem TauCeti.MvPowerSeries.coe_restrictedRadiusAlgHom {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) : ↑(restrictedRadiusAlgHom hr hrs) = restrictedRadiusHom hr hrs

The algebra homomorphism of radius restriction has the same underlying ring map.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRadiusAlgHom_apply {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) (f : ↥(MvPowerSeries.IsRestricted.subring s)) : (restrictedRadiusAlgHom hr hrs) f = (restrictedRadiusHom hr hrs) f

The algebra form of radius restriction agrees with its ring form on each series.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_polynomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) (p : MvPolynomial σ R) : (restrictedRadiusHom hr hrs) ⟨↑p, ⋯⟩ = ⟨↑p, ⋯⟩

Polynomial inclusion commutes with radius restriction.

theorem TauCeti.MvPowerSeries.restrictedRadiusHom_renameAlgEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} (hr : ∀ (i : σ), 0 ≤ r i) (hrs : r ≤ s) {τ : Type u_3} (e : τ ≃ σ) (f : ↥(MvPowerSeries.IsRestricted.subring (s ∘ ⇑e))) : (restrictedRadiusHom hr hrs) ((MvPowerSeries.IsRestricted.renameAlgEquiv e s) f) = (MvPowerSeries.IsRestricted.renameAlgEquiv e r) ((restrictedRadiusHom ⋯ ⋯) f)

Radius restriction commutes with renaming variables along an equivalence.

noncomputable def TauCeti.MvPowerSeries.restrictedRadiusCLM {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} [∀ (i : σ), Fact (0 < r i)] [∀ (i : σ), Fact (0 < s i)] (hrs : r ≤ s) : ↥(MvPowerSeries.IsRestricted.subring s) →L[R] ↥(MvPowerSeries.IsRestricted.subring r)

Radius restriction as a continuous linear map over the coefficient ring. It is contractive for the Gauss norms (TauCeti.MvPowerSeries.norm_restrictedRadiusHom_le).

@[simp]

theorem TauCeti.MvPowerSeries.restrictedRadiusCLM_apply {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {r s : σ → ℝ} [∀ (i : σ), Fact (0 < r i)] [∀ (i : σ), Fact (0 < s i)] (hrs : r ≤ s) (f : ↥(MvPowerSeries.IsRestricted.subring s)) : (restrictedRadiusCLM hrs) f = (restrictedRadiusHom ⋯ hrs) f

The continuous linear form of radius restriction agrees with its ring form.