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.

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⁻¹

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

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.

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.

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

A version of the global continuous_inv suitable for dot notation.

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

A version of the global continuous_neg suitable for dot notation.

theorem GroupTopology.toTopologicalSpace_injective {α : Type u} [Group α] : Function.Injective toTopologicalSpace

theorem AddGroupTopology.toTopologicalSpace_injective {α : Type u} [AddGroup α] : Function.Injective toTopologicalSpace

theorem AddGroupTopology.ext' {α : Type u} [AddGroup α] {f g : AddGroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) : f = g

theorem GroupTopology.ext' {α : Type u} [Group α] {f g : GroupTopology α} (h : TopologicalSpace.IsOpen = TopologicalSpace.IsOpen) : f = g

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 ⋯

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 ⋯

@[simp]

theorem GroupTopology.toTopologicalSpace_le {α : Type u} [Group α] {x y : GroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

@[simp]

theorem AddGroupTopology.toTopologicalSpace_le {α : Type u} [AddGroup α] {x y : AddGroupTopology α} : x.toTopologicalSpace ≤ y.toTopologicalSpace ↔ x ≤ y

instance GroupTopology.instTop {α : Type u} [Group α] : Top (GroupTopology α)

Equations

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

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

Equations

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

@[simp]

theorem GroupTopology.toTopologicalSpace_top {α : Type u} [Group α] : ⊤.toTopologicalSpace = ⊤

@[simp]

theorem AddGroupTopology.toTopologicalSpace_top {α : Type u} [AddGroup α] : ⊤.toTopologicalSpace = ⊤

instance GroupTopology.instBot {α : Type u} [Group α] : Bot (GroupTopology α)

Equations

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

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

Equations

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

@[simp]

theorem GroupTopology.toTopologicalSpace_bot {α : Type u} [Group α] : ⊥.toTopologicalSpace = ⊥

@[simp]

theorem AddGroupTopology.toTopologicalSpace_bot {α : Type u} [AddGroup α] : ⊥.toTopologicalSpace = ⊥

instance GroupTopology.instBoundedOrder {α : Type u} [Group α] : BoundedOrder (GroupTopology α)

Equations

• GroupTopology.instBoundedOrder = BoundedOrder.mk

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

Equations

• AddGroupTopology.instBoundedOrder = BoundedOrder.mk

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

Equations

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

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

Equations

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

@[simp]

theorem GroupTopology.toTopologicalSpace_inf {α : Type u} [Group α] (x y : GroupTopology α) : (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

@[simp]

theorem AddGroupTopology.toTopologicalSpace_inf {α : Type u} [AddGroup α] (x y : AddGroupTopology α) : (x ⊓ y).toTopologicalSpace = x.toTopologicalSpace ⊓ y.toTopologicalSpace

instance GroupTopology.instSemilatticeInf {α : Type u} [Group α] : SemilatticeInf (GroupTopology α)

Equations

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

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

Equations

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

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

Equations

• GroupTopology.instInhabited = { default := ⊤ }

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

Equations

• AddGroupTopology.instInhabited = { default := ⊤ }

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

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

@[simp]

theorem GroupTopology.toTopologicalSpace_sInf {α : Type u} [Group α] (s : Set (GroupTopology α)) : (sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)

@[simp]

theorem AddGroupTopology.toTopologicalSpace_sInf {α : Type u} [AddGroup α] (s : Set (AddGroupTopology α)) : (sInf s).toTopologicalSpace = sInf (toTopologicalSpace '' s)

@[simp]

theorem GroupTopology.toTopologicalSpace_iInf {α : Type u} [Group α] {ι : Sort u_1} (s : ι → GroupTopology α) : (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace

@[simp]

theorem AddGroupTopology.toTopologicalSpace_iInf {α : Type u} [AddGroup α] {ι : Sort u_1} (s : ι → AddGroupTopology α) : (⨅ (i : ι), s i).toTopologicalSpace = ⨅ (i : ι), (s i).toTopologicalSpace

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

• GroupTopology.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

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

• AddGroupTopology.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

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

Equations

• GroupTopology.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• AddGroupTopology.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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}

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}

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

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