Mathlib.Topology.Algebra.Group.Basic

Homeomorph.mulLeft definition

(a : G) : G ≃ₜ G

Full source

/-- Multiplication from the left in a topological group as a homeomorphism. -/
@[to_additive "Addition from the left in a topological additive group as a homeomorphism."]
protected def Homeomorph.mulLeft (a : G) : G ≃ₜ G :=
  { Equiv.mulLeft a with
    continuous_toFun := continuous_const.mul continuous_id
    continuous_invFun := continuous_const.mul continuous_id }

Homeomorphism of left multiplication in a topological group

Informal description

For an element $a$ in a topological group $G$, the left multiplication map $x \mapsto a \cdot x$ is a homeomorphism of $G$. This means it is a continuous bijection with a continuous inverse, where the inverse is given by left multiplication with $a^{-1}$.

Homeomorph.coe_mulLeft theorem

(a : G) : ⇑(Homeomorph.mulLeft a) = (a * ·)

Full source

@[to_additive (attr := simp)]
theorem Homeomorph.coe_mulLeft (a : G) : ⇑(Homeomorph.mulLeft a) = (a * ·) :=
  rfl

Underlying Function of Left Multiplication Homeomorphism

Informal description

For any element $a$ in a topological group $G$, the underlying function of the homeomorphism $\text{mulLeft}(a)$ is equal to the left multiplication map $x \mapsto a \cdot x$.

Homeomorph.mulLeft_symm theorem

(a : G) : (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹

Full source

@[to_additive]
theorem Homeomorph.mulLeft_symm (a : G) : (Homeomorph.mulLeft a).symm = Homeomorph.mulLeft a⁻¹ := by
  ext
  rfl

Inverse of Left Multiplication Homeomorphism in a Topological Group

Informal description

For any element $a$ in a topological group $G$, the inverse of the left multiplication homeomorphism $x \mapsto a \cdot x$ is equal to the left multiplication homeomorphism by the inverse element $a^{-1}$, i.e., $(\text{mulLeft}(a))^{-1} = \text{mulLeft}(a^{-1})$.

isOpenMap_mul_left theorem

(a : G) : IsOpenMap (a * ·)

Full source

@[to_additive]
lemma isOpenMap_mul_left (a : G) : IsOpenMap (a * ·) := (Homeomorph.mulLeft a).isOpenMap

Left multiplication is an open map in a topological group

Informal description

For any element $a$ in a topological group $G$, the left multiplication map $x \mapsto a \cdot x$ is an open map. That is, for every open subset $U \subseteq G$, the image $a \cdot U$ is open in $G$.

IsOpen.leftCoset theorem

{U : Set G} (h : IsOpen U) (x : G) : IsOpen (x • U)

Full source

@[to_additive IsOpen.left_addCoset]
theorem IsOpen.leftCoset {U : Set G} (h : IsOpen U) (x : G) : IsOpen (x • U) :=
  isOpenMap_mul_left x _ h

Openness of Left Cosets in a Topological Group

Informal description

For any open subset $U$ of a topological group $G$ and any element $x \in G$, the left coset $x \cdot U$ is open in $G$.

isClosedMap_mul_left theorem

(a : G) : IsClosedMap (a * ·)

Full source

@[to_additive]
lemma isClosedMap_mul_left (a : G) : IsClosedMap (a * ·) := (Homeomorph.mulLeft a).isClosedMap

Left multiplication is a closed map in a topological group

Informal description

For any element $a$ in a topological group $G$, the left multiplication map $x \mapsto a \cdot x$ is a closed map. That is, for every closed subset $U \subseteq G$, the image $a \cdot U$ is closed in $G$.

IsClosed.leftCoset theorem

{U : Set G} (h : IsClosed U) (x : G) : IsClosed (x • U)

Full source

@[to_additive IsClosed.left_addCoset]
theorem IsClosed.leftCoset {U : Set G} (h : IsClosed U) (x : G) : IsClosed (x • U) :=
  isClosedMap_mul_left x _ h

Left Coset of a Closed Set is Closed in a Topological Group

Informal description

For any closed subset $U$ of a topological group $G$ and any element $x \in G$, the left coset $x \cdot U$ is closed in $G$.

Homeomorph.mulRight definition

(a : G) : G ≃ₜ G

Full source

/-- Multiplication from the right in a topological group as a homeomorphism. -/
@[to_additive "Addition from the right in a topological additive group as a homeomorphism."]
protected def Homeomorph.mulRight (a : G) : G ≃ₜ G :=
  { Equiv.mulRight a with
    continuous_toFun := continuous_id.mul continuous_const
    continuous_invFun := continuous_id.mul continuous_const }

Homeomorphism of right multiplication in a topological group

Informal description

For any element $a$ in a topological group $G$, the right multiplication map $x \mapsto x \cdot a$ is a homeomorphism of $G$. This means it is a continuous bijection with a continuous inverse, where the inverse is given by right multiplication by $a^{-1}$.

Homeomorph.coe_mulRight theorem

(a : G) : ⇑(Homeomorph.mulRight a) = (· * a)

Full source

@[to_additive (attr := simp)]
lemma Homeomorph.coe_mulRight (a : G) : ⇑(Homeomorph.mulRight a) = (· * a) := rfl

Underlying Function of Right Multiplication Homeomorphism

Informal description

For any element $a$ in a topological group $G$, the underlying function of the homeomorphism $\text{mulRight}(a)$ is equal to the right multiplication map $x \mapsto x \cdot a$.

Homeomorph.mulRight_symm theorem

(a : G) : (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹

Full source

@[to_additive]
theorem Homeomorph.mulRight_symm (a : G) :
    (Homeomorph.mulRight a).symm = Homeomorph.mulRight a⁻¹ := by
  ext
  rfl

Inverse of Right Multiplication Homeomorphism in a Topological Group

Informal description

For any element $a$ in a topological group $G$, the inverse of the right multiplication homeomorphism $x \mapsto x \cdot a$ is equal to the right multiplication homeomorphism by the inverse element $a^{-1}$, i.e., $(x \mapsto x \cdot a)^{-1} = (x \mapsto x \cdot a^{-1})$.

isOpenMap_mul_right theorem

(a : G) : IsOpenMap (· * a)

Full source

@[to_additive]
theorem isOpenMap_mul_right (a : G) : IsOpenMap (· * a) :=
  (Homeomorph.mulRight a).isOpenMap

Right multiplication is an open map in a topological group

Informal description

For any element $a$ in a topological group $G$, the right multiplication map $x \mapsto x \cdot a$ is an open map. That is, for every open subset $U \subseteq G$, the image $U \cdot a$ is open in $G$.

IsOpen.rightCoset theorem

{U : Set G} (h : IsOpen U) (x : G) : IsOpen (op x • U)

Full source

@[to_additive IsOpen.right_addCoset]
theorem IsOpen.rightCoset {U : Set G} (h : IsOpen U) (x : G) : IsOpen (op x • U) :=
  isOpenMap_mul_right x _ h

Openness of Right Cosets in Topological Groups

Informal description

For any open subset $U$ of a topological group $G$ and any element $x \in G$, the right coset $U \cdot x$ is open in $G$.

isClosedMap_mul_right theorem

(a : G) : IsClosedMap (· * a)

Full source

@[to_additive]
theorem isClosedMap_mul_right (a : G) : IsClosedMap (· * a) :=
  (Homeomorph.mulRight a).isClosedMap

Right multiplication is a closed map in a topological group

Informal description

For any element $a$ in a topological group $G$, the right multiplication map $x \mapsto x \cdot a$ is a closed map. That is, for every closed subset $U \subseteq G$, the image $U \cdot a$ is closed in $G$.

IsClosed.rightCoset theorem

{U : Set G} (h : IsClosed U) (x : G) : IsClosed (op x • U)

Full source

@[to_additive IsClosed.right_addCoset]
theorem IsClosed.rightCoset {U : Set G} (h : IsClosed U) (x : G) : IsClosed (op x • U) :=
  isClosedMap_mul_right x _ h

Closedness of Right Cosets in Topological Groups

Informal description

For any closed subset $U$ of a topological group $G$ and any element $x \in G$, the right coset $U \cdot x$ is closed in $G$.

discreteTopology_of_isOpen_singleton_one theorem

(h : IsOpen ({ 1 } : Set G)) : DiscreteTopology G

Full source

@[to_additive]
theorem discreteTopology_of_isOpen_singleton_one (h : IsOpen ({1} : Set G)) :
    DiscreteTopology G := by
  rw [← singletons_open_iff_discrete]
  intro g
  suffices {g} = (g⁻¹ * ·) ⁻¹' {1} by
    rw [this]
    exact (continuous_mul_left g⁻¹).isOpen_preimage _ h
  simp only [mul_one, Set.preimage_mul_left_singleton, eq_self_iff_true, inv_inv,
    Set.singleton_eq_singleton_iff]

Discrete Topology Criterion via Open Identity Singleton in Topological Groups

Informal description

If the singleton set containing the identity element $\{1\}$ is open in a topological group $G$, then $G$ has the discrete topology.

discreteTopology_iff_isOpen_singleton_one theorem

: DiscreteTopology G ↔ IsOpen ({ 1 } : Set G)

Full source

@[to_additive]
theorem discreteTopology_iff_isOpen_singleton_one : DiscreteTopologyDiscreteTopology G ↔ IsOpen ({1} : Set G) :=
  ⟨fun h => forall_open_iff_discrete.mpr h {1}, discreteTopology_of_isOpen_singleton_one⟩

Discrete Topology Characterization via Open Identity Singleton in Topological Groups

Informal description

A topological group $G$ has the discrete topology if and only if the singleton set $\{1\}$ containing the identity element is open in $G$.

ContinuousInv.induced theorem

 {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Group α] [DivisionMonoid β] [MonoidHomClass F α β]
  [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) : @ContinuousInv α (tβ.induced f) _

Full source

@[to_additive]
theorem ContinuousInv.induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Group α]
    [DivisionMonoid β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) :
    @ContinuousInv α (tβ.induced f) _ := by
  let _tα := tβ.induced f
  refine ⟨continuous_induced_rng.2 ?_⟩
  simp only [Function.comp_def, map_inv]
  fun_prop

Continuity of Inversion under Induced Topology via Monoid Homomorphism

Informal description

Let $\alpha$ and $\beta$ be types, with $\alpha$ a group and $\beta$ a division monoid. Let $F$ be a type of functions from $\alpha$ to $\beta$ that are monoid homomorphisms. Suppose $\beta$ is equipped with a topology $t_\beta$ under which inversion is continuous. Then for any $f \in F$, the induced topology on $\alpha$ makes inversion continuous.

Specializes.inv theorem

{x y : G} (h : x ⤳ y) : (x⁻¹) ⤳ (y⁻¹)

Full source

@[to_additive]
protected theorem Specializes.inv {x y : G} (h : x ⤳ y) : (x⁻¹) ⤳ (y⁻¹) :=
  h.map continuous_inv

Specialization is Preserved Under Inversion in Topological Groups

Informal description

Let $G$ be a topological group with continuous inversion. For any $x, y \in G$, if $x$ specializes to $y$ (i.e., $x \rightsquigarrow y$), then $x^{-1}$ specializes to $y^{-1}$ (i.e., $x^{-1} \rightsquigarrow y^{-1}$).

Inseparable.inv theorem

{x y : G} (h : Inseparable x y) : Inseparable (x⁻¹) (y⁻¹)

Full source

@[to_additive]
protected theorem Inseparable.inv {x y : G} (h : Inseparable x y) : Inseparable (x⁻¹) (y⁻¹) :=
  h.map continuous_inv

Inseparability is Preserved Under Inversion in Topological Groups

Informal description

Let $G$ be a topological group with continuous inversion. For any $x, y \in G$, if $x$ and $y$ are inseparable (i.e., they have identical neighborhood filters), then their inverses $x^{-1}$ and $y^{-1}$ are also inseparable.

Specializes.zpow theorem

 {G : Type*} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G} (h : x ⤳ y) :
  ∀ m : ℤ, (x ^ m) ⤳ (y ^ m)

Full source

@[to_additive]
protected theorem Specializes.zpow {G : Type*} [DivInvMonoid G] [TopologicalSpace G]
    [ContinuousMul G] [ContinuousInv G] {x y : G} (h : x ⤳ y) : ∀ m : ℤ, (x ^ m) ⤳ (y ^ m)
  | .ofNat n => by simpa using h.pow n
  | .negSucc n => by simpa using (h.pow (n + 1)).inv

Specialization is preserved under integer exponentiation in topological groups

Informal description

Let $G$ be a topological group with continuous multiplication and inversion operations. For any elements $x, y \in G$ such that $x$ specializes to $y$ (i.e., $x \rightsquigarrow y$), and for any integer $m$, the $m$-th power $x^m$ specializes to $y^m$ (i.e., $x^m \rightsquigarrow y^m$).

Inseparable.zpow theorem

 {G : Type*} [DivInvMonoid G] [TopologicalSpace G] [ContinuousMul G] [ContinuousInv G] {x y : G} (h : Inseparable x y)
  (m : ℤ) : Inseparable (x ^ m) (y ^ m)

Full source

