NYLL
Module

TopologicalGroups.lean

Nyll.ProCGroups.TopologicalGroups
27 declarations indexed from sourceView source ↗

Module documentation

Pro C Groups / Topological Groups

This module formalizes basic topological-group constructions used by the pro-\(C\) library.

Imports2
  • Mathlib.CategoryTheory.ConcreteCategory.Basic
  • Mathlib.Topology.Algebra.ContinuousMonoidHom
Imported by4

Declarations

structure

TopGrp

L25 ↗
ProCGroups.TopGrp
Documentation

Bundled topological groups with continuous homomorphisms.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
Lean source · full declaration
structure TopGrp where
  /-- The underlying type of the topological group. -/
  carrier : Type u
  /-- The group structure on the carrier. -/
  [group : Group carrier]
  /-- The topology on the carrier. -/
  [topologicalSpace : TopologicalSpace carrier]
  /-- Multiplication and inversion are continuous for the stored topology. -/
  [isTopologicalGroup : IsTopologicalGroup carrier]
instance

instCoeSort

L40 ↗
ProCGroups.TopGrp.instCoeSort
Documentation

The category object coerces to its underlying type.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
instance instCoeSort : CoeSort TopGrp (Type u) where
  coe G := G.carrier
abbrev

of

L44 ↗
ProCGroups.TopGrp.of
Documentation

Bundle an unbundled topological group.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
abbrev of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : TopGrp where
  carrier := G
structure

Hom

L49 ↗
ProCGroups.TopGrp.Hom
Documentation

Morphisms of topological groups are continuous homomorphisms.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
structure Hom (G H : TopGrp.{u}) where
  /-- The continuous group homomorphism underlying the bundled morphism. -/
  hom' : G →ₜ* H
instance

instCategory

L54 ↗
ProCGroups.TopGrp.instCategory
Documentation

Topological groups form a category.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
instance instCategory : Category TopGrp where
  Hom G H := Hom G H
  id G := ⟨ContinuousMonoidHom.id G⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩
instance

instConcreteCategory

L63 ↗
ProCGroups.TopGrp.instConcreteCategory
Documentation

The category of topological groups has the concrete category structure inherited from its underlying type.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
instance instConcreteCategory : ConcreteCategory TopGrp (fun G H => G →ₜ* H) where
  hom f := f.hom'
  ofHom f := ⟨f⟩
abbrev

hom

L68 ↗
ProCGroups.TopGrp.Hom.hom
Documentation

The underlying continuous homomorphism of a morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
abbrev Hom.hom {G H : TopGrp.{u}} (f : G ⟶ H) : G →ₜ* H
instance

instCoeFunHom

L72 ↗
ProCGroups.TopGrp.instCoeFunHom
Documentation

