mathlib documentation

topology.algebra.uniform_group

Uniform structure on topological groups

@[class]
structure uniform_add_group (α : Type u_3) [uniform_space α] [add_group α] :
Prop

A uniform (additive) group is a group in which the addition and negation are uniformly continuous.

Instances
theorem uniform_add_group.mk' {α : Type u_1} [uniform_space α] [add_group α] :
uniform_continuous (λ (p : α × α), p.fst + p.snd)uniform_continuous (λ (p : α), -p)uniform_add_group α

theorem uniform_continuous_sub {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (p : α × α), p.fst - p.snd)

theorem uniform_continuous.sub {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f g : β → α} :
uniform_continuous funiform_continuous guniform_continuous (λ (x : β), f x - g x)

theorem uniform_continuous.neg {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f : β → α} :
uniform_continuous funiform_continuous (λ (x : β), -f x)

theorem uniform_continuous_neg {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (x : α), -x)

theorem uniform_continuous.add {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] {f g : β → α} :
uniform_continuous funiform_continuous guniform_continuous (λ (x : β), f x + g x)

theorem uniform_continuous_add {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] :
uniform_continuous (λ (p : α × α), p.fst + p.snd)

@[instance]
def prod.uniform_add_group {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] :

theorem uniformity_translate {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
filter.map (λ (x : α × α), (x.fst + a, x.snd + a)) (𝓤 α) = 𝓤 α

theorem uniform_embedding_translate {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (a : α) :
uniform_embedding (λ (x : α), x + a)

theorem uniformity_eq_comap_nhds_zero (α : Type u_1) [uniform_space α] [add_group α] [uniform_add_group α] :
𝓤 α = filter.comap (λ (x : α × α), x.snd - x.fst) (𝓝 0)

theorem group_separation_rel {α : Type u_1} [uniform_space α] [add_group α] [uniform_add_group α] (x y : α) :
(x, y) 𝓢 α x - y closure {0}

theorem uniform_continuous_of_tendsto_zero {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] {f : α → β} [is_add_group_hom f] :

theorem uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [add_group α] [uniform_add_group α] [uniform_space β] [add_group β] [uniform_add_group β] {f : α → β} [is_add_group_hom f] :

The right uniformity on a topological group.

Equations
@[class]
structure add_comm_group.is_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] :
× β → γ) → Prop
  • add_left : ∀ (a a' : α) (b : β), f (a + a', b) = f (a, b) + f (a', b)
  • add_right : ∀ (a : α) (b b' : β), f (a, b + b') = f (a, b) + f (a, b')

-bilinearity for maps between additive commutative groups.

Instances
theorem add_comm_group.is_Z_bilin.comp_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] {g : γ → δ} [add_comm_group δ] [is_add_group_hom g] :

@[instance]
def add_comm_group.is_Z_bilin.comp_swap {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] :

theorem add_comm_group.is_Z_bilin.zero_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (b : β) :
f (0, b) = 0

theorem add_comm_group.is_Z_bilin.zero_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (a : α) :
f (a, 0) = 0

theorem add_comm_group.is_Z_bilin.zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] :
f (0, 0) = 0

theorem add_comm_group.is_Z_bilin.neg_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (a : α) (b : β) :
f (-a, b) = -f (a, b)

theorem add_comm_group.is_Z_bilin.neg_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (a : α) (b : β) :
f (a, -b) = -f (a, b)

theorem add_comm_group.is_Z_bilin.sub_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (a a' : α) (b : β) :
f (a - a', b) = f (a, b) - f (a', b)

theorem add_comm_group.is_Z_bilin.sub_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_group α] [add_comm_group β] [add_comm_group γ] (f : α × β → γ) [add_comm_group.is_Z_bilin f] (a : α) (b b' : β) :
f (a, b - b') = f (a, b) - f (a, b')

theorem is_Z_bilin.tendsto_zero_left {α : Type u_1} {β : Type u_2} [topological_space α] [add_comm_group α] [topological_space β] [add_comm_group β] {G : Type u_5} [uniform_space G] [add_comm_group G] {ψ : α × β → G} (hψ : continuous ψ) [ψbilin : add_comm_group.is_Z_bilin ψ] (x₁ : α) :
filter.tendsto ψ (𝓝 (x₁, 0)) (𝓝 0)

theorem is_Z_bilin.tendsto_zero_right {α : Type u_1} {β : Type u_2} [topological_space α] [add_comm_group α] [topological_space β] [add_comm_group β] {G : Type u_5} [uniform_space G] [add_comm_group G] {ψ : α × β → G} (hψ : continuous ψ) [ψbilin : add_comm_group.is_Z_bilin ψ] (y₁ : β) :
filter.tendsto ψ (𝓝 (0, y₁)) (𝓝 0)

theorem tendsto_sub_comap_self {α : Type u_1} {β : Type u_2} [topological_space α] [add_comm_group α] [topological_add_group α] [topological_space β] [add_comm_group β] {e : β → α} [is_add_group_hom e] (de : dense_inducing e) (x₀ : α) :
filter.tendsto (λ (t : β × β), t.snd - t.fst) (filter.comap (λ (p : β × β), (e p.fst, e p.snd)) (𝓝 (x₀, x₀))) (𝓝 0)

theorem dense_inducing.extend_Z_bilin {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [topological_space α] [add_comm_group α] [topological_add_group α] [topological_space β] [add_comm_group β] [topological_add_group β] [topological_space γ] [add_comm_group γ] [topological_add_group γ] [topological_space δ] [add_comm_group δ] [topological_add_group δ] [uniform_space G] [add_comm_group G] [uniform_add_group G] [separated_space G] [complete_space G] {e : β → α} [is_add_group_hom e] (de : dense_inducing e) {f : δ → γ} [is_add_group_hom f] (df : dense_inducing f) {φ : β × δ → G} (hφ : continuous φ) [bilin : add_comm_group.is_Z_bilin φ] :

Bourbaki GT III.6.5 Theorem I: ℤ-bilinear continuous maps from dense images into a complete Hausdorff group extend by continuity. Note: Bourbaki assumes that α and β are also complete Hausdorff, but this is not necessary.