Theorems · Definition · category theory

CategoryTheory.Functor.mapContActionComp

{V : Type u_5} →
  {W : Type u_6} →
    [inst : CategoryTheory.Category.{v_2, u_5} V] →
      {FV : V → V → Type u_7} →
        {CV : V → Type u_8} →
          [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory V FV] →
              [inst_3 : CategoryTheory.HasForget₂ V TopCat] →
                [inst_4 : CategoryTheory.Category.{v_3, u_6} W] →
                  {FW : W → W → Type u_9} →
                    {CW : W → Type u_10} →
                      [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] →
                        [inst_6 : CategoryTheory.ConcreteCategory W FW] →
                          [inst_7 : CategoryTheory.HasForget₂ W TopCat] →
                            (G : Type u_11) →
                              [inst_8 : Monoid G] →
                                [inst_9 : TopologicalSpace G] →
                                  {T : Type u_12} →
                                    [inst_10 : CategoryTheory.Category.{v_4, u_12} T] →
                                      {FT : T → T → Type u_13} →
                                        {CT : T → Type u_14} →
                                          [inst_11 : (X Y : T) → FunLike (FT X Y) (CT X) (CT Y)] →
                                            [inst_12 : CategoryTheory.ConcreteCategory T FT] →
                                              [inst_13 : CategoryTheory.HasForget₂ T TopCat] →
                                                (F : CategoryTheory.Functor V W) →
                                                  (H :
                                                      ∀ (X : ContAction V G),
                                                        ((F.mapAction G).obj X.obj).IsContinuous) →
                                                    (F' : CategoryTheory.Functor W T) →
                                                      (H' :
                                                          ∀ (X : ContAction W G),
                                                            ((F'.mapAction G).obj X.obj).IsContinuous) →
                                                        CategoryTheory.Functor.mapContAction G (F.comp F') ⋯ ≅
                                                          (CategoryTheory.Functor.mapContAction G F H).comp
                                                            (CategoryTheory.Functor.mapContAction G F' H')

Continuous version of Functor.mapActionComp.

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

2 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpaceCategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