3.1. Preliminaries on p-adic Banach spaces🔗

We first fix the functional-analytic language. The reader comfortable with p-adic Banach spaces and orthonormal bases may skip to the next section.

Definition3.1.1

uses 0used by 0✓L∃∀N

Let B be an L-vector space. A valuation on B is a function v : B \to \R \cup \set{+\infty} such that (i) v(x) = +\infty iff x = 0; (ii) v(x+y) \geq \min(v(x), v(y)) for all x,y \in B; and (iii) v(\lambda x) = \vp(\lambda) + v(x) for all \lambda \in L, x \in B. Such a valuation induces a norm, hence a topology, on B. (In mathlib, valuations on rings and fields are abstracted by ValuativeRel; the vector-space notion above corresponds, via v = -\log\norm{\cdot}, to ultrametric norms, i.e. IsUltrametricDist, which is the language the formalisation uses throughout.)

Lean code for Definition3.1.1●2 definitions

class(8 methods)defined in Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean

complete

class ValuativeRel.{u_1} (R : Type u_1) [Semiring R] : Type u_1

class ValuativeRel.{u_1} (R : Type u_1)
  [Semiring R] : Type u_1

The class `[ValuativeRel R]` class introduces an operator `x ≤ᵥ y : Prop` for `x y : R`
which is the natural relation arising from (the equivalence class of) a valuation on `R` when `R`
is a ring. More precisely, if `v` is a valuation on `R` then the associated relation is
`x ≤ᵥ y ↔ v x ≤ v y`. Use this class to talk about the case where `R` is equipped
with an equivalence class of valuations.

Methods

vle : R → R → Prop

The valuation less-equal operator arising from `ValuativeRel`.

vle_total : ∀ (x y : R), x ≤ᵥ y ∨ y ≤ᵥ x

vle_trans : ∀ {z y x : R}, x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z

vle_add : ∀ {x y z : R}, x ≤ᵥ z → y ≤ᵥ z → x + y ≤ᵥ z

mul_vle_mul_left : ∀ {x y : R}, x ≤ᵥ y → ∀ (z : R), x * z ≤ᵥ y * z

vle_mul_cancel : ∀ {x y z : R}, ¬z ≤ᵥ 0 → x * z ≤ᵥ y * z → x ≤ᵥ y

not_vle_one_zero : ¬1 ≤ᵥ 0

vle_mul_comm : ∀ {x y : R}, x * y ≤ᵥ y * x

class(1 method)defined in Mathlib/Topology/MetricSpace/Ultra/Basic.lean

complete

class IsUltrametricDist.{u_2} (X : Type u_2) [Dist X] : Prop

class IsUltrametricDist.{u_2} (X : Type u_2)
  [Dist X] : Prop

The `dist : X → X → ℝ` respects the ultrametric inequality
of `dist(x, z) ≤ max (dist(x,y)) (dist(y,z))`.

Methods

dist_triangle_max : ∀ (x y z : X), dist x z ≤ max (dist x y) (dist y z)

Definition3.1.2

uses 0used by 1✓L∃∀N

An L-Banach space is a complete topological L-vector space B whose topology is induced from a valuation v (in the sense of Definition 3.1.1). (Mathlib expresses this as a complete normed space, NormedSpace + CompleteSpace, with the ultrametric inequality supplied per-space.)

Lean code for Definition3.1.2●2 definitions

class(extends 5, 8 methods)defined in Mathlib/Analysis/Normed/Module/Basic.lean

complete

class NormedSpace.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜]
  [SeminormedAddCommGroup E] : Type (max u_6 u_7)

class NormedSpace.{u_6, u_7} (𝕜 : Type u_6)
  (E : Type u_7) [NormedField 𝕜]
  [SeminormedAddCommGroup E] :
  Type (max u_6 u_7)

A normed space over a normed field is a vector space endowed with a norm which satisfies the
equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove
`‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`.

Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this
typeclass can be used for "seminormed spaces" too, just as `Module` can be used for
"semimodules".

Extends

Module 𝕜 E

Methods

smul : 𝕜 → E → E

Inherited from

Module
DistribMulAction
MulAction
SemigroupAction
SMul

mul_smul : ∀ (x y : 𝕜) (b : E), (x * y) • b = x • y • b

Inherited from

Module
DistribMulAction
MulAction
SemigroupAction

one_smul : ∀ (b : E), 1 • b = b

Inherited from

Module
DistribMulAction
MulAction

smul_zero : ∀ (a : 𝕜), a • 0 = 0

Inherited from

Module
DistribMulAction

smul_add : ∀ (a : 𝕜) (x y : E), a • (x + y) = a • x + a • y

Inherited from

