Documentation

TauCeti.RingTheory.Huber.Restricted.GaussNorm

The Gauss norm topology on restricted multivariate series #

The trivial-weight Huber restricted-series ring and Mathlib's unit-radius restricted-series subring have the same underlying power series. Their topologies also agree: the Huber topology requires every coefficient to lie in a prescribed open additive subgroup, while the Gauss norm measures the supremum of all coefficient norms.

The comparison below is an algebra equivalence continuous in both directions. Over a complete base it identifies the completed Huber Tate algebra with the Banach algebra of restricted series. This allows normed-ring results, including Weierstrass division, to be transported to the completed topological algebra without changing its topology.

The normed series are Mathlib's MvPowerSeries.IsRestricted.subring, with the Gauss norm constructed using William Coram's MvPowerSeries.gaussNorm infrastructure; no second series type or norm is introduced here.

Main results #

References #

source
theorem TauCeti.Huber.isRestricted_iff_isRestricted_one {n : ℕ} {R : Type u_1} [NormedRing R] {f : MvPowerSeries (Fin n) R} :
IsRestricted f ↔ MvPowerSeries.IsRestricted (fun (x : Fin n) => 1) f

The topological restrictedness condition is Mathlib's normed restrictedness condition at unit polyradius.

source
theorem TauCeti.Huber.weightedRestrictedSubring_eq_isRestricted_subring {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
weightedRestrictedSubring (fun (x : Fin n) => {1}) ⋯ = MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1

The trivial-weight Huber subring is Mathlib's subring of unit-radius restricted series. This is an equality of subrings; their topological structures are compared separately below.

source
noncomputable def TauCeti.Huber.restrictedMvPowerSeriesGaussEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
↥(weightedRestrictedSubring (fun (x : Fin n) => {1}) ⋯) ≃+* ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)

The identity on underlying series identifies the trivial-weight Huber ring with the Gauss-normed unit-radius restricted-series ring.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Huber.coe_restrictedMvPowerSeriesGaussEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] (f : ↥(weightedRestrictedSubring (fun (x : Fin n) => {1}) ⋯)) :
    ↑(restrictedMvPowerSeriesGaussEquiv f) = ↑f

    The Gauss comparison preserves the underlying formal power series.

    source
    @[simp]
    theorem TauCeti.Huber.coe_restrictedMvPowerSeriesGaussEquiv_symm {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)) :
    ↑(restrictedMvPowerSeriesGaussEquiv.symm f) = ↑f

    The inverse Gauss comparison also preserves the underlying formal power series.

    source
    noncomputable def TauCeti.Huber.restrictedMvPowerSeriesGaussAlgEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
    ↥(weightedRestrictedSubring (fun (x : Fin n) => {1}) ⋯) ≃ₐ[R] ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)

    The identity Gauss comparison also respects the coefficient-algebra structure.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Huber.coe_restrictedMvPowerSeriesGaussAlgEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
      ⇑restrictedMvPowerSeriesGaussAlgEquiv = ⇑restrictedMvPowerSeriesGaussEquiv

      The algebra Gauss comparison has the same underlying map as the ring comparison.

      source
      @[simp]
      theorem TauCeti.Huber.coe_restrictedMvPowerSeriesGaussAlgEquiv_symm {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
      ⇑restrictedMvPowerSeriesGaussAlgEquiv.symm = ⇑restrictedMvPowerSeriesGaussEquiv.symm

      The inverse algebra Gauss comparison has the same map as the inverse ring comparison.

      source
      theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesGaussEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
      Continuous ⇑restrictedMvPowerSeriesGaussEquiv

      The Huber restricted-series topology makes the comparison to the Gauss topology continuous. All coefficients in a sufficiently small open subgroup give a uniformly small Gauss norm.

      source
      theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesGaussEquiv_symm {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] :
      Continuous ⇑restrictedMvPowerSeriesGaussEquiv.symm

      The inverse comparison is continuous for the Gauss topology. A small Gauss norm places every coefficient in any prescribed open additive subgroup of the coefficient ring.

      source
      noncomputable def TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
      restrictedMvPowerSeriesCompletion n R ≃+* ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)

      Over a complete nonarchimedean normed ring, the completed Huber Tate algebra is the Gauss-normed ring of unit-radius restricted series. The equivalence is continuous in both directions by the theorems below.

      Equations
      Instances For
        source
        noncomputable def TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussAlgEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
        restrictedMvPowerSeriesCompletion n R ≃ₐ[R] ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)

        Over a complete coefficient ring, the completed Gauss comparison is an algebra equivalence. It composes the completion's coefficient-algebra comparison with the identity on series.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Huber.coe_restrictedMvPowerSeriesCompletionGaussAlgEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
          ⇑restrictedMvPowerSeriesCompletionGaussAlgEquiv = ⇑restrictedMvPowerSeriesCompletionGaussEquiv

          The completed algebra Gauss comparison has the same map as the completed ring comparison.

          source
          @[simp]
          theorem TauCeti.Huber.coe_restrictedMvPowerSeriesCompletionGaussAlgEquiv_symm {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
          ⇑restrictedMvPowerSeriesCompletionGaussAlgEquiv.symm = ⇑restrictedMvPowerSeriesCompletionGaussEquiv.symm

          The inverse completed algebra Gauss comparison agrees with the inverse ring comparison.

          source
          @[simp]
          theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv_coe {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] (f : ↥(weightedRestrictedSubring (fun (x : Fin n) => {1}) ⋯)) :
          restrictedMvPowerSeriesCompletionGaussEquiv ↑f = restrictedMvPowerSeriesGaussEquiv f

          On a series in the dense subring, the completed comparison is the identity on formal power series, regarded as a unit-radius restricted series.

          source
          @[simp]
          theorem TauCeti.Huber.restrictedMvPowerSeriesCompletionGaussEquiv_symm_apply {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] (f : ↥(MvPowerSeries.IsRestricted.subring fun (x : Fin n) => 1)) :
          restrictedMvPowerSeriesCompletionGaussEquiv.symm f = ↑(restrictedMvPowerSeriesGaussEquiv.symm f)

          The inverse completed comparison takes a Gauss-normed restricted series to its canonical image in the Huber completion.

          source
          theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesCompletionGaussEquiv {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
          Continuous ⇑restrictedMvPowerSeriesCompletionGaussEquiv

          The completed comparison is continuous from the canonical completion topology to the Gauss norm topology.

          source
          theorem TauCeti.Huber.continuous_restrictedMvPowerSeriesCompletionGaussEquiv_symm {n : ℕ} {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] [CompleteSpace R] :
          Continuous ⇑restrictedMvPowerSeriesCompletionGaussEquiv.symm

          The inverse completed comparison is continuous from the Gauss norm topology to the canonical completion topology.