@[to_additive]
protected theorem Inseparable.zpow {G : Type*} [DivInvMonoid G] [TopologicalSpace G]
    [ContinuousMul G] [ContinuousInv G] {x y : G} (h : Inseparable x y) (m : ℤ) :
    Inseparable (x ^ m) (y ^ m) :=
  (h.specializes.zpow m).antisymm (h.specializes'.zpow m)

Inseparability is preserved under integer exponentiation in topological groups

Informal description

Let $G$ be a topological group with continuous multiplication and inversion operations. For any two inseparable points $x, y \in G$ (i.e., $x$ and $y$ have identical neighborhood filters) and any integer $m$, the $m$-th powers $x^m$ and $y^m$ are also inseparable.

instContinuousInvULift instance

: ContinuousInv (ULift G)

Full source

@[to_additive]
instance : ContinuousInv (ULift G) :=
  ⟨continuous_uliftUp.comp (continuous_inv.comp continuous_uliftDown)⟩

Continuous Inversion on Lifted Topological Groups

Informal description

For any topological group $G$, the lifted type $\mathrm{ULift}\, G$ equipped with the inherited topology has a continuous inversion operation.

continuousOn_inv theorem

{s : Set G} : ContinuousOn Inv.inv s

Full source

@[to_additive]
theorem continuousOn_inv {s : Set G} : ContinuousOn Inv.inv s :=
  continuous_inv.continuousOn

Continuity of inversion on subsets of a topological group

Informal description

For any subset $s$ of a topological group $G$ with continuous inversion, the inversion operation $x \mapsto x^{-1}$ is continuous on $s$.

continuousWithinAt_inv theorem

{s : Set G} {x : G} : ContinuousWithinAt Inv.inv s x

Full source

@[to_additive]
theorem continuousWithinAt_inv {s : Set G} {x : G} : ContinuousWithinAt Inv.inv s x :=
  continuous_inv.continuousWithinAt

Continuity of Inversion Within a Subset at a Point in a Topological Group

Informal description

Let $G$ be a topological group with continuous inversion, $s$ a subset of $G$, and $x$ an element of $G$. Then the inversion operation $x \mapsto x^{-1}$ is continuous at $x$ within the subset $s$.

continuousAt_inv theorem

{x : G} : ContinuousAt Inv.inv x

Full source

@[to_additive]
theorem continuousAt_inv {x : G} : ContinuousAt Inv.inv x :=
  continuous_inv.continuousAt

Continuity of Inversion at a Point in a Topological Group

Informal description

For any element $x$ in a topological group $G$ with continuous inversion, the inversion operation $x \mapsto x^{-1}$ is continuous at $x$.

tendsto_inv theorem

(a : G) : Tendsto Inv.inv (𝓝 a) (𝓝 a⁻¹)

Full source

@[to_additive]
theorem tendsto_inv (a : G) : Tendsto Inv.inv (𝓝 a) (𝓝 a⁻¹) :=
  continuousAt_inv

Inversion is Continuous at a Point in a Topological Group

Informal description

For any element $a$ in a topological group $G$ with continuous inversion, the inversion operation $x \mapsto x^{-1}$ maps the neighborhood filter of $a$ to the neighborhood filter of $a^{-1}$. In other words, the inversion operation tends to $a^{-1}$ as $x$ tends to $a$.

OrderDual.instContinuousInv instance

: ContinuousInv Gᵒᵈ

Full source

@[to_additive]
instance OrderDual.instContinuousInv : ContinuousInv Gᵒᵈ := ‹ContinuousInv G›

Continuous Inversion on Order Dual of a Topological Group

Informal description

For any topological group $G$ with continuous inversion, the order dual $G^{\text{op}}$ also has continuous inversion.

Prod.continuousInv instance

[TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousInv (G × H)

Full source

@[to_additive]
instance Prod.continuousInv [TopologicalSpace H] [Inv H] [ContinuousInv H] :
    ContinuousInv (G × H) :=
  ⟨continuous_inv.fst'.prodMk continuous_inv.snd'⟩

Continuous Inversion in Product Spaces

Informal description

For any topological spaces $G$ and $H$ equipped with inversion operations and continuous inversion, the product space $G \times H$ also has continuous inversion. Specifically, the inversion operation $(x, y) \mapsto (x^{-1}, y^{-1})$ is continuous.

Pi.continuousInv instance

 {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Inv (C i)] [∀ i, ContinuousInv (C i)] : ContinuousInv (∀ i, C i)

Full source

@[to_additive]
instance Pi.continuousInv {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Inv (C i)]
    [∀ i, ContinuousInv (C i)] : ContinuousInv (∀ i, C i) where
  continuous_inv := continuous_pi fun i => (continuous_apply i).inv

Continuous Inversion in Product Spaces

Informal description

For any family of topological spaces $\{C_i\}_{i \in \iota}$ where each $C_i$ is equipped with an inversion operation and has continuous inversion, the product space $\prod_{i \in \iota} C_i$ also has continuous inversion.

Pi.has_continuous_inv' instance

: ContinuousInv (ι → G)

Full source

/-- A version of `Pi.continuousInv` for non-dependent functions. It is needed because sometimes
Lean fails to use `Pi.continuousInv` for non-dependent functions. -/
@[to_additive
  "A version of `Pi.continuousNeg` for non-dependent functions. It is needed
  because sometimes Lean fails to use `Pi.continuousNeg` for non-dependent functions."]
instance Pi.has_continuous_inv' : ContinuousInv (ι → G) :=
  Pi.continuousInv

Continuous Inversion in Product Spaces of a Fixed Type

Informal description

For any family of topological spaces indexed by $\iota$ where each space is equipped with an inversion operation and has continuous inversion, the product space $\prod_{i \in \iota} G$ also has continuous inversion.

continuousInv_of_discreteTopology instance

[TopologicalSpace H] [Inv H] [DiscreteTopology H] : ContinuousInv H

Full source

@[to_additive]
instance (priority := 100) continuousInv_of_discreteTopology [TopologicalSpace H] [Inv H]
    [DiscreteTopology H] : ContinuousInv H :=
  ⟨continuous_of_discreteTopology⟩

Continuous Inversion in Discrete Topological Spaces

Informal description

For any topological space $H$ equipped with an inversion operation and the discrete topology, the inversion operation is continuous.

isClosed_setOf_map_inv theorem

[Inv G₁] [Inv G₂] [ContinuousInv G₂] : IsClosed {f : G₁ → G₂ | ∀ x, f x⁻¹ = (f x)⁻¹}

Full source

@[to_additive]
theorem isClosed_setOf_map_inv [Inv G₁] [Inv G₂] [ContinuousInv G₂] :
    IsClosed { f : G₁ → G₂ | ∀ x, f x⁻¹ = (f x)⁻¹ } := by
  simp only [setOf_forall]
  exact isClosed_iInter fun i => isClosed_eq (continuous_apply _) (continuous_apply _).inv

Closedness of the Set of Inversion-Preserving Functions

Informal description

Let $G_1$ and $G_2$ be types equipped with inversion operations, and suppose $G_2$ has a topology with continuous inversion. Then the set of all functions $f \colon G_1 \to G_2$ satisfying $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G_1$ is closed in the function space $G_1 \to G_2$ equipped with the product topology.

instContinuousNegAdditiveOfContinuousInv instance

[TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousNeg (Additive H)

Full source

instance [TopologicalSpace H] [Inv H] [ContinuousInv H] : ContinuousNeg (Additive H) where
  continuous_neg := @continuous_inv H _ _ _

Continuous Negation on Additive Types from Continuous Inversion

Informal description

For any topological space $H$ with a continuous inversion operation, the additive version of $H$ has a continuous negation operation.

instContinuousInvMultiplicativeOfContinuousNeg instance

[TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousInv (Multiplicative H)

Full source

instance [TopologicalSpace H] [Neg H] [ContinuousNeg H] : ContinuousInv (Multiplicative H) where
  continuous_inv := @continuous_neg H _ _ _

Continuous Inversion on Multiplicative Types from Continuous Negation

Informal description

For any topological space $H$ with a negation operation that is continuous, the multiplicative version of $H$ has a continuous inversion operation.

IsCompact.inv theorem

(hs : IsCompact s) : IsCompact s⁻¹

Full source

@[to_additive]
theorem IsCompact.inv (hs : IsCompact s) : IsCompact s⁻¹ := by
  rw [← image_inv_eq_inv]
  exact hs.image continuous_inv

Compactness of Inverses in Topological Groups

Informal description

Let $G$ be a topological space with a continuous inversion operation and let $s \subseteq G$ be a compact subset. Then the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is also compact.

Homeomorph.inv definition

(G : Type*) [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : G ≃ₜ G

Full source

/-- Inversion in a topological group as a homeomorphism. -/
@[to_additive "Negation in a topological group as a homeomorphism."]
protected def Homeomorph.inv (G : Type*) [TopologicalSpace G] [InvolutiveInv G]
    [ContinuousInv G] : G ≃ₜ G :=
  { Equiv.inv G with
    continuous_toFun := continuous_inv
    continuous_invFun := continuous_inv }

Inversion homeomorphism of a topological group

Informal description

The homeomorphism on a topological group $G$ induced by the inversion operation $x \mapsto x^{-1}$. This map is continuous in both directions, as inversion is continuous and involutive (i.e., $(x^{-1})^{-1} = x$ for all $x \in G$).

Homeomorph.coe_inv theorem

{G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] : ⇑(Homeomorph.inv G) = Inv.inv

Full source

@[to_additive (attr := simp)]
lemma Homeomorph.coe_inv {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] :
    ⇑(Homeomorph.inv G) = Inv.inv := rfl

Inversion Homeomorphism Equals Inversion Operation

Informal description

For a topological space $G$ with a continuous and involutive inversion operation, the underlying function of the inversion homeomorphism $\text{Homeomorph.inv}(G)$ is equal to the inversion operation $\text{Inv.inv}$ on $G$.

nhds_inv theorem

(a : G) : 𝓝 a⁻¹ = (𝓝 a)⁻¹

Full source

@[to_additive]
theorem nhds_inv (a : G) : 𝓝 a⁻¹ = (𝓝 a)⁻¹ :=
  ((Homeomorph.inv G).map_nhds_eq a).symm

Neighborhood Filter of Inverse Equals Preimage of Neighborhood Filter

Informal description

For any element $a$ in a topological group $G$, the neighborhood filter of $a^{-1}$ is equal to the preimage of the neighborhood filter of $a$ under the inversion operation. That is, $\mathcal{N}(a^{-1}) = (\mathcal{N}(a))^{-1}$.

isOpenMap_inv theorem

: IsOpenMap (Inv.inv : G → G)

Full source

@[to_additive]
theorem isOpenMap_inv : IsOpenMap (Inv.inv : G → G) :=
  (Homeomorph.inv _).isOpenMap

Inversion is an open map in topological groups

Informal description

Let $G$ be a topological group with continuous inversion. Then the inversion map $x \mapsto x^{-1}$ is an open map, i.e., it maps open subsets of $G$ to open subsets of $G$.

isClosedMap_inv theorem

: IsClosedMap (Inv.inv : G → G)

Full source

@[to_additive]
theorem isClosedMap_inv : IsClosedMap (Inv.inv : G → G) :=
  (Homeomorph.inv _).isClosedMap

Inversion is a closed map in topological groups

Informal description

Let $G$ be a topological group with continuous inversion. Then the inversion map $x \mapsto x^{-1}$ is a closed map, i.e., it maps closed subsets of $G$ to closed subsets of $G$.

IsOpen.inv theorem

(hs : IsOpen s) : IsOpen s⁻¹

Full source

@[to_additive]
theorem IsOpen.inv (hs : IsOpen s) : IsOpen s⁻¹ :=
  hs.preimage continuous_inv

Inversion Preserves Openness in Topological Groups

Informal description

For any open subset $s$ of a topological group $G$, the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is also open.

IsClosed.inv theorem

(hs : IsClosed s) : IsClosed s⁻¹

Full source

@[to_additive]
theorem IsClosed.inv (hs : IsClosed s) : IsClosed s⁻¹ :=
  hs.preimage continuous_inv

Inversion Preserves Closedness in Topological Groups

Informal description

For any closed subset $s$ of a topological group $G$, the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is also closed.

inv_closure theorem

: ∀ s : Set G, (closure s)⁻¹ = closure s⁻¹

Full source

@[to_additive]
theorem inv_closure : ∀ s : Set G, (closure s)⁻¹ = closure s⁻¹ :=
  (Homeomorph.inv G).preimage_closure

Closure of Inverses Equals Inverses of Closure in Topological Groups

Informal description

For any subset $s$ of a topological group $G$ with continuous inversion, the closure of the set of inverses $s^{-1} = \{x^{-1} \mid x \in s\}$ is equal to the set of inverses of the closure of $s$. That is, \[ \overline{s^{-1}} = (\overline{s})^{-1}. \]

continuous_inv_iff theorem

: Continuous f⁻¹ ↔ Continuous f

Full source

@[to_additive (attr := simp)]
lemma continuous_inv_iff : ContinuousContinuous f⁻¹ ↔ Continuous f := (Homeomorph.inv G).comp_continuous_iff

Continuity of Inversion vs. Original Function in Topological Groups

Informal description

For a function $f \colon X \to G$ from a topological space $X$ to a topological group $G$ with continuous inversion, the function $f^{-1} \colon X \to G$ defined by $f^{-1}(x) = (f(x))^{-1}$ is continuous if and only if $f$ is continuous.

continuousAt_inv_iff theorem

: ContinuousAt f⁻¹ x ↔ ContinuousAt f x

Full source

@[to_additive (attr := simp)]
lemma continuousAt_inv_iff : ContinuousAtContinuousAt f⁻¹ x ↔ ContinuousAt f x :=
  (Homeomorph.inv G).comp_continuousAt_iff _ _

Continuity of Inversion at a Point: $f^{-1}$ continuous at $x$ iff $f$ continuous at $x$

Informal description

For a function $f \colon G \to G$ on a topological group $G$ with continuous inversion, the function $f^{-1}$ is continuous at a point $x \in G$ if and only if $f$ is continuous at $x$.

continuousOn_inv_iff theorem

: ContinuousOn f⁻¹ s ↔ ContinuousOn f s

Full source

@[to_additive (attr := simp)]
lemma continuousOn_inv_iff : ContinuousOnContinuousOn f⁻¹ s ↔ ContinuousOn f s :=
  (Homeomorph.inv G).comp_continuousOn_iff _ _

Continuity of Inversion on Subsets

Informal description

For a function $f$ defined on a subset $s$ of a topological space, the inversion $f^{-1}$ is continuous on $s$ if and only if $f$ is continuous on $s$.

continuousInv_sInf theorem

{ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, @ContinuousInv G t _) : @ContinuousInv G (sInf ts) _

Full source

@[to_additive]
theorem continuousInv_sInf {ts : Set (TopologicalSpace G)}
    (h : ∀ t ∈ ts, @ContinuousInv G t _) : @ContinuousInv G (sInf ts) _ :=
  letI := sInf ts
  { continuous_inv :=
      continuous_sInf_rng.2 fun t ht =>
        continuous_sInf_dom ht (@ContinuousInv.continuous_inv G t _ (h t ht)) }

Continuity of inversion preserved under infimum of topologies

Informal description

Let $G$ be a group with inversion operation and let $\{t_i\}_{i \in I}$ be a collection of topologies on $G$. If for each topology $t_i$ in the collection, the inversion operation is continuous with respect to $t_i$, then inversion is also continuous with respect to the infimum topology $\bigsqcap \{t_i\}_{i \in I}$.

continuousInv_iInf theorem

{ts' : ι' → TopologicalSpace G} (h' : ∀ i, @ContinuousInv G (ts' i) _) : @ContinuousInv G (⨅ i, ts' i) _

Full source

@[to_additive]
theorem continuousInv_iInf {ts' : ι' → TopologicalSpace G}
    (h' : ∀ i, @ContinuousInv G (ts' i) _) : @ContinuousInv G (⨅ i, ts' i) _ := by
  rw [← sInf_range]
  exact continuousInv_sInf (Set.forall_mem_range.mpr h')

Continuity of Inversion Preserved under Indexed Infimum of Topologies

Informal description

Let $G$ be a group with an inversion operation, and let $\{t_i\}_{i \in I}$ be a family of topologies on $G$. If for each index $i$, the inversion operation is continuous with respect to the topology $t_i$, then inversion is also continuous with respect to the infimum topology $\bigsqcap_{i \in I} t_i$.

continuousInv_inf theorem

 {t₁ t₂ : TopologicalSpace G} (h₁ : @ContinuousInv G t₁ _) (h₂ : @ContinuousInv G t₂ _) : @ContinuousInv G (t₁ ⊓ t₂) _

Full source

@[to_additive]
theorem continuousInv_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @ContinuousInv G t₁ _)
    (h₂ : @ContinuousInv G t₂ _) : @ContinuousInv G (t₁ ⊓ t₂) _ := by
  rw [inf_eq_iInf]
  refine continuousInv_iInf fun b => ?_
  cases b <;> assumption

Continuity of Inversion Preserved under Infimum of Topologies

Informal description

Let $G$ be a group with an inversion operation, and let $t_1$ and $t_2$ be two topologies on $G$. If the inversion operation is continuous with respect to both $t_1$ and $t_2$, then it is also continuous with respect to the infimum topology $t_1 \sqcap t_2$.

Topology.IsInducing.continuousInv theorem

 {G H : Type*} [Inv G] [Inv H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv H] {f : G → H}
  (hf : IsInducing f) (hf_inv : ∀ x, f x⁻¹ = (f x)⁻¹) : ContinuousInv G

Full source

@[to_additive]
theorem Topology.IsInducing.continuousInv {G H : Type*} [Inv G] [Inv H] [TopologicalSpace G]
    [TopologicalSpace H] [ContinuousInv H] {f : G → H} (hf : IsInducing f)
    (hf_inv : ∀ x, f x⁻¹ = (f x)⁻¹) : ContinuousInv G :=
  ⟨hf.continuous_iff.2 <| by simpa only [Function.comp_def, hf_inv] using hf.continuous.inv⟩

Inducing Maps Preserve Continuous Inversion

Informal description

Let $G$ and $H$ be types equipped with inversion operations and topological structures, and suppose $H$ has continuous inversion. Given an inducing map $f \colon G \to H$ such that $f(x^{-1}) = (f(x))^{-1}$ for all $x \in G$, then $G$ also has continuous inversion.

ConjAct.units_continuousConstSMul instance

{M} [Monoid M] [TopologicalSpace M] [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M

Full source

instance ConjAct.units_continuousConstSMul {M} [Monoid M] [TopologicalSpace M]
    [ContinuousMul M] : ContinuousConstSMul (ConjAct Mˣ) M :=
  ⟨fun _ => (continuous_const.mul continuous_id).mul continuous_const⟩

Continuity of the Conjugation Action by Units in a Topological Monoid

Informal description

For any monoid $M$ with a topological space structure and continuous multiplication, the conjugation action of the group of units $M^\times$ on $M$ is continuous in the second variable. Specifically, for each fixed unit $g \in M^\times$, the map $h \mapsto g h g^{-1}$ is continuous.

IsTopologicalGroup.continuous_conj_prod theorem

[ContinuousInv G] : Continuous fun g : G × G => g.fst * g.snd * g.fst⁻¹

Full source

/-- Conjugation is jointly continuous on `G × G` when both `mul` and `inv` are continuous. -/
@[to_additive continuous_addConj_prod
  "Conjugation is jointly continuous on `G × G` when both `add` and `neg` are continuous."]
theorem IsTopologicalGroup.continuous_conj_prod [ContinuousInv G] :
    Continuous fun g : G × G => g.fst * g.snd * g.fst⁻¹ :=
  continuous_mul.mul (continuous_inv.comp continuous_fst)

Joint continuity of conjugation in topological groups

Informal description

Let $G$ be a topological group with continuous inversion. Then the conjugation map $(g, h) \mapsto g * h * g^{-1}$ is jointly continuous on $G \times G$.

IsTopologicalGroup.continuous_conj theorem

(g : G) : Continuous fun h : G => g * h * g⁻¹

Full source

/-- Conjugation by a fixed element is continuous when `mul` is continuous. -/
@[to_additive (attr := continuity)
  "Conjugation by a fixed element is continuous when `add` is continuous."]
theorem IsTopologicalGroup.continuous_conj (g : G) : Continuous fun h : G => g * h * g⁻¹ :=
  (continuous_mul_right g⁻¹).comp (continuous_mul_left g)

Continuity of Conjugation in Topological Groups

Informal description

For any element $g$ in a topological group $G$, the conjugation map $h \mapsto g * h * g^{-1}$ is continuous.

IsTopologicalGroup.continuous_conj' theorem

[ContinuousInv G] (h : G) : Continuous fun g : G => g * h * g⁻¹

Full source

/-- Conjugation acting on fixed element of the group is continuous when both `mul` and
`inv` are continuous. -/
@[to_additive (attr := continuity)
  "Conjugation acting on fixed element of the additive group is continuous when both
    `add` and `neg` are continuous."]
theorem IsTopologicalGroup.continuous_conj' [ContinuousInv G] (h : G) :
    Continuous fun g : G => g * h * g⁻¹ :=
  (continuous_mul_right h).mul continuous_inv

Continuity of Conjugation by Fixed Element in Topological Groups

Informal description

Let $G$ be a topological group with continuous inversion. For any fixed element $h \in G$, the conjugation map $g \mapsto g * h * g^{-1}$ is continuous.

instIsTopologicalGroupULift instance

: IsTopologicalGroup (ULift G)

Full source

instance : IsTopologicalGroup (ULift G) where

Topological Group Structure on Lifted Types

Informal description

For any topological group $G$, the lifted type $\mathrm{ULift}\, G$ is also a topological group, with the group operations and topology inherited from $G$.

continuous_zpow theorem

: ∀ z : ℤ, Continuous fun a : G => a ^ z

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem continuous_zpow : ∀ z : ℤ, Continuous fun a : G => a ^ z
  | Int.ofNat n => by simpa using continuous_pow n
  | Int.negSucc n => by simpa using (continuous_pow (n + 1)).inv

Continuity of Integer Powers in Topological Groups

Informal description

For every integer $z$, the function $a \mapsto a^z$ is continuous on a topological group $G$.

AddGroup.continuousConstSMul_int instance

{A} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousConstSMul ℤ A

Full source

instance AddGroup.continuousConstSMul_int {A} [AddGroup A] [TopologicalSpace A]
    [IsTopologicalAddGroup A] : ContinuousConstSMul ℤ A :=
  ⟨continuous_zsmul⟩

Continuous Integer Scalar Multiplication in Additive Topological Groups

Informal description

For any additive topological group $A$ with a topology, the scalar multiplication by integers $\mathbb{Z} \times A \to A$ is continuous in the second variable for each fixed integer.

AddGroup.continuousSMul_int instance

{A} [AddGroup A] [TopologicalSpace A] [IsTopologicalAddGroup A] : ContinuousSMul ℤ A

Full source

instance AddGroup.continuousSMul_int {A} [AddGroup A] [TopologicalSpace A]
    [IsTopologicalAddGroup A] : ContinuousSMul ℤ A :=
  ⟨continuous_prod_of_discrete_left.mpr continuous_zsmul⟩

Joint Continuity of Integer Scalar Multiplication in Additive Topological Groups

Informal description

For any additive topological group $A$ with a topology, the scalar multiplication operation $\mathbb{Z} \times A \to A$ is jointly continuous.

Continuous.zpow theorem

{f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun b => f b ^ z

Full source

@[to_additive (attr := continuity, fun_prop)]
theorem Continuous.zpow {f : α → G} (h : Continuous f) (z : ℤ) : Continuous fun b => f b ^ z :=
  (continuous_zpow z).comp h

Continuity of Integer Powers of Continuous Functions in Topological Groups

Informal description

Let $G$ be a topological group and $\alpha$ a topological space. For any continuous function $f \colon \alpha \to G$ and any integer $z$, the function $b \mapsto (f(b))^z$ is continuous.

continuousOn_zpow theorem

{s : Set G} (z : ℤ) : ContinuousOn (fun x => x ^ z) s

Full source

@[to_additive]
theorem continuousOn_zpow {s : Set G} (z : ℤ) : ContinuousOn (fun x => x ^ z) s :=
  (continuous_zpow z).continuousOn

Continuity of Integer Power Function on Subsets of a Topological Group

Informal description

For any integer $z$ and any subset $s$ of a topological group $G$, the function $x \mapsto x^z$ is continuous on $s$.

continuousAt_zpow theorem

(x : G) (z : ℤ) : ContinuousAt (fun x => x ^ z) x

Full source

@[to_additive]
theorem continuousAt_zpow (x : G) (z : ℤ) : ContinuousAt (fun x => x ^ z) x :=
  (continuous_zpow z).continuousAt

Continuity of Integer Power Function at a Point in Topological Groups

Informal description

For any element $x$ in a topological group $G$ and any integer $z$, the function $x \mapsto x^z$ is continuous at $x$.

Filter.Tendsto.zpow theorem

 {α} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (𝓝 x)) (z : ℤ) : Tendsto (fun x => f x ^ z) l (𝓝 (x ^ z))

Full source

@[to_additive]
theorem Filter.Tendsto.zpow {α} {l : Filter α} {f : α → G} {x : G} (hf : Tendsto f l (𝓝 x))
    (z : ℤ) : Tendsto (fun x => f x ^ z) l (𝓝 (x ^ z)) :=
  (continuousAt_zpow _ _).tendsto.comp hf

Limit of Integer Powers in Topological Groups

Informal description

Let $G$ be a topological group, $\alpha$ a type, $l$ a filter on $\alpha$, and $f \colon \alpha \to G$ a function. If $f$ tends to $x \in G$ along the filter $l$, then for any integer $z$, the function $x \mapsto f(x)^z$ tends to $x^z$ along $l$.

ContinuousWithinAt.zpow theorem

 {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (z : ℤ) : ContinuousWithinAt (fun x => f x ^ z) s x

Full source

@[to_additive]
theorem ContinuousWithinAt.zpow {f : α → G} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x)
    (z : ℤ) : ContinuousWithinAt (fun x => f x ^ z) s x :=
  Filter.Tendsto.zpow hf z

Continuity of integer powers within a subset

Informal description

Let $G$ be a topological group, $X$ a topological space, $f \colon X \to G$ a function, $x \in X$ a point, and $s \subseteq X$ a subset. If $f$ is continuous at $x$ within $s$, then for any integer $z$, the function $x \mapsto f(x)^z$ is also continuous at $x$ within $s$.

ContinuousAt.zpow theorem

{f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) : ContinuousAt (fun x => f x ^ z) x

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousAt.zpow {f : α → G} {x : α} (hf : ContinuousAt f x) (z : ℤ) :
    ContinuousAt (fun x => f x ^ z) x :=
  Filter.Tendsto.zpow hf z

Continuity of Integer Powers in Topological Groups

Informal description

Let $G$ be a topological group, $X$ a topological space, and $f \colon X \to G$ a function. If $f$ is continuous at a point $x \in X$, then for any integer $z$, the function $x \mapsto f(x)^z$ is also continuous at $x$.

ContinuousOn.zpow theorem

{f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) : ContinuousOn (fun x => f x ^ z) s

Full source

@[to_additive (attr := fun_prop)]
theorem ContinuousOn.zpow {f : α → G} {s : Set α} (hf : ContinuousOn f s) (z : ℤ) :
    ContinuousOn (fun x => f x ^ z) s := fun x hx => (hf x hx).zpow z

Continuity of Integer Powers on a Subset in Topological Groups

Informal description

Let $G$ be a topological group, $X$ a topological space, $f \colon X \to G$ a function, and $s \subseteq X$ a subset. If $f$ is continuous on $s$, then for any integer $z$, the function $x \mapsto f(x)^z$ is also continuous on $s$.

tendsto_inv_nhdsGT theorem

{a : H} : Tendsto Inv.inv (𝓝[>] a) (𝓝[<] a⁻¹)

Full source

@[to_additive]
theorem tendsto_inv_nhdsGT {a : H} : Tendsto Inv.inv (𝓝[>] a) (𝓝[<] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Inversion Maps Right Neighborhoods to Left Neighborhoods in Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion. For any element $a \in H$, the inversion map $x \mapsto x^{-1}$ sends the right neighborhood filter of $a$ (i.e., the filter of sets containing an open interval $(a, b)$) to the left neighborhood filter of $a^{-1}$ (i.e., the filter of sets containing an open interval $(c, a^{-1})$).

tendsto_inv_nhdsLT theorem

{a : H} : Tendsto Inv.inv (𝓝[<] a) (𝓝[>] a⁻¹)

Full source

@[to_additive]
theorem tendsto_inv_nhdsLT {a : H} : Tendsto Inv.inv (𝓝[<] a) (𝓝[>] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Inversion Maps Left-Neighborhoods to Right-Neighborhoods in Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion. For any element $a \in H$, the inversion map $x \mapsto x^{-1}$ sends the left-neighborhood filter of $a$ (i.e., the filter of sets containing all elements less than $a$) to the right-neighborhood filter of $a^{-1}$ (i.e., the filter of sets containing all elements greater than $a^{-1}$). In other words, if $x$ approaches $a$ from the left ($x \to a^-$), then $x^{-1}$ approaches $a^{-1}$ from the right ($x^{-1} \to (a^{-1})^+$).

tendsto_inv_nhdsGT_inv theorem

{a : H} : Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a)

Full source

@[to_additive]
theorem tendsto_inv_nhdsGT_inv {a : H} : Tendsto Inv.inv (𝓝[>] a⁻¹) (𝓝[<] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsGT (a := a⁻¹)

Inversion Maps Right Neighborhoods of $a^{-1}$ to Left Neighborhoods of $a$ in Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion. For any element $a \in H$, the inversion map $x \mapsto x^{-1}$ sends the right neighborhood filter of $a^{-1}$ (i.e., the filter of sets containing an open interval $(a^{-1}, b)$) to the left neighborhood filter of $a$ (i.e., the filter of sets containing an open interval $(c, a)$).

tendsto_inv_nhdsLT_inv theorem

{a : H} : Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a)

Full source

@[to_additive]
theorem tendsto_inv_nhdsLT_inv {a : H} : Tendsto Inv.inv (𝓝[<] a⁻¹) (𝓝[>] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsLT (a := a⁻¹)

Inversion Maps Left-Neighborhoods of Inverse to Right-Neighborhoods in Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion. For any element $a \in H$, the inversion map $x \mapsto x^{-1}$ sends the left-neighborhood filter of $a^{-1}$ (i.e., the filter of sets containing all elements less than $a^{-1}$) to the right-neighborhood filter of $a$ (i.e., the filter of sets containing all elements greater than $a$). In other words, if $x$ approaches $a^{-1}$ from the left ($x \to (a^{-1})^-$), then $x^{-1}$ approaches $a$ from the right ($x^{-1} \to a^+$).

tendsto_inv_nhdsGE theorem

{a : H} : Tendsto Inv.inv (𝓝[≥] a) (𝓝[≤] a⁻¹)

Full source

@[to_additive]
theorem tendsto_inv_nhdsGE {a : H} : Tendsto Inv.inv (𝓝[≥] a) (𝓝[≤] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Inversion Preserves Neighborhood Filters for Upper Sets in Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion. For any element $a \in H$, the inversion function $x \mapsto x^{-1}$ maps the neighborhood filter of $a$ restricted to the set $\{x \in H \mid x \geq a\}$ to the neighborhood filter of $a^{-1}$ restricted to the set $\{x \in H \mid x \leq a^{-1}\}$.

tendsto_inv_nhdsLE theorem

{a : H} : Tendsto Inv.inv (𝓝[≤] a) (𝓝[≥] a⁻¹)

Full source

@[to_additive]
theorem tendsto_inv_nhdsLE {a : H} : Tendsto Inv.inv (𝓝[≤] a) (𝓝[≥] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Inversion Preserves Neighborhood Filters for Order-Bounded Sets

Informal description

For any element $a$ in a topological group $H$ with a partial order, the inversion operation $x \mapsto x^{-1}$ maps the neighborhood filter of elements less than or equal to $a$ to the neighborhood filter of elements greater than or equal to $a^{-1}$. In other words, the inversion operation is continuous and order-reversing in this context.

tendsto_inv_nhdsGE_inv theorem

{a : H} : Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a)

Full source

@[to_additive]
theorem tendsto_inv_nhdsGE_inv {a : H} : Tendsto Inv.inv (𝓝[≥] a⁻¹) (𝓝[≤] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsGE (a := a⁻¹)

Inversion Maps Neighborhood Filters of Inverses in Ordered Topological Groups

Informal description

Let $H$ be a topological group with continuous inversion and a partial order. For any element $a \in H$, the inversion function $x \mapsto x^{-1}$ maps the neighborhood filter of $a^{-1}$ restricted to the set $\{x \in H \mid x \geq a^{-1}\}$ to the neighborhood filter of $a$ restricted to the set $\{x \in H \mid x \leq a\}$.

tendsto_inv_nhdsLE_inv theorem

{a : H} : Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a)

Full source

@[to_additive]
theorem tendsto_inv_nhdsLE_inv {a : H} : Tendsto Inv.inv (𝓝[≤] a⁻¹) (𝓝[≥] a) := by
  simpa only [inv_inv] using tendsto_inv_nhdsLE (a := a⁻¹)

Inversion Preserves Neighborhood Filters for Order-Bounded Sets at Inverse Elements

Informal description

For any element $a$ in a topological group $H$ with a partial order, the inversion operation $x \mapsto x^{-1}$ maps the neighborhood filter of elements less than or equal to $a^{-1}$ to the neighborhood filter of elements greater than or equal to $a$. In other words, the inversion operation is continuous and order-reversing in this context.

Prod.instIsTopologicalGroup instance

[TopologicalSpace H] [Group H] [IsTopologicalGroup H] : IsTopologicalGroup (G × H)

Full source

@[to_additive]
instance Prod.instIsTopologicalGroup [TopologicalSpace H] [Group H] [IsTopologicalGroup H] :
    IsTopologicalGroup (G × H) where
  continuous_inv := continuous_inv.prodMap continuous_inv

Product of Topological Groups is a Topological Group

Informal description

For any topological groups $G$ and $H$, the product group $G \times H$ equipped with the product topology is also a topological group. That is, the componentwise multiplication and inversion operations on $G \times H$ are continuous with respect to the product topology.

OrderDual.instIsTopologicalGroup instance

: IsTopologicalGroup Gᵒᵈ

Full source

@[to_additive]
instance OrderDual.instIsTopologicalGroup : IsTopologicalGroup Gᵒᵈ where

Order Dual of a Topological Group is a Topological Group

Informal description

For any topological group $G$, the order dual $G^{\text{op}}$ is also a topological group. That is, the group operations of multiplication and inversion on $G^{\text{op}}$ are continuous with respect to the inherited topology.

Pi.topologicalGroup instance

 {C : β → Type*} [∀ b, TopologicalSpace (C b)] [∀ b, Group (C b)] [∀ b, IsTopologicalGroup (C b)] :
  IsTopologicalGroup (∀ b, C b)

Full source

@[to_additive]
instance Pi.topologicalGroup {C : β → Type*} [∀ b, TopologicalSpace (C b)] [∀ b, Group (C b)]
    [∀ b, IsTopologicalGroup (C b)] : IsTopologicalGroup (∀ b, C b) where
  continuous_inv := continuous_pi fun i => (continuous_apply i).inv

Product of Topological Groups is a Topological Group

Informal description

For any family of topological groups $\{C_b\}_{b \in \beta}$ indexed by a type $\beta$, the product group $\prod_{b \in \beta} C_b$ equipped with the product topology is also a topological group. That is, the pointwise multiplication and inversion operations on the product group are continuous with respect to the product topology.

instContinuousInvMulOpposite instance

[Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ

Full source

@[to_additive]
instance [Inv α] [ContinuousInv α] : ContinuousInv αᵐᵒᵖ :=
  opHomeomorph.symm.isInducing.continuousInv unop_inv

Continuous Inversion on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with an inversion operation and a topological space structure such that inversion is continuous, the multiplicative opposite $\alpha^\text{op}$ also has a continuous inversion operation.

instIsTopologicalGroupMulOpposite instance

[Group α] [IsTopologicalGroup α] : IsTopologicalGroup αᵐᵒᵖ

Full source

/-- If multiplication is continuous in `α`, then it also is in `αᵐᵒᵖ`. -/
@[to_additive "If addition is continuous in `α`, then it also is in `αᵃᵒᵖ`."]
instance [Group α] [IsTopologicalGroup α] : IsTopologicalGroup αᵐᵒᵖ where

Topological Group Structure on the Multiplicative Opposite

Informal description

For any group $\alpha$ with a topological group structure, the multiplicative opposite $\alpha^\text{op}$ is also a topological group. That is, the multiplication and inversion operations in $\alpha^\text{op}$ are continuous with respect to the inherited topology.

nhds_one_symm theorem

: comap Inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G)

Full source

@[to_additive]
theorem nhds_one_symm : comap Inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G) :=
  ((Homeomorph.inv G).comap_nhds_eq _).trans (congr_arg nhds inv_one)

Inversion Preserves Neighborhood Filter of Identity in Topological Groups

Informal description

For any topological group $G$, the preimage of the neighborhood filter of the identity element $1$ under the inversion operation is equal to the neighborhood filter of $1$, i.e., $\text{Inv}^{-1}(\mathcal{N}_1) = \mathcal{N}_1$.

nhds_one_symm' theorem

: map Inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G)

Full source

@[to_additive]
theorem nhds_one_symm' : map Inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G) :=
  ((Homeomorph.inv G).map_nhds_eq _).trans (congr_arg nhds inv_one)

Inversion Preserves Neighborhood Filter of Identity in Topological Groups

Informal description

In a topological group $G$, the image of the neighborhood filter of the identity element $1$ under the inversion operation is equal to the neighborhood filter of $1$, i.e., $\text{inv}_*(\mathcal{N}_1) = \mathcal{N}_1$.

inv_mem_nhds_one theorem

{S : Set G} (hS : S ∈ (𝓝 1 : Filter G)) : S⁻¹ ∈ 𝓝 (1 : G)

Full source

@[to_additive]
theorem inv_mem_nhds_one {S : Set G} (hS : S ∈ (𝓝 1 : Filter G)) : S⁻¹S⁻¹ ∈ 𝓝 (1 : G) := by
  rwa [← nhds_one_symm'] at hS

Inversion Preserves Neighborhoods of Identity in Topological Groups

Informal description

For any topological group $G$ and any set $S$ in the neighborhood filter of the identity element $1$, the set of inverses $S^{-1} = \{x^{-1} \mid x \in S\}$ is also in the neighborhood filter of $1$.

Homeomorph.shearMulRight definition

: G × G ≃ₜ G × G

Full source

/-- The map `(x, y) ↦ (x, x * y)` as a homeomorphism. This is a shear mapping. -/
@[to_additive "The map `(x, y) ↦ (x, x + y)` as a homeomorphism. This is a shear mapping."]
protected def Homeomorph.shearMulRight : G × GG × G ≃ₜ G × G :=
  { Equiv.prodShear (Equiv.refl _) Equiv.mulLeft with
    continuous_toFun := by dsimp; fun_prop
    continuous_invFun := by dsimp; fun_prop }

Shear multiplication homeomorphism on a topological group

Informal description

The homeomorphism from $G \times G$ to itself defined by $(x, y) \mapsto (x, x \cdot y)$, where $G$ is a topological group. This is a shear mapping that preserves the first component and multiplies it with the second component. The inverse mapping is given by $(x, y) \mapsto (x, x^{-1} \cdot y)$.

Homeomorph.shearMulRight_coe theorem

: ⇑(Homeomorph.shearMulRight G) = fun z : G × G => (z.1, z.1 * z.2)

Full source

@[to_additive (attr := simp)]
theorem Homeomorph.shearMulRight_coe :
    ⇑(Homeomorph.shearMulRight G) = fun z : G × G => (z.1, z.1 * z.2) :=
  rfl

Definition of the Shear Multiplication Homeomorphism on a Topological Group

Informal description

The homeomorphism $\text{shearMulRight} \colon G \times G \to G \times G$ is defined by $\text{shearMulRight}(x, y) = (x, x \cdot y)$ for all $(x, y) \in G \times G$, where $G$ is a topological group.

Homeomorph.shearMulRight_symm_coe theorem

: ⇑(Homeomorph.shearMulRight G).symm = fun z : G × G => (z.1, z.1⁻¹ * z.2)

Full source

@[to_additive (attr := simp)]
theorem Homeomorph.shearMulRight_symm_coe :
    ⇑(Homeomorph.shearMulRight G).symm = fun z : G × G => (z.1, z.1⁻¹ * z.2) :=
  rfl

Inverse of Shear Multiplication Homeomorphism: $(x, y) \mapsto (x, x^{-1} \cdot y)$

Informal description

The inverse of the shear multiplication homeomorphism $\text{shearMulRight} \colon G \times G \to G \times G$ on a topological group $G$ is given by the function $(x, y) \mapsto (x, x^{-1} \cdot y)$ for all $(x, y) \in G \times G$.

Topology.IsInducing.topologicalGroup theorem

 {F : Type*} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : IsInducing f) :
  IsTopologicalGroup H

Full source

@[to_additive]
protected theorem Topology.IsInducing.topologicalGroup {F : Type*} [Group H] [TopologicalSpace H]
    [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : IsInducing f) : IsTopologicalGroup H :=
  { toContinuousMul := hf.continuousMul _
    toContinuousInv := hf.continuousInv (map_inv f) }

Induced Topological Group Structure via Monoid Homomorphism

Informal description

Let $H$ be a group with a topological space structure, and let $G$ be a topological group. Given a monoid homomorphism $f \colon H \to G$ that induces the topology on $H$ (i.e., the topology on $H$ is the coinduced topology from $G$ via $f$), then $H$ is also a topological group.

topologicalGroup_induced theorem

{F : Type*} [Group H] [FunLike F H G] [MonoidHomClass F H G] (f : F) : @IsTopologicalGroup H (induced f ‹_›) _

Full source

@[to_additive]
theorem topologicalGroup_induced {F : Type*} [Group H] [FunLike F H G] [MonoidHomClass F H G]
    (f : F) :
    @IsTopologicalGroup H (induced f ‹_›) _ :=
  letI := induced f ‹_›
  IsInducing.topologicalGroup f ⟨rfl⟩

Induced Topological Group Structure via Monoid Homomorphism

Informal description

Let $H$ be a group and $G$ be a topological group. Given a monoid homomorphism $f \colon H \to G$, the group $H$ equipped with the topology induced by $f$ is a topological group.

Subgroup.instIsTopologicalGroupSubtypeMem instance

(S : Subgroup G) : IsTopologicalGroup S

Full source

@[to_additive]
instance (S : Subgroup G) : IsTopologicalGroup S :=
  IsInducing.subtypeVal.topologicalGroup S.subtype

Subgroups of Topological Groups are Topological Groups

Informal description

For any subgroup $S$ of a topological group $G$, the subgroup $S$ inherits a topological group structure from $G$ where the group operations (multiplication and inversion) are continuous with respect to the subspace topology.

Subgroup.topologicalClosure definition

(s : Subgroup G) : Subgroup G

Full source

/-- The (topological-space) closure of a subgroup of a topological group is
itself a subgroup. -/
@[to_additive
  "The (topological-space) closure of an additive subgroup of an additive topological group is
  itself an additive subgroup."]
def Subgroup.topologicalClosure (s : Subgroup G) : Subgroup G :=
  { s.toSubmonoid.topologicalClosure with
    carrier := _root_.closure (s : Set G)
    inv_mem' := fun {g} hg => by simpa only [← Set.mem_inv, inv_closure, inv_coe_set] using hg }

Topological closure of a subgroup

Informal description

Given a subgroup $ s $ of a topological group $ G $, the topological closure of $ s $ is itself a subgroup of $ G $. The underlying set of this closure is the topological closure of the underlying set of $ s $, and it is closed under the group operations (multiplication and inversion).

Subgroup.topologicalClosure_coe theorem

{s : Subgroup G} : (s.topologicalClosure : Set G) = _root_.closure s

Full source

@[to_additive (attr := simp)]
theorem Subgroup.topologicalClosure_coe {s : Subgroup G} :
    (s.topologicalClosure : Set G) = _root_.closure s :=
  rfl

Equality of Subgroup Closure and Set Closure in Topological Groups

Informal description

For any subgroup $s$ of a topological group $G$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$, i.e., $\overline{s} = \overline{(s : \text{Set } G)}$.

Subgroup.le_topologicalClosure theorem

(s : Subgroup G) : s ≤ s.topologicalClosure

Full source

@[to_additive]
theorem Subgroup.le_topologicalClosure (s : Subgroup G) : s ≤ s.topologicalClosure :=
  _root_.subset_closure

Subgroup is Contained in its Topological Closure

Informal description

For any subgroup $s$ of a topological group $G$, the subgroup $s$ is contained in its topological closure, i.e., $s \leq \overline{s}$.

Subgroup.isClosed_topologicalClosure theorem

(s : Subgroup G) : IsClosed (s.topologicalClosure : Set G)

Full source

@[to_additive]
theorem Subgroup.isClosed_topologicalClosure (s : Subgroup G) :
    IsClosed (s.topologicalClosure : Set G) := isClosed_closure

Topological Closure of a Subgroup is Closed

Informal description

For any subgroup $s$ of a topological group $G$, the topological closure of $s$ is a closed subset of $G$.

Subgroup.topologicalClosure_minimal theorem

(s : Subgroup G) {t : Subgroup G} (h : s ≤ t) (ht : IsClosed (t : Set G)) : s.topologicalClosure ≤ t

Full source

@[to_additive]
theorem Subgroup.topologicalClosure_minimal (s : Subgroup G) {t : Subgroup G} (h : s ≤ t)
    (ht : IsClosed (t : Set G)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Subgroup Closure: $\overline{s} \leq t$ for $s \leq t$ and $t$ closed

Informal description

Let $G$ be a topological group and let $s$ and $t$ be subgroups of $G$ such that $s \leq t$ and $t$ is closed in the topology of $G$. Then the topological closure of $s$ is contained in $t$, i.e., $\overline{s} \leq t$.

DenseRange.topologicalClosure_map_subgroup theorem

 [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {f : G →* H} (hf : Continuous f) (hf' : DenseRange f)
  {s : Subgroup G} (hs : s.topologicalClosure = ⊤) : (s.map f).topologicalClosure = ⊤

Full source

@[to_additive]
theorem DenseRange.topologicalClosure_map_subgroup [Group H] [TopologicalSpace H]
    [IsTopologicalGroup H] {f : G →* H} (hf : Continuous f) (hf' : DenseRange f) {s : Subgroup G}
    (hs : s.topologicalClosure = ⊤) : (s.map f).topologicalClosure = ⊤ := by
  rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢
  exact hf'.dense_image hf hs

Density Preservation of Subgroup Images under Continuous Homomorphisms with Dense Range

Informal description

Let $G$ and $H$ be topological groups, and let $f \colon G \to H$ be a continuous group homomorphism with dense range. If $s$ is a subgroup of $G$ whose topological closure is the entire group $G$ (i.e., $\overline{s} = G$), then the topological closure of the image subgroup $f(s)$ is the entire group $H$ (i.e., $\overline{f(s)} = H$).

Subgroup.is_normal_topologicalClosure theorem

 {G : Type*} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] :
  (Subgroup.topologicalClosure N).Normal

Full source

/-- The topological closure of a normal subgroup is normal. -/
@[to_additive "The topological closure of a normal additive subgroup is normal."]
theorem Subgroup.is_normal_topologicalClosure {G : Type*} [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] :
    (Subgroup.topologicalClosure N).Normal where
  conj_mem n hn g := by
    apply map_mem_closure (IsTopologicalGroup.continuous_conj g) hn
    exact fun m hm => Subgroup.Normal.conj_mem inferInstance m hm g

Normality of Topological Closure of a Normal Subgroup

Informal description

Let $G$ be a topological group and $N$ a normal subgroup of $G$. Then the topological closure of $N$ is also a normal subgroup of $G$.

mul_mem_connectedComponent_one theorem

 {G : Type*} [TopologicalSpace G] [MulOneClass G] [ContinuousMul G] {g h : G} (hg : g ∈ connectedComponent (1 : G))
  (hh : h ∈ connectedComponent (1 : G)) : g * h ∈ connectedComponent (1 : G)

Full source

@[to_additive]
theorem mul_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [MulOneClass G]
    [ContinuousMul G] {g h : G} (hg : g ∈ connectedComponent (1 : G))
    (hh : h ∈ connectedComponent (1 : G)) : g * h ∈ connectedComponent (1 : G) := by
  rw [connectedComponent_eq hg]
  have hmul : g ∈ connectedComponent (g * h) := by
    apply Continuous.image_connectedComponent_subset (continuous_mul_left g)
    rw [← connectedComponent_eq hh]
    exact ⟨(1 : G), mem_connectedComponent, by simp only [mul_one]⟩
  simpa [← connectedComponent_eq hmul] using mem_connectedComponent

Product of Elements in Identity's Connected Component Remains in Connected Component

Informal description

Let $G$ be a topological space equipped with a multiplicative monoid structure and continuous multiplication. For any two elements $g, h \in G$ that belong to the connected component of the identity element $1$, their product $g * h$ also belongs to the connected component of $1$.

inv_mem_connectedComponent_one theorem

 {G : Type*} [TopologicalSpace G] [DivisionMonoid G] [ContinuousInv G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
  g⁻¹ ∈ connectedComponent (1 : G)

Full source

@[to_additive]
theorem inv_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [DivisionMonoid G]
    [ContinuousInv G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
    g⁻¹g⁻¹ ∈ connectedComponent (1 : G) := by
  rw [← inv_one]
  exact
    Continuous.image_connectedComponent_subset continuous_inv _
      ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)

Inverse of Element in Identity's Connected Component Remains in Connected Component

Informal description

Let $G$ be a topological space equipped with a division monoid structure and continuous inversion. For any element $g \in G$ that belongs to the connected component of the identity element $1$, its inverse $g^{-1}$ also belongs to the connected component of $1$.

Subgroup.connectedComponentOfOne definition

(G : Type*) [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : Subgroup G

Full source

/-- The connected component of 1 is a subgroup of `G`. -/
@[to_additive "The connected component of 0 is a subgroup of `G`."]
def Subgroup.connectedComponentOfOne (G : Type*) [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] : Subgroup G where
  carrier := connectedComponent (1 : G)
  one_mem' := mem_connectedComponent
  mul_mem' hg hh := mul_mem_connectedComponent_one hg hh
  inv_mem' hg := inv_mem_connectedComponent_one hg

Connected component of identity as a subgroup

Informal description

The connected component of the identity element $1$ in a topological group $G$ forms a subgroup of $G$. This subgroup consists of all elements that are path-connected to $1$ in the topology of $G$.

Subgroup.commGroupTopologicalClosure abbrev

[T2Space G] (s : Subgroup G) (hs : ∀ x y : s, x * y = y * x) : CommGroup s.topologicalClosure

Full source

/-- If a subgroup of a topological group is commutative, then so is its topological closure.

See note [reducible non-instances]. -/
@[to_additive
  "If a subgroup of an additive topological group is commutative, then so is its
topological closure.

See note [reducible non-instances]."]
abbrev Subgroup.commGroupTopologicalClosure [T2Space G] (s : Subgroup G)
    (hs : ∀ x y : s, x * y = y * x) : CommGroup s.topologicalClosure :=
  { s.topologicalClosure.toGroup, s.toSubmonoid.commMonoidTopologicalClosure hs with }

Commutativity of Topological Closure for Commutative Subgroups in Hausdorff Topological Groups

Informal description

Let $G$ be a Hausdorff topological group. If $s$ is a subgroup of $G$ such that $x \cdot y = y \cdot x$ for all $x, y \in s$, then the topological closure of $s$ is a commutative group.

Subgroup.coe_topologicalClosure_bot theorem

: ((⊥ : Subgroup G).topologicalClosure : Set G) = _root_.closure ({ 1 } : Set G)

Full source

@[to_additive]
lemma Subgroup.coe_topologicalClosure_bot :
    ((⊥ : Subgroup G).topologicalClosure : Set G) = _root_.closure ({1} : Set G) := by simp

Closure of Trivial Subgroup Equals Closure of Identity Element

Informal description

The topological closure of the trivial subgroup $\{1\}$ in a topological group $G$ is equal to the closure of the singleton set $\{1\}$ in the underlying topological space of $G$.

exists_nhds_split_inv theorem

{s : Set G} (hs : s ∈ 𝓝 (1 : G)) : ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s

Full source

@[to_additive exists_nhds_half_neg]
theorem exists_nhds_split_inv {s : Set G} (hs : s ∈ 𝓝 (1 : G)) :
    ∃ V ∈ 𝓝 (1 : G), ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s := by
  have : (fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s(fun p : G × G => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 ((1, 1) : G × G) :=
    continuousAt_fst.mul continuousAt_snd.inv (by simpa)
  simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff, mem_preimage] using
    this

Existence of a neighborhood $V$ of $1$ such that $V/V \subseteq s$ for any neighborhood $s$ of $1$ in a topological group

Informal description

For any neighborhood $s$ of the identity element $1$ in a topological group $G$, there exists a neighborhood $V$ of $1$ such that for all $v, w \in V$, the quotient $v / w$ belongs to $s$.

nhds_translation_mul_inv theorem

(x : G) : comap (· * x⁻¹) (𝓝 1) = 𝓝 x

Full source

@[to_additive]
theorem nhds_translation_mul_inv (x : G) : comap (· * x⁻¹) (𝓝 1) = 𝓝 x :=
  ((Homeomorph.mulRight x⁻¹).comap_nhds_eq 1).trans <| show 𝓝 (1 * x⁻¹x⁻¹⁻¹) = 𝓝 x by simp

Neighborhood Filter Translation via Right Multiplication by Inverse in Topological Groups

Informal description

For any element $x$ in a topological group $G$, the preimage of the neighborhood filter of the identity element $1$ under the map $y \mapsto y * x^{-1}$ is equal to the neighborhood filter of $x$, i.e., $(y \mapsto y * x^{-1})^{-1}(\mathcal{N}_1) = \mathcal{N}_x$.

map_mul_left_nhds theorem

(x y : G) : map (x * ·) (𝓝 y) = 𝓝 (x * y)

Full source

@[to_additive (attr := simp)]
theorem map_mul_left_nhds (x y : G) : map (x * ·) (𝓝 y) = 𝓝 (x * y) :=
  (Homeomorph.mulLeft x).map_nhds_eq y

Left Multiplication Preserves Neighborhood Filters in a Topological Group

Informal description

For any elements $x$ and $y$ in a topological group $G$, the pushforward of the neighborhood filter $\mathcal{N}_y$ under the left multiplication map $z \mapsto x \cdot z$ equals the neighborhood filter $\mathcal{N}_{x \cdot y}$ at $x \cdot y$.

map_mul_left_nhds_one theorem

(x : G) : map (x * ·) (𝓝 1) = 𝓝 x

Full source

@[to_additive]
theorem map_mul_left_nhds_one (x : G) : map (x * ·) (𝓝 1) = 𝓝 x := by simp

Left multiplication by $x$ maps the identity's neighborhood filter to $x$'s neighborhood filter

Informal description

For any element $x$ in a topological group $G$, the pushforward of the neighborhood filter $\mathcal{N}_1$ of the identity element under the left multiplication map $z \mapsto x \cdot z$ equals the neighborhood filter $\mathcal{N}_x$ at $x$.

map_mul_right_nhds theorem

(x y : G) : map (· * x) (𝓝 y) = 𝓝 (y * x)

Full source

@[to_additive (attr := simp)]
theorem map_mul_right_nhds (x y : G) : map (· * x) (𝓝 y) = 𝓝 (y * x) :=
  (Homeomorph.mulRight x).map_nhds_eq y

Right Multiplication Preserves Neighborhood Filters in a Topological Group

Informal description

For any elements $x$ and $y$ in a topological group $G$, the pushforward of the neighborhood filter $\mathcal{N}_y$ under the right multiplication map $(\cdot) * x$ equals the neighborhood filter $\mathcal{N}_{y * x}$ at $y * x$. In other words, $(\cdot * x)_*(\mathcal{N}_y) = \mathcal{N}_{y * x}$.

map_mul_right_nhds_one theorem

(x : G) : map (· * x) (𝓝 1) = 𝓝 x

Full source

@[to_additive]
theorem map_mul_right_nhds_one (x : G) : map (· * x) (𝓝 1) = 𝓝 x := by simp

Right multiplication by $x$ maps the identity's neighborhood filter to $x$'s neighborhood filter

Informal description

For any element $x$ in a topological group $G$, the pushforward of the neighborhood filter $\mathcal{N}_1$ of the identity element under the right multiplication map $(\cdot) * x$ equals the neighborhood filter $\mathcal{N}_x$ at $x$. In other words, $(\cdot * x)_*(\mathcal{N}_1) = \mathcal{N}_x$.

Filter.HasBasis.nhds_of_one theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set G} (hb : HasBasis (𝓝 1 : Filter G) p s) (x : G) :
  HasBasis (𝓝 x) p fun i => {y | y / x ∈ s i}

Full source

@[to_additive]
theorem Filter.HasBasis.nhds_of_one {ι : Sort*} {p : ι → Prop} {s : ι → Set G}
    (hb : HasBasis (𝓝 1 : Filter G) p s) (x : G) :
    HasBasis (𝓝 x) p fun i => { y | y / x ∈ s i } := by
  rw [← nhds_translation_mul_inv]
  simp_rw [div_eq_mul_inv]
  exact hb.comap _

Neighborhood Filter Basis Characterization via Division in Topological Groups

Informal description

Let $G$ be a topological group with neighborhood filter $\mathcal{N}_1$ of the identity element having a basis $\{s_i \mid p_i\}$ indexed by a predicate $p$. Then for any $x \in G$, the neighborhood filter $\mathcal{N}_x$ of $x$ has a basis $\{y \mid y/x \in s_i\}$ indexed by the same predicate $p$.

mem_closure_iff_nhds_one theorem

{x : G} {s : Set G} : x ∈ closure s ↔ ∀ U ∈ (𝓝 1 : Filter G), ∃ y ∈ s, y / x ∈ U

Full source

@[to_additive]
theorem mem_closure_iff_nhds_one {x : G} {s : Set G} :
    x ∈ closure sx ∈ closure s ↔ ∀ U ∈ (𝓝 1 : Filter G), ∃ y ∈ s, y / x ∈ U := by
  rw [mem_closure_iff_nhds_basis ((𝓝 1 : Filter G).basis_sets.nhds_of_one x)]
  simp_rw [Set.mem_setOf, id]

Closure Membership Criterion via Identity Neighborhoods in Topological Groups

Informal description

Let $G$ be a topological group and $s \subseteq G$ a subset. A point $x \in G$ belongs to the closure of $s$ if and only if for every neighborhood $U$ of the identity element $1 \in G$, there exists $y \in s$ such that $y/x \in U$.

continuous_of_continuousAt_one theorem

 {M hom : Type*} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M]
  (f : hom) (hf : ContinuousAt f 1) : Continuous f

Full source

/-- A monoid homomorphism (a bundled morphism of a type that implements `MonoidHomClass`) from a
topological group to a topological monoid is continuous provided that it is continuous at one. See
also `uniformContinuous_of_continuousAt_one`. -/
@[to_additive
  "An additive monoid homomorphism (a bundled morphism of a type that implements
  `AddMonoidHomClass`) from an additive topological group to an additive topological monoid is
  continuous provided that it is continuous at zero. See also
  `uniformContinuous_of_continuousAt_zero`."]
theorem continuous_of_continuousAt_one {M hom : Type*} [MulOneClass M] [TopologicalSpace M]
    [ContinuousMul M] [FunLike hom G M] [MonoidHomClass hom G M] (f : hom)
    (hf : ContinuousAt f 1) :
    Continuous f :=
  continuous_iff_continuousAt.2 fun x => by
    simpa only [ContinuousAt, ← map_mul_left_nhds_one x, tendsto_map'_iff, Function.comp_def,
      map_mul, map_one, mul_one] using hf.tendsto.const_mul (f x)

Continuity of Monoid Homomorphisms via Continuity at Identity

Informal description

Let $G$ and $M$ be topological monoids with continuous multiplication, where $G$ is also a group. For any monoid homomorphism $f \colon G \to M$ that is continuous at the identity element $1 \in G$, the homomorphism $f$ is continuous on the whole group $G$.

continuous_of_continuousAt_one₂ theorem

 {H M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] [Group H] [TopologicalSpace H]
  [IsTopologicalGroup H] (f : G →* H →* M) (hf : ContinuousAt (fun x : G × H ↦ f x.1 x.2) (1, 1))
  (hl : ∀ x, ContinuousAt (f x) 1) (hr : ∀ y, ContinuousAt (f · y) 1) : Continuous (fun x : G × H ↦ f x.1 x.2)

Full source

@[to_additive continuous_of_continuousAt_zero₂]
theorem continuous_of_continuousAt_one₂ {H M : Type*} [CommMonoid M] [TopologicalSpace M]
    [ContinuousMul M] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H →* M)
    (hf : ContinuousAt (fun x : G × H ↦ f x.1 x.2) (1, 1))
    (hl : ∀ x, ContinuousAt (f x) 1) (hr : ∀ y, ContinuousAt (f · y) 1) :
    Continuous (fun x : G × H ↦ f x.1 x.2) := continuous_iff_continuousAt.2 fun (x, y) => by
  simp only [ContinuousAt, nhds_prod_eq, ← map_mul_left_nhds_one x, ← map_mul_left_nhds_one y,
    prod_map_map_eq, tendsto_map'_iff, Function.comp_def, map_mul, MonoidHom.mul_apply] at *
  refine ((tendsto_const_nhds.mul ((hr y).comp tendsto_fst)).mul
    (((hl x).comp tendsto_snd).mul hf)).mono_right (le_of_eq ?_)
  simp only [map_one, mul_one, MonoidHom.one_apply]

Joint Continuity of Bihomomorphisms via Continuity at Identity

Informal description

Let $G$ and $H$ be topological groups, and let $M$ be a commutative topological monoid with continuous multiplication. Given a monoid homomorphism $f \colon G \to (H \to^* M)$ such that: 1. The map $(x,y) \mapsto f(x)(y)$ is continuous at $(1,1) \in G \times H$; 2. For every $x \in G$, the map $f(x) \colon H \to M$ is continuous at $1 \in H$; 3. For every $y \in H$, the map $f(\cdot)(y) \colon G \to M$ is continuous at $1 \in G$; then the map $(x,y) \mapsto f(x)(y)$ is continuous on $G \times H$.

IsTopologicalGroup.isInducing_iff_nhds_one theorem

 {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {F : Type*} [FunLike F G H] [MonoidHomClass F G H]
  {f : F} : Topology.IsInducing f ↔ 𝓝 (1 : G) = (𝓝 (1 : H)).comap f

Full source

@[to_additive]
lemma IsTopologicalGroup.isInducing_iff_nhds_one
    {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {F : Type*}
    [FunLike F G H] [MonoidHomClass F G H] {f : F} :
    Topology.IsInducingTopology.IsInducing f ↔ 𝓝 (1 : G) = (𝓝 (1 : H)).comap f := by
  rw [Topology.isInducing_iff_nhds]
  refine ⟨(map_one f ▸ · 1), fun hf x ↦ ?_⟩
  rw [← nhds_translation_mul_inv, ← nhds_translation_mul_inv (f x), Filter.comap_comap, hf,
    Filter.comap_comap]
  congr 1
  ext; simp

Characterization of Inducing Group Homomorphisms via Neighborhood Filters at Identity

Informal description

Let $G$ and $H$ be topological groups, and let $f \colon G \to H$ be a group homomorphism. Then $f$ is an inducing map (i.e., the topology on $G$ is the coarsest topology making $f$ continuous) if and only if the neighborhood filter of the identity in $G$ is equal to the preimage under $f$ of the neighborhood filter of the identity in $H$, i.e., $\mathcal{N}_1^G = f^{-1}(\mathcal{N}_1^H)$.

TopologicalGroup.isOpenMap_iff_nhds_one theorem

 {H : Type*} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H] {F : Type*} [FunLike F G H]
  [MonoidHomClass F G H] {f : F} : IsOpenMap f ↔ 𝓝 1 ≤ .map f (𝓝 1)

Full source

@[to_additive]
lemma TopologicalGroup.isOpenMap_iff_nhds_one
    {H : Type*} [Monoid H] [TopologicalSpace H] [ContinuousConstSMul H H]
    {F : Type*} [FunLike F G H] [MonoidHomClass F G H] {f : F} :
    IsOpenMapIsOpenMap f ↔ 𝓝 1 ≤ .map f (𝓝 1) := by
  refine ⟨fun H ↦ map_one f ▸ H.nhds_le 1, fun h ↦ IsOpenMap.of_nhds_le fun x ↦ ?_⟩
  have : Filter.map (f x * ·) (𝓝 1) = 𝓝 (f x) := by
    simpa [-Homeomorph.map_nhds_eq, Units.smul_def] using
      (Homeomorph.smul ((toUnits x).map (MonoidHomClass.toMonoidHom f))).map_nhds_eq (1 : H)
  rw [← map_mul_left_nhds_one x, Filter.map_map, Function.comp_def, ← this]
  refine (Filter.map_mono h).trans ?_
  simp [Function.comp_def]

Open Map Criterion for Monoid Homomorphisms via Identity Neighborhoods

Informal description

Let $G$ and $H$ be topological monoids with $H$ having continuous scalar multiplication by itself, and let $f \colon G \to H$ be a monoid homomorphism. Then $f$ is an open map if and only if the neighborhood filter of the identity in $H$ is contained in the image under $f$ of the neighborhood filter of the identity in $G$, i.e., $\mathcal{N}_1^H \leq f_*(\mathcal{N}_1^G)$.

MonoidHom.isOpenQuotientMap_of_isQuotientMap theorem

 {A : Type*} [Group A] [TopologicalSpace A] [ContinuousMul A] {B : Type*} [Group B] [TopologicalSpace B] {F : Type*}
  [FunLike F A B] [MonoidHomClass F A B] {φ : F} (hφ : IsQuotientMap φ) : IsOpenQuotientMap φ

Full source

/-- Let `A` and `B` be topological groups, and let `φ : A → B` be a continuous surjective group
homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map. -/
@[to_additive "Let `A` and `B` be topological additive groups, and let `φ : A → B` be a continuous
surjective additive group homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map."]
lemma MonoidHom.isOpenQuotientMap_of_isQuotientMap {A : Type*} [Group A]
    [TopologicalSpace A] [ContinuousMul A] {B : Type*} [Group B] [TopologicalSpace B]
    {F : Type*} [FunLike F A B] [MonoidHomClass F A B] {φ : F}
    (hφ : IsQuotientMap φ) : IsOpenQuotientMap φ where
    surjective := hφ.surjective
    continuous := hφ.continuous
    isOpenMap := by
      -- We need to check that if `U ⊆ A` is open then `φ⁻¹ (φ U)` is open.
      intro U hU
      rw [← hφ.isOpen_preimage]
      -- It suffices to show that `φ⁻¹ (φ U) = ⋃ (U * k⁻¹)` as `k` runs through the kernel of `φ`,
      -- as `U * k⁻¹` is open because `x ↦ x * k` is continuous.
      -- Remark: here is where we use that we have groups not monoids (you cannot avoid
      -- using both `k` and `k⁻¹` at this point).
      suffices ⇑φ ⁻¹' (⇑φ '' U) = ⋃ k ∈ ker (φ : A →* B), (fun x ↦ x * k) ⁻¹' U by
        exact this ▸ isOpen_biUnion (fun k _ ↦ Continuous.isOpen_preimage (by fun_prop) _ hU)
      ext x
      -- But this is an elementary calculation.
      constructor
      · rintro ⟨y, hyU, hyx⟩
        apply Set.mem_iUnion_of_mem (x⁻¹ * y)
        simp_all
      · rintro ⟨_, ⟨k, rfl⟩, _, ⟨(hk : φ k = 1), rfl⟩, hx⟩
        use x * k, hx
        rw [map_mul, hk, mul_one]

Openness of Quotient Maps for Topological Group Homomorphisms

Informal description

Let $A$ and $B$ be topological groups, and let $\varphi \colon A \to B$ be a continuous surjective group homomorphism. If $\varphi$ is a quotient map (i.e., for any subset $V \subseteq B$, $V$ is open if and only if $\varphi^{-1}(V)$ is open), then $\varphi$ is an open quotient map.

IsTopologicalGroup.ext theorem

 {G : Type*} [Group G] {t t' : TopologicalSpace G} (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _)
  (h : @nhds G t 1 = @nhds G t' 1) : t = t'

Full source

@[to_additive]
theorem IsTopologicalGroup.ext {G : Type*} [Group G] {t t' : TopologicalSpace G}
    (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _)
    (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
  TopologicalSpace.ext_nhds fun x ↦ by
    rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]

Uniqueness of Topological Group Structure via Identity Neighborhoods

Informal description

Let $G$ be a group with two topological space structures $t$ and $t'$ such that both $(G, t)$ and $(G, t')$ are topological groups. If the neighborhood filters of the identity element $1$ coincide in both topologies (i.e., $\mathcal{N}_t(1) = \mathcal{N}_{t'}(1)$), then the two topologies $t$ and $t'$ are equal.

IsTopologicalGroup.ext_iff theorem

 {G : Type*} [Group G] {t t' : TopologicalSpace G} (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _) :
  t = t' ↔ @nhds G t 1 = @nhds G t' 1

Full source

@[to_additive]
theorem IsTopologicalGroup.ext_iff {G : Type*} [Group G] {t t' : TopologicalSpace G}
    (tg : @IsTopologicalGroup G t _) (tg' : @IsTopologicalGroup G t' _) :
    t = t' ↔ @nhds G t 1 = @nhds G t' 1 :=
  ⟨fun h => h ▸ rfl, tg.ext tg'⟩

Equivalence of Topological Group Structures via Identity Neighborhoods

Informal description

Let $G$ be a group with two topological space structures $t$ and $t'$ such that both $(G, t)$ and $(G, t')$ are topological groups. Then $t = t'$ if and only if the neighborhood filters of the identity element $1$ coincide in both topologies (i.e., $\mathcal{N}_t(1) = \mathcal{N}_{t'}(1)$).

ContinuousInv.of_nhds_one theorem

 {G : Type*} [Group G] [TopologicalSpace G] (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
  (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x : G => x₀ * x) (𝓝 1))
  (hconj : ∀ x₀ : G, Tendsto (fun x : G => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)) : ContinuousInv G

Full source

@[to_additive]
theorem ContinuousInv.of_nhds_one {G : Type*} [Group G] [TopologicalSpace G]
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x : G => x₀ * x) (𝓝 1))
    (hconj : ∀ x₀ : G, Tendsto (fun x : G => x₀ * x * x₀⁻¹) (𝓝 1) (𝓝 1)) : ContinuousInv G := by
  refine ⟨continuous_iff_continuousAt.2 fun x₀ => ?_⟩
  have : Tendsto (fun x => x₀⁻¹ * (x₀ * x⁻¹ * x₀⁻¹)) (𝓝 1) (map (x₀⁻¹ * ·) (𝓝 1)) :=
    (tendsto_map.comp <| hconj x₀).comp hinv
  simpa only [ContinuousAt, hleft x₀, hleft x₀⁻¹, tendsto_map'_iff, Function.comp_def, mul_assoc,
    mul_inv_rev, inv_mul_cancel_left] using this

Sufficient Conditions for Continuous Inversion in Topological Groups

Informal description

Let $G$ be a group equipped with a topology. If the following conditions hold: 1. The inversion map $x \mapsto x^{-1}$ tends to $1$ along the neighborhood filter of $1$, 2. For every $x_0 \in G$, the neighborhood filter of $x_0$ is equal to the image of the neighborhood filter of $1$ under left multiplication by $x_0$, 3. For every $x_0 \in G$, the conjugation map $x \mapsto x_0 * x * x_0^{-1}$ tends to $1$ along the neighborhood filter of $1$, then the inversion operation on $G$ is continuous.

IsTopologicalGroup.of_nhds_one' theorem

 {G : Type u} [Group G] [TopologicalSpace G] (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
  (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
  (hright : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : IsTopologicalGroup G

Full source

@[to_additive]
theorem IsTopologicalGroup.of_nhds_one' {G : Type u} [Group G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x₀ * x) (𝓝 1))
    (hright : ∀ x₀ : G, 𝓝 x₀ = map (fun x => x * x₀) (𝓝 1)) : IsTopologicalGroup G :=
  { toContinuousMul := ContinuousMul.of_nhds_one hmul hleft hright
    toContinuousInv :=
      ContinuousInv.of_nhds_one hinv hleft fun x₀ =>
        le_of_eq
          (by
            rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]
            simp [(· ∘ ·)]) }

Sufficient Conditions for a Topological Group via Neighborhoods of Identity

Informal description

Let $G$ be a group equipped with a topology. If the following conditions hold: 1. The multiplication operation $(x,y) \mapsto x * y$ is continuous at $(1,1)$, 2. The inversion map $x \mapsto x^{-1}$ is continuous at $1$, 3. For every $x_0 \in G$, the neighborhood filter of $x_0$ equals the image of the neighborhood filter of $1$ under left multiplication by $x_0$, 4. For every $x_0 \in G$, the neighborhood filter of $x_0$ equals the image of the neighborhood filter of $1$ under right multiplication by $x_0$, then $G$ is a topological group (i.e., multiplication and inversion are globally continuous).

IsTopologicalGroup.of_nhds_one theorem

 {G : Type u} [Group G] [TopologicalSpace G] (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
  (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1))
  (hconj : ∀ x₀ : G, Tendsto (x₀ * · * x₀⁻¹) (𝓝 1) (𝓝 1)) : IsTopologicalGroup G

Full source

@[to_additive]
theorem IsTopologicalGroup.of_nhds_one {G : Type u} [Group G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1))
    (hconj : ∀ x₀ : G, Tendsto (x₀ * · * x₀⁻¹) (𝓝 1) (𝓝 1)) : IsTopologicalGroup G := by
  refine IsTopologicalGroup.of_nhds_one' hmul hinv hleft fun x₀ => ?_
  replace hconj : ∀ x₀ : G, map (x₀ * · * x₀⁻¹) (𝓝 1) = 𝓝 1 :=
    fun x₀ => map_eq_of_inverse (x₀⁻¹ * · * x₀⁻¹x₀⁻¹⁻¹) (by ext; simp [mul_assoc]) (hconj _) (hconj _)
  rw [← hconj x₀]
  simpa [Function.comp_def] using hleft _

Sufficient Conditions for Topological Group via Continuity at Identity

Informal description

Let $G$ be a group equipped with a topology. If the following conditions hold: 1. The multiplication operation $(x,y) \mapsto x \cdot y$ is continuous at $(1,1)$, 2. The inversion map $x \mapsto x^{-1}$ is continuous at $1$, 3. For every $x_0 \in G$, the neighborhood filter of $x_0$ equals the image of the neighborhood filter of $1$ under left multiplication by $x_0$, 4. For every $x_0 \in G$, the conjugation map $x \mapsto x_0 \cdot x \cdot x_0^{-1}$ is continuous at $1$, then $G$ is a topological group (i.e., multiplication and inversion are globally continuous).

IsTopologicalGroup.of_comm_of_nhds_one theorem

 {G : Type u} [CommGroup G] [TopologicalSpace G] (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
  (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1)) (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1)) : IsTopologicalGroup G

Full source

@[to_additive]
theorem IsTopologicalGroup.of_comm_of_nhds_one {G : Type u} [CommGroup G] [TopologicalSpace G]
    (hmul : Tendsto (uncurry ((· * ·) : G → G → G)) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1))
    (hinv : Tendsto (fun x : G => x⁻¹) (𝓝 1) (𝓝 1))
    (hleft : ∀ x₀ : G, 𝓝 x₀ = map (x₀ * ·) (𝓝 1)) : IsTopologicalGroup G :=
  IsTopologicalGroup.of_nhds_one hmul hinv hleft (by simpa using tendsto_id)

Sufficient Conditions for Commutative Topological Group via Continuity at Identity

Informal description

Let $G$ be a commutative group equipped with a topology. If the following conditions hold: 1. The multiplication operation $(x,y) \mapsto x \cdot y$ is continuous at $(1,1)$, 2. The inversion map $x \mapsto x^{-1}$ is continuous at $1$, 3. For every $x_0 \in G$, the neighborhood filter of $x_0$ equals the image of the neighborhood filter of $1$ under left multiplication by $x_0$, then $G$ is a topological group (i.e., multiplication and inversion are globally continuous).

IsTopologicalGroup.exists_antitone_basis_nhds_one theorem

 [FirstCountableTopology G] : ∃ u : ℕ → Set G, (𝓝 1).HasAntitoneBasis u ∧ ∀ n, u (n + 1) * u (n + 1) ⊆ u n

Full source

/-- Any first countable topological group has an antitone neighborhood basis `u : ℕ → Set G` for
which `(u (n + 1)) ^ 2 ⊆ u n`. The existence of such a neighborhood basis is a key tool for
`QuotientGroup.completeSpace` -/
@[to_additive
  "Any first countable topological additive group has an antitone neighborhood basis
  `u : ℕ → set G` for which `u (n + 1) + u (n + 1) ⊆ u n`.
  The existence of such a neighborhood basis is a key tool for `QuotientAddGroup.completeSpace`"]
theorem IsTopologicalGroup.exists_antitone_basis_nhds_one [FirstCountableTopology G] :
    ∃ u : ℕ → Set G, (𝓝 1).HasAntitoneBasis u ∧ ∀ n, u (n + 1) * u (n + 1) ⊆ u n := by
  rcases (𝓝 (1 : G)).exists_antitone_basis with ⟨u, hu, u_anti⟩
  have :=
    ((hu.prod_nhds hu).tendsto_iff hu).mp
      (by simpa only [mul_one] using continuous_mul.tendsto ((1, 1) : G × G))
  simp only [and_self_iff, mem_prod, and_imp, Prod.forall, exists_true_left, Prod.exists,
    forall_true_left] at this
  have event_mul : ∀ n : ℕ, ∀ᶠ m in atTop, u m * u m ⊆ u n := by
    intro n
    rcases this n with ⟨j, k, -, h⟩
    refine atTop_basis.eventually_iff.mpr ⟨max j k, True.intro, fun m hm => ?_⟩
    rintro - ⟨a, ha, b, hb, rfl⟩
    exact h a b (u_anti ((le_max_left _ _).trans hm) ha) (u_anti ((le_max_right _ _).trans hm) hb)
  obtain ⟨φ, -, hφ, φ_anti_basis⟩ := HasAntitoneBasis.subbasis_with_rel ⟨hu, u_anti⟩ event_mul
  exact ⟨u ∘ φ, φ_anti_basis, fun n => hφ n.lt_succ_self⟩

Existence of Antitone Neighborhood Basis with Squaring Property in First-Countable Topological Groups

Informal description

Let $G$ be a first-countable topological group. Then there exists a decreasing sequence $(u_n)_{n \in \mathbb{N}}$ of neighborhoods of the identity element $1 \in G$ such that: 1. The sequence $(u_n)$ forms an antitone basis for the neighborhood filter of $1$. 2. For every $n \in \mathbb{N}$, the product set $u_{n+1} \cdot u_{n+1}$ is contained in $u_n$.

Filter.Tendsto.const_div' theorem

 (b : G) {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (𝓝 c)) : Tendsto (fun k : α => b / f k) l (𝓝 (b / c))

Full source

@[to_additive const_sub]
theorem Filter.Tendsto.const_div' (b : G) {c : G} {f : α → G} {l : Filter α}
    (h : Tendsto f l (𝓝 c)) : Tendsto (fun k : α => b / f k) l (𝓝 (b / c)) :=
  tendsto_const_nhds.div' h

Continuity of Constant Division in Topological Division Spaces

Informal description

Let $G$ be a topological space with a continuous division operation, and let $f : \alpha \to G$ be a function. If $f$ tends to $c \in G$ along a filter $l$ on $\alpha$, then for any fixed element $b \in G$, the function $k \mapsto b / f(k)$ tends to $b / c$ along $l$. In symbols: \[ f \underset{l}{\to} c \implies (k \mapsto b / f(k)) \underset{l}{\to} b / c \]

Filter.tendsto_const_div_iff theorem

 {G : Type*} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G] (b : G) {c : G} {f : α → G} {l : Filter α} :
  Tendsto (fun k : α ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c)

Full source

@[to_additive]
lemma Filter.tendsto_const_div_iff {G : Type*} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G]
    (b : G) {c : G} {f : α → G} {l : Filter α} :
    TendstoTendsto (fun k : α ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c) := by
  refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩
  convert h.const_div' b with k <;> rw [div_div_cancel]

Limit Characterization via Constant Division in Topological Groups

Informal description

Let $G$ be a commutative topological group with continuous division. For any fixed element $b \in G$ and any function $f : \alpha \to G$, the function $k \mapsto b / f(k)$ tends to $b / c$ along a filter $l$ if and only if $f$ tends to $c$ along $l$. In symbols: \[ \left(k \mapsto \frac{b}{f(k)}\right) \underset{l}{\to} \frac{b}{c} \iff f \underset{l}{\to} c \]

Filter.Tendsto.div_const' theorem

{c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (𝓝 c)) (b : G) : Tendsto (f · / b) l (𝓝 (c / b))

Full source

@[to_additive sub_const]
theorem Filter.Tendsto.div_const' {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (𝓝 c))
    (b : G) : Tendsto (f · / b) l (𝓝 (c / b)) :=
  h.div' tendsto_const_nhds

Limit of Function Divided by Constant in Topological Division Space

Informal description

Let $G$ be a topological space with a continuous division operation, and let $f : \alpha \to G$ be a function. If $f$ tends to $c \in G$ along a filter $l$ on $\alpha$, then for any $b \in G$, the function $x \mapsto f(x) / b$ tends to $c / b$ along $l$. In symbols: \[ f \underset{l}{\to} c \implies (x \mapsto f(x) / b) \underset{l}{\to} c / b \]

Filter.tendsto_div_const_iff theorem

 {G : Type*} [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G] {b : G} (hb : b ≠ 0) {c : G} {f : α → G}
  {l : Filter α} : Tendsto (f · / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Full source

lemma Filter.tendsto_div_const_iff {G : Type*}
    [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G]
    {b : G} (hb : b ≠ 0) {c : G} {f : α → G} {l : Filter α} :
    TendstoTendsto (f · / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c) := by
  refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩
  convert h.div_const' b⁻¹ with k <;> rw [div_div, mul_inv_cancel₀ hb, div_one]

Limit Characterization via Division by Nonzero Constant in Topological Group with Zero

Informal description

Let $G$ be a commutative group with zero equipped with a topological space structure and continuous division operation. For any nonzero element $b \in G$ and any $c \in G$, a function $f : \alpha \to G$ tends to $c$ along a filter $l$ on $\alpha$ if and only if the function $x \mapsto f(x) / b$ tends to $c / b$ along $l$. In symbols: \[ f \underset{l}{\to} c \iff (x \mapsto f(x) / b) \underset{l}{\to} c / b \]

Filter.tendsto_sub_const_iff theorem

 {G : Type*} [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G] (b : G) {c : G} {f : α → G} {l : Filter α} :
  Tendsto (f · - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c)

Full source

lemma Filter.tendsto_sub_const_iff {G : Type*}
    [AddCommGroup G] [TopologicalSpace G] [ContinuousSub G]
    (b : G) {c : G} {f : α → G} {l : Filter α} :
    TendstoTendsto (f · - b) l (𝓝 (c - b)) ↔ Tendsto f l (𝓝 c) := by
  refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.sub_const h b⟩
  convert h.sub_const (-b) with k <;> rw [sub_sub, ← sub_eq_add_neg, sub_self, sub_zero]

Limit of Shifted Function in Topological Additive Group

Informal description

Let $G$ be an additive commutative group with a topology and continuous subtraction operation. For any $b \in G$, a function $f : \alpha \to G$ tends to $c \in G$ along a filter $l$ on $\alpha$ if and only if the function $x \mapsto f(x) - b$ tends to $c - b$ along $l$. In symbols: \[ \lim_{l} (f(x) - b) = c - b \iff \lim_{l} f(x) = c \]

continuous_div_left' theorem

(a : G) : Continuous (a / ·)

Full source

@[to_additive (attr := continuity) continuous_sub_left]
lemma continuous_div_left' (a : G) : Continuous (a / ·) := continuous_const.div' continuous_id

Continuity of Left Division by a Fixed Element in a Topological Group

Informal description

For any element $a$ in a topological group $G$ with continuous division, the function $x \mapsto a / x$ is continuous.

continuous_div_right' theorem

(a : G) : Continuous (· / a)

Full source

@[to_additive (attr := continuity) continuous_sub_right]
lemma continuous_div_right' (a : G) : Continuous (· / a) := continuous_id.div' continuous_const

Continuity of Right Division in a Topological Group

Informal description

For any element $a$ in a topological group $G$, the right division map $x \mapsto x / a$ is continuous.

Homeomorph.divLeft definition

(x : G) : G ≃ₜ G

Full source

/-- A version of `Homeomorph.mulLeft a b⁻¹` that is defeq to `a / b`. -/
@[to_additive (attr := simps! +simpRhs)
  "A version of `Homeomorph.addLeft a (-b)` that is defeq to `a - b`."]
def Homeomorph.divLeft (x : G) : G ≃ₜ G :=
  { Equiv.divLeft x with
    continuous_toFun := continuous_const.div' continuous_id
    continuous_invFun := continuous_inv.mul continuous_const }

Homeomorphism of left division by an element in a topological group

Informal description

For an element $ x $ in a topological group $ G $, the homeomorphism $ \text{divLeft}_x : G \to G $ is defined by $ \text{divLeft}_x(y) = x / y $, with its inverse given by $ \text{invFun}_x(y) = y^{-1} * x $. This map is continuous in both directions, making it a homeomorphism.

isOpenMap_div_left theorem

(a : G) : IsOpenMap (a / ·)

Full source

@[to_additive]
theorem isOpenMap_div_left (a : G) : IsOpenMap (a / ·) :=
  (Homeomorph.divLeft _).isOpenMap

Left division is an open map in a topological group

Informal description

For any element $a$ in a topological group $G$, the left division map $x \mapsto a / x$ is an open map, i.e., it sends open subsets of $G$ to open subsets of $G$.

isClosedMap_div_left theorem

(a : G) : IsClosedMap (a / ·)

Full source

@[to_additive]
theorem isClosedMap_div_left (a : G) : IsClosedMap (a / ·) :=
  (Homeomorph.divLeft _).isClosedMap

Left division is a closed map in a topological group

Informal description

For any element $a$ in a topological group $G$, the left division map $x \mapsto a / x$ is a closed map, i.e., it sends closed subsets of $G$ to closed subsets of $G$.

Homeomorph.divRight definition

(x : G) : G ≃ₜ G

Full source

/-- A version of `Homeomorph.mulRight a⁻¹ b` that is defeq to `b / a`. -/
@[to_additive (attr := simps! +simpRhs)
  "A version of `Homeomorph.addRight (-a) b` that is defeq to `b - a`. "]
def Homeomorph.divRight (x : G) : G ≃ₜ G :=
  { Equiv.divRight x with
    continuous_toFun := continuous_id.div' continuous_const
    continuous_invFun := continuous_id.mul continuous_const }

Right division homeomorphism in a topological group

Informal description

For an element $x$ in a topological group $G$, the right division homeomorphism $\text{divRight}_x : G \to G$ is defined by $\text{divRight}_x(y) = y / x$, where $/$ denotes the group division operation. This is a homeomorphism (continuous bijection with continuous inverse) whose inverse is given by $\text{invFun}_x(y) = y * x$.

isOpenMap_div_right theorem

(a : G) : IsOpenMap (· / a)

Full source

@[to_additive]
lemma isOpenMap_div_right (a : G) : IsOpenMap (· / a) := (Homeomorph.divRight a).isOpenMap

Right division is an open map in a topological group

Informal description

For any element $a$ in a topological group $G$, the right division map $x \mapsto x / a$ is an open map, i.e., it maps open subsets of $G$ to open subsets of $G$.

isClosedMap_div_right theorem

(a : G) : IsClosedMap (· / a)

Full source

@[to_additive]
lemma isClosedMap_div_right (a : G) : IsClosedMap (· / a) := (Homeomorph.divRight a).isClosedMap

Right division is a closed map in a topological group

Informal description

For any element $a$ in a topological group $G$, the right division map $x \mapsto x / a$ is a closed map, i.e., it maps closed subsets of $G$ to closed subsets of $G$.

tendsto_div_nhds_one_iff theorem

{α : Type*} {l : Filter α} {x : G} {u : α → G} : Tendsto (u · / x) l (𝓝 1) ↔ Tendsto u l (𝓝 x)

Full source

@[to_additive]
theorem tendsto_div_nhds_one_iff {α : Type*} {l : Filter α} {x : G} {u : α → G} :
    TendstoTendsto (u · / x) l (𝓝 1) ↔ Tendsto u l (𝓝 x) :=
  haveI A : Tendsto (fun _ : α => x) l (𝓝 x) := tendsto_const_nhds
  ⟨fun h => by simpa using h.mul A, fun h => by simpa using h.div' A⟩

Limit Characterization via Division in Topological Groups: $\lim (u/x) = 1 \iff \lim u = x$

Informal description

For a topological group $G$, a filter $l$ on a type $\alpha$, a point $x \in G$, and a function $u : \alpha \to G$, the following are equivalent: 1. The function $y \mapsto u(y) / x$ tends to the identity element $1$ along the filter $l$. 2. The function $u$ tends to $x$ along the filter $l$. In symbols: \[ \lim_{l} (u(y) / x) = 1 \iff \lim_{l} u(y) = x \]

nhds_translation_div theorem

(x : G) : comap (· / x) (𝓝 1) = 𝓝 x

Full source

@[to_additive]
theorem nhds_translation_div (x : G) : comap (· / x) (𝓝 1) = 𝓝 x := by
  simpa only [div_eq_mul_inv] using nhds_translation_mul_inv x

Neighborhood Filter Translation via Right Division in Topological Groups

Informal description

For any element $x$ in a topological group $G$, the preimage of the neighborhood filter of the identity element $1$ under the right division map $y \mapsto y / x$ is equal to the neighborhood filter of $x$, i.e., $(y \mapsto y / x)^{-1}(\mathcal{N}_1) = \mathcal{N}_x$.

IsTopologicalGroup.t1Space theorem

(h : @IsClosed G _ { 1 }) : T1Space G

Full source

@[to_additive]
theorem IsTopologicalGroup.t1Space (h : @IsClosed G _ {1}) : T1Space G :=
  ⟨fun x => by simpa using isClosedMap_mul_right x _ h⟩

Closed Identity Implies $T_1$ Space in Topological Groups

Informal description

If the singleton set $\{1\}$ is closed in a topological group $G$, then $G$ is a $T_1$ space.

Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite theorem

(S : Subgroup G) (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S G

Full source

/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the left, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.) -/
@[to_additive
  "A subgroup `S` of an additive topological group `G` acts on `G` properly
  discontinuously on the left, if it is discrete in the sense that `S ∩ K` is finite for all compact
  `K`. (See also `DiscreteTopology`."]
theorem Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite (S : Subgroup G)
    (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S G :=
  { finite_disjoint_inter_image := by
      intro K L hK hL
      have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
      rw [preimage_compl, compl_compl] at H
      convert H
      ext x
      simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
      exact Set.smul_inter_ne_empty_iff' }

Properly Discontinuous Action of Cofinite-Tending Subgroups in Topological Groups

Informal description

Let $G$ be a topological group and $S$ a subgroup of $G$. If the inclusion map $S \hookrightarrow G$ tends to the cofinite filter along the cocompact filter (i.e., for every compact subset $K \subseteq G$, the intersection $S \cap K$ is finite), then $S$ acts on $G$ properly discontinuously via left multiplication.

Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite theorem

(S : Subgroup G) (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.op G

Full source

/-- A subgroup `S` of a topological group `G` acts on `G` properly discontinuously on the right, if
it is discrete in the sense that `S ∩ K` is finite for all compact `K`. (See also
`DiscreteTopology`.)

If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousSMul_of_t2Space`
to show that the quotient group `G ⧸ S` is Hausdorff. -/
@[to_additive
  "A subgroup `S` of an additive topological group `G` acts on `G` properly discontinuously
  on the right, if it is discrete in the sense that `S ∩ K` is finite for all compact `K`.
  (See also `DiscreteTopology`.)

  If `G` is Hausdorff, this can be combined with `t2Space_of_properlyDiscontinuousVAdd_of_t2Space`
  to show that the quotient group `G ⧸ S` is Hausdorff."]
theorem Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite (S : Subgroup G)
    (hS : Tendsto S.subtype cofinite (cocompact G)) : ProperlyDiscontinuousSMul S.op G :=
  { finite_disjoint_inter_image := by
      intro K L hK hL
      have : Continuous fun p : G × G => (p.1⁻¹, p.2) := continuous_inv.prodMap continuous_id
      have H : Set.Finite _ :=
        hS ((hK.prod hL).image (continuous_mul.comp this)).compl_mem_cocompact
      simp only [preimage_compl, compl_compl, coe_subtype, comp_apply] at H
      apply Finite.of_preimage _ (equivOp S).surjective
      convert H using 1
      ext x
      simp only [image_smul, mem_setOf_eq, coe_subtype, mem_preimage, mem_image, Prod.exists]
      exact Set.op_smul_inter_ne_empty_iff }

Properly Discontinuous Right Action of Cofinite Subgroups in Topological Groups

Informal description

Let $G$ be a topological group and $S$ a subgroup of $G$. If the inclusion map $S \hookrightarrow G$ tends to the cofinite filter along the cocompact filter (i.e., for every compact subset $K \subseteq G$, the set $\{s \in S \mid s \in K\}$ is finite), then the opposite group $S^\text{op}$ acts on $G$ properly discontinuously via right multiplication.

compact_open_separated_mul_right theorem

{K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), K * V ⊆ U

Full source

/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
  such that `K * V ⊆ U`. -/
@[to_additive
  "Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
  `0` such that `K + V ⊆ U`."]
theorem compact_open_separated_mul_right {K U : Set G} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), K * V ⊆ U := by
  refine hK.induction_on ?_ ?_ ?_ ?_
  · exact ⟨univ, by simp⟩
  · rintro s t hst ⟨V, hV, hV'⟩
    exact ⟨V, hV, (mul_subset_mul_right hst).trans hV'⟩
  · rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')
  · intro x hx
    have := tendsto_mul (show U ∈ 𝓝 (x * 1) by simpa using hU.mem_nhds (hKU hx))
    rw [nhds_prod_eq, mem_map, mem_prod_iff] at this
    rcases this with ⟨t, ht, s, hs, h⟩
    rw [← image_subset_iff, image_mul_prod] at h
    exact ⟨t, mem_nhdsWithin_of_mem_nhds ht, s, hs, h⟩

Existence of Identity Neighborhood for Compact-Open Separation in Topological Groups

Informal description

Let $G$ be a topological group, $K \subseteq G$ a compact subset, and $U \subseteq G$ an open subset containing $K$. Then there exists an open neighborhood $V$ of the identity element $1 \in G$ such that the product set $K \cdot V$ is contained in $U$.

compact_open_separated_mul_left theorem

{K U : Set G} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), V * K ⊆ U

Full source

/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of `1`
  such that `V * K ⊆ U`. -/
@[to_additive
  "Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
  `0` such that `V + K ⊆ U`."]
theorem compact_open_separated_mul_left {K U : Set G} (hK : IsCompact K) (hU : IsOpen U)
    (hKU : K ⊆ U) : ∃ V ∈ 𝓝 (1 : G), V * K ⊆ U := by
  rcases compact_open_separated_mul_right (hK.image continuous_op) (opHomeomorph.isOpenMap U hU)
      (image_subset op hKU) with
    ⟨V, hV : V ∈ 𝓝 (op (1 : G)), hV' : opop '' Kop '' K * V ⊆ op '' U⟩
  refine ⟨op ⁻¹' V, continuous_op.continuousAt hV, ?_⟩
  rwa [← image_preimage_eq V op_surjective, ← image_op_mul, image_subset_iff,
    preimage_image_eq _ op_injective] at hV'

Existence of Identity Neighborhood for Left-Sided Compact-Open Separation in Topological Groups

Informal description

Let $G$ be a topological group, $K \subseteq G$ a compact subset, and $U \subseteq G$ an open subset containing $K$. Then there exists an open neighborhood $V$ of the identity element $1 \in G$ such that the product set $V \cdot K$ is contained in $U$.

compact_covered_by_mul_left_translates theorem

{K V : Set G} (hK : IsCompact K) (hV : (interior V).Nonempty) : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (g * ·) ⁻¹' V

Full source

/-- A compact set is covered by finitely many left multiplicative translates of a set
  with non-empty interior. -/
@[to_additive
  "A compact set is covered by finitely many left additive translates of a set
    with non-empty interior."]
theorem compact_covered_by_mul_left_translates {K V : Set G} (hK : IsCompact K)
    (hV : (interior V).Nonempty) : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (g * ·) ⁻¹' V := by
  obtain ⟨t, ht⟩ : ∃ t : Finset G, K ⊆ ⋃ x ∈ t, interior ((x * ·) ⁻¹' V) := by
    refine
      hK.elim_finite_subcover (fun x => interior <| (x * ·) ⁻¹' V) (fun x => isOpen_interior) ?_
    obtain ⟨g₀, hg₀⟩ := hV
    refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩
    refine preimage_interior_subset_interior_preimage (continuous_const.mul continuous_id) ?_
    rwa [mem_preimage, Function.id_def, inv_mul_cancel_right]
  exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩

Finite Cover of Compact Set by Left Translates of a Set with Non-Empty Interior

Informal description

Let $G$ be a topological group, $K \subseteq G$ a compact subset, and $V \subseteq G$ a subset with non-empty interior. Then there exists a finite subset $t \subseteq G$ such that $K$ is covered by the left translates of $V$ by elements of $t$, i.e., $$ K \subseteq \bigcup_{g \in t} g^{-1} V. $$

SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace instance

[SeparableSpace G] [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G

Full source

/-- Every weakly locally compact separable topological group is σ-compact.
  Note: this is not true if we drop the topological group hypothesis. -/
@[to_additive SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace
  "Every weakly locally compact separable topological additive group is σ-compact.
  Note: this is not true if we drop the topological group hypothesis."]
instance (priority := 100) SeparableWeaklyLocallyCompactGroup.sigmaCompactSpace [SeparableSpace G]
    [WeaklyLocallyCompactSpace G] : SigmaCompactSpace G := by
  obtain ⟨L, hLc, hL1⟩ := exists_compact_mem_nhds (1 : G)
  refine ⟨⟨fun n => (fun x => x * denseSeq G n) ⁻¹' L, ?_, ?_⟩⟩
  · intro n
    exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc
  · refine iUnion_eq_univ_iff.2 fun x => ?_
    obtain ⟨_, ⟨n, rfl⟩, hn⟩ : (rangerange (denseSeq G) ∩ (fun y => x * y) ⁻¹' L).Nonempty := by
      rw [← (Homeomorph.mulLeft x).apply_symm_apply 1] at hL1
      exact (denseRange_denseSeq G).inter_nhds_nonempty
          ((Homeomorph.mulLeft x).continuous.continuousAt <| hL1)
    exact ⟨n, hn⟩

σ-Compactness of Separable Weakly Locally Compact Groups

Informal description

Every separable weakly locally compact topological group is σ-compact.

exists_disjoint_smul_of_isCompact theorem

[NoncompactSpace G] {K L : Set G} (hK : IsCompact K) (hL : IsCompact L) : ∃ g : G, Disjoint K (g • L)

Full source

/-- Given two compact sets in a noncompact topological group, there is a translate of the second
one that is disjoint from the first one. -/
@[to_additive
  "Given two compact sets in a noncompact additive topological group, there is a
  translate of the second one that is disjoint from the first one."]
theorem exists_disjoint_smul_of_isCompact [NoncompactSpace G] {K L : Set G} (hK : IsCompact K)
    (hL : IsCompact L) : ∃ g : G, Disjoint K (g • L) := by
  have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
  obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
    contrapose! A
    exact eq_univ_iff_forall.2 A
  refine ⟨g, ?_⟩
  refine disjoint_left.2 fun a ha h'a => hg ?_
  rcases h'a with ⟨b, bL, rfl⟩
  refine ⟨g * b, ha, b⁻¹, by simpa only [Set.mem_inv, inv_inv] using bL, ?_⟩
  simp only [smul_eq_mul, mul_inv_cancel_right]

Existence of Disjoint Translate for Compact Sets in Noncompact Topological Groups

Informal description

Let $G$ be a noncompact topological group, and let $K, L \subseteq G$ be compact subsets. Then there exists an element $g \in G$ such that $K$ and the left translate $g \cdot L$ are disjoint, i.e., $K \cap (g \cdot L) = \emptyset$.

nhds_mul theorem

(x y : G) : 𝓝 (x * y) = 𝓝 x * 𝓝 y

Full source

@[to_additive]
theorem nhds_mul (x y : G) : 𝓝 (x * y) = 𝓝 x * 𝓝 y :=
  calc
    𝓝 (x * y) = map (x * ·) (map (· * y) (𝓝 1 * 𝓝 1)) := by simp
    _ = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) := by rw [← map₂_mul, map_map₂, map_map₂]
    _ = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) := by simp only [mul_assoc]
    _ = 𝓝 x * 𝓝 y := by
      rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left,
        map₂_map_right]

Neighborhood Filter of Product Equals Product of Neighborhood Filters in Topological Groups

Informal description

For any elements $x$ and $y$ in a topological group $G$, the neighborhood filter of the product $x \cdot y$ is equal to the product of the neighborhood filters of $x$ and $y$, i.e., $\mathcal{N}_{x \cdot y} = \mathcal{N}_x * \mathcal{N}_y$.

nhdsMulHom definition

: G →ₙ* Filter G

Full source

/-- On a topological group, `𝓝 : G → Filter G` can be promoted to a `MulHom`. -/
@[to_additive (attr := simps)
  "On an additive topological group, `𝓝 : G → Filter G` can be promoted to an `AddHom`."]
def nhdsMulHom : G →ₙ* Filter G where
  toFun := 𝓝
  map_mul' _ _ := nhds_mul _ _

Neighborhood filter as a multiplicative homomorphism

Informal description

The function that maps each element $x$ of a topological group $G$ to its neighborhood filter $\mathcal{N}_x$ is a non-unital multiplicative homomorphism, meaning it preserves the group multiplication operation on filters, i.e., $\mathcal{N}_{x \cdot y} = \mathcal{N}_x * \mathcal{N}_y$ for all $x, y \in G$.

instIsTopologicalAddGroupAdditiveOfIsTopologicalGroup instance

{G} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] : IsTopologicalAddGroup (Additive G)

Full source

instance {G} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] :
    IsTopologicalAddGroup (Additive G) where
  continuous_neg := @continuous_inv G _ _ _

Additive Topological Group from Multiplicative Topological Group

Informal description

For any topological group $G$, the additive version of $G$ (where multiplication is reinterpreted as addition) forms an additive topological group. That is, the addition and negation operations on $\text{Additive}(G)$ are continuous with respect to the inherited topology from $G$.

instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup instance

{G} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] : IsTopologicalGroup (Multiplicative G)

Full source

instance {G} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] :
    IsTopologicalGroup (Multiplicative G) where
  continuous_inv := @continuous_neg G _ _ _

Topological Group Structure on Multiplicative Version of an Additive Topological Group

Informal description

For any additive topological group $G$, the multiplicative version of $G$ (where addition is reinterpreted as multiplication) forms a topological group. That is, the multiplication and inversion operations on $\text{Multiplicative}(G)$ are continuous with respect to the inherited topology from $G$.

toUnits_homeomorph definition

[Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ

Full source

/-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units. -/
@[to_additive "If `G` is an additive group with topological negation, then it is homeomorphic to
its additive units."]
def toUnits_homeomorph [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ where
  toEquiv := toUnits.toEquiv
  continuous_toFun := Units.continuous_iff.2 ⟨continuous_id, continuous_inv⟩
  continuous_invFun := Units.continuous_val

Homeomorphism between a group and its units under continuous inversion

Informal description

Given a group $ G $ with a topological space structure and continuous inversion operation, the map $ \text{toUnits} : G \to G^\times $ is a homeomorphism between $ G $ and its group of units $ G^\times $. Here, $ G^\times $ is equipped with the topology induced by the embedding $ G^\times \to G \times G $ that sends each unit to itself and its inverse.

Units.isEmbedding_val theorem

[Group G] [TopologicalSpace G] [ContinuousInv G] : IsEmbedding (val : Gˣ → G)

Full source

@[to_additive] theorem Units.isEmbedding_val [Group G] [TopologicalSpace G] [ContinuousInv G] :
    IsEmbedding (val : Gˣ → G) :=
  toUnits_homeomorph.symm.isEmbedding

Embedding of Units into a Topological Group with Continuous Inversion

Informal description

For a topological group $G$ with continuous inversion, the canonical inclusion map $\text{val} \colon G^\times \to G$ from the group of units $G^\times$ to $G$ is a topological embedding. That is, $\text{val}$ is injective and the topology on $G^\times$ is the coarsest topology that makes $\text{val}$ continuous.

Continuous.of_coeHom_comp theorem

 [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H] [ContinuousInv G] {f : G →* Hˣ}
  (hf : Continuous ((Units.coeHom H).comp f)) : Continuous f

Full source

lemma Continuous.of_coeHom_comp [Group G] [Monoid H] [TopologicalSpace G] [TopologicalSpace H]
    [ContinuousInv G] {f : G →* Hˣ} (hf : Continuous ((Units.coeHom H).comp f)) : Continuous f := by
  apply continuous_induced_rng.mpr ?_
  refine continuous_prodMk.mpr ⟨hf, ?_⟩
  simp_rw [← map_inv]
  exact MulOpposite.continuous_op.comp (hf.comp continuous_inv)

Continuity of Monoid Homomorphisms into Units via Composition with Inclusion

Informal description

Let $G$ be a topological group with continuous inversion, and let $H$ be a monoid with a topological space structure. Given a monoid homomorphism $f \colon G \to H^\times$ from $G$ to the group of units of $H$, if the composition of $f$ with the canonical inclusion $H^\times \to H$ is continuous, then $f$ itself is continuous.

Units.instIsTopologicalGroupOfContinuousMul instance

[ContinuousMul α] : IsTopologicalGroup αˣ

Full source

@[to_additive]
instance [ContinuousMul α] : IsTopologicalGroup αˣ where
  continuous_inv := Units.continuous_iff.2 <| ⟨continuous_coe_inv, continuous_val⟩

Topological Group Structure on the Group of Units

Informal description

For any topological monoid $\alpha$ with continuous multiplication, the group of units $\alpha^\times$ is a topological group. That is, the multiplication and inversion operations on $\alpha^\times$ are continuous with respect to the induced topology.

Homeomorph.prodUnits definition

: (α × β)ˣ ≃ₜ αˣ × βˣ

Full source

/-- The topological group isomorphism between the units of a product of two monoids, and the product
of the units of each monoid. -/
@[to_additive prodAddUnits
  "The topological group isomorphism between the additive units of a product of two
  additive monoids, and the product of the additive units of each additive monoid."]
def _root_.Homeomorph.prodUnits : (α × β)ˣ(α × β)ˣ ≃ₜ αˣ × βˣ where
  continuous_toFun :=
    (continuous_fst.units_map (MonoidHom.fst α β)).prodMk
      (continuous_snd.units_map (MonoidHom.snd α β))
  continuous_invFun :=
    Units.continuous_iff.2
      ⟨continuous_val.fst'.prodMk continuous_val.snd',
        continuous_coe_inv.fst'.prodMk continuous_coe_inv.snd'⟩
  toEquiv := MulEquiv.prodUnits.toEquiv

Homeomorphism between units of a product and product of units

Informal description

The homeomorphism between the group of units of the product monoid $\alpha \times \beta$ and the product of the groups of units of $\alpha$ and $\beta$. This is a topological group isomorphism that preserves both the group structure and the topological structure.

topologicalGroup_sInf theorem

{ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, @IsTopologicalGroup G t _) : @IsTopologicalGroup G (sInf ts) _

Full source

@[to_additive]
theorem topologicalGroup_sInf {ts : Set (TopologicalSpace G)}
    (h : ∀ t ∈ ts, @IsTopologicalGroup G t _) : @IsTopologicalGroup G (sInf ts) _ :=
  letI := sInf ts
  { toContinuousInv :=
      @continuousInv_sInf _ _ _ fun t ht => @IsTopologicalGroup.toContinuousInv G t _ <| h t ht
    toContinuousMul :=
      @continuousMul_sInf _ _ _ fun t ht =>
        @IsTopologicalGroup.toContinuousMul G t _ <| h t ht }

Infimum of Topological Group Topologies is a Topological Group

Informal description

Let $G$ be a group and let $\{t_i\}_{i \in I}$ be a collection of topologies on $G$. If for each topology $t_i$ in the collection, $G$ equipped with $t_i$ forms a topological group (i.e., multiplication and inversion are continuous), then $G$ equipped with the infimum topology $\bigsqcap \{t_i\}_{i \in I}$ also forms a topological group.

topologicalGroup_iInf theorem

 {ts' : ι → TopologicalSpace G} (h' : ∀ i, @IsTopologicalGroup G (ts' i) _) : @IsTopologicalGroup G (⨅ i, ts' i) _

Full source

@[to_additive]
theorem topologicalGroup_iInf {ts' : ι → TopologicalSpace G}
    (h' : ∀ i, @IsTopologicalGroup G (ts' i) _) : @IsTopologicalGroup G (⨅ i, ts' i) _ := by
  rw [← sInf_range]
  exact topologicalGroup_sInf (Set.forall_mem_range.mpr h')

Infimum of Family of Topological Group Topologies is a Topological Group

Informal description

Let $G$ be a group and let $\{t_i\}_{i \in \iota}$ be a family of topologies on $G$. If for each index $i \in \iota$, $G$ equipped with $t_i$ forms a topological group (i.e., multiplication and inversion are continuous), then $G$ equipped with the infimum topology $\bigsqcap_{i \in \iota} t_i$ also forms a topological group.

topologicalGroup_inf theorem

 {t₁ t₂ : TopologicalSpace G} (h₁ : @IsTopologicalGroup G t₁ _) (h₂ : @IsTopologicalGroup G t₂ _) :
  @IsTopologicalGroup G (t₁ ⊓ t₂) _

Full source

@[to_additive]
theorem topologicalGroup_inf {t₁ t₂ : TopologicalSpace G} (h₁ : @IsTopologicalGroup G t₁ _)
    (h₂ : @IsTopologicalGroup G t₂ _) : @IsTopologicalGroup G (t₁ ⊓ t₂) _ := by
  rw [inf_eq_iInf]
  refine topologicalGroup_iInf fun b => ?_
  cases b <;> assumption

Infimum of Two Topological Group Topologies is a Topological Group

Informal description

Let $G$ be a group equipped with two topologies $t_1$ and $t_2$. If $G$ is a topological group with respect to both $t_1$ and $t_2$, then $G$ is also a topological group with respect to the infimum topology $t_1 \sqcap t_2$.

Tags