Documentation

TauCeti.Analysis.Normed.Ring.PseudoUniformizer

Multiplicative pseudo-uniformisers of seminormed rings #

A multiplicative pseudo-uniformiser of a seminormed ring R is a unit ϖ with 0 < ‖ϖ‖ < 1 such that multiplication by ϖ scales the norm exactly: ‖ϖ * x‖ = ‖ϖ‖ * ‖x‖ for every x. A seminormed ring is Tate (for its given norm) when it has one. These are the quantitative counterparts of the topological notions TauCeti.Huber.IsPseudoUniformizer and TauCeti.Huber.IsTateRing: the topological Tate property of a ring does not imply that an arbitrary compatible norm admits a multiplicative pseudo-uniformiser, so the normed notion records a property of the specified norm.

The exact scaling law propagates to every module with contractive scalar action: for IsBoundedSMul R M and every integer n, ‖ϖ ^ n • m‖ = ‖ϖ‖ ^ n * ‖m‖. Consequently every vector m of nonzero norm has a unique rescaling ϖ ^ n • m into the shell ‖ϖ‖ < ‖ϖ ^ n • m‖ ≤ 1. These are the shell arguments used throughout nonarchimedean functional analysis over Banach–Tate rings, for instance to turn topological statements about bounded maps into norm estimates. The inverse norm formula and the scaling law hold more generally for any unit u of positive norm with ‖u * x‖ = ‖u‖ * ‖x‖, whatever the size of ‖u‖.

The existence of a multiplicative pseudo-uniformiser forces ‖1‖ = 1, so a Tate ring is nonzero, and its powers provide a zero sequence of units (TauCeti.HasZeroSequenceOfUnits). An ultrametric Tate commutative ring is a Tate ring in the topological sense. A seminormed algebra with ‖1‖ = 1 over a normed field has a multiplicative pseudo-uniformiser given by any scalar c with 0 < ‖c‖ < 1; in particular nontrivially normed fields are Tate.

In an ultrametric commutative ring with ‖1‖ = 1, the powers of the ideal ϖ R° of the closed unit ball R° are the closed balls of radius ‖ϖ‖ ^ n. So the norm topology of R° is its ϖ-adic topology, and R° is ϖ-adically complete when R is complete. This is how ϖ-adic completeness of the unit ball of a Banach algebra, such as the ring of restricted series with integral coefficients, follows from metric completeness.

Main definitions #

Main results #

References #

Units scaling the norm exactly #

source
theorem TauCeti.NormedRing.norm_units_smul_of_norm_mul {R : Type u_1} [SeminormedRing R] {u : Rˣ} (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (m : M) :
‖↑u • m‖ = ‖↑u‖ * ‖m‖

Exact scaling on modules: a unit by which left multiplication scales the norm exactly scales the norm of every vector exactly under a contractive scalar action.

source
theorem TauCeti.NormedRing.norm_units_inv_smul_of_norm_mul {R : Type u_1} [SeminormedRing R] {u : Rˣ} (hu0 : 0 < ‖↑u‖) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (m : M) :
‖↑u⁻¹ • m‖ = ‖↑u‖⁻¹ * ‖m‖

The inverse of a unit of positive norm by which left multiplication scales the norm exactly scales the norm of every vector by ‖u‖⁻¹ under a contractive scalar action.

source
theorem TauCeti.NormedRing.norm_units_zpow_smul_of_norm_mul {R : Type u_1} [SeminormedRing R] {u : Rˣ} (hu0 : 0 < ‖↑u‖) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (n : ℤ) (m : M) :
‖↑(u ^ n) • m‖ = ‖↑u‖ ^ n * ‖m‖

Exact scaling by integer powers: ‖u ^ n • m‖ = ‖u‖ ^ n * ‖m‖ for every integer n, for a unit u of positive norm by which left multiplication scales the norm exactly, under a contractive scalar action.

source
theorem TauCeti.NormedRing.norm_units_zpow_of_norm_mul {R : Type u_1} [SeminormedRing R] {u : Rˣ} (hu0 : 0 < ‖↑u‖) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) (n : ℤ) :
‖↑(u ^ n)‖ = ‖↑u‖ ^ n

An integer power of a unit of positive norm by which left multiplication scales the norm exactly has the corresponding power of its norm.

