Theorems · Theorem · category theory

ContAction.resCongr_inv

∀ (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] (f f' : G →ₜ* H) (h : f = f'),
  (ContAction.resCongr V f f' h).inv =
    { app := fun X => CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).inv,
      naturality := ⋯ }

Defined in

Mathlib.CategoryTheory.Action.Continuous

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.HasForget₂MonoidTopologicalSpaceMonoidTopologicalSpace