The Gauss norm on overconvergent series

The Monsky–Washnitzer algebra carries the unit-radius Gauss norm, induced by its inclusion into the Tate algebra. This makes it an ultrametric normed commutative ring, with multiplicative norm when the coefficient norm is multiplicative. Over a normed field it is a normed algebra. This is the norm used to form residue norms of dagger algebras.

The inclusion toTate is an isometry. Coefficient bounds characterize the norm, constants retain their norm, the variables have norm one, and renaming the variables preserves the norm. Polynomials are dense for this norm. Over a nontrivially normed ultrametric field, the power-bounded elements for the Gauss norm topology are the series of Gauss norm at most one.

References

• E. Grosse-Klönne, Rigid analytic spaces with overconvergent structure sheaf, J. reine angew. Math. 519 (2000), §1.2.

@[instance_reducible]

noncomputable instance TauCeti.Dagger.washnitzerAlgebra.instNormedCommRingSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : NormedCommRing ↥(washnitzerAlgebra σ R)

The unit-radius Gauss norm on overconvergent power series.

instance TauCeti.Dagger.washnitzerAlgebra.instUniformContinuousConstSMulSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : UniformContinuousConstSMul R ↥(washnitzerAlgebra σ R)

Multiplication by a fixed coefficient is uniformly continuous for the Gauss norm.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.norm_toTate {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (f : ↥(washnitzerAlgebra σ R)) : ‖(toTate σ R) f‖ = ‖f‖

The inclusion into the Tate algebra preserves the Gauss norm.

theorem TauCeti.Dagger.washnitzerAlgebra.norm_eq_gaussNorm {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (f : ↥(washnitzerAlgebra σ R)) : ‖f‖ = MvPowerSeries.gaussNorm norm (fun (x : σ) => 1) ↑f

The norm on the Monsky–Washnitzer algebra is the unit-radius Gauss norm.

theorem TauCeti.Dagger.washnitzerAlgebra.isometry_toTate {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : Isometry ⇑(toTate σ R)

The inclusion into the Tate algebra is an isometry for the Gauss norms.

instance TauCeti.Dagger.washnitzerAlgebra.instIsUltrametricDistSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : IsUltrametricDist ↥(washnitzerAlgebra σ R)

The Gauss norm on overconvergent series is ultrametric.

instance TauCeti.Dagger.washnitzerAlgebra.instNormMulClassSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] : NormMulClass ↥(washnitzerAlgebra σ R)

The Gauss norm is multiplicative when the coefficient norm is.

instance TauCeti.Dagger.washnitzerAlgebra.instNormOneClassSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] : NormOneClass ↥(washnitzerAlgebra σ R)

The Gauss norm of one agrees with that of the coefficient ring.

theorem TauCeti.Dagger.washnitzerAlgebra.norm_coeff_le {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (f : ↥(washnitzerAlgebra σ R)) (t : σ →₀ ℕ) : ‖(MvPowerSeries.coeff t) ↑f‖ ≤ ‖f‖

Every coefficient is bounded by the Gauss norm of an overconvergent series.

theorem TauCeti.Dagger.washnitzerAlgebra.norm_le_iff {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {f : ↥(washnitzerAlgebra σ R)} {r : ℝ} (hr : 0 ≤ r) : ‖f‖ ≤ r ↔ ∀ (t : σ →₀ ℕ), ‖(MvPowerSeries.coeff t) ↑f‖ ≤ r

A nonnegative bound on the Gauss norm is equivalent to the same bound on all coefficients.

theorem TauCeti.Dagger.washnitzerAlgebra.norm_lt_iff {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {f : ↥(washnitzerAlgebra σ R)} {r : ℝ} : ‖f‖ < r ↔ ∀ (t : σ →₀ ℕ), ‖(MvPowerSeries.coeff t) ↑f‖ < r

A strict bound on the Gauss norm is equivalent to a strict bound on all coefficients.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.norm_algebraMap {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] (a : R) : ‖(algebraMap R ↥(washnitzerAlgebra σ R)) a‖ = ‖a‖

Constants retain their coefficient norm.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.norm_X {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] (i : σ) : ‖X σ R i‖ = 1

Each coordinate variable has Gauss norm one.

@[simp]

theorem TauCeti.Dagger.washnitzerAlgebra.norm_renameAlgEquiv {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {τ : Type u_3} (e : σ ≃ τ) (f : ↥(washnitzerAlgebra σ R)) : ‖(renameAlgEquiv e) f‖ = ‖f‖

Renaming the variables preserves the Gauss norm.

theorem TauCeti.Dagger.washnitzerAlgebra.denseRange_ofMvPolynomial {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] : DenseRange ⇑(ofMvPolynomial σ R)

Polynomials are dense in the Monsky–Washnitzer algebra for the Gauss norm.

@[instance_reducible]

noncomputable instance TauCeti.Dagger.washnitzerAlgebra.instNormedAlgebraSubtypeMvPowerSeriesMemSubalgebra {σ : Type u_1} {R : Type u_2} [NormedCommRing R] [IsUltrametricDist R] {K : Type u_3} [NormedField K] [NormedAlgebra K R] : NormedAlgebra K ↥(washnitzerAlgebra σ R)

Overconvergent series over a normed algebra carry the induced normed-algebra structure.

theorem TauCeti.Dagger.washnitzerAlgebra.isPowerBounded_iff_norm_le_one {σ : Type u_1} {K : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] {f : ↥(washnitzerAlgebra σ K)} : Huber.IsPowerBounded f ↔ ‖f‖ ≤ 1

The power-bounded overconvergent series are the Gauss unit ball: f ∈ K⟨X⟩† is power-bounded for the Gauss norm topology iff ‖f‖ ≤ 1.