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.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] : CategoryTheory.HasForget₂ (Action V G) TopCat

instance Action.instMulActionCarrierObjTopCatForget₂ (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] (X : Action V G) : MulAction G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)

@[reducible, inline]

abbrev Action.IsContinuous {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [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.

theorem Action.isContinuous_def {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] (X : Action V G) : X.IsContinuous ↔ Continuous fun (p : G × ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)) => (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ V TopCat).map (X.ρ p.1))) p.2

def ContAction (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : Type (max (max u_1 u_2) u_3)

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

instance ContAction.instCategory (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.Category.{u_3, max (max u_3 u_2) u_1} (ContAction V G)

instance ContAction.instHasForget (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget (ContAction V G)

instance ContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousV (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(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

instance ContAction.instHasForget₂Action (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget₂ (ContAction V G) (Action V G)

instance ContAction.instHasForget₂ (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget₂ (ContAction V G) V

instance ContAction.instHasForget₂TopCat (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget₂ (ContAction V G) TopCat

instance ContAction.instCoeAction (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : Coe (ContAction V G) (Action V G)

@[reducible, inline]

abbrev ContAction.IsDiscrete {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [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.

def ContAction.res (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G →ₜ* H) : CategoryTheory.Functor (ContAction V H) (ContAction V G)

The "restriction" functor along a monoid homomorphism f : G →* H, taking actions of H to actions of G. This is the analogue of Action.res in the continuous setting.

@[simp]

theorem ContAction.res_map (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G →ₜ* H) {X✝ Y✝ : ContAction V H} (f✝ : X✝ ⟶ Y✝) : (res V f).map f✝ = (Action.res V ↑f).map f✝

@[simp]

theorem ContAction.res_obj_obj (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G →ₜ* H) (X : ContAction V H) : ((res V f).obj X).obj = (Action.res V ↑f).obj X.obj

def ContAction.resComp (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] {K : Type u_4} [Monoid K] [TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K) : res V (h.comp f) ≅ (res V h).comp (res V f)

Restricting scalars along a composition is naturally isomorphic to restricting scalars twice.

@[simp]

theorem ContAction.resComp_inv (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] {K : Type u_4} [Monoid K] [TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K) : (resComp V f h).inv = { app := fun (X : ContAction V K) => CategoryTheory.CategoryStruct.id ((res V (h.comp f)).obj X), naturality := ⋯ }

@[simp]

theorem ContAction.resComp_hom (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] {K : Type u_4} [Monoid K] [TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K) : (resComp V f h).hom = { app := fun (X : ContAction V K) => CategoryTheory.CategoryStruct.id ((res V (h.comp f)).obj X), naturality := ⋯ }

def ContAction.resCongr (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f') : res V f ≅ res V f'

If f = f', restriction of scalars along f and f' is the same.

@[simp]

theorem ContAction.resCongr_hom (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f') : (resCongr V f f' h).hom = { app := fun (X : ContAction V H) => (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).hom, naturality := ⋯ }

@[simp]

theorem ContAction.resCongr_inv (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f f' : G →ₜ* H) (h : f = f') : (resCongr V f f' h).inv = { app := fun (X : ContAction V H) => (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).inv, naturality := ⋯ }

def ContAction.resEquiv (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G ≃ₜ* H) : ContAction V H ≌ ContAction V G

Restriction of scalars along a topological monoid isomorphism induces an equivalence of categories.

@[simp]

theorem ContAction.resEquiv_inverse (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G ≃ₜ* H) : (resEquiv V f).inverse = res V ↑f.symm

@[simp]

theorem ContAction.resEquiv_functor (V : Type u_1) [CategoryTheory.Category.{u_4, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] {H : Type u_3} [Monoid H] [TopologicalSpace H] (f : G ≃ₜ* H) : (resEquiv V f).functor = res V ↑f

def DiscreteContAction (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : Type (max (max u_1 u_2) u_3)

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

instance DiscreteContAction.instCategory (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.Category.{u_3, max (max u_3 u_2) u_1} (DiscreteContAction V G)

instance DiscreteContAction.instHasForget (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget (DiscreteContAction V G)

instance DiscreteContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV (V : Type u_1) [CategoryTheory.Category.{u_5, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] {FV : V → V → Type u_3} {CV : V → Type u_4} [(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

instance DiscreteContAction.instHasForget₂ContAction (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget₂ (DiscreteContAction V G) (ContAction V G)

instance DiscreteContAction.instHasForget₂TopCat (V : Type u_1) [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] (G : Type u_2) [Monoid G] [TopologicalSpace G] : CategoryTheory.HasForget₂ (DiscreteContAction V G) TopCat

instance DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ {V : Type u_1} [CategoryTheory.Category.{u_3, u_1} V] [CategoryTheory.HasForget V] [CategoryTheory.HasForget₂ V TopCat] {G : Type u_2} [Monoid G] [TopologicalSpace G] (X : DiscreteContAction V G) : DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj X)

def CategoryTheory.Functor.mapContAction {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) : Functor (ContAction V G) (ContAction W G)

Continuous version of Functor.mapAction.

@[simp]

theorem CategoryTheory.Functor.mapContAction_obj_obj {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (X : ContAction V G) : ((mapContAction G F H).obj X).obj = (F.mapAction G).obj X.obj

@[simp]

theorem CategoryTheory.Functor.mapContAction_map {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) {X✝ Y✝ : ContAction V G} (f : X✝ ⟶ Y✝) : (mapContAction G F H).map f = (F.mapAction G).map f

def CategoryTheory.Functor.mapContActionComp {V : Type u_3} {W : Type u_4} [Category.{u_7, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_9, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {T : Type u_6} [Category.{u_11, u_6} T] [HasForget T] [HasForget₂ T TopCat] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (F' : Functor W T) (H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous) : mapContAction G (F.comp F') ⋯ ≅ (mapContAction G F H).comp (mapContAction G F' H')

Continuous version of Functor.mapActionComp.

@[simp]

theorem CategoryTheory.Functor.mapContActionComp_hom {V : Type u_3} {W : Type u_4} [Category.{u_7, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_9, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {T : Type u_6} [Category.{u_11, u_6} T] [HasForget T] [HasForget₂ T TopCat] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (F' : Functor W T) (H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous) : (mapContActionComp G F H F' H').hom = { app := fun (X : ContAction V G) => CategoryStruct.id ((mapContAction G (F.comp F') ⋯).obj X), naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapContActionComp_inv {V : Type u_3} {W : Type u_4} [Category.{u_7, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_9, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {T : Type u_6} [Category.{u_11, u_6} T] [HasForget T] [HasForget₂ T TopCat] (F : Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (F' : Functor W T) (H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous) : (mapContActionComp G F H F' H').inv = { app := fun (X : ContAction V G) => CategoryStruct.id ((mapContAction G (F.comp F') ⋯).obj X), naturality := ⋯ }

def CategoryTheory.Functor.mapContActionCongr {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {F F' : Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : mapContAction G F H ≅ mapContAction G F' H'

Continuous version of Functor.mapActionCongr.

@[simp]

theorem CategoryTheory.Functor.mapContActionCongr_inv {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {F F' : Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (mapContActionCongr G e H H').inv = { app := fun (X : ContAction V G) => (Action.mkIso (e.app X.obj.V) ⋯).inv, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapContActionCongr_hom {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] {F F' : Functor V W} (e : F ≅ F') (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous) (H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous) : (mapContActionCongr G e H H').hom = { app := fun (X : ContAction V G) => (Action.mkIso (e.app X.obj.V) ⋯).hom, naturality := ⋯ }

def CategoryTheory.Equivalence.mapContAction {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (E : V ≌ W) (H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous) (H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous) : ContAction V G ≌ ContAction W G

Continuous version of Equivalence.mapAction.

@[simp]

theorem CategoryTheory.Equivalence.mapContAction_functor {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (E : V ≌ W) (H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous) (H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous) : (mapContAction G E H₁ H₂).functor = Functor.mapContAction G E.functor H₁

@[simp]

theorem CategoryTheory.Equivalence.mapContAction_inverse {V : Type u_3} {W : Type u_4} [Category.{u_6, u_3} V] [HasForget V] [HasForget₂ V TopCat] [Category.{u_8, u_4} W] [HasForget W] [HasForget₂ W TopCat] (G : Type u_5) [Monoid G] [TopologicalSpace G] (E : V ≌ W) (H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous) (H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous) : (mapContAction G E H₁ H₂).inverse = Functor.mapContAction G E.inverse H₂