mathlib3 documentation

topology.algebra.group_with_zero

Topological group with zero #

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

In this file we define has_continuous_inv₀ to be a mixin typeclass a type with has_inv and has_zero (e.g., a group_with_zero) such that λ x, x⁻¹ is continuous at all nonzero points. Any normed (semi)field has this property. Currently the only example of has_continuous_inv₀ in mathlib which is not a normed field is the type nnnreal (a.k.a. ℝ≥0) of nonnegative real numbers.

Then we prove lemmas about continuity of x ↦ x⁻¹ and f / g providing dot-style *.inv' and *.div operations on filter.tendsto, continuous_at, continuous_within_at, continuous_on, and continuous. As a special case, we provide *.div_const operations that require only group_with_zero and has_continuous_mul instances.

All lemmas about (⁻¹) use inv' in their names because lemmas without ' are used for topological_groups. We also use ' in the typeclass name has_continuous_inv₀ for the sake of consistency of notation.

On a group_with_zero with continuous multiplication, we also define left and right multiplication as homeomorphisms.

A group with zero with continuous multiplication #

If G₀ is a group with zero with continuous (*), then (/y) is continuous for any y. In this section we prove lemmas that immediately follow from this fact providing *.div_const dot-style operations on filter.tendsto, continuous_at, continuous_within_at, continuous_on, and continuous.

theorem filter.tendsto.div_const {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α G₀} {l : filter α} {x : G₀} (hf : filter.tendsto f l (nhds x)) (y : G₀) :
filter.tendsto (λ (a : α), f a / y) l (nhds (x / y))
theorem continuous_at.div_const {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α G₀} [topological_space α] {a : α} (hf : continuous_at f a) (y : G₀) :
continuous_at (λ (x : α), f x / y) a
theorem continuous_within_at.div_const {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α G₀} {s : set α} [topological_space α] {a : α} (hf : continuous_within_at f s a) (y : G₀) :
continuous_within_at (λ (x : α), f x / y) s a
theorem continuous_on.div_const {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α G₀} {s : set α} [topological_space α] (hf : continuous_on f s) (y : G₀) :
continuous_on (λ (x : α), f x / y) s
@[continuity]
theorem continuous.div_const {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α G₀} [topological_space α] (hf : continuous f) (y : G₀) :
continuous (λ (x : α), f x / y)
@[class]
structure has_continuous_inv₀ (G₀ : Type u_4) [has_zero G₀] [has_inv G₀] [topological_space G₀] :
Prop

A type with 0 and has_inv such that λ x, x⁻¹ is continuous at all nonzero points. Any normed (semi)field has this property.

Instances of this typeclass

Continuity of λ x, x⁻¹ at a non-zero point #

We define topological_group_with_zero to be a group_with_zero such that the operation x ↦ x⁻¹ is continuous at all nonzero points. In this section we prove dot-style *.inv' lemmas for filter.tendsto, continuous_at, continuous_within_at, continuous_on, and continuous.