A morphism coerces to its underlying continuous homomorphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · full declaration
instance instCoeFunHom {G H : TopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
  coe f := f.hom
theorem

hom_id

L76 ↗
ProCGroups.TopGrp.hom_id
Documentation

The underlying homomorphism of the identity morphism is the identity continuous homomorphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
theorem hom_id {G : TopGrp.{u}} :
    (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G
theorem

hom_comp

L81 ↗
ProCGroups.TopGrp.hom_comp
Documentation

The underlying homomorphism of a composite is the composite of underlying homomorphisms.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
theorem hom_comp {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
    (f ≫ g).hom = g.hom.comp f.hom
theorem

comp_apply

L89 ↗
ProCGroups.TopGrp.comp_apply
Documentation

The composite map is computed pointwise by applying the constituent coordinate formulas in succession.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
theorem comp_apply {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
    (f ≫ g) x = g (f x)
theorem

hom_ext

L94 ↗
ProCGroups.TopGrp.hom_ext
Documentation

Morphisms in TopGrp are equal when their underlying continuous homomorphisms are equal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
theorem hom_ext {G H : TopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
    f = g
abbrev

ofHom

L99 ↗
ProCGroups.TopGrp.ofHom
Documentation

Bundle a continuous homomorphism as a topological-group morphism.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
namespace TopGrp
Lean source · statement
abbrev ofHom {G H : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →ₜ* H) : of G ⟶ of H
structure

CommTopGrp

L109 ↗
ProCGroups.CommTopGrp
Documentation

Bundled commutative topological groups with continuous homomorphisms.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
Lean source · full declaration
structure CommTopGrp where
  /-- The underlying type of the commutative topological group. -/
  carrier : Type u
  /-- The commutative group structure on the carrier. -/
  [commGroup : CommGroup carrier]
  /-- The topology on the carrier. -/
  [topologicalSpace : TopologicalSpace carrier]
  /-- Multiplication and inversion are continuous for the stored topology. -/
  [isTopologicalGroup : IsTopologicalGroup carrier]
instance

instCoeSort

L125 ↗
ProCGroups.CommTopGrp.instCoeSort
Documentation

The category object coerces to its underlying type.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
instance instCoeSort : CoeSort CommTopGrp (Type u) where
  coe G := G.carrier
abbrev

of

L129 ↗
ProCGroups.CommTopGrp.of
Documentation

Bundle an unbundled commutative topological group.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] :
    CommTopGrp where
  carrier := G
structure

Hom

L135 ↗
ProCGroups.CommTopGrp.Hom
Documentation

Morphisms of commutative topological groups are continuous homomorphisms.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
structure Hom (G H : CommTopGrp.{u}) where
  /-- The continuous homomorphism underlying the bundled morphism. -/
  hom' : G →ₜ* H
instance

instCategory

L140 ↗
ProCGroups.CommTopGrp.instCategory
Documentation

Commutative topological groups form a category.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
instance instCategory : Category CommTopGrp where
  Hom G H := Hom G H
  id G := ⟨ContinuousMonoidHom.id G⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩
instance

instConcreteCategory

L149 ↗
ProCGroups.CommTopGrp.instConcreteCategory
Documentation

The category of commutative topological groups has the concrete category structure inherited from its underlying type.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
instance instConcreteCategory : ConcreteCategory CommTopGrp (fun G H => G →ₜ* H) where
  hom f := f.hom'
  ofHom f := ⟨f⟩
abbrev

hom

L154 ↗
ProCGroups.CommTopGrp.Hom.hom
Documentation

The underlying continuous homomorphism of a morphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
abbrev Hom.hom {G H : CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H
instance

instCoeFunHom

L158 ↗
ProCGroups.CommTopGrp.instCoeFunHom
Documentation

A morphism coerces to its underlying continuous homomorphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · full declaration
instance instCoeFunHom {G H : CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
  coe f := f.hom
theorem

hom_id

L162 ↗
ProCGroups.CommTopGrp.hom_id
Documentation

The underlying homomorphism of the identity morphism is the identity continuous homomorphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
theorem hom_id {G : CommTopGrp.{u}} :
    (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G
theorem

hom_comp

L167 ↗
ProCGroups.CommTopGrp.hom_comp
Documentation

The underlying homomorphism of a composite is the composite of underlying homomorphisms.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
theorem hom_comp {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
    (f ≫ g).hom = g.hom.comp f.hom
theorem

comp_apply

L175 ↗
ProCGroups.CommTopGrp.comp_apply
Documentation

The composite map is computed pointwise by applying the constituent coordinate formulas in succession.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
theorem comp_apply {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
    (f ≫ g) x = g (f x)
theorem

hom_ext

L180 ↗
ProCGroups.CommTopGrp.hom_ext
Documentation

Morphisms in CommTopGrp are equal when their underlying continuous homomorphisms are equal.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
theorem hom_ext {G H : CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
    f = g
abbrev

ofHom

L185 ↗
ProCGroups.CommTopGrp.ofHom
Documentation

Bundle a continuous homomorphism as a commutative topological-group morphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
namespace CommTopGrp
Lean source · statement
abbrev ofHom {G H : Type u}
    [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H]
    (f : G →ₜ* H) : of G ⟶ of H
def

commTopGrpForgetToTopGrp

L194 ↗
ProCGroups.commTopGrpForgetToTopGrp
Documentation

Forget the commutativity of a bundled commutative topological group.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory
open scoped Topology
universe u
namespace ProCGroups
attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
  CommTopGrp.isTopologicalGroup
Lean source · full declaration
def commTopGrpForgetToTopGrp : CommTopGrp.{u} ⥤ TopGrp.{u} where
  obj G := TopGrp.of G
  map f := TopGrp.ofHom f.hom
  map_id G := by
    apply TopGrp.hom_ext
    rfl
  map_comp f g := by
    apply TopGrp.hom_ext
    rfl

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.