Documentation

TauCeti.Topology.Category.TopCat.Action

Continuous actions as functors to TopCat #

A monoid G acting on a space X by continuous maps g • · is the same as a functor SingleObj G ⥤ TopCat sending the unique object to X. This file defines that functor, TopCat.actionFunctor X G, and records how it acts on objects and morphisms.

source
def TopCat.actionFunctor (X : TopCat) (G : Type u_1) [Monoid G] [MulAction G ↑X] [ContinuousConstSMul G ↑X] :
CategoryTheory.Functor (CategoryTheory.SingleObj G) TopCat

A continuous action of a monoid G on a space X, as the functor SingleObj G ⥤ TopCat sending the unique object to X and g to the continuous map g • ·.

Instances For
    source
    @[simp]
    theorem TopCat.actionFunctor_obj (X : TopCat) (G : Type u_1) [Monoid G] [MulAction G ↑X] [ContinuousConstSMul G ↑X] (Y : CategoryTheory.SingleObj G) :
    (X.actionFunctor G).obj Y = X
    source
    theorem TopCat.actionFunctor_map (X : TopCat) (G : Type u_1) [Monoid G] [MulAction G ↑X] [ContinuousConstSMul G ↑X] (g : G) :
    (X.actionFunctor G).map g = ofHom { toFun := fun (x : ↑X) => g • x, continuous_toFun := ⋯ }
    source
    @[simp]
    theorem TopCat.actionFunctor_map_apply (X : TopCat) (G : Type u_1) [Monoid G] [MulAction G ↑X] [ContinuousConstSMul G ↑X] (g : G) (x : ↑X) :
    (CategoryTheory.ConcreteCategory.hom ((X.actionFunctor G).map g)) x = g • x