mathlib documentation

topology.algebra.monoid

Theory of topological monoids #

In this file we define mixin classes has_continuous_mul and has_continuous_add. While in many applications the underlying type is a monoid (multiplicative or additive), we do not require this in the definitions.

@[class]
structure has_continuous_add (M : Type u_6) [topological_space M] [has_add M] :
Prop

Basic hypothesis to talk about a topological additive monoid or a topological additive semigroup. A topological additive monoid over M, for example, is obtained by requiring both the instances add_monoid M and has_continuous_add M.

Instances
theorem continuous_mul {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] :
continuous (λ (p : M × M), (p.fst) * p.snd)
theorem continuous_add {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] :
continuous (λ (p : M × M), p.fst + p.snd)
theorem continuous.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), f x + g x)
theorem continuous.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : X), (f x) * g x)
theorem continuous_add_left {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] (a : M) :
continuous (λ (b : M), a + b)
theorem continuous_mul_left {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] (a : M) :
continuous (λ (b : M), a * b)
theorem continuous_add_right {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] (a : M) :
continuous (λ (b : M), b + a)
theorem continuous_mul_right {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] (a : M) :
continuous (λ (b : M), b * a)
theorem continuous_on.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {s : set X} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : X), f x + g x) s
theorem continuous_on.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {s : set X} (hf : continuous_on f s) (hg : continuous_on g s) :
continuous_on (λ (x : X), (f x) * g x) s
theorem tendsto_add {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] {a b : M} :
filter.tendsto (λ (p : M × M), p.fst + p.snd) (𝓝 (a, b)) (𝓝 (a + b))
theorem tendsto_mul {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] {a b : M} :
filter.tendsto (λ (p : M × M), (p.fst) * p.snd) (𝓝 (a, b)) (𝓝 (a * b))
theorem filter.tendsto.add {α : Type u_2} {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] {f g : α → M} {x : filter α} {a b : M} (hf : filter.tendsto f x (𝓝 a)) (hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : α), f x + g x) x (𝓝 (a + b))
theorem filter.tendsto.mul {α : Type u_2} {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] {f g : α → M} {x : filter α} {a b : M} (hf : filter.tendsto f x (𝓝 a)) (hg : filter.tendsto g x (𝓝 b)) :
filter.tendsto (λ (x : α), (f x) * g x) x (𝓝 (a * b))
theorem filter.tendsto.const_add {α : Type u_2} {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] (b : M) {c : M} {f : α → M} {l : filter α} (h : filter.tendsto (λ (k : α), f k) l (𝓝 c)) :
filter.tendsto (λ (k : α), b + f k) l (𝓝 (b + c))
theorem filter.tendsto.const_mul {α : Type u_2} {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] (b : M) {c : M} {f : α → M} {l : filter α} (h : filter.tendsto (λ (k : α), f k) l (𝓝 c)) :
filter.tendsto (λ (k : α), b * f k) l (𝓝 (b * c))
theorem filter.tendsto.mul_const {α : Type u_2} {M : Type u_4} [topological_space M] [has_mul M] [has_continuous_mul M] (b : M) {c : M} {f : α → M} {l : filter α} (h : filter.tendsto (λ (k : α), f k) l (𝓝 c)) :
filter.tendsto (λ (k : α), (f k) * b) l (𝓝 (c * b))
theorem filter.tendsto.add_const {α : Type u_2} {M : Type u_4} [topological_space M] [has_add M] [has_continuous_add M] (b : M) {c : M} {f : α → M} {l : filter α} (h : filter.tendsto (λ (k : α), f k) l (𝓝 c)) :
filter.tendsto (λ (k : α), f k + b) l (𝓝 (c + b))
theorem continuous_at.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : X), f x + g x) x
theorem continuous_at.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {x : X} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : X), (f x) * g x) x
theorem continuous_within_at.add {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_add M] [has_continuous_add M] {f g : X → M} {s : set X} {x : X} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : X), f x + g x) s x
theorem continuous_within_at.mul {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [has_mul M] [has_continuous_mul M] {f g : X → M} {s : set X} {x : X} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
continuous_within_at (λ (x : X), (f x) * g x) s x
@[instance]
@[instance]
@[instance]
def pi.has_continuous_mul {ι : Type u_1} {C : ι → Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_mul (C i)] [∀ (i : ι), has_continuous_mul (C i)] :
has_continuous_mul (Π (i : ι), C i)
@[instance]
def pi.has_continuous_add {ι : Type u_1} {C : ι → Type u_2} [Π (i : ι), topological_space (C i)] [Π (i : ι), has_add (C i)] [∀ (i : ι), has_continuous_add (C i)] :
has_continuous_add (Π (i : ι), C i)
theorem has_continuous_add.of_nhds_zero {M : Type (max u_1 u_2)} [add_monoid M] [topological_space M] (hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ + x) (𝓝 0)) (hright : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x + x₀) (𝓝 0)) :
theorem has_continuous_mul.of_nhds_one {M : Type (max u_1 u_2)} [monoid M] [topological_space M] (hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ * x) (𝓝 1)) (hright : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x * x₀) (𝓝 1)) :
theorem has_continuous_mul_of_comm_of_nhds_one (M : Type (max u_1 u_2)) [comm_monoid M] [topological_space M] (hmul : filter.tendsto (function.uncurry has_mul.mul) (𝓝 1 ×ᶠ 𝓝 1) (𝓝 1)) (hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ * x) (𝓝 1)) :
theorem has_continuous_add_of_comm_of_nhds_zero (M : Type (max u_1 u_2)) [add_comm_monoid M] [topological_space M] (hmul : filter.tendsto (function.uncurry has_add.add) (𝓝 0 ×ᶠ 𝓝 0) (𝓝 0)) (hleft : ∀ (x₀ : M), 𝓝 x₀ = filter.map (λ (x : M), x₀ + x) (𝓝 0)) :

