Mathlib.Topology.Algebra.Group.GroupTopology

GroupTopology structure

(α : Type u) [Group α] : Type u
  extends TopologicalSpace α, IsTopologicalGroup α

Full source

/-- A group topology on a group `α` is a topology for which multiplication and inversion
are continuous. -/
structure GroupTopology (α : Type u) [Group α] : Type u
  extends TopologicalSpace α, IsTopologicalGroup α

Group Topology

Informal description

A group topology on a group $\alpha$ is a topology on $\alpha$ such that the group operations (multiplication and inversion) are continuous. More precisely, a group topology consists of: 1. A topological space structure on $\alpha$ 2. A proof that the multiplication map $\alpha \times \alpha \to \alpha$ and inversion map $\alpha \to \alpha$ are continuous

AddGroupTopology structure

(α : Type u) [AddGroup α] : Type u
  extends TopologicalSpace α, IsTopologicalAddGroup α

Full source

/-- An additive group topology on an additive group `α` is a topology for which addition and
negation are continuous. -/
structure AddGroupTopology (α : Type u) [AddGroup α] : Type u
  extends TopologicalSpace α, IsTopologicalAddGroup α

Additive Group Topology

Informal description

An additive group topology on an additive group $\alpha$ is a topology on $\alpha$ for which the addition operation $+ : \alpha \times \alpha \to \alpha$ and the negation operation $- : \alpha \to \alpha$ are continuous with respect to this topology.

GroupTopology.continuous_mul' theorem

 (g : GroupTopology α) :
  haveI := g.toTopologicalSpace
  Continuous fun p : α × α => p.1 * p.2

Full source

/-- A version of the global `continuous_mul` suitable for dot notation. -/
@[to_additive "A version of the global `continuous_add` suitable for dot notation."]
theorem continuous_mul' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous fun p : α × α => p.1 * p.2 := by
  letI := g.toTopologicalSpace
  haveI := g.toIsTopologicalGroup
  exact continuous_mul

Continuity of Multiplication in Group Topology

Informal description

For any group topology $g$ on a group $\alpha$, the multiplication operation $* \colon \alpha \times \alpha \to \alpha$ is continuous with respect to the topology induced by $g$.

GroupTopology.continuous_inv' theorem

 (g : GroupTopology α) :
  haveI := g.toTopologicalSpace
  Continuous (Inv.inv : α → α)

Full source

/-- A version of the global `continuous_inv` suitable for dot notation. -/
@[to_additive "A version of the global `continuous_neg` suitable for dot notation."]
theorem continuous_inv' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous (Inv.inv : α → α) := by
  letI := g.toTopologicalSpace
  haveI := g.toIsTopologicalGroup
  exact continuous_inv

Continuity of Inversion in Group Topology

Informal description

For any group topology $g$ on a group $\alpha$, the inversion operation $^{-1} \colon \alpha \to \alpha$ is continuous with respect to the topology induced by $g$.

GroupTopology.toTopologicalSpace_injective theorem

: Function.Injective (toTopologicalSpace : GroupTopology α → TopologicalSpace α)

Full source

@[to_additive]
theorem toTopologicalSpace_injective :
    Function.Injective (toTopologicalSpace : GroupTopology α → TopologicalSpace α) :=
  fun f g h => by
    cases f
    cases g
    congr

Injectivity of the Group Topology to Topological Space Map

Informal description

The map that associates to each group topology on $\alpha$ its underlying topological space structure is injective. In other words, if two group topologies on $\alpha$ induce the same topology, then they must be equal.

GroupTopology.ext' theorem

{f g : GroupTopology α} (h : f.IsOpen = g.IsOpen) : f = g

Full source

@[to_additive (attr := ext)]
theorem ext' {f g : GroupTopology α} (h : f.IsOpen = g.IsOpen) : f = g :=
  toTopologicalSpace_injective <| TopologicalSpace.ext h

Equality of Group Topologies via Open Sets

Informal description

For any two group topologies $f$ and $g$ on a group $\alpha$, if their collections of open sets are equal, then the group topologies are equal, i.e., $f = g$.

GroupTopology.instPartialOrder instance

: PartialOrder (GroupTopology α)

