Topological representations #

This file defines the category TopRep k G of topological representations of a monoid G over a topological ring k, and shows that it is equivalent to the category Action (TopModuleCat k) G.

source

structure TopRep (k : Type u) (G : Type v) [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

Type (max (max u v) (w + 1))

The category of topological representations of a monoid G over a topological ring k, and their morphisms.

V : Type w
the underlying type of an object in TopRep k G
hV1 : AddCommGroup ↑self
hV2 : Module k ↑self
hV3 : TopologicalSpace ↑self
hV4 : IsTopologicalAddGroup ↑self
hV5 : ContinuousSMul k ↑self
ρ : ContRepresentation k G ↑self
the underlying continuous representation of an object in TopRep k G

Instances For

source

@[implicit_reducible]

instance TopRep.instCoeSortType {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

CoeSort (TopRep k G) (Type w)

Equations

TopRep.instCoeSortType = { coe := TopRep.V }

source

@[reducible, inline]

abbrev TopRep.of {k : Type u} {G : Type v} {X : Type w} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] [AddCommGroup X] [Module k X] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul k X] (ρ : ContRepresentation k G X) :

TopRep k G

The object in the category of topological representations associated to a type equipped with a continuous representation. This is the preferred way to construct a term of TopRep k G.

Equations

TopRep.of ρ = { V := X, hV1 := inst✝⁴, hV2 := inst✝³, hV3 := inst✝², hV4 := inst✝¹, hV5 := inst✝, ρ := ρ }

Instances For

source

theorem TopRep.of_V {k : Type u} {G : Type v} (X : Type w) [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] [AddCommGroup X] [Module k X] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul k X] (ρ : ContRepresentation k G X) :

↑(of ρ) = X

source

theorem TopRep.of_ρ {k : Type u} {G : Type v} (X : Type w) [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] [AddCommGroup X] [Module k X] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul k X] (ρ : ContRepresentation k G X) :

(of ρ).ρ = ρ

source

structure TopRep.Hom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (A : TopRep k G) (B : TopRep k G) :

Type (max u_1 u_2)

The type of morphisms in TopRep k G.

hom' : ContIntertwiningMap A.ρ B.ρ
The underlying G-equivariant linear map.

Instances For

source

theorem TopRep.Hom.ext_iff {k : Type u} {G : Type v} {inst✝ : TopologicalSpace k} {inst✝¹ : Ring k} {inst✝² : IsTopologicalRing k} {inst✝³ : Monoid G} {A : TopRep k G} {B : TopRep k G} {x y : A.Hom B} :

x = y ↔ x.hom' = y.hom'

source

theorem TopRep.Hom.ext {k : Type u} {G : Type v} {inst✝ : TopologicalSpace k} {inst✝¹ : Ring k} {inst✝² : IsTopologicalRing k} {inst✝³ : Monoid G} {A : TopRep k G} {B : TopRep k G} {x y : A.Hom B} (hom' : x.hom' = y.hom') :

x = y

source

@[implicit_reducible]

instance TopRep.instCategory {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

CategoryTheory.Category.{w, max (max (w + 1) v) u} (TopRep k G)

Equations

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

source

@[implicit_reducible]

instance TopRep.instConcreteCategoryContIntertwiningMapVρ {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

CategoryTheory.ConcreteCategory (TopRep k G) fun (A B : TopRep k G) => ContIntertwiningMap A.ρ B.ρ

Equations

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

source

@[reducible, inline]

abbrev TopRep.Hom.hom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B : TopRep k G} (f : A.Hom B) :

ContIntertwiningMap A.ρ B.ρ

Turn a morphism in TopRep back into an IntertwiningMap.

Equations

f.hom = CategoryTheory.ConcreteCategory.hom f

Instances For

source

@[reducible, inline]

abbrev TopRep.ofHom {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] [AddCommGroup X] [Module k X] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul k X] [AddCommGroup Y] [Module k Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul k Y] {ρ : ContRepresentation k G X} {σ : ContRepresentation k G Y} (f : ContIntertwiningMap ρ σ) :

of ρ ⟶ of σ

Typecheck an IntertwiningMap as a morphism in TopRep.

Equations

TopRep.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

Instances For

source

@[simp]

theorem TopRep.hom_ofHom {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] [AddCommGroup X] [Module k X] [TopologicalSpace X] [IsTopologicalAddGroup X] [ContinuousSMul k X] [AddCommGroup Y] [Module k Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y] [ContinuousSMul k Y] {ρ : ContRepresentation k G X} {σ : ContRepresentation k G Y} (f : ContIntertwiningMap ρ σ) :

Hom.hom (ofHom f) = f

source

@[simp]

theorem TopRep.ofHom_hom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (A B : TopRep k G) (f : A ⟶ B) :

ofHom (Hom.hom f) = f

source

@[reducible, inline]

abbrev TopRep.Hom.toTopModuleCatHom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B : TopRep k G} (f : A.Hom B) :

