Documentation

Mathlib.CategoryTheory.Action.Continuous

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.

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]

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
Instances For

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

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For

        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.

        Equations
        Instances For
          @[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✝

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

          Equations
          Instances For
            @[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 := }

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[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 := }

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                @[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.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[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) :

                  Continuous version of Functor.mapActionCongr.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[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 := }

                    Continuous version of Equivalence.mapAction.

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