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_2} [group_with_zero G₀] [topological_space G₀] [has_continuous_mul G₀] {f : α → G₀} {l : filter α} {x y : G₀} (hf : filter.tendsto f l (𝓝 x)) :

filter.tendsto (λ (a : α), f a / y) l (𝓝 (x / y))

theorem continuous_at.div_const {α : Type u_1} {G₀ : Type u_2} [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)

theorem continuous_within_at.div_const {α : Type u_1} {G₀ : Type u_2} [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_2} [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

theorem continuous.div_const {α : Type u_1} {G₀ : Type u_2} [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_3) [has_zero G₀] [has_inv G₀] [topological_space G₀] :

Type

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

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_2} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv' G₀] {x : G₀} (hx : x ≠ 0) :

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

theorem continuous_on_inv' {G₀ : Type u_2} [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_2} [has_zero G₀] [has_inv G₀] [topological_space G₀] [has_continuous_inv' G₀] {l : filter α} {f : α → G₀} {a : G₀} (hf : filter.tendsto f l (𝓝 a)) (ha : a ≠ 0) :

filter.tendsto (λ (x : α), (f x)⁻¹) l (𝓝 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_2} [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_2} [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

theorem continuous.inv' {α : Type u_1} {G₀ : Type u_2} [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_2} [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_2} [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 (𝓝 a)) (hg : filter.tendsto g l (𝓝 b)) (hy : b ≠ 0) :

filter.tendsto (f / g) l (𝓝 (a / b))

theorem continuous_within_at.div {α : Type u_1} {G₀ : Type u_2} [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_2} [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_2} [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.

theorem continuous.div {α : Type u_1} {G₀ : Type u_2} [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_2} [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}

Left and right multiplication as homeomorphisms #

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 := _}

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 tendsto_fpow {G₀ : Type u_2} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv' G₀] [has_continuous_mul G₀] {x : G₀} (hx : x ≠ 0) (m : ℤ) :

filter.tendsto (λ (x : G₀), x ^ m) (𝓝 x) (𝓝 (x ^ m))

theorem continuous_at_fpow {G₀ : Type u_2} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv' G₀] [has_continuous_mul G₀] {x : G₀} (hx : x ≠ 0) (m : ℤ) :

continuous_at (λ (x : G₀), x ^ m) x

theorem continuous_on_fpow {G₀ : Type u_2} [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.fpow {α : Type u_1} {G₀ : Type u_2} [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 (𝓝 a)) (ha : a ≠ 0) (m : ℤ) :

filter.tendsto (λ (x : α), f x ^ m) l (𝓝 (a ^ m))

theorem continuous_at.fpow {α : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv' G₀] [has_continuous_mul G₀] {f : α → G₀} [topological_space α] {a : α} (hf : continuous_at f a) (ha : f a ≠ 0) (m : ℤ) :

continuous_at (λ (x : α), f x ^ m) a

theorem continuous.fpow {α : Type u_1} {G₀ : Type u_2} [group_with_zero G₀] [topological_space G₀] [has_continuous_inv' G₀] [has_continuous_mul G₀] {f : α → G₀} [topological_space α] (hf : continuous f) (h0 : ∀ (a : α), f a ≠ 0) (m : ℤ) :

continuous (λ (x : α), f x ^ m)