Mathlib.Topology.Algebra.Group.Defs

Module docstring

{"# Definitions about topological groups

In this file we define mixin classes ContinuousInv, IsTopologicalGroup, and ContinuousDiv, as well as their additive versions.

These classes say that the corresponding operations are continuous:

ContinuousInv G says that (·⁻¹) is continuous on G;
IsTopologicalGroup G says that (· * ·) is continuous on G × G and (·⁻¹) is continuous on G;
ContinuousDiv G says that (· / ·) is continuous on G.

For groups, ContinuousDiv G is equivalent to IsTopologicalGroup G, but we use the additive version ContinuousSub for types like NNReal, where subtraction is not given by a - b = a + (-b).

We also provide convenience dot notation lemmas like ContinuousAt.neg. "}

ContinuousNeg structure

(G : Type u) [TopologicalSpace G] [Neg G]

Full source

/-- Basic hypothesis to talk about a topological additive group. A topological additive group
over `M`, for example, is obtained by requiring the instances `AddGroup M` and
`ContinuousAdd M` and `ContinuousNeg M`. -/
class ContinuousNeg (G : Type u) [TopologicalSpace G] [Neg G] : Prop where
  continuous_neg : Continuous fun a : G => -a

Continuous negation

Informal description

The structure `ContinuousNeg` asserts that the negation operation `(·⁻¹)` is continuous on a topological space `G` equipped with a negation operation.

ContinuousInv structure

(G : Type u) [TopologicalSpace G] [Inv G]

Full source

/-- Basic hypothesis to talk about a topological group. A topological group over `M`, for example,
is obtained by requiring the instances `Group M` and `ContinuousMul M` and
`ContinuousInv M`. -/
@[to_additive (attr := continuity)]
class ContinuousInv (G : Type u) [TopologicalSpace G] [Inv G] : Prop where
  continuous_inv : Continuous fun a : G => a⁻¹

Continuous inversion

Informal description

A structure asserting that the inversion operation $ ( \cdot )^{-1} $ on a topological space $ G $ equipped with an inversion operation is continuous.

Filter.Tendsto.inv theorem

{f : α → G} {l : Filter α} {y : G} (h : Tendsto f l (𝓝 y)) : Tendsto (fun x => (f x)⁻¹) l (𝓝 y⁻¹)

Full source

/-- If a function converges to a value in a multiplicative topological group, then its inverse
converges to the inverse of this value.
For the version in topological groups with zero (including topological fields)
assuming additionally that the limit is nonzero, use `Filter.Tendsto.inv₀`. -/
@[to_additive
  "If a function converges to a value in an additive topological group, then its
  negation converges to the negation of this value."]
theorem Filter.Tendsto.inv {f : α → G} {l : Filter α} {y : G} (h : Tendsto f l (𝓝 y)) :
    Tendsto (fun x => (f x)⁻¹) l (𝓝 y⁻¹) :=
  (continuous_inv.tendsto y).comp h

Inversion Preserves Limits in Topological Groups

Informal description

Let $G$ be a topological group with continuous inversion, and let $f : \alpha \to G$ be a function. If $f$ tends to $y$ along a filter $l$ (i.e., $\lim_{x \to l} f(x) = y$), then the function $x \mapsto (f(x))^{-1}$ tends to $y^{-1}$ along the same filter (i.e., $\lim_{x \to l} (f(x))^{-1} = y^{-1}$).

Continuous.inv theorem

(hf : Continuous f) : Continuous fun x => (f x)⁻¹

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem Continuous.inv (hf : Continuous f) : Continuous fun x => (f x)⁻¹ :=
  continuous_inv.comp hf

Continuity of Pointwise Inversion

Informal description

Let $G$ be a topological group with continuous inversion. If $f \colon X \to G$ is a continuous function, then the function $x \mapsto (f(x))^{-1}$ is also continuous.

ContinuousWithinAt.inv theorem

(hf : ContinuousWithinAt f s x) : ContinuousWithinAt (fun x => (f x)⁻¹) s x

Full source

@[to_additive]
nonrec theorem ContinuousWithinAt.inv (hf : ContinuousWithinAt f s x) :
    ContinuousWithinAt (fun x => (f x)⁻¹) s x :=
  hf.inv

Continuity of inversion within a subset at a point

Informal description

Let $G$ be a topological group with continuous inversion. If a function $f \colon X \to G$ is continuous at a point $x$ within a subset $s \subseteq X$, then the function $x \mapsto (f(x))^{-1}$ is also continuous at $x$ within $s$.

ContinuousAt.inv theorem

(hf : ContinuousAt f x) : ContinuousAt (fun x => (f x)⁻¹) x

Full source

@[to_additive (attr := fun_prop)]
nonrec theorem ContinuousAt.inv (hf : ContinuousAt f x) : ContinuousAt (fun x => (f x)⁻¹) x :=
  hf.inv

Continuity of inversion at a point

Informal description

Let $G$ be a topological group with continuous inversion. If a function $f \colon X \to G$ is continuous at a point $x \in X$, then the function $x \mapsto (f(x))^{-1}$ is also continuous at $x$.

ContinuousOn.inv theorem

(hf : ContinuousOn f s) : ContinuousOn (fun x => (f x)⁻¹) s

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousOn.inv (hf : ContinuousOn f s) : ContinuousOn (fun x => (f x)⁻¹) s := fun x hx ↦
  (hf x hx).inv

Continuity of inversion preserves continuity on subsets

Informal description

Let $G$ be a topological group with continuous inversion. If a function $f \colon X \to G$ is continuous on a subset $s \subseteq X$, then the function $x \mapsto (f(x))^{-1}$ is also continuous on $s$.

IsTopologicalAddGroup structure

(G : Type u) [TopologicalSpace G] [AddGroup G] : Prop
    extends ContinuousAdd G, ContinuousNeg G

Full source

/-- A topological (additive) group is a group in which the addition and negation operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformAddGroup` using
`IsTopologicalAddGroup.toUniformSpace` and `isUniformAddGroup_of_addCommGroup`. -/
class IsTopologicalAddGroup (G : Type u) [TopologicalSpace G] [AddGroup G] : Prop
    extends ContinuousAdd G, ContinuousNeg G

Additive topological group

Informal description

An additive topological group is an additive group $ G $ equipped with a topology such that both the addition operation $ (x, y) \mapsto x + y $ and the negation operation $ x \mapsto -x $ are continuous with respect to this topology.

IsTopologicalGroup structure

(G : Type*) [TopologicalSpace G] [Group G] : Prop
    extends ContinuousMul G, ContinuousInv G

Full source

/-- A topological group is a group in which the multiplication and inversion operations are
continuous.

When you declare an instance that does not already have a `UniformSpace` instance,
you should also provide an instance of `UniformSpace` and `IsUniformGroup` using
`IsTopologicalGroup.toUniformSpace` and `isUniformGroup_of_commGroup`. -/
@[to_additive]
class IsTopologicalGroup (G : Type*) [TopologicalSpace G] [Group G] : Prop
    extends ContinuousMul G, ContinuousInv G

Topological group

Informal description

A topological group is a group $G$ equipped with a topology such that the group multiplication operation $(x, y) \mapsto x * y$ and the inversion operation $x \mapsto x^{-1}$ are continuous with respect to this topology.

ContinuousSub structure

(G : Type*) [TopologicalSpace G] [Sub G]

Full source

/-- A typeclass saying that `p : G × G ↦ p.1 - p.2` is a continuous function. This property
automatically holds for topological additive groups but it also holds, e.g., for `ℝ≥0`. -/
class ContinuousSub (G : Type*) [TopologicalSpace G] [Sub G] : Prop where
  continuous_sub : Continuous fun p : G × G => p.1 - p.2

Continuous subtraction

Informal description

A structure asserting that the subtraction operation $(a, b) \mapsto a - b$ is continuous on the topological space $G$ equipped with a subtraction operation. This property is automatically satisfied for topological additive groups but also holds for other structures like the non-negative real numbers $\mathbb{R}_{\geq 0}$.

ContinuousDiv structure

(G : Type*) [TopologicalSpace G] [Div G]

Full source

/-- A typeclass saying that `p : G × G ↦ p.1 / p.2` is a continuous function. This property
automatically holds for topological groups. Lemmas using this class have primes.
The unprimed version is for `GroupWithZero`. -/
@[to_additive existing]
class ContinuousDiv (G : Type*) [TopologicalSpace G] [Div G] : Prop where
  continuous_div' : Continuous fun p : G × G => p.1 / p.2

Continuous division structure

Informal description

A structure asserting that the division operation `(· / ·)` on a topological space `G` equipped with a division operation is continuous. This property is automatically satisfied for topological groups, where division is defined via multiplication and inversion. The structure is used to state lemmas about continuous division, with primed versions for general division operations and unprimed versions for groups with zero.

IsTopologicalGroup.to_continuousDiv instance

{G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ContinuousDiv G

Full source

@[to_additive]
instance (priority := 100) IsTopologicalGroup.to_continuousDiv
    {G : Type u} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : ContinuousDiv G where
  continuous_div' := by
    simp only [div_eq_mul_inv]
    exact continuous_mul.comp₂ continuous_fst <| continuous_inv.comp continuous_snd

Continuity of Division in Topological Groups

Informal description

For any topological group $G$, the division operation $(a, b) \mapsto a / b$ is continuous.

Filter.Tendsto.div' theorem

 {f g : α → G} {l : Filter α} {a b : G} (hf : Tendsto f l (𝓝 a)) (hg : Tendsto g l (𝓝 b)) :
  Tendsto (fun x => f x / g x) l (𝓝 (a / b))

Full source

@[to_additive sub]
theorem Filter.Tendsto.div' {f g : α → G} {l : Filter α} {a b : G} (hf : Tendsto f l (𝓝 a))
    (hg : Tendsto g l (𝓝 b)) : Tendsto (fun x => f x / g x) l (𝓝 (a / b)) :=
  (continuous_div'.tendsto (a, b)).comp (hf.prodMk_nhds hg)

Limit of Quotient of Functions in a Topological Division Space

Informal description

Let $G$ be a topological space with a division operation, and let $f, g : \alpha \to G$ be functions. Suppose $f$ tends to $a \in G$ and $g$ tends to $b \in G$ along a filter $l$ on $\alpha$. Then the function $x \mapsto f(x) / g(x)$ tends to $a / b$ along $l$. In symbols: \[ f \underset{l}{\to} a \text{ and } g \underset{l}{\to} b \implies (x \mapsto f(x) / g(x)) \underset{l}{\to} a / b \]

ContinuousAt.div' theorem

(hf : ContinuousAt f x) (hg : ContinuousAt g x) : ContinuousAt (fun x => f x / g x) x

Full source

@[to_additive (attr := fun_prop) sub]
nonrec theorem ContinuousAt.div' (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
    ContinuousAt (fun x => f x / g x) x :=
  hf.div' hg

Continuity of Quotient at a Point in Topological Division Space

Informal description

Let $G$ be a topological space with a division operation, and let $f, g : X \to G$ be functions. If $f$ is continuous at $x \in X$ and $g$ is continuous at $x$, then the function $x \mapsto f(x) / g(x)$ is continuous at $x$. In symbols: \[ \text{ContinuousAt}(f, x) \text{ and } \text{ContinuousAt}(g, x) \implies \text{ContinuousAt}(x \mapsto f(x) / g(x), x) \]

ContinuousWithinAt.div' theorem

(hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) : ContinuousWithinAt (fun x => f x / g x) s x

Full source

@[to_additive sub]
theorem ContinuousWithinAt.div' (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :
    ContinuousWithinAt (fun x => f x / g x) s x :=
  Filter.Tendsto.div' hf hg

Continuity of Quotient within a Subset at a Point

Informal description

Let $G$ be a topological space with a division operation, and let $f, g : X \to G$ be functions. If $f$ is continuous at $x$ within $s \subseteq X$ and $g$ is continuous at $x$ within $s$, then the function $x \mapsto f(x) / g(x)$ is continuous at $x$ within $s$. In symbols: \[ f \text{ continuous at } x \text{ within } s \text{ and } g \text{ continuous at } x \text{ within } s \implies (x \mapsto f(x) / g(x)) \text{ continuous at } x \text{ within } s \]

ContinuousOn.div' theorem

(hf : ContinuousOn f s) (hg : ContinuousOn g s) : ContinuousOn (fun x => f x / g x) s

Full source

@[to_additive (attr := fun_prop) sub]
theorem ContinuousOn.div' (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x => f x / g x) s := fun x hx => (hf x hx).div' (hg x hx)

Continuity of Pointwise Division on a Subset

Informal description

Let $G$ be a topological space with a division operation, and let $f, g : X \to G$ be functions. If $f$ is continuous on a subset $s \subseteq X$ and $g$ is continuous on $s$, then the function $x \mapsto f(x) / g(x)$ is continuous on $s$. In symbols: \[ f \text{ continuous on } s \text{ and } g \text{ continuous on } s \implies (x \mapsto f(x) / g(x)) \text{ continuous on } s \]

Continuous.div' theorem

(hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x / g x

Full source

@[to_additive (attr := continuity, fun_prop) sub]
theorem Continuous.div' (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f x / g x :=
  continuous_div'.comp₂ hf hg

Continuity of Pointwise Division of Continuous Functions

Informal description

Let $X$ and $G$ be topological spaces, where $G$ is equipped with a continuous division operation. If $f \colon X \to G$ and $g \colon X \to G$ are continuous functions, then the function $x \mapsto f(x) / g(x)$ is also continuous.