The unit ball and the residue module of an ultrametric normed module #
Let R be an ultrametric seminormed commutative ring with ‖1‖ = 1, with closed unit ball
R⁰ = Subring.unitClosedBall R and open-ball ideal R⁰⁰ = TauCeti.unitBallIdeal R, and let M
be an ultrametric seminormed R-module with contractive scalar action. The vectors of norm at
most one form an R⁰-submodule M⁰ = TauCeti.unitClosedBallSubmodule R M of M, and the
residue module of M is
M~ = TauCeti.ResidueModule R M = M⁰ ⧸ R⁰⁰ • M⁰,
a module over the residue ring R~ = R⁰ ⧸ R⁰⁰. Reduction modulo R⁰⁰ • M⁰ is the
R⁰-linear map TauCeti.ResidueModule.mk.
Every vector of R⁰⁰ • M⁰ has norm less than one. The converse holds when the norm of M takes
its values in ‖ϖ‖ ^ ℤ ∪ {0} for a multiplicative pseudo-uniformiser ϖ of R (this is the
condition zpowCeil ‖ϖ‖ ‖m‖ = ‖m‖ of TauCeti.zpowCeil, which rounding the norm achieves): a
vector of norm less than one then has norm at most ‖ϖ‖, so it is ϖ times a vector of M⁰.
Thus for such norms R⁰⁰ • M⁰ = ϖ M⁰ is the open unit ball of M, and two vectors of M⁰ have
the same residue exactly when they are at distance less than one
(TauCeti.ResidueModule.mk_eq_mk_iff). This is the reduction used by Serre to compare
orthonormal bases of M with bases of M~.
Main definitions #
TauCeti.unitClosedBallSubmodule R M: the closed unit ballM⁰as anR⁰-submodule ofM.TauCeti.ResidueModule R M: the residue moduleM⁰ ⧸ R⁰⁰ • M⁰, a module overR⁰ ⧸ R⁰⁰.TauCeti.ResidueModule.mk: the reduction mapM⁰ → M~.
Main results #
TauCeti.norm_lt_one_of_mem_unitBallIdeal_smul_top: the vectors ofR⁰⁰ • M⁰have norm less than one.TauCeti.mem_unitBallIdeal_smul_top_of_norm_le: the vectors ofM⁰of norm at most‖ϖ‖lie inR⁰⁰ • M⁰, for any multiplicative pseudo-uniformiserϖ.TauCeti.mem_unitBallIdeal_smul_top_iff: for a norm with values in‖ϖ‖ ^ ℤ ∪ {0}, these are exactly the vectors ofM⁰of norm less than one.TauCeti.ResidueModule.mk_eq_zero_iffandTauCeti.ResidueModule.mk_eq_mk_iff: the same statement for the reduction map.
References #
- J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §1.
- C. Johansson and J. Newton, Extended eigenvarieties for overconvergent cohomology, arXiv:1604.07739, §2.1.
The closed unit ball of a module. In an ultrametric seminormed module with contractive
scalar action, the open additive subgroup IsUltrametricDist.closedBall_openAddSubgroup of
vectors of norm at most one is a submodule over the closed unit ball Subring.unitClosedBall R
of the scalars.
Instances For
A vector lies in the closed unit ball exactly when its norm is at most one.
The carrier of unitClosedBallSubmodule R M is Metric.closedBall 0 1.
The residue module M⁰ ⧸ R⁰⁰ • M⁰ of an ultrametric seminormed module: the closed unit
ball modulo the multiples of the open-ball ideal unitBallIdeal R of the scalars. It is a module
over the residue ring Subring.unitClosedBall R ⧸ unitBallIdeal R.
Instances For
The reduction map from the closed unit ball to the residue module.
Instances For
The reduction map is the quotient map.
Every element of the residue module is the residue of a vector of the closed unit ball.
The residue ring acts on residues through representatives:
the residue of a times the residue of m is the residue of a • m.
The multiples R⁰⁰ • M⁰ of the open-ball ideal have norm less than one.
A vector of the closed unit ball of norm at most ‖ϖ‖, for a multiplicative
pseudo-uniformiser ϖ, is ϖ times a vector of the closed unit ball, so it lies in R⁰⁰ • M⁰.
The residue module of a discretely normed module. If the norm of M takes its values in
‖ϖ‖ ^ ℤ ∪ {0} for a multiplicative pseudo-uniformiser ϖ, then R⁰⁰ • M⁰ consists exactly of
the vectors of M⁰ of norm less than one.
The residue of a vector vanishes exactly when the vector has norm less than one, for a norm
with values in ‖ϖ‖ ^ ℤ ∪ {0}.
Two vectors of the closed unit ball have the same residue exactly when they are at distance
less than one, for a norm with values in ‖ϖ‖ ^ ℤ ∪ {0}.