Theorems · Definition · category theory

ContAction

(V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [CategoryTheory.HasForget₂ V TopCat] →
              (G : Type u_4) → [Monoid G] → [TopologicalSpace G] → Type (max (max u_1 u_4) v_1)

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

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

19 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpace