Theorems · Theorem · category theory

CategoryTheory.Equivalence.mapContAction_functor

∀ {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]
  (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),
  (CategoryTheory.Equivalence.mapContAction G E H₁ H₂).functor = CategoryTheory.Functor.mapContAction G E.functor H₁

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpace