ProCGroups.TopologicalGroups

Structure TopGrp GitHub

structure TopGrp where
  carrier : Type u

Bundled topological groups with continuous homomorphisms.

Instance TopGrp.instCoeSort GitHub

instance instCoeSort : CoeSort TopGrp (Type u) where
  coe G := G.carrier

The category object coerces to its underlying type.

Abbreviation TopGrp.of GitHub

abbrev of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : TopGrp where
  carrier := G

Bundle an unbundled topological group.

Structure TopGrp.Hom GitHub

structure Hom (G H : TopGrp.{u}) where
  hom' : G →ₜ* H

Morphisms of topological groups are continuous homomorphisms.

Instance TopGrp.instCategory GitHub

instance instCategory : Category TopGrp where
  Hom G H := Hom G H
  id G := ⟨ContinuousMonoidHom.id G⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

Topological groups form a category.

Instance TopGrp.instConcreteCategory GitHub

instance instConcreteCategory : ConcreteCategory TopGrp (fun G H => G →ₜ* H) where
  hom f := f.hom'
  ofHom f := ⟨f⟩

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

Abbreviation TopGrp.Hom.hom GitHub

abbrev Hom.hom {G H : TopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
  ConcreteCategory.hom (C := TopGrp) f

The underlying continuous homomorphism of a morphism.

Instance TopGrp.instCoeFunHom GitHub

instance instCoeFunHom {G H : TopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
  coe f := f.hom

A morphism coerces to its underlying continuous homomorphism.

Theorem TopGrp.hom_id GitHub

@[simp] theorem hom_id {G : TopGrp.{u}} :
    (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G

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

Show proof

Theorem TopGrp.hom_comp GitHub

@[simp] theorem hom_comp {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
    (f ≫ g).hom = g.hom.comp f.hom

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

Show proof

Theorem TopGrp.comp_apply GitHub

@[simp] theorem comp_apply {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
    (f ≫ g) x = g (f x)

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

Show proof

Theorem TopGrp.hom_ext GitHub

@[ext] theorem hom_ext {G H : TopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
    f = g

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

Show proof

Abbreviation TopGrp.ofHom GitHub

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 :=
  ConcreteCategory.ofHom f

Bundle a continuous homomorphism as a topological-group morphism.

Structure CommTopGrp GitHub

structure CommTopGrp where
  carrier : Type u

Bundled commutative topological groups with continuous homomorphisms.

Instance CommTopGrp.instCoeSort GitHub

instance instCoeSort : CoeSort CommTopGrp (Type u) where
  coe G := G.carrier

The category object coerces to its underlying type.

Abbreviation CommTopGrp.of GitHub

abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] :
    CommTopGrp where
  carrier := G

Bundle an unbundled commutative topological group.

Structure CommTopGrp.Hom GitHub

structure Hom (G H : CommTopGrp.{u}) where
  hom' : G →ₜ* H

Morphisms of commutative topological groups are continuous homomorphisms.

Instance CommTopGrp.instCategory GitHub

instance instCategory : Category CommTopGrp where
  Hom G H := Hom G H
  id G := ⟨ContinuousMonoidHom.id G⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

Commutative topological groups form a category.

Instance CommTopGrp.instConcreteCategory GitHub

instance instConcreteCategory : ConcreteCategory CommTopGrp (fun G H => G →ₜ* H) where
  hom f := f.hom'
  ofHom f := ⟨f⟩

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

Abbreviation CommTopGrp.Hom.hom GitHub

abbrev Hom.hom {G H : CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
  ConcreteCategory.hom (C := CommTopGrp) f

The underlying continuous homomorphism of a morphism.

Instance CommTopGrp.instCoeFunHom GitHub

instance instCoeFunHom {G H : CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
  coe f := f.hom

A morphism coerces to its underlying continuous homomorphism.

Theorem CommTopGrp.hom_id GitHub

@[simp] theorem hom_id {G : CommTopGrp.{u}} :
    (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G

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

Show proof

Theorem CommTopGrp.hom_comp GitHub

@[simp] theorem hom_comp {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
    (f ≫ g).hom = g.hom.comp f.hom

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

Show proof

Theorem CommTopGrp.comp_apply GitHub

@[simp] theorem comp_apply {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
    (f ≫ g) x = g (f x)

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

Show proof

Theorem CommTopGrp.hom_ext GitHub

@[ext] theorem hom_ext {G H : CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
    f = g

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

Show proof

Abbreviation CommTopGrp.ofHom GitHub

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 :=
  ConcreteCategory.ofHom f

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

Definition commTopGrpForgetToTopGrp GitHub

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

Forget the commutativity of a bundled commutative topological group.

Declarations