### Lattice of group topologies #

We define a type class `GroupTopology α` which endows a group `α` with a topology such that all group operations are continuous.

Group topologies on a fixed group `α` are ordered, by reverse inclusion. They form a complete lattice, with `⊥` the discrete topology and `⊤` the indiscrete topology.

Any function `f : α → β` induces `coinduced f : TopologicalSpace α → GroupTopology β`.

The additive version `AddGroupTopology α` and corresponding results are provided as well.

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

A group topology on a group `α` is a topology for which multiplication and inversion are continuous.

- IsOpen : Set α → Prop
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
- continuous_mul : Continuous fun (p : α × α) => p.1 * p.2
- continuous_inv : Continuous fun (a : α) => a⁻¹

Instances For

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

An additive group topology on an additive group `α` is a topology for which addition and negation are continuous.

- IsOpen : Set α → Prop
- isOpen_univ : TopologicalSpace.IsOpen Set.univ
- isOpen_inter (s t : Set α) : TopologicalSpace.IsOpen s → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s ∩ t)
- isOpen_sUnion (s : Set (Set α)) : (∀ t ∈ s, TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s)
- continuous_add : Continuous fun (p : α × α) => p.1 + p.2
- continuous_neg : Continuous fun (a : α) => -a

Instances For

source
theorem GroupTopology.continuous_mul' {α : Type u} [Group α] (g : GroupTopology α) :
Continuous fun (p : α × α) => p.1 * p.2

A version of the global `continuous_mul` suitable for dot notation.

source
theorem AddGroupTopology.continuous_add' {α : Type u} [AddGroup α] (g : AddGroupTopology α) :
Continuous fun (p : α × α) => p.1 + p.2

A version of the global `continuous_add` suitable for dot notation.

source
theorem GroupTopology.continuous_inv' {α : Type u} [Group α] (g : GroupTopology α) :
Continuous Inv.inv

A version of the global `continuous_inv` suitable for dot notation.

source
theorem AddGroupTopology.continuous_neg' {α : Type u} [AddGroup α] (g : AddGroupTopology α) :
Continuous Neg.neg

A version of the global `continuous_neg` suitable for dot notation.

source
theorem GroupTopology.toTopologicalSpace_injective {α : Type u} [Group α] :
Function.Injective toTopologicalSpace
source
theorem AddGroupTopology.toTopologicalSpace_injective {α : Type u} [AddGroup α] :
Function.Injective toTopologicalSpace
source
theorem GroupTopology.ext' {α : Type u} [Group α] {f g : GroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
f = g
source
theorem AddGroupTopology.ext' {α : Type u} [AddGroup α] {f g : AddGroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) :
f = g
source
theorem AddGroupTopology.ext'_iff {α : Type u} [AddGroup α] {f g : AddGroupTopology α} :
f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
source
theorem GroupTopology.ext'_iff {α : Type u} [Group α] {f g : GroupTopology α} :
f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
source
instance GroupTopology.instPartialOrder {α : Type u} [Group α] :
PartialOrder (GroupTopology α)

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`).

Equations

- GroupTopology.instPartialOrder = PartialOrder.lift GroupTopology.toTopologicalSpace ⋯

source
instance AddGroupTopology.instPartialOrder {α : Type u} [AddGroup α] :
PartialOrder (AddGroupTopology α)

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`).

Equations

- AddGroupTopology.instPartialOrder = PartialOrder.lift AddGroupTopology.toTopologicalSpace ⋯

source
@[simp]
theorem GroupTopology.toTopologicalSpace_le {α : Type u} [Group α] {x y : GroupTopology α} :
x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_le {α : Type u} [AddGroup α] {x y : AddGroupTopology α} :
x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y
source
instance GroupTopology.instTop {α : Type u} [Group α] :
Top (GroupTopology α)
Equations

- GroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toIsTopologicalGroup := ⋯ } }

source
instance AddGroupTopology.instTop {α : Type u} [AddGroup α] :
Top (AddGroupTopology α)
Equations

- AddGroupTopology.instTop = { top := { toTopologicalSpace := ⊤, toIsTopologicalAddGroup := ⋯ } }

source
@[simp]
theorem GroupTopology.toTopologicalSpace_top {α : Type u} [Group α] :
⊤.toTopologicalSpace = ⊤
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_top {α : Type u} [AddGroup α] :
⊤.toTopologicalSpace = ⊤
source
instance GroupTopology.instBot {α : Type u} [Group α] :
Bot (GroupTopology α)
Equations

- GroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toIsTopologicalGroup := ⋯ } }

source
instance AddGroupTopology.instBot {α : Type u} [AddGroup α] :
Bot (AddGroupTopology α)
Equations

- AddGroupTopology.instBot = { bot := { toTopologicalSpace := ⊥, toIsTopologicalAddGroup := ⋯ } }

source
@[simp]
theorem GroupTopology.toTopologicalSpace_bot {α : Type u} [Group α] :
⊥.toTopologicalSpace = ⊥
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_bot {α : Type u} [AddGroup α] :
⊥.toTopologicalSpace = ⊥
source
instance GroupTopology.instBoundedOrder {α : Type u} [Group α] :
BoundedOrder (GroupTopology α)
Equations

