mathlib3 documentation

topology.algebra.uniform_convergence

Algebraic facts about the topology of uniform convergence #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains algebraic compatibility results about the uniform structure of uniform convergence / 𝔖-convergence. They will mostly be useful for defining strong topologies on the space of continuous linear maps between two topological vector spaces.

Main statements #

uniform_fun.uniform_group : if G is a uniform group, then α →ᵤ G a uniform group
uniform_on_fun.uniform_group : if G is a uniform group, then for any 𝔖 : set (set α), α →ᵤ[𝔖] G a uniform group.
uniform_on_fun.has_continuous_smul_of_image_bounded : let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology induced from α →ᵤ[𝔖] E, is a TVS.

Implementation notes #

Like in topology/uniform_space/uniform_convergence_topology, we use the type aliases uniform_fun (denoted α →ᵤ β) and uniform_on_fun (denoted α →ᵤ[𝔖] β) for functions from α to β endowed with the structures of uniform convergence and 𝔖-convergence.

TODO #

uniform_on_fun.has_continuous_smul_of_image_bounded unnecessarily asks for 𝔖 to be nonempty and directed. This will be easy to solve once we know that replacing 𝔖 by its noncovering bornology (i.e not what bornology currently refers to in mathlib) doesn't change the topology.

References #

Tags #

uniform convergence, strong dual

@[protected, instance]

def uniform_fun.add_monoid {α : Type u_1} {β : Type u_2} [add_monoid β] :

add_monoid (uniform_fun α β)

Equations

uniform_fun.add_monoid = pi.add_monoid

@[protected, instance]

def uniform_fun.monoid {α : Type u_1} {β : Type u_2} [monoid β] :

monoid (uniform_fun α β)

Equations

uniform_fun.monoid = pi.monoid

@[protected, instance]

def uniform_on_fun.monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [monoid β] :

monoid (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.monoid = pi.monoid

@[protected, instance]

def uniform_on_fun.add_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_monoid β] :

add_monoid (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.add_monoid = pi.add_monoid

@[protected, instance]

def uniform_fun.add_comm_monoid {α : Type u_1} {β : Type u_2} [add_comm_monoid β] :

add_comm_monoid (uniform_fun α β)

Equations

uniform_fun.add_comm_monoid = pi.add_comm_monoid

@[protected, instance]

def uniform_fun.comm_monoid {α : Type u_1} {β : Type u_2} [comm_monoid β] :

comm_monoid (uniform_fun α β)

Equations

uniform_fun.comm_monoid = pi.comm_monoid

@[protected, instance]

def uniform_on_fun.add_comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_comm_monoid β] :

add_comm_monoid (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.add_comm_monoid = pi.add_comm_monoid

@[protected, instance]

def uniform_on_fun.comm_monoid {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_monoid β] :

comm_monoid (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.comm_monoid = pi.comm_monoid

@[protected, instance]

def uniform_fun.group {α : Type u_1} {β : Type u_2} [group β] :

group (uniform_fun α β)

Equations

uniform_fun.group = pi.group

@[protected, instance]

def uniform_fun.add_group {α : Type u_1} {β : Type u_2} [add_group β] :

add_group (uniform_fun α β)

Equations

uniform_fun.add_group = pi.add_group

@[protected, instance]

def uniform_on_fun.add_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_group β] :

add_group (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.add_group = pi.add_group

@[protected, instance]

def uniform_on_fun.group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [group β] :

group (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.group = pi.group

@[protected, instance]

def uniform_fun.comm_group {α : Type u_1} {β : Type u_2} [comm_group β] :

comm_group (uniform_fun α β)

Equations

uniform_fun.comm_group = pi.comm_group

@[protected, instance]

def uniform_fun.add_comm_group {α : Type u_1} {β : Type u_2} [add_comm_group β] :

add_comm_group (uniform_fun α β)

Equations

uniform_fun.add_comm_group = pi.add_comm_group

@[protected, instance]

def uniform_on_fun.add_comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [add_comm_group β] :

add_comm_group (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.add_comm_group = pi.add_comm_group

@[protected, instance]

def uniform_on_fun.comm_group {α : Type u_1} {β : Type u_2} {𝔖 : set (set α)} [comm_group β] :

comm_group (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.comm_group = pi.comm_group

@[protected, instance]

def uniform_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} [semiring R] [add_comm_monoid β] [module R β] :

module R (uniform_fun α β)

Equations

uniform_fun.module = pi.module α (λ (ᾰ : α), β) R

@[protected, instance]

def uniform_on_fun.module {α : Type u_1} {β : Type u_2} {R : Type u_4} {𝔖 : set (set α)} [semiring R] [add_comm_monoid β] [module R β] :

module R (uniform_on_fun α β 𝔖)

Equations

uniform_on_fun.module = pi.module α (λ (ᾰ : α), β) R

@[protected, instance]

def uniform_fun.uniform_group {α : Type u_1} {G : Type u_2} [group G] [uniform_space G] [uniform_group G] :

uniform_group (uniform_fun α G)

If G is a uniform group, then α →ᵤ G is a uniform group as well.

@[protected, instance]

def uniform_fun.uniform_add_group {α : Type u_1} {G : Type u_2} [add_group G] [uniform_space G] [uniform_add_group G] :

uniform_add_group (uniform_fun α G)

If G is a uniform additive group, then α →ᵤ G is a uniform additive group as well.

@[protected]

theorem uniform_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] [uniform_space G] [uniform_group G] {p : ι → Prop} {b : ι → set G} (h : (nhds 1).has_basis p b) :

(nhds 1).has_basis p (λ (i : ι), {f : uniform_fun α G | ∀ (x : α), f x ∈ b i})

@[protected]

theorem uniform_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] [uniform_space G] [uniform_add_group G] {p : ι → Prop} {b : ι → set G} (h : (nhds 0).has_basis p b) :

(nhds 0).has_basis p (λ (i : ι), {f : uniform_fun α G | ∀ (x : α), f x ∈ b i})

@[protected]

theorem uniform_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G] [uniform_space G] [uniform_add_group G] :

(nhds 0).has_basis (λ (V : set G), V ∈ nhds 0) (λ (V : set G), {f : α → G | ∀ (x : α), f x ∈ V})

@[protected]

theorem uniform_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G] [uniform_space G] [uniform_group G] :

