The coefficient model of module-valued restricted series

At unit polyradius, a restricted family with coefficients in a seminormed additive group E is precisely a null family on the discrete exponent set. Taking coefficients identifies the carrier IsRestrictedFamily.Gauss (fun _ : σ ↦ 1) E with C₀(WithDiscreteTopology (σ →₀ ℕ), E). The coefficient equivalence preserves the Gauss seminorm defined in Module.Norm. It is a norm when the coefficient seminorm is a norm, and it is complete when the coefficient space is complete.

The coefficient comparison is linearly isometric for every bounded coefficient-module action. Finite-support inclusions preserve single-coordinate norms, and every restricted family is the unconditional sum of its single coefficients. Consequently finite-support families are dense. For ring-valued coefficients this norm agrees with the existing unit Gauss norm.

The scalar coefficient comparison in TauCeti.RingTheory.MvPowerSeries.TateAlgebra.Coefficients specializes this construction; IsRestrictedFamily.Gauss.norm_subringLinearEquiv identifies its norm with the scalar Gauss norm. The coefficient comparison uses the coordinate expansion of ZeroAtInftyContinuousMap.

The one-field wrapper retains the existing algebraic restricted-family carrier, but its Gauss topology is distinct from the subgroup's inherited pointwise topology. Only the additive and module structures are transported from that subgroup.

References

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

noncomputable def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffAddEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] : Gauss (fun (x : σ) => 1) E ≃+ ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) E

Taking coefficients identifies unit-radius restricted families with discrete null families.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffAddEquiv_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (a : Gauss (fun (x : σ) => 1) E) (t : σ →₀ ℕ) : (coeffAddEquiv a) (WithTopology.toTopology ⊥ t) = ↑a.toAddSubgroup t

The additive coefficient comparison evaluates by taking the indicated coefficient.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffAddEquiv_symm_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (f : ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) E) (t : σ →₀ ℕ) : ↑(coeffAddEquiv.symm f).toAddSubgroup t = f (WithTopology.toTopology ⊥ t)

The inverse additive comparison has the prescribed coefficients.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.norm_coeffAddEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (a : Gauss (fun (x : σ) => 1) E) : ‖coeffAddEquiv a‖ = ‖a‖

Taking coefficients preserves the unit Gauss seminorm.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.isometry_coeffAddEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] : Isometry ⇑coeffAddEquiv

Taking coefficients preserves the unit Gauss seminorm distance.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.exists_norm_coeff_eq_norm {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (a : Gauss (fun (x : σ) => 1) E) : ∃ (t : σ →₀ ℕ), ‖↑a.toAddSubgroup t‖ = ‖a‖

The unit Gauss seminorm is attained by a coefficient, including for the zero family.

noncomputable def TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffLinearIsometryEquiv {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : Gauss (fun (x : σ) => 1) E ≃ₗᵢ[R] ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) E

Taking coefficients identifies unit-radius restricted families with the discrete c₀ model, preserving the scalar action and the sup seminorm.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffLinearIsometryEquiv_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : Gauss (fun (x : σ) => 1) E) (t : σ →₀ ℕ) : ((coeffLinearIsometryEquiv R) a) (WithTopology.toTopology ⊥ t) = ↑a.toAddSubgroup t

The coefficient comparison evaluates at each exponent by taking that coefficient.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffLinearIsometryEquiv_symm_apply {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (f : ZeroAtInftyContinuousMap (WithDiscreteTopology (σ →₀ ℕ)) E) (t : σ →₀ ℕ) : ↑((coeffLinearIsometryEquiv R).symm f).toAddSubgroup t = f (WithTopology.toTopology ⊥ t)

The inverse coefficient comparison has the prescribed coefficients.

@[simp]

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.coeffLinearIsometryEquiv_ofFinsupp_single {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [DecidableEq (WithDiscreteTopology (σ →₀ ℕ))] (t : σ →₀ ℕ) (e : E) : (coeffLinearIsometryEquiv R) ((ofFinsupp R fun (x : σ) => 1) (Finsupp.single t e)) = ZeroAtInftyContinuousMap.single (WithTopology.toTopology ⊥ t) e

A single coefficient becomes the corresponding coordinate vector. The equality decision is a parameter because the coordinate vector occurs in the public statement.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.hasSum_ofFinsupp_single {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] (a : Gauss (fun (x : σ) => 1) E) : HasSum (fun (t : σ →₀ ℕ) => (ofFinsupp R fun (x : σ) => 1) (Finsupp.single t (↑a.toAddSubgroup t))) a

A unit-radius restricted family is the unconditional sum of its single coefficients.

theorem TauCeti.MvPowerSeries.IsRestrictedFamily.Gauss.denseRange_ofFinsupp {σ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] (R : Type u_3) [SeminormedRing R] [Module R E] [IsBoundedSMul R E] : DenseRange ⇑(ofFinsupp R fun (x : σ) => 1)

Finite-support coefficient families are dense in the unit Gauss topology.