TopModuleCat.of k ↑A ⟶ TopModuleCat.of k ↑B

The morphism of topological modules underlying a morphism in TopRep k G.

Equations

f.toTopModuleCatHom = TopModuleCat.ofHom f.hom.toContinuousLinearMap

Instances For

source

@[simp]

theorem TopRep.hom_id {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (A : TopRep k G) :

Hom.hom (CategoryTheory.CategoryStruct.id A) = ContIntertwiningMap.id

source

theorem TopRep.id_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (A : TopRep k G) (a : ↑A) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

source

@[simp]

theorem TopRep.hom_comp {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (A B C : TopRep k G) (f : A ⟶ B) (g : B ⟶ C) :

Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

source

theorem TopRep.comp_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B C : TopRep k G} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A) :

(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)

source

theorem TopRep.hom_ext {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B : TopRep k G} {f g : A ⟶ B} (hf : Hom.hom f = Hom.hom g) :

f = g

source

theorem TopRep.hom_ext_iff {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B : TopRep k G} {f g : A ⟶ B} :

f = g ↔ Hom.hom f = Hom.hom g

source

theorem TopRep.hom_comm_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] {A B : TopRep k G} (f : A ⟶ B) (g : G) (a : ↑A) :

(Hom.hom f) ((A.ρ g) a) = (B.ρ g) ((Hom.hom f) a)

source

def TopRep.toActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

CategoryTheory.Functor (TopRep k G) (Action (TopModuleCat k) G)

The functor sending a topological representation to the corresponding object in Action (TopModuleCat k) G.

Equations

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

Instances For

source

def TopRep.fromActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

CategoryTheory.Functor (Action (TopModuleCat k) G) (TopRep k G)

The functor sending an object in Action (TopModuleCat k) G to the corresponding topological representation.

Equations

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

Instances For

source

def TopRep.toActionFromAction {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (X : TopRep k G) :

fromActionTopModFunc.obj (toActionTopModFunc.obj X) ≅ X

The unit isomorphism of the equivalence TopRepIsoActionTop.

Equations

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

Instances For

source

def TopRep.fromActionToAction {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] (X : Action (TopModuleCat k) G) :

toActionTopModFunc.obj (fromActionTopModFunc.obj X) ≅ X

The counit isomorphism of the equivalence TopRepIsoActionTop.

Equations

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

Instances For

source

def TopRep.TopRepEquivActionTop {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

TopRep k G ≌ Action (TopModuleCat k) G

The equivalence of categories between TopRep k G and Action (TopModuleCat k) G.

Equations

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

Instances For

source

instance TopRep.instIsEquivalenceActionTopModuleCatToActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

toActionTopModFunc.IsEquivalence

source

instance TopRep.instIsEquivalenceActionTopModuleCatFromActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [IsTopologicalRing k] [Monoid G] :

fromActionTopModFunc.IsEquivalence

Documentation

Mathlib.RepresentationTheory.Continuous.TopRep

Topological representations #