Topological subcategories of Action V G

For a concrete category V, where the forgetful functor factors via TopCat, and a monoid G, equipped with a topological space instance, we define the full subcategory ContAction V G of all objects of Action V G where the induced action is continuous.

We also define a category DiscreteContAction V G as the full subcategory of ContAction V G, where the underlying topological space is discrete.

Finally we define inclusion functors into Action V G and TopCat in terms of HasForget₂ instances.

instance Action.instHasForget₂TopCat (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) : CategoryTheory.HasForget₂ (Action V G) TopCat

Equations

• Action.instHasForget₂TopCat V G = CategoryTheory.HasForget₂.trans (Action V G) V TopCat

instance Action.instMulActionαMonoidTopologicalSpaceObjTopCatForget₂ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) (X : Action V G) : MulAction ↑G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)

Equations

• Action.instMulActionαMonoidTopologicalSpaceObjTopCatForget₂ V G X = MulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev Action.IsContinuous {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] {G : MonCat} [TopologicalSpace ↑G] (X : Action V G) : Prop

For HasForget₂ V TopCat a predicate on an X : Action V G saying that the induced action on the underlying topological space is continuous.

Equations

• X.IsContinuous = ContinuousSMul ↑G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)

def ContAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : Type (u + 1)

For HasForget₂ V TopCat, this is the full subcategory of Action V G where the induced action is continuous.

Equations

• ContAction V G = CategoryTheory.FullSubcategory Action.IsContinuous

instance ContAction.instCategory (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.Category.{u, u + 1} (ContAction V G)

Equations

• ContAction.instCategory V G = CategoryTheory.FullSubcategory.category Action.IsContinuous

instance ContAction.instConcreteCategory (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.ConcreteCategory (ContAction V G)

Equations

• ContAction.instConcreteCategory V G = CategoryTheory.FullSubcategory.concreteCategory Action.IsContinuous

instance ContAction.instHasForget₂Action (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget₂ (ContAction V G) (Action V G)

Equations

• ContAction.instHasForget₂Action V G = CategoryTheory.FullSubcategory.hasForget₂ Action.IsContinuous

instance ContAction.instHasForget₂ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget₂ (ContAction V G) V

Equations

• ContAction.instHasForget₂ V G = CategoryTheory.HasForget₂.trans (ContAction V G) (Action V G) V

instance ContAction.instHasForget₂TopCat (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget₂ (ContAction V G) TopCat

Equations

• ContAction.instHasForget₂TopCat V G = CategoryTheory.HasForget₂.trans (ContAction V G) (Action V G) TopCat

instance ContAction.instCoeAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : Coe (ContAction V G) (Action V G)

Equations

• ContAction.instCoeAction V G = { coe := fun (X : ContAction V G) => X.obj }

@[reducible, inline]

abbrev ContAction.IsDiscrete {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] {G : MonCat} [TopologicalSpace ↑G] (X : ContAction V G) : Prop

A predicate on an X : ContAction V G saying that the topology on the underlying type of X is discrete.

Equations

• X.IsDiscrete = DiscreteTopology ↑((CategoryTheory.forget₂ (ContAction V G) TopCat).obj X)

def DiscreteContAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : Type (u + 1)

The subcategory of ContAction V G where the topology is discrete.

Equations

• DiscreteContAction V G = CategoryTheory.FullSubcategory ContAction.IsDiscrete

instance DiscreteContAction.instCategory (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.Category.{u, u + 1} (DiscreteContAction V G)

Equations

• DiscreteContAction.instCategory V G = CategoryTheory.FullSubcategory.category ContAction.IsDiscrete

instance DiscreteContAction.instConcreteCategory (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.ConcreteCategory (DiscreteContAction V G)

Equations

• DiscreteContAction.instConcreteCategory V G = CategoryTheory.FullSubcategory.concreteCategory ContAction.IsDiscrete

instance DiscreteContAction.instHasForget₂ContAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget₂ (DiscreteContAction V G) (ContAction V G)

Equations

• DiscreteContAction.instHasForget₂ContAction V G = CategoryTheory.FullSubcategory.hasForget₂ ContAction.IsDiscrete

instance DiscreteContAction.instHasForget₂TopCat (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget₂ (DiscreteContAction V G) TopCat

Equations

• DiscreteContAction.instHasForget₂TopCat V G = CategoryTheory.HasForget₂.trans (DiscreteContAction V G) (ContAction V G) TopCat

instance DiscreteContAction.instDiscreteTopologyαTopologicalSpaceObjTopCatForget₂ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.ConcreteCategory V] [CategoryTheory.HasForget₂ V TopCat] {G : MonCat} [TopologicalSpace ↑G] (X : DiscreteContAction V G) : DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj X)