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.

For a topological group G we define the invariants functor TopRep.invariantsFunctor, the coinduction functor TopRep.coind₁Functor, the restriction functor TopRep.resFunctor along a group homomorphism φ : H →* G, and the morphism TopRep.invariantsResMap φ f between invariant submodules induced by a morphism f : res φ X ⟶ Y.

structure TopRep (k : Type u) (G : Type v) [Ring k] [TopologicalSpace 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

@[implicit_reducible]

instance TopRep.instCoeSortType {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] : CoeSort (TopRep k G) (Type w)

Equations

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

@[reducible, inline]

abbrev TopRep.of {k : Type u} {G : Type v} {X : Type w} [TopologicalSpace k] [Ring 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✝, ρ := ρ }

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

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

structure TopRep.Hom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

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

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

@[implicit_reducible]

instance TopRep.instCategory {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

@[implicit_reducible]

instance TopRep.instConcreteCategoryContIntertwiningMapVρ {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

@[reducible, inline]

abbrev TopRep.Hom.hom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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

@[reducible, inline]

abbrev TopRep.ofHom {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring 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

@[simp]

theorem TopRep.hom_ofHom {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring 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

@[simp]

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

@[reducible, inline]

abbrev TopRep.Hom.toTopModuleCatHom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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

@[simp]

theorem TopRep.hom_id {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A : TopRep k G) : Hom.hom (CategoryTheory.CategoryStruct.id A) = ContIntertwiningMap.id

theorem TopRep.id_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A : TopRep k G) (a : ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a

@[simp]

theorem TopRep.hom_comp {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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)

theorem TopRep.comp_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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)

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

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

theorem TopRep.hom_comm_apply {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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)

@[implicit_reducible]

instance TopRep.instAddCommGroupHom {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A B : TopRep k G) : AddCommGroup (A ⟶ B)

Equations

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

@[simp]

theorem TopRep.hom_zero {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A B : TopRep k G) : Hom.hom 0 = 0

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

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

theorem TopRep.ofHom_add {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring 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 g : ContIntertwiningMap ρ σ) : ofHom (f + g) = ofHom f + ofHom g

theorem TopRep.ofHom_sub {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [Ring 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 g : ContIntertwiningMap ρ σ) : ofHom (f - g) = ofHom f - ofHom g

theorem TopRep.comp_add' {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A B C : TopRep k G) (f : A ⟶ B) (g h : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (g + h) = CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f h

theorem TopRep.add_comp' {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] (A B C : TopRep k G) (f g : A ⟶ B) (h : B ⟶ C) : CategoryTheory.CategoryStruct.comp (f + g) h = CategoryTheory.CategoryStruct.comp f h + CategoryTheory.CategoryStruct.comp g h

@[implicit_reducible]

instance TopRep.instPreadditive {k : Type u} {G : Type v} [TopologicalSpace k] [Ring k] [Monoid G] : CategoryTheory.Preadditive (TopRep k G)

Equations

• TopRep.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

@[implicit_reducible]

instance TopRep.instModuleHom {k : Type u} {G : Type v} [TopologicalSpace k] [CommRing k] [Monoid G] {A B : TopRep k G} : Module k (A ⟶ B)

Equations

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

theorem TopRep.hom_smul {k : Type u} {G : Type v} [TopologicalSpace k] [CommRing k] [Monoid G] {A B : TopRep k G} (r : k) (f : A ⟶ B) : Hom.hom (r • f) = r • Hom.hom f

theorem TopRep.ofHom_smul {k : Type u} {G : Type v} {X Y : Type w} [TopologicalSpace k] [CommRing 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} (r : k) (f : ContIntertwiningMap ρ σ) : ofHom (r • f) = r • ofHom f

theorem TopRep.smul_comp' {k : Type u} {G : Type v} [TopologicalSpace k] [CommRing k] [Monoid G] (A B C : TopRep k G) (r : k) (f : A ⟶ B) (g : B ⟶ C) : CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g

theorem TopRep.comp_smul' {k : Type u} {G : Type v} [TopologicalSpace k] [CommRing k] [Monoid G] (A B C : TopRep k G) (f : A ⟶ B) (r : k) (g : B ⟶ C) : CategoryTheory.CategoryStruct.comp f (r • g) = r • CategoryTheory.CategoryStruct.comp f g

@[implicit_reducible]

instance TopRep.instLinear {k : Type u} {G : Type v} [TopologicalSpace k] [CommRing k] [Monoid G] : CategoryTheory.Linear k (TopRep k G)

Equations

• TopRep.instLinear = { homModule := inferInstance, smul_comp := ⋯, comp_smul := ⋯ }

def TopRep.toActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

def TopRep.fromActionTopModFunc {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

def TopRep.toActionFromAction {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

def TopRep.fromActionToAction {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

def TopRep.TopRepEquivActionTop {k : Type u} {G : Type v} [TopologicalSpace k] [Ring 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.

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

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

@[reducible, inline]

abbrev TopRep.invariants {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] (X : TopRep k G) : TopModuleCat k

The G-invariant topologicalsubmodule of a topological representation.

Equations

• X.invariants = TopModuleCat.of k ↥X.ρ.invariants

@[reducible, inline]

abbrev TopRep.invariantsFunctor (k : Type u) [TopologicalSpace k] [Ring k] (G : Type v) [Group G] : CategoryTheory.Functor (TopRep k G) (TopModuleCat k)

The functor taking an R-linear G-representation to its G-invariant submodule.

Equations

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

instance TopRep.instAdditiveTopModuleCatInvariantsFunctor {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] : (invariantsFunctor k G).Additive

instance TopRep.instLinearTopModuleCatInvariantsFunctor {G : Type v} [Group G] {k : Type u} [CommRing k] [TopologicalSpace k] : CategoryTheory.Functor.Linear k (invariantsFunctor k G)

@[reducible, inline]

abbrev TopRep.coind₁ {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (A : TopRep k G) : TopRep k G

The top rep induced by the coinduced representation.

Equations

• A.coind₁ = TopRep.of A.ρ.coind₁

@[reducible, inline]

abbrev TopRep.coind₁Functor (k : Type u) [TopologicalSpace k] [Ring k] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor (TopRep k G) (TopRep k G)

The functor taking a representation rep to the representation C(G, rep). The G action is defined by g • f := x ↦ g • f (g⁻¹ * x).

Equations

• TopRep.coind₁Functor k G = { obj := TopRep.coind₁, map := fun {X Y : TopRep k G} (φ : X ⟶ Y) => TopRep.ofHom (ContRepresentation.coind₁Map (TopRep.Hom.hom φ)), map_id := ⋯, map_comp := ⋯ }

instance TopRep.instAdditiveCoind₁Functor {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (coind₁Functor k G).Additive

instance TopRep.instLinearCoind₁Functor {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : Type u} [CommRing k] [TopologicalSpace k] : CategoryTheory.Functor.Linear k (coind₁Functor k G)

@[implicit_reducible]

def TopRep.coind₁ι {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor.id (TopRep k G) ⟶ coind₁Functor k G

The constant function rep ⟶ C(G, rep) as a natural transformation.

Equations

• TopRep.coind₁ι = { app := fun (rep : TopRep k G) => TopRep.ofHom rep.ρ.coind₁ι, naturality := ⋯ }

@[simp]

theorem TopRep.coind₁ι_app {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (rep : TopRep k G) : coind₁ι.app rep = ofHom rep.ρ.coind₁ι

@[reducible, inline]

abbrev TopRep.res {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] {H : Type u_1} [Monoid H] (φ : H →* G) (A : TopRep k G) : TopRep k H

The restriction of a topological representation along a monoid homomorphism.

Equations

• TopRep.res φ A = TopRep.of (A.ρ.restrict φ)

@[reducible, inline]

abbrev TopRep.resFunctor {k : Type u} [TopologicalSpace k] [Ring k] {G : Type v} [Group G] {H : Type u_1} [Monoid H] (φ : H →* G) : CategoryTheory.Functor (TopRep k G) (TopRep k H)

The functor taking a topological G-representation to a topological H-representation along a monoid homomorphism φ : H →* G.

Equations

• TopRep.resFunctor φ = { obj := TopRep.res φ, map := fun {X Y : TopRep k G} (f : X ⟶ Y) => TopRep.ofHom (ContIntertwiningMap.restrict φ (TopRep.Hom.hom f)), map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem TopRep.resFunctor_map_hom {k : Type u} [TopologicalSpace k] [Ring k] {G : Type u_1} {H : Type u_2} [Group G] [Monoid H] (φ : H →* G) {A B : TopRep k G} (f : A ⟶ B) : Hom.hom ((resFunctor φ).map f) = ContIntertwiningMap.restrict φ (Hom.hom f)

def TopRep.invariantsResMap {k : Type u} [TopologicalSpace k] [Ring k] {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : H →* G) {X : TopRep k G} {Y : TopRep k H} (f : res φ X ⟶ Y) : X.invariants ⟶ Y.invariants

The morphism between invariant submodules induced by a morphism res φ X ⟶ Y of topological H-representations, where φ : H →* G is a group homomorphism.

Equations

• TopRep.invariantsResMap φ f = TopModuleCat.ofHom (ContIntertwiningMap.mapInvariantsOfRes φ (TopRep.Hom.hom f))

theorem TopRep.invariantsResMap_comp {k : Type u} [TopologicalSpace k] [Ring k] {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : TopRep k G} {Y Y' : TopRep k H} (φ : H →* G) (f : res φ X ⟶ Y) (g : Y ⟶ Y') : invariantsResMap φ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (invariantsResMap φ f) ((invariantsFunctor k H).map g)

theorem TopRep.invariantsResMap_map_comp {k : Type u} [TopologicalSpace k] [Ring k] {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X X' : TopRep k G} {Y : TopRep k H} (φ : H →* G) (f : X ⟶ X') (g : res φ X' ⟶ Y) : invariantsResMap φ (CategoryTheory.CategoryStruct.comp ((resFunctor φ).map f) g) = CategoryTheory.CategoryStruct.comp ((invariantsFunctor k G).map f) (invariantsResMap φ g)