source
theorem TauCeti.NormedRing.norm_units_pow_of_norm_mul {R : Type u_1} [SeminormedRing R] {u : Rˣ} (hu0 : 0 < ‖↑u‖) (hu : ∀ (x : R), ‖↑u * x‖ = ‖↑u‖ * ‖x‖) (n : ℕ) :
‖↑u ^ n‖ = ‖↑u‖ ^ n

A natural power of a unit of positive norm by which left multiplication scales the norm exactly has the corresponding power of its norm.

source
theorem TauCeti.NormedRing.norm_smul_of_isUnit_of_norm_eq_one {R : Type u_1} {M : Type u_2} [SeminormedRing R] [NormMulClass R] [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] {u : R} (hu : IsUnit u) (h1 : ‖u‖ = 1) (m : M) :
‖u • m‖ = ‖m‖

A unit of norm one of a ring with multiplicative norm acts isometrically under a contractive scalar action.

source
structure TauCeti.NormedRing.PseudoUniformizer (R : Type u_1) [SeminormedRing R] :
Type u_1

A multiplicative pseudo-uniformiser of a seminormed ring R: a unit ϖ with 0 < ‖ϖ‖ < 1 by which left multiplication scales the norm exactly, ‖ϖ * x‖ = ‖ϖ‖ * ‖x‖. This is data: it records a choice of such a unit for the given norm.

  • unit : Rˣ

    The chosen unit.

  • norm_mul (x : R) : ‖↑self.unit * x‖ = ‖↑self.unit‖ * ‖x‖

    Left multiplication by the chosen unit scales the norm exactly.

  • norm_pos : 0 < ‖↑self.unit‖

    The chosen unit has positive norm.

  • norm_lt_one : ‖↑self.unit‖ < 1

    The chosen unit has norm less than one.

