mathlib documentation

topology.algebra.group_with_zero

Topological group with zero #

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 y : G₀} (hf : filter.tendsto f l (nhds x)) :

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

continuous_at_inv₀ : ∀ ⦃x : G₀⦄, x ≠ 0 → continuous_at has_inv.inv x

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) :

filter.tendsto has_inv.inv (nhds x) (nhds x⁻¹)

theorem continuous_on_inv₀ {G₀ : Type u_3} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv₀ G₀] :

continuous_on has_inv.inv {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

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 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) :

continuous_within_at (f / g) s a

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) :

continuous_on (f / g) s

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) :

continuous_at (f / g) a

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) :

continuous (f / g)

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

homeomorph.mul_left₀ c hc = {to_equiv := {to_fun := (equiv.mul_left₀ c hc).to_fun, inv_fun := (equiv.mul_left₀ c hc).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

@[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

homeomorph.mul_right₀ c hc = {to_equiv := {to_fun := (equiv.mul_right₀ c hc).to_fun, inv_fun := (equiv.mul_right₀ c hc).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}

@[simp]

theorem homeomorph.coe_mul_left₀ {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c ≠ 0) :

⇑(homeomorph.mul_left₀ c hc) = has_mul.mul c

@[simp]

theorem homeomorph.mul_left₀_symm_apply {α : Type u_1} [topological_space α] [group_with_zero α] [has_continuous_mul α] (c : α) (hc : c ≠ 0) :

⇑((homeomorph.mul_left₀ c hc).symm) = has_mul.mul c⁻¹

@[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)