Full source

/-- The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s` is also open
in `t` (`t` is finer than `s`). -/
@[to_additive
  "The ordering on group topologies on the group `γ`. `t ≤ s` if every set open in `s`
  is also open in `t` (`t` is finer than `s`)."]
instance : PartialOrder (GroupTopology α) :=
  PartialOrder.lift toTopologicalSpace toTopologicalSpace_injective

Partial Order on Group Topologies by Fineness

Informal description

The collection of all group topologies on a group $\alpha$ forms a partial order under the relation of fineness. Specifically, for two group topologies $t$ and $s$ on $\alpha$, we say $t \leq s$ if every open set in $s$ is also open in $t$ (i.e., $t$ is finer than $s$).

GroupTopology.toTopologicalSpace_le theorem

{x y : GroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_le {x y : GroupTopology α} :
    x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y :=
  Iff.rfl

Equivalence of Fineness Between Group Topologies and Their Underlying Topological Spaces

Informal description

For any two group topologies $x$ and $y$ on a group $\alpha$, the underlying topological space of $x$ is finer than that of $y$ (i.e., $x.\text{toTopologicalSpace} \leq y.\text{toTopologicalSpace}$) if and only if $x$ is finer than $y$ in the partial order of group topologies (i.e., $x \leq y$).

GroupTopology.instTop instance

: Top (GroupTopology α)

Full source

@[to_additive]
instance : Top (GroupTopology α) :=
  let _t : TopologicalSpace α := ⊤
  ⟨{  continuous_mul := continuous_top
      continuous_inv := continuous_top }⟩

Indiscrete Topology as a Group Topology

Informal description

The indiscrete topology on a group $\alpha$ is a group topology, where the only open sets are the empty set and $\alpha$ itself.

GroupTopology.toTopologicalSpace_top theorem

: (⊤ : GroupTopology α).toTopologicalSpace = ⊤

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_top : (⊤ : GroupTopology α).toTopologicalSpace = ⊤ :=
  rfl

Indiscrete Group Topology Yields Indiscrete Topological Space

Informal description

The underlying topological space of the indiscrete group topology $\top$ on a group $\alpha$ is equal to the indiscrete topology $\top$ on $\alpha$.

GroupTopology.instBot instance

: Bot (GroupTopology α)

Full source

@[to_additive]
instance : Bot (GroupTopology α) :=
  let _t : TopologicalSpace α := ⊥
  ⟨{  continuous_mul := by
        haveI := discreteTopology_bot α
        fun_prop
      continuous_inv := continuous_bot }⟩

Discrete Topology as Bottom Element in Group Topologies

Informal description

For any group $\alpha$, the group topology structure on $\alpha$ has a bottom element $\bot$ which corresponds to the discrete topology (where every subset is open).

GroupTopology.toTopologicalSpace_bot theorem

: (⊥ : GroupTopology α).toTopologicalSpace = ⊥

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_bot : (⊥ : GroupTopology α).toTopologicalSpace = ⊥ :=
  rfl

Discrete Group Topology Yields Discrete Topological Space

Informal description

For any group $\alpha$ equipped with the discrete group topology $\bot$, the underlying topological space structure coincides with the discrete topology $\bot$ on $\alpha$.

GroupTopology.instBoundedOrder instance

: BoundedOrder (GroupTopology α)

Full source

@[to_additive]
instance : BoundedOrder (GroupTopology α) where
  top := ⊤
  le_top x := show x.toTopologicalSpace ≤ ⊤ from le_top
  bot := ⊥
  bot_le x := show ⊥ ≤ x.toTopologicalSpace from bot_le

Bounded Order of Group Topologies

Informal description

The collection of all group topologies on a group $\alpha$ forms a bounded order, where the discrete topology is the bottom element $\bot$ and the indiscrete topology is the top element $\top$.

GroupTopology.instMin instance

: Min (GroupTopology α)

Full source

@[to_additive]
instance : Min (GroupTopology α) where min x y := ⟨x.1 ⊓ y.1, topologicalGroup_inf x.2 y.2⟩

Minimum Operation on Group Topologies

Informal description

For any group $\alpha$ with a group topology, the collection of group topologies on $\alpha$ has a minimum operation.

GroupTopology.toTopologicalSpace_inf theorem

(x y : GroupTopology α) : (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_inf (x y : GroupTopology α) :
    (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace :=
  rfl

Infimum of Group Topologies Preserves Underlying Topological Space Structure

Informal description

For any two group topologies $x$ and $y$ on a group $\alpha$, the underlying topological space structure of their infimum $x \sqcap y$ is equal to the infimum of their underlying topological space structures. That is, $(x \sqcap y).\text{toTopologicalSpace} = x.\text{toTopologicalSpace} \sqcap y.\text{toTopologicalSpace}$.

GroupTopology.instSemilatticeInf instance

: SemilatticeInf (GroupTopology α)

Full source

@[to_additive]
instance : SemilatticeInf (GroupTopology α) :=
  toTopologicalSpace_injective.semilatticeInf _ toTopologicalSpace_inf

Meet-Semilattice Structure on Group Topologies

Informal description

For any group $\alpha$, the collection of group topologies on $\alpha$ forms a meet-semilattice under the reverse inclusion order. That is, for any two group topologies $x$ and $y$ on $\alpha$, their infimum $x \sqcap y$ exists and is the group topology whose underlying topological space is the infimum of the underlying topological spaces of $x$ and $y$.

GroupTopology.instInhabited instance

: Inhabited (GroupTopology α)

Full source

@[to_additive]
instance : Inhabited (GroupTopology α) :=
  ⟨⊤⟩

Nonempty Collection of Group Topologies

Informal description

For any group $\alpha$, the collection of group topologies on $\alpha$ is nonempty.

GroupTopology.instInfSet instance

: InfSet (GroupTopology α)

Full source

/-- Infimum of a collection of group topologies. -/
@[to_additive "Infimum of a collection of additive group topologies"]
instance : InfSet (GroupTopology α) where
  sInf S :=
    ⟨sInf (toTopologicalSpace '' S), topologicalGroup_sInf <| forall_mem_image.2 fun t _ => t.2⟩

Infimum Structure on Group Topologies

Informal description

For any group $\alpha$, the collection of group topologies on $\alpha$ forms an infimum structure, where the infimum of a set of group topologies is the group topology whose underlying topological space is the infimum of their underlying topological spaces.

GroupTopology.toTopologicalSpace_sInf theorem

(s : Set (GroupTopology α)) : (sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_sInf (s : Set (GroupTopology α)) :
    (sInf s).toTopologicalSpace = sInf (toTopologicalSpacetoTopologicalSpace '' s) := rfl

Infimum of Group Topologies Preserves Underlying Topology

Informal description

For any set $s$ of group topologies on a group $\alpha$, the underlying topological space of the infimum of $s$ is equal to the infimum of the underlying topological spaces of all group topologies in $s$.

GroupTopology.toTopologicalSpace_iInf theorem

{ι} (s : ι → GroupTopology α) : (⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace

Full source

@[to_additive (attr := simp)]
theorem toTopologicalSpace_iInf {ι} (s : ι → GroupTopology α) :
    (⨅ i, s i).toTopologicalSpace = ⨅ i, (s i).toTopologicalSpace :=
  congr_arg sInf (range_comp _ _).symm

Infimum of Group Topologies Preserves Underlying Topological Space

Informal description

For any family of group topologies $\{s_i\}_{i \in \iota}$ on a group $\alpha$, the underlying topological space of their infimum $\bigsqcap_i s_i$ is equal to the infimum of their underlying topological spaces $\bigsqcap_i (s_i.\text{toTopologicalSpace})$.

GroupTopology.instCompleteSemilatticeInf instance

: CompleteSemilatticeInf (GroupTopology α)

Full source

/-- Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and `⊤` the
indiscrete topology.

The infimum of a collection of group topologies is the topology generated by all their open sets
(which is a group topology).

The supremum of two group topologies `s` and `t` is the infimum of the family of all group
topologies contained in the intersection of `s` and `t`. -/
@[to_additive
  "Group topologies on `γ` form a complete lattice, with `⊥` the discrete topology and
  `⊤` the indiscrete topology.

  The infimum of a collection of group topologies is the topology generated by all their open sets
  (which is a group topology).

  The supremum of two group topologies `s` and `t` is the infimum of the family of all group
  topologies contained in the intersection of `s` and `t`."]
instance : CompleteSemilatticeInf (GroupTopology α) :=
  { inferInstanceAs (InfSet (GroupTopology α)),
    inferInstanceAs (PartialOrder (GroupTopology α)) with
    sInf_le := fun _ a haS => toTopologicalSpace_le.1 <| sInf_le ⟨a, haS, rfl⟩
    le_sInf := by
      intro S a hab
      apply (inferInstanceAs (CompleteLattice (TopologicalSpace α))).le_sInf
      rintro _ ⟨b, hbS, rfl⟩
      exact hab b hbS }

Complete Meet-Semilattice Structure on Group Topologies

Informal description

For any group $\alpha$, the collection of group topologies on $\alpha$ forms a complete meet-semilattice. In this lattice: - The infimum of a collection of group topologies is the topology generated by all their open sets (which is a group topology) - The bottom element $\bot$ is the discrete topology - The top element $\top$ is the indiscrete topology The ordering is given by reverse inclusion, where $t \leq s$ means $t$ is finer than $s$ (every open set in $s$ is open in $t$).

GroupTopology.instCompleteLattice instance

: CompleteLattice (GroupTopology α)

Full source

@[to_additive]
instance : CompleteLattice (GroupTopology α) :=
  { inferInstanceAs (BoundedOrder (GroupTopology α)),
    inferInstanceAs (SemilatticeInf (GroupTopology α)),
    completeLatticeOfCompleteSemilatticeInf _ with
    inf := (· ⊓ ·)
    top := ⊤
    bot := ⊥ }

Complete Lattice Structure on Group Topologies

Informal description

For any group $\alpha$, the collection of group topologies on $\alpha$ forms a complete lattice. In this lattice: - The ordering is given by reverse inclusion, where $t \leq s$ means $t$ is finer than $s$ (every open set in $s$ is open in $t$) - The infimum of a collection of group topologies is the topology generated by all their open sets - The supremum of a collection of group topologies is the infimum of all group topologies containing their union - The bottom element $\bot$ is the discrete topology - The top element $\top$ is the indiscrete topology

GroupTopology.coinduced definition

{α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) : GroupTopology β

Full source

/-- Given `f : α → β` and a topology on `α`, the coinduced group topology on `β` is the finest
topology such that `f` is continuous and `β` is a topological group. -/
@[to_additive
  "Given `f : α → β` and a topology on `α`, the coinduced additive group topology on `β`
  is the finest topology such that `f` is continuous and `β` is a topological additive group."]
def coinduced {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) : GroupTopology β :=
  sInf { b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace }

Coinduced group topology

Informal description

Given a function $ f : \alpha \to \beta $ between groups, where $ \alpha $ is equipped with a topological space structure $ t $, the *coinduced group topology* on $ \beta $ is the finest group topology such that $ f $ is continuous. More precisely, it is the infimum of all group topologies $ b $ on $ \beta $ for which the coinduced topology $ \text{TopologicalSpace.coinduced } f t $ is finer than $ b $ (i.e., $ \text{TopologicalSpace.coinduced } f t \leq b.\text{toTopologicalSpace} $).

GroupTopology.coinduced_continuous theorem

 {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) : Continuous[t, (coinduced f).toTopologicalSpace] f

Full source

@[to_additive]
theorem coinduced_continuous {α β : Type*} [t : TopologicalSpace α] [Group β] (f : α → β) :
    Continuous[t, (coinduced f).toTopologicalSpace] f := by
  rw [continuous_sInf_rng]
  rintro _ ⟨t', ht', rfl⟩
  exact continuous_iff_coinduced_le.2 ht'

Continuity of Functions under Coinduced Group Topology

Informal description

Let $\alpha$ and $\beta$ be groups, with $\alpha$ equipped with a topological space structure $t$. For any function $f \colon \alpha \to \beta$, the coinduced group topology on $\beta$ makes $f$ continuous. That is, $f$ is continuous when $\beta$ is given the topology $\text{coinduced}\, f\, t$.