The coefficient model of the unit-radius Tate algebra

At unit polyradius, restrictedness says exactly that the coefficient family tends to zero along the cofinite filter; at a constant radius ρ, it says that ‖aₜ‖ ρ^|t| tends to zero. The unit-radius case identifies the native restricted-series module with the model space C₀(WithDiscreteTopology (σ →₀ ℕ), R). The identification is linear and isometric for the Gauss norm, and it sends a restricted monomial to the corresponding coordinate vector.

The construction specializes the module-valued coefficient comparison TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffLinearIsometryEquiv; the family seminorm agrees with the Gauss norm on the native restricted-series subring.

The discrete-topology wrapper is essential when σ is infinite: the exponent type may carry a different topology from its use here as the discrete index of a null family.

Main result

• TauCeti.MvPowerSeries.restrictedCoeffLinearIsometryEquiv: the coefficient linear isometry between unit-radius restricted series and null coefficient families.

References

• S. Bosch, U. Güntzer and R. Remmert, Non-Archimedean Analysis, §5.1.1.

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

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

theorem MvPowerSeries.isRestricted_const_iff {σ : Type u_1} {R : Type u_2} [NormedRing R] {f : MvPowerSeries σ R} {ρ : ℝ} : IsRestricted (fun (x : σ) => ρ) f ↔ Filter.Tendsto (fun (t : σ →₀ ℕ) => ‖(coeff t) f‖ * ρ ^ Finsupp.degree t) Filter.cofinite (nhds 0)

Restrictedness at a constant radius ρ: the weighted coefficient norms ‖aᵥ‖ ρ^|ν| tend to zero. The case ρ = 1 is isRestricted_one_iff.

noncomputable def TauCeti.MvPowerSeries.restrictedCoeffLinearIsometryEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1) ≃ₗᵢ[R] ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) R

Taking coefficients is a linear isometric equivalence from the unit-radius restricted-series module to the space of coefficient families vanishing at infinity on the discrete exponent set.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedCoeffLinearIsometryEquiv_apply {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : σ) => 1)) (t : σ →₀ ℕ) : (restrictedCoeffLinearIsometryEquiv f) (WithTopology.toTopology ⊥ t) = (MvPowerSeries.coeff t) ↑f

The coefficient isometry evaluates a restricted series at each exponent by taking that coefficient.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedCoeffLinearIsometryEquiv_symm_apply {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (a : ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) R) (t : σ →₀ ℕ) : (MvPowerSeries.coeff t) ↑(restrictedCoeffLinearIsometryEquiv.symm a) = a (WithTopology.toTopology ⊥ t)

The inverse coefficient isometry builds the restricted series with the prescribed null coefficient family.

@[instance_reducible]

noncomputable def TauCeti.MvPowerSeries.restrictedExponentDecidableEq {σ : Type u_1} : DecidableEq (WithDiscreteTopology (σ →₀ ℕ))

A classical equality decision procedure for the discrete exponent set, used to form coordinate vectors.

@[instance_reducible]

noncomputable def TauCeti.MvPowerSeries.restrictedVariableDecidableEq {σ : Type u_1} : DecidableEq σ

A classical equality decision procedure for variables, used to compute monomial coefficients.

@[simp]

theorem TauCeti.MvPowerSeries.restrictedCoeffLinearIsometryEquiv_monomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (t : σ →₀ ℕ) (a : R) : restrictedCoeffLinearIsometryEquiv ⟨(MvPowerSeries.monomial t) a, ⋯⟩ = ZeroAtInftyContinuousMap.single (WithTopology.toTopology ⊥ t) a

A restricted monomial maps to the coordinate vector at its exponent.