The (topological-space) closure of a submonoid of a space M with has_continuous_mul is itself a submonoid.

Equations

The (topological-space) closure of an additive submonoid of a space M with has_continuous_add is itself an additive submonoid.

theorem exists_open_nhds_one_split {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} (hs : s 𝓝 1) :
∃ (V : set M), is_open V 1 V ∀ (v : M), v V∀ (w : M), w Vv * w s
theorem exists_open_nhds_zero_half {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} (hs : s 𝓝 0) :
∃ (V : set M), is_open V 0 V ∀ (v : M), v V∀ (w : M), w Vv + w s
theorem exists_nhds_zero_half {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] {s : set M} (hs : s 𝓝 0) :
∃ (V : set M) (H : V 𝓝 0), ∀ (v : M), v V∀ (w : M), w Vv + w s
theorem exists_nhds_one_split {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {s : set M} (hs : s 𝓝 1) :
∃ (V : set M) (H : V 𝓝 1), ∀ (v : M), v V∀ (w : M), w Vv * w s
theorem exists_nhds_one_split4 {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {u : set M} (hu : u 𝓝 1) :
∃ (V : set M) (H : V 𝓝 1), ∀ {v w s t : M}, v Vw Vs Vt V((v * w) * s) * t u
theorem exists_nhds_zero_quarter {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] {u : set M} (hu : u 𝓝 0) :
∃ (V : set M) (H : V 𝓝 0), ∀ {v w s t : M}, v Vw Vs Vt Vv + w + s + t u
theorem exists_open_nhds_zero_add_subset {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] {U : set M} (hU : U 𝓝 0) :
∃ (V : set M), is_open V 0 V V + V U

Given a open neighborhood U of 0 there is a open neighborhood V of 0 such that V + V ⊆ U.

theorem exists_open_nhds_one_mul_subset {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {U : set M} (hU : U 𝓝 1) :
∃ (V : set M), is_open V 1 V V * V U

Given a neighborhood U of 1 there is an open neighborhood V of 1 such that VV ⊆ U.

theorem tendsto_list_prod {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (l : list ι) :
(∀ (i : ι), i lfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), (list.map (λ (c : ι), f c b) l).prod) x (𝓝 (list.map a l).prod)
theorem tendsto_list_sum {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [add_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (l : list ι) :
(∀ (i : ι), i lfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), (list.map (λ (c : ι), f c b) l).sum) x (𝓝 (list.map a l).sum)
theorem continuous_list_prod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : ι → X → M} (l : list ι) (h : ∀ (i : ι), i lcontinuous (f i)) :
continuous (λ (a : X), (list.map (λ (i : ι), f i a) l).prod)
theorem continuous_list_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_monoid M] [has_continuous_add M] {f : ι → X → M} (l : list ι) (h : ∀ (i : ι), i lcontinuous (f i)) :
continuous (λ (a : X), (list.map (λ (i : ι), f i a) l).sum)
theorem continuous_pow {M : Type u_4} [topological_space M] [monoid M] [has_continuous_mul M] (n : ) :
continuous (λ (a : M), a ^ n)
theorem continuous.pow {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [monoid M] [has_continuous_mul M] {f : X → M} (h : continuous f) (n : ) :
continuous (λ (b : X), f b ^ n)
@[instance]

Put the same topological space structure on the opposite monoid as on the original space.

Equations
theorem continuous_op {α : Type u_2} [topological_space α] :
@[instance]

If multiplication is continuous in the monoid α, then it also is in the monoid αᵒᵖ.

@[instance]

The units of a monoid are equipped with a topology, via the embedding into α × α.

Equations
theorem units.continuous_coe {α : Type u_2} [topological_space α] [monoid α] :
@[instance]

If multiplication on a monoid is continuous, then multiplication on the units of the monoid, with respect to the induced topology, is continuous.

Inversion is also continuous, but we register this in a later file, topology.algebra.group, because the predicate has_continuous_inv has not yet been defined.

theorem submonoid.mem_nhds_one {M : Type u_4} [topological_space M] [comm_monoid M] (S : submonoid M) (oS : is_open S) :
theorem tendsto_multiset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : multiset ι) :
(∀ (i : ι), i sfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), (multiset.map (λ (c : ι), f c b) s).sum) x (𝓝 (multiset.map a s).sum)
theorem tendsto_multiset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : multiset ι) :
(∀ (i : ι), i sfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), (multiset.map (λ (c : ι), f c b) s).prod) x (𝓝 (multiset.map a s).prod)
theorem tendsto_finset_sum {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : finset ι) :
(∀ (i : ι), i sfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), ∑ (c : ι) in s, f c b) x (𝓝 (∑ (c : ι) in s, a c))
theorem tendsto_finset_prod {ι : Type u_1} {α : Type u_2} {M : Type u_4} [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → α → M} {x : filter α} {a : ι → M} (s : finset ι) :
(∀ (i : ι), i sfilter.tendsto (f i) x (𝓝 (a i)))filter.tendsto (λ (b : α), ∏ (c : ι) in s, f c b) x (𝓝 (∏ (c : ι) in s, a c))
theorem continuous_multiset_prod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (s : multiset ι) :
(∀ (i : ι), i scontinuous (f i))continuous (λ (a : X), (multiset.map (λ (i : ι), f i a) s).prod)
theorem continuous_multiset_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (s : multiset ι) :
(∀ (i : ι), i scontinuous (f i))continuous (λ (a : X), (multiset.map (λ (i : ι), f i a) s).sum)
theorem continuous_finset_prod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (s : finset ι) :
(∀ (i : ι), i scontinuous (f i))continuous (λ (a : X), ∏ (i : ι) in s, f i a)
theorem continuous_finset_sum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (s : finset ι) :
(∀ (i : ι), i scontinuous (f i))continuous (λ (a : X), ∑ (i : ι) in s, f i a)
theorem continuous_finprod {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} (hc : ∀ (i : ι), continuous (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
continuous (λ (x : X), ∏ᶠ (i : ι), f i x)
theorem continuous_finsum {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} (hc : ∀ (i : ι), continuous (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
continuous (λ (x : X), ∑ᶠ (i : ι), f i x)
theorem continuous_finprod_cond {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [comm_monoid M] [has_continuous_mul M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p icontinuous (f i)) (hf : locally_finite (λ (i : ι), function.mul_support (f i))) :
continuous (λ (x : X), ∏ᶠ (i : ι) (hi : p i), f i x)
theorem continuous_finsum_cond {ι : Type u_1} {X : Type u_3} {M : Type u_4} [topological_space X] [topological_space M] [add_comm_monoid M] [has_continuous_add M] {f : ι → X → M} {p : ι → Prop} (hc : ∀ (i : ι), p icontinuous (f i)) (hf : locally_finite (λ (i : ι), function.support (f i))) :
continuous (λ (x : X), ∑ᶠ (i : ι) (hi : p i), f i x)