- GroupTopology.instBoundedOrder = { toTop := GroupTopology.instTop, le_top := ⋯, toBot := GroupTopology.instBot, bot_le := ⋯ }

source
instance AddGroupTopology.instBoundedOrder {α : Type u} [AddGroup α] :
BoundedOrder (AddGroupTopology α)
Equations

- AddGroupTopology.instBoundedOrder = { toTop := AddGroupTopology.instTop, le_top := ⋯, toBot := AddGroupTopology.instBot, bot_le := ⋯ }

source
instance GroupTopology.instMin {α : Type u} [Group α] :
Min (GroupTopology α)
Equations

- GroupTopology.instMin = { min := fun (x y : GroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toIsTopologicalGroup := ⋯ } }

source
instance AddGroupTopology.instMin {α : Type u} [AddGroup α] :
Min (AddGroupTopology α)
Equations

- AddGroupTopology.instMin = { min := fun (x y : AddGroupTopology α) => { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toIsTopologicalAddGroup := ⋯ } }

source
@[simp]
theorem GroupTopology.toTopologicalSpace_inf {α : Type u} [Group α] (x y : GroupTopology α) :
(x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_inf {α : Type u} [AddGroup α] (x y : AddGroupTopology α) :
(x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace
source
instance GroupTopology.instSemilatticeInf {α : Type u} [Group α] :
SemilatticeInf (GroupTopology α)
Equations

- GroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf GroupTopology.toTopologicalSpace ⋯ ⋯

source
instance AddGroupTopology.instSemilatticeInf {α : Type u} [AddGroup α] :
SemilatticeInf (AddGroupTopology α)
Equations

- AddGroupTopology.instSemilatticeInf = Function.Injective.semilatticeInf AddGroupTopology.toTopologicalSpace ⋯ ⋯

source
instance GroupTopology.instInhabited {α : Type u} [Group α] :
Inhabited (GroupTopology α)
Equations

- GroupTopology.instInhabited = { default := ⊤ }

source
instance AddGroupTopology.instInhabited {α : Type u} [AddGroup α] :
Inhabited (AddGroupTopology α)
Equations

- AddGroupTopology.instInhabited = { default := ⊤ }

source
instance GroupTopology.instInfSet {α : Type u} [Group α] :
InfSet (GroupTopology α)

Infimum of a collection of group topologies.

Equations

- GroupTopology.instInfSet = { sInf := fun (S : Set (GroupTopology α)) => { toTopologicalSpace := sInf (GroupTopology.toTopologicalSpace '' S), toIsTopologicalGroup := ⋯ } }

source
instance AddGroupTopology.instInfSet {α : Type u} [AddGroup α] :
InfSet (AddGroupTopology α)

Infimum of a collection of additive group topologies

Equations

- AddGroupTopology.instInfSet = { sInf := fun (S : Set (AddGroupTopology α)) => { toTopologicalSpace := sInf (AddGroupTopology.toTopologicalSpace '' S), toIsTopologicalAddGroup := ⋯ } }

source
@[simp]
theorem GroupTopology.toTopologicalSpace_sInf {α : Type u} [Group α] (s : Set (GroupTopology α)) :
(sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_sInf {α : Type u} [AddGroup α] (s : Set (AddGroupTopology α)) :
(sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)
source
@[simp]
theorem GroupTopology.toTopologicalSpace_iInf {α : Type u} [Group α] {ι : Sort u_1} (s : ι → GroupTopology α) :
(⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
source
@[simp]
theorem AddGroupTopology.toTopologicalSpace_iInf {α : Type u} [AddGroup α] {ι : Sort u_1} (s : ι → AddGroupTopology α) :
(⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace
source
instance GroupTopology.instCompleteSemilatticeInf {α : Type u} [Group α] :
CompleteSemilatticeInf (GroupTopology α)

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`.

Equations

- One or more equations did not get rendered due to their size.

source
instance AddGroupTopology.instCompleteSemilatticeInf {α : Type u} [AddGroup α] :
CompleteSemilatticeInf (AddGroupTopology α)

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`.

Equations

- One or more equations did not get rendered due to their size.

source
instance GroupTopology.instCompleteLattice {α : Type u} [Group α] :
CompleteLattice (GroupTopology α)
Equations

- One or more equations did not get rendered due to their size.

source
instance AddGroupTopology.instCompleteLattice {α : Type u} [AddGroup α] :
CompleteLattice (AddGroupTopology α)
Equations

- One or more equations did not get rendered due to their size.

source
def GroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : α → β) :
GroupTopology β

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.

Equations

- GroupTopology.coinduced f = sInf {b : GroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

Instances For

source
def AddGroupTopology.coinduced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : α → β) :
AddGroupTopology β

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.

Equations

- AddGroupTopology.coinduced f = sInf {b : AddGroupTopology β | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}

Instances For

source
theorem GroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [Group β] (f : α → β) :
Continuous f
source
theorem AddGroupTopology.coinduced_continuous {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [AddGroup β] (f : α → β) :
Continuous f