Theorems · Theorem · category theory

ContAction.resComp_hom

∀ (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]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] {K : Type u_6} [inst_8 : Monoid K]
  [inst_9 : TopologicalSpace K] (f : G →ₜ* H) (h : H →ₜ* K),
  (ContAction.resComp V f h).hom =
    { app := fun X => CategoryTheory.CategoryStruct.id ((ContAction.res V (h.comp f)).obj X), naturality := ⋯ }

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpaceMonoidTopologicalSpaceMonoidTopologicalSpace