Instances For
    source
    class TauCeti.NormedRing.IsTate (R : Type u_1) [SeminormedRing R] :
    Prop

    A seminormed ring is Tate for its given norm when it admits a multiplicative pseudo-uniformiser. This is a property of the specified norm; for an ultrametric commutative ring it is stronger than the topological TauCeti.Huber.IsTateRing (IsTate.isTateRing). Neither completeness nor the ultrametric inequality is included.

    Instances
      source
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_one {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) :
      ‖1‖ = 1

      The existence of a multiplicative pseudo-uniformiser forces ‖1‖ = 1.

      source
      theorem TauCeti.NormedRing.PseudoUniformizer.normOneClass {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) :
      NormOneClass R

      A seminormed ring with a multiplicative pseudo-uniformiser satisfies ‖1‖ = 1.

      source
      theorem TauCeti.NormedRing.PseudoUniformizer.nontrivial {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) :
      Nontrivial R

      A seminormed ring with a multiplicative pseudo-uniformiser is nonzero.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_inv {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) :
      ‖↑ϖ.unit⁻¹‖ = ‖↑ϖ.unit‖⁻¹

      The inverse of a multiplicative pseudo-uniformiser has the inverse norm.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_smul {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (m : M) :
      ‖↑ϖ.unit • m‖ = ‖↑ϖ.unit‖ * ‖m‖

      Exact scaling on modules: a multiplicative pseudo-uniformiser scales the norm of every vector exactly under a contractive scalar action.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_inv_smul {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (m : M) :
      ‖↑ϖ.unit⁻¹ • m‖ = ‖↑ϖ.unit‖⁻¹ * ‖m‖

      The inverse of a multiplicative pseudo-uniformiser scales the norm of every vector by ‖ϖ‖⁻¹ under a contractive scalar action.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_zpow_smul {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (n : ℤ) (m : M) :
      ‖↑(ϖ.unit ^ n) • m‖ = ‖↑ϖ.unit‖ ^ n * ‖m‖

      Exact scaling by integer powers: ‖ϖ ^ n • m‖ = ‖ϖ‖ ^ n * ‖m‖ for every integer n, under a contractive scalar action.

      source
      theorem TauCeti.NormedRing.PseudoUniformizer.existsUnique_norm_zpow_smul_mem_Ioc {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] {m : M} (hm : ‖m‖ ≠ 0) :
      ∃! n : ℤ, ‖↑(ϖ.unit ^ n) • m‖ ∈ Set.Ioc ‖↑ϖ.unit‖ 1

      The shell: every vector m of nonzero norm has a unique rescaling ϖ ^ n • m, n ∈ ℤ, with ‖ϖ‖ < ‖ϖ ^ n • m‖ ≤ 1.

      source
      theorem TauCeti.NormedRing.PseudoUniformizer.exists_zpow_mul_norm_lt {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] {m : M} (hm : ‖m‖ ≠ 0) {δ : ℝ} (k : ℤ) (hδ : ‖↑ϖ.unit‖ ^ k < δ) :
      ∃ (n : ℤ), ‖↑ϖ.unit‖ ^ n * ‖m‖ < δ ∧ (‖↑ϖ.unit‖ ^ n)⁻¹ ≤ (‖↑ϖ.unit‖ ^ (k + 1))⁻¹ * ‖m‖

      For a vector m of nonzero norm and δ > ‖ϖ‖ ^ k, there is an integer n with ‖ϖ‖ ^ n * ‖m‖ < δ whose inverse factor satisfies (‖ϖ‖ ^ n)⁻¹ ≤ (‖ϖ‖ ^ (k + 1))⁻¹ * ‖m‖. This is the common shell estimate for global operator bounds and quantitative preimage bounds.

      source
      theorem TauCeti.NormedRing.PseudoUniformizer.zpowCeil_norm_zpow_smul {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) {M : Type u_2} [SeminormedAddGroup M] [MulActionWithZero R M] [IsBoundedSMul R M] (n : ℤ) (m : M) :
      zpowCeil ‖↑ϖ.unit‖ ‖↑(ϖ.unit ^ n) • m‖ = ‖↑ϖ.unit‖ ^ n * zpowCeil ‖↑ϖ.unit‖ ‖m‖

      Exact scaling of the rounded norm: after rounding the norm of M up to ‖ϖ‖ ^ ℤ ∪ {0}, integer powers of ϖ still scale it exactly, zpowCeil ‖ϖ‖ ‖ϖ ^ n • m‖ = ‖ϖ‖ ^ n * zpowCeil ‖ϖ‖ ‖m‖.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_zpow {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) (n : ℤ) :
      ‖↑(ϖ.unit ^ n)‖ = ‖↑ϖ.unit‖ ^ n

      An integer power of a multiplicative pseudo-uniformiser has the corresponding power of its norm.

      source
      @[simp]
      theorem TauCeti.NormedRing.PseudoUniformizer.norm_pow {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) (n : ℕ) :
      ‖↑ϖ.unit ^ n‖ = ‖↑ϖ.unit‖ ^ n

      A natural power of a multiplicative pseudo-uniformiser has the corresponding power of its norm.

      source
      def TauCeti.NormedRing.PseudoUniformizer.pow {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) (n : ℕ) (hn : n ≠ 0) :
      PseudoUniformizer R

      A positive power of a multiplicative pseudo-uniformiser is again one.

      Instances For
        source
        @[simp]
        theorem TauCeti.NormedRing.PseudoUniformizer.pow_unit {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) (n : ℕ) (hn : n ≠ 0) :
        (ϖ.pow n hn).unit = ϖ.unit ^ n

        The unit of ϖ.pow n hn is ϖ.unit ^ n.

        source
        theorem TauCeti.NormedRing.PseudoUniformizer.isPseudoUniformizer {R : Type u_1} [SeminormedRing R] (ϖ : PseudoUniformizer R) :
        Huber.IsPseudoUniformizer ↑ϖ.unit

        A multiplicative pseudo-uniformiser is a pseudo-uniformiser in the topological sense of TauCeti.Huber.IsPseudoUniformizer: a topologically nilpotent unit.

        source
        noncomputable def TauCeti.NormedRing.PseudoUniformizer.ofAlgebraMap {K : Type u_2} {A : Type u_3} [NormedField K] [SeminormedRing A] [NormedAlgebra K A] [NormOneClass A] {c : K} (hc : c ≠ 0) (hc1 : ‖c‖ < 1) :
        PseudoUniformizer A

        Small nonzero scalars are multiplicative pseudo-uniformisers of a seminormed algebra with ‖1‖ = 1 over a normed field: the image of c with c ≠ 0 and ‖c‖ < 1.

        Instances For
          source
          @[simp]
          theorem TauCeti.NormedRing.PseudoUniformizer.coe_unit_ofAlgebraMap {K : Type u_2} {A : Type u_3} [NormedField K] [SeminormedRing A] [NormedAlgebra K A] [NormOneClass A] {c : K} (hc : c ≠ 0) (hc1 : ‖c‖ < 1) :
          ↑(ofAlgebraMap hc hc1).unit = (algebraMap K A) c

          The unit of ofAlgebraMap hc hc1 is the image of c.

          The closed unit ball is ϖ-adic #

          source
          def TauCeti.NormedRing.PseudoUniformizer.toUnitClosedBall {R : Type u_2} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] (ϖ : PseudoUniformizer R) :
          ↥(Subring.unitClosedBall R)

          A multiplicative pseudo-uniformiser as an element of the closed unit ball R°.

          Instances For
            source
            @[simp]
            theorem TauCeti.NormedRing.PseudoUniformizer.coe_toUnitClosedBall {R : Type u_2} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] (ϖ : PseudoUniformizer R) :
            ↑ϖ.toUnitClosedBall = ↑ϖ.unit
            source
            theorem TauCeti.NormedRing.PseudoUniformizer.mem_span_toUnitClosedBall_pow_iff {R : Type u_2} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] (ϖ : PseudoUniformizer R) (n : ℕ) {x : ↥(Subring.unitClosedBall R)} :
            x ∈ Ideal.span {ϖ.toUnitClosedBall} ^ n ↔ ‖↑x‖ ≤ ‖↑ϖ.unit‖ ^ n

            The powers of ϖ R° are closed balls: an element of the closed unit ball R° lies in (ϖ R°) ^ n exactly when its norm is at most ‖ϖ‖ ^ n.

            source
            theorem TauCeti.NormedRing.PseudoUniformizer.isAdic_span_toUnitClosedBall {R : Type u_2} [SeminormedCommRing R] [IsUltrametricDist R] [NormOneClass R] (ϖ : PseudoUniformizer R) :
            IsAdic (Ideal.span {ϖ.toUnitClosedBall})

            The closed unit ball is ϖ-adic: its norm topology is the ϖ R°-adic topology.

            source
            theorem TauCeti.NormedRing.PseudoUniformizer.isAdicComplete_span_toUnitClosedBall {R : Type u_3} [NormedCommRing R] [IsUltrametricDist R] [NormOneClass R] [CompleteSpace R] (ϖ : PseudoUniformizer R) :
            IsAdicComplete (Ideal.span {ϖ.toUnitClosedBall}) ↥(Subring.unitClosedBall R)

            The closed unit ball of a complete ring is ϖ-adically complete.

            source
            @[instance 100]
            instance TauCeti.NormedRing.IsTate.normOneClass {R : Type u_1} [SeminormedRing R] [IsTate R] :
            NormOneClass R

            A Tate seminormed ring satisfies ‖1‖ = 1.

            source
            @[instance 100]
            instance TauCeti.NormedRing.IsTate.hasZeroSequenceOfUnits {R : Type u_1} [SeminormedRing R] [IsTate R] :
            HasZeroSequenceOfUnits R

            A Tate seminormed ring admits a zero sequence of units via the powers of any multiplicative pseudo-uniformiser.

            source
            @[instance 100]
            instance TauCeti.NormedRing.IsTate.isTateRing {R : Type u_2} [SeminormedCommRing R] [IsUltrametricDist R] [IsTate R] :
            Huber.IsTateRing R

            An ultrametric Tate seminormed commutative ring is a Tate ring in the topological sense: its closed unit ball is a ring of definition and a multiplicative pseudo-uniformiser is a topologically nilpotent unit (TauCeti.Huber.IsTateRing.of_isUnit_norm_lt_one).

            source
            theorem TauCeti.NormedRing.IsTate.of_normedAlgebra (K : Type u_2) {A : Type u_3} [NontriviallyNormedField K] [SeminormedRing A] [NormedAlgebra K A] [NormOneClass A] :
            IsTate A

            A seminormed algebra with ‖1‖ = 1 over a nontrivially normed field is Tate, by a scalar c with 0 < ‖c‖ < 1 (PseudoUniformizer.ofAlgebraMap).

            source
            instance TauCeti.NormedRing.IsTate.of_nontriviallyNormedField (K : Type u_2) [NontriviallyNormedField K] :
            IsTate K

            A nontrivially normed field is Tate; for instance ℚ_[p].