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.HasForget 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.instMulActionCarrierCarrierObjTopCatForget₂ (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) (X : Action V G) : MulAction ↑G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)

Equations

• Action.instMulActionCarrierCarrierObjTopCatForget₂ V G X = MulAction.mk ⋯ ⋯

@[reducible, inline]

abbrev Action.IsContinuous {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget 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.HasForget 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.HasForget 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.instHasForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget (ContAction V G)

Equations

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

instance ContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousV (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] {FV : V → V → Type u_1} {CV : V → Type u_2} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.ConcreteCategory (ContAction V G) fun (X Y : ContAction V G) => Action.HomSubtype V G X.obj Y.obj

Equations

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

instance ContAction.instHasForget₂Action (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget 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.HasForget 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.HasForget 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.HasForget 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.HasForget 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.HasForget 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.HasForget 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.instHasForget (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] : CategoryTheory.HasForget (DiscreteContAction V G)

Equations

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

instance DiscreteContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : MonCat) [TopologicalSpace ↑G] {FV : V → V → Type u_1} {CV : V → Type u_2} [(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [CategoryTheory.ConcreteCategory V FV] : CategoryTheory.ConcreteCategory (DiscreteContAction V G) fun (X Y : DiscreteContAction V G) => Action.HomSubtype V G X.obj.obj Y.obj.obj

Equations

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

instance DiscreteContAction.instHasForget₂ContAction (V : Type (u + 1)) [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget 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.HasForget 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.instDiscreteTopologyCarrierObjTopCatForget₂ {V : Type (u + 1)} [CategoryTheory.LargeCategory V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : MonCat} [TopologicalSpace ↑G] (X : DiscreteContAction V G) : DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj X)