theorem tendsto_inv₀ {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {x : G₀} (hx : x 0) :
theorem filter.tendsto.inv₀ {α : Type u_1} {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {l : filter α} {f : α G₀} {a : G₀} (hf : filter.tendsto f l (nhds a)) (ha : a 0) :
filter.tendsto (λ (x : α), (f x)⁻¹) l (nhds a⁻¹)

If a function converges to a nonzero value, its inverse converges to the inverse of this value. We use the name tendsto.inv₀ as tendsto.inv is already used in multiplicative topological groups.

theorem continuous_within_at.inv₀ {α : Type u_1} {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {f : α G₀} {s : set α} {a : α} [topological_space α] (hf : continuous_within_at f s a) (ha : f a 0) :
continuous_within_at (λ (x : α), (f x)⁻¹) s a
theorem continuous_at.inv₀ {α : Type u_1} {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {f : α G₀} {a : α} [topological_space α] (hf : continuous_at f a) (ha : f a 0) :
continuous_at (λ (x : α), (f x)⁻¹) a
@[continuity]
theorem continuous.inv₀ {α : Type u_1} {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {f : α G₀} [topological_space α] (hf : continuous f) (h0 : (x : α), f x 0) :
continuous (λ (x : α), (f x)⁻¹)
theorem continuous_on.inv₀ {α : Type u_1} {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] {f : α G₀} {s : set α} [topological_space α] (hf : continuous_on f s) (h0 : (x : α), x s f x 0) :
continuous_on (λ (x : α), (f x)⁻¹) s

If G₀ is a group with zero with topology such that x ↦ x⁻¹ is continuous at all nonzero points. Then the coercion Mˣ → M is a topological embedding.

Continuity of division #

If G₀ is a group_with_zero with x ↦ x⁻¹ continuous at all nonzero points and (*), then division (/) is continuous at any point where the denominator is continuous.

theorem filter.tendsto.div {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f g : α G₀} {l : filter α} {a b : G₀} (hf : filter.tendsto f l (nhds a)) (hg : filter.tendsto g l (nhds b)) (hy : b 0) :
filter.tendsto (f / g) l (nhds (a / b))
theorem filter.tendsto_mul_iff_of_ne_zero {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] [t1_space G₀] {f g : α G₀} {l : filter α} {x y : G₀} (hg : filter.tendsto g l (nhds y)) (hy : y 0) :
filter.tendsto (λ (n : α), f n * g n) l (nhds (x * y)) filter.tendsto f l (nhds x)
theorem continuous_within_at.div {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f g : α G₀} [topological_space α] {s : set α} {a : α} (hf : continuous_within_at f s a) (hg : continuous_within_at g s a) (h₀ : g a 0) :
theorem continuous_on.div {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f g : α G₀} [topological_space α] {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) (h₀ : (x : α), x s g x 0) :
theorem continuous_at.div {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f g : α G₀} [topological_space α] {a : α} (hf : continuous_at f a) (hg : continuous_at g a) (h₀ : g a 0) :

Continuity at a point of the result of dividing two functions continuous at that point, where the denominator is nonzero.

@[continuity]
theorem continuous.div {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f g : α G₀} [topological_space α] (hf : continuous f) (hg : continuous g) (h₀ : (x : α), g x 0) :
theorem continuous_on_div {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] :
continuous_on (λ (p : G₀ × G₀), p.fst / p.snd) {p : G₀ × G₀ | p.snd 0}
theorem continuous_at.comp_div_cases {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] [topological_space α] [topological_space β] {a : α} {f g : α G₀} (h : α G₀ β) (hf : continuous_at f a) (hg : continuous_at g a) (hh : g a 0 continuous_at h (a, f a / g a)) (h2h : g a = 0 filter.tendsto h ((nhds a).prod ) (nhds (h a 0))) :
continuous_at (λ (x : α), h x (f x / g x)) a

The function f x / g x is discontinuous when g x = 0. However, under appropriate conditions, h x (f x / g x) is still continuous. The condition is that if g a = 0 then h x y must tend to h a 0 when x tends to a, with no information about y. This is represented by the filter. Note: filter.tendsto_prod_top_iff characterizes this convergence in uniform spaces. See also filter.prod_top and filter.mem_prod_top.

theorem continuous.comp_div_cases {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] [topological_space α] [topological_space β] {f g : α G₀} (h : α G₀ β) (hf : continuous f) (hg : continuous g) (hh : (a : α), g a 0 continuous_at h (a, f a / g a)) (h2h : (a : α), g a = 0 filter.tendsto h ((nhds a).prod ) (nhds (h a 0))) :
continuous (λ (x : α), h x (f x / g x))

h x (f x / g x) is continuous under certain conditions, even if the denominator is sometimes 0. See docstring of continuous_at.comp_div_cases.

Left and right multiplication as homeomorphisms #

@[protected]
def homeomorph.mul_left₀ {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c 0) :
α ≃ₜ α

Left multiplication by a nonzero element in a group_with_zero with continuous multiplication is a homeomorphism of the underlying type.

Equations
@[protected]
def homeomorph.mul_right₀ {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c 0) :
α ≃ₜ α

Right multiplication by a nonzero element in a group_with_zero with continuous multiplication is a homeomorphism of the underlying type.

Equations
@[simp]
@[simp]
theorem homeomorph.coe_mul_right₀ {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c 0) :
(homeomorph.mul_right₀ c hc) = λ (x : α), x * c
@[simp]
theorem homeomorph.mul_right₀_symm_apply {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c 0) :
((homeomorph.mul_right₀ c hc).symm) = λ (x : α), x * c⁻¹
theorem continuous_at_zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] (x : G₀) (m : ) (h : x 0 0 m) :
continuous_at (λ (x : G₀), x ^ m) x
theorem continuous_on_zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] (m : ) :
continuous_on (λ (x : G₀), x ^ m) {0}
theorem filter.tendsto.zpow₀ {α : Type u_1} {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {f : α G₀} {l : filter α} {a : G₀} (hf : filter.tendsto f l (nhds a)) (m : ) (h : a 0 0 m) :
filter.tendsto (λ (x : α), f x ^ m) l (nhds (a ^ m))
theorem continuous_at.zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {X : Type u_4} [topological_space X] {a : X} {f : X G₀} (hf : continuous_at f a) (m : ) (h : f a 0 0 m) :
continuous_at (λ (x : X), f x ^ m) a
theorem continuous_within_at.zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {X : Type u_4} [topological_space X] {a : X} {s : set X} {f : X G₀} (hf : continuous_within_at f s a) (m : ) (h : f a 0 0 m) :
continuous_within_at (λ (x : X), f x ^ m) s a
theorem continuous_on.zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {X : Type u_4} [topological_space X] {s : set X} {f : X G₀} (hf : continuous_on f s) (m : ) (h : (a : X), a s f a 0 0 m) :
continuous_on (λ (x : X), f x ^ m) s
@[continuity]
theorem continuous.zpow₀ {G₀ : Type u_3} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀] [has_continuous_mul G₀] {X : Type u_4} [topological_space X] {f : X G₀} (hf : continuous f) (m : ) (h0 : (a : X), f a 0 0 m) :
continuous (λ (x : X), f x ^ m)