Uniform structure on topological groups
topological_add_group.to_uniform_spaceandtopological_add_group_is_uniformcan be used to construct a canonical uniformity for a topological add group.extension of ℤ-bilinear maps to complete groups (useful for ring completions)
add_group_with_zero_nhd: construct the topological structure from a group with a neighbourhood around zero. Then withtopological_add_group.to_uniform_spaceone can derive auniform_space.
@[class]
- uniform_continuous_sub : uniform_continuous (λ (p : α × α), p.fst - p.snd)
A uniform (additive) group is a group in which the addition and negation are uniformly continuous.
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 f → uniform_continuous g → uniform_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 f → uniform_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 f → uniform_continuous g → uniform_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
uniform_add_group.to_topological_add_group
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α] :
Equations
@[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 β] :
uniform_add_group (α × β)
Equations
theorem
uniformity_translate
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(a : α) :
filter.map (λ (x : α × α), (x.fst + a, x.snd + a)) (uniformity α) = uniformity α
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 α] :
uniformity α = filter.comap (λ (x : α × α), x.snd - x.fst) (nhds 0)
theorem
group_separation_rel
{α : Type u_1}
[uniform_space α]
[add_group α]
[uniform_add_group α]
(x y : α) :
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] :
filter.tendsto f (nhds 0) (nhds 0) → uniform_continuous 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] :
continuous f → uniform_continuous f
def
topological_add_group.to_uniform_space
(G : Type u)
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
Equations
- topological_add_group.to_uniform_space G = {to_topological_space := _inst_2, to_core := {uniformity := filter.comap (λ (p : G × G), p.snd - p.fst) (nhds 0), refl := _, symm := _, comp := _}, is_open_uniformity := _}
theorem
uniformity_eq_comap_nhds_zero'
(G : Type u)
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
uniformity G = filter.comap (λ (p : G × G), p.snd - p.fst) (nhds 0)
theorem
topological_add_group_is_uniform
{G : Type u}
[add_comm_group G]
[topological_space G]
[topological_add_group G] :
theorem
to_uniform_space_eq
{α : Type u}
[u : uniform_space α]
[add_comm_group α]
[uniform_add_group α] :
@[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')
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] :
add_comm_group.is_Z_bilin (g ∘ f)
@[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] :
Equations
- _ = _
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 : β) :
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 : β) :
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 : β) :
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' : β) :
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 ψ (nhds (x₁, 0)) (nhds 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 ψ (nhds (0, y₁)) (nhds 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₀ : α) :
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 φ] :
continuous (_.extend φ)
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.