(nhds 1).has_basis (λ (V : set G), V ∈ nhds 1) (λ (V : set G), {f : α → G | ∀ (x : α), f x ∈ V})

@[protected, instance]

def uniform_on_fun.uniform_add_group {α : Type u_1} {G : Type u_2} [add_group G] {𝔖 : set (set α)} [uniform_space G] [uniform_add_group G] :

uniform_add_group (uniform_on_fun α G 𝔖)

Let 𝔖 : set (set α). If G is a uniform additive group, then α →ᵤ[𝔖] G is a uniform additive group as well.

@[protected, instance]

def uniform_on_fun.uniform_group {α : Type u_1} {G : Type u_2} [group G] {𝔖 : set (set α)} [uniform_space G] [uniform_group G] :

uniform_group (uniform_on_fun α G 𝔖)

Let 𝔖 : set (set α). If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group as well.

@[protected]

theorem uniform_on_fun.has_basis_nhds_one_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [group G] [uniform_space G] [uniform_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {p : ι → Prop} {b : ι → set G} (h : (nhds 1).has_basis p b) :

(nhds 1).has_basis (λ (Si : set α × ι), Si.fst ∈ 𝔖 ∧ p Si.snd) (λ (Si : set α × ι), {f : uniform_on_fun α G 𝔖 | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd})

@[protected]

theorem uniform_on_fun.has_basis_nhds_zero_of_basis {α : Type u_1} {G : Type u_2} {ι : Type u_3} [add_group G] [uniform_space G] [uniform_add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {p : ι → Prop} {b : ι → set G} (h : (nhds 0).has_basis p b) :

(nhds 0).has_basis (λ (Si : set α × ι), Si.fst ∈ 𝔖 ∧ p Si.snd) (λ (Si : set α × ι), {f : uniform_on_fun α G 𝔖 | ∀ (x : α), x ∈ Si.fst → f x ∈ b Si.snd})

@[protected]

theorem uniform_on_fun.has_basis_nhds_one {α : Type u_1} {G : Type u_2} [group G] [uniform_space G] [uniform_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :

(nhds 1).has_basis (λ (SV : set α × set G), SV.fst ∈ 𝔖 ∧ SV.snd ∈ nhds 1) (λ (SV : set α × set G), {f : uniform_on_fun α G 𝔖 | ∀ (x : α), x ∈ SV.fst → f x ∈ SV.snd})

@[protected]

theorem uniform_on_fun.has_basis_nhds_zero {α : Type u_1} {G : Type u_2} [add_group G] [uniform_space G] [uniform_add_group G] (𝔖 : set (set α)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :

(nhds 0).has_basis (λ (SV : set α × set G), SV.fst ∈ 𝔖 ∧ SV.snd ∈ nhds 0) (λ (SV : set α × set G), {f : uniform_on_fun α G 𝔖 | ∀ (x : α), x ∈ SV.fst → f x ∈ SV.snd})

theorem uniform_on_fun.has_continuous_smul_induced_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [normed_field 𝕜] [add_comm_group H] [module 𝕜 H] [add_comm_group E] [module 𝕜 E] [topological_space H] [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E] {𝔖 : set (set α)} [linear_map_class hom 𝕜 H (uniform_on_fun α E 𝔖)] (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (φ : hom) (hφ : inducing ⇑φ) (h : ∀ (u : H) (s : set α), s ∈ 𝔖 → bornology.is_vonN_bounded 𝕜 (⇑φ u '' s)) :

has_continuous_smul 𝕜 H

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

For convenience, we don't literally ask for H : submodule (α →ᵤ[𝔖] E). Instead, we prove the result for any vector space H equipped with a linear inducing to α →ᵤ[𝔖] E, which is often easier to use. We also state the submodule version as uniform_on_fun.has_continuous_smul_submodule_of_image_bounded.

theorem uniform_on_fun.has_continuous_smul_submodule_of_image_bounded (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] [uniform_space E] [uniform_add_group E] [has_continuous_smul 𝕜 E] {𝔖 : set (set α)} (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (H : submodule 𝕜 (uniform_on_fun α E 𝔖)) (h : ∀ (u : α → E), u ∈ H → ∀ (s : set α), s ∈ 𝔖 → bornology.is_vonN_bounded 𝕜 (u '' s)) :

has_continuous_smul 𝕜 ↥H

Let E be a TVS, 𝔖 : set (set α) and H a submodule of α →ᵤ[𝔖] E. If the image of any S ∈ 𝔖 by any u ∈ H is bounded (in the sense of bornology.is_vonN_bounded), then H, equipped with the topology of 𝔖-convergence, is a TVS.

If you have a hard time using this lemma, try the one above instead.