Module
DistribMulAction

add_smul : ∀ (r s : 𝕜) (x : E), (r + s) • x = r • x + s • x

Inherited from

Module

zero_smul : ∀ (x : E), 0 • x = 0

Inherited from

Module

norm_smul_le : ∀ (a : 𝕜) (b : E), ‖a • b‖ ≤ ‖a‖ * ‖b‖

A normed space over a normed field is a vector space endowed with a norm which satisfies the
equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove
`‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`.

Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this
typeclass can be used for "seminormed spaces" too, just as `Module` can be used for
"semimodules".

class(1 method)defined in Mathlib/Topology/UniformSpace/Cauchy.lean

complete

class CompleteSpace.{u} (α : Type u) [UniformSpace α] : Prop

class CompleteSpace.{u} (α : Type u)
  [UniformSpace α] : Prop

A complete space is defined here using uniformities. A uniform space
is complete if every Cauchy filter converges.

Methods

complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds x

In a complete uniform space, every Cauchy filter converges.

Definition3.1.3

uses 0used by 1✓L∃∀N

Let I be a set and \ell^0_\infty(I, L) the L-Banach space of families (a_i)_{i \in I} in L tending to 0 (for every \epsilon > 0, \abs{a_i}_L < \epsilon for all but finitely many i), with valuation v((a_i)_i) = \inf_{i} \vp(a_i). An orthonormal basis of an L-Banach space B is a family (e_i)_{i \in I} for which the map \ell^0_\infty(I, L) \longrightarrow B, \qquad (a_i)_i \longmapsto \sum_{i} a_i e_i is an isometric isomorphism. (If B has valuation v_B with v_B(B) = \vp(L), such a basis always exists. Mathlib has the space \ell^0_\infty(I,L) as ZeroAtInftyContinuousMap — written C_0(I, L) — and orthonormal bases appear as concrete isometric equivalences onto it, such as PadicInt.mahlerEquiv below.)

Lean code for Definition3.1.3●1 definition

structure(extends 1, 3 fields)defined in Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

complete

structure ZeroAtInftyContinuousMap.{u, v} (α : Type u) (β : Type v)
  [TopologicalSpace α] [Zero β] [TopologicalSpace β] : Type (max u v)

structure ZeroAtInftyContinuousMap.{u, v}
  (α : Type u) (β : Type v)
  [TopologicalSpace α] [Zero β]
  [TopologicalSpace β] : Type (max u v)

`C₀(α, β)` is the type of continuous functions `α → β` which vanish at infinity from a
topological space to a metric space with a zero element.

When possible, instead of parametrizing results over `(f : C₀(α, β))`,
you should parametrize over `(F : Type*) [ZeroAtInftyContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `ZeroAtInftyContinuousMapClass`.

Extends

C(α, β)

Fields

toFun : α → β

Inherited from

ContinuousMap

continuous_toFun : Continuous self.toFun

Inherited from

ContinuousMap

zero_at_infty' : Filter.Tendsto self.toFun (Filter.cocompact α) (nhds 0)

The function tends to zero along the `cocompact` filter.

Definition3.1.4

uses 0used by 0!L∃∀N

Let B be an L-Banach space and B^* = \mathrm{Hom}_{\mathrm{cts}}(B, L) its continuous dual. (Mathlib: NormedSpace.Dual carries the strong topology, WeakDual the weak one.) The strong topology is induced by the dual valuation v^*(\mu) = \inf_{x \in B}\big(\vp(\mu(x)) - v(x)\big); it is the topology of uniform convergence. The weak topology is induced by the semivaluations v_x(\mu) = \vp(\mu(x)) for x \in B; it is the topology of pointwise convergence. The dual is complete for both, is an L-Banach space for the strong topology, and B is reflexive precisely when B^* carries the weak topology.

Lean code for Definition3.1.4●2 declarations, 1 missing

NormedSpace.Dualmissing declaration

declaration not found (name was not present during directive/code-block registration)

defdefined in Mathlib/Topology/Algebra/Module/Spaces/WeakDual.lean

complete

def WeakDual.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜]
  [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜]
  [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
  Type (max u_6 u_7)

def WeakDual.{u_6, u_7} (𝕜 : Type u_6)
  (E : Type u_7) [CommSemiring 𝕜]
  [TopologicalSpace 𝕜] [ContinuousAdd 𝕜]
  [ContinuousConstSMul 𝕜 𝕜]
  [AddCommMonoid E] [Module 𝕜 E]
  [TopologicalSpace E] :
  Type (max u_6 u_7)

The weak star topology is the topology coarsest topology on `E →L[𝕜] 𝕜` such that all
functionals `fun v => v x` are continuous.