Theorems · Theorem · Lie groups

TopRep.invariantsResMap_comp

∀ {k : Type u} [inst : TopologicalSpace k] [inst_1 : Ring k] {G : Type u_1} {H : Type u_2} [inst_2 : Group G]
  [inst_3 : Group H] {X : TopRep k G} {Y Y' : TopRep k H} (φ : H →* G) (f : TopRep.res φ X ⟶ Y) (g : Y ⟶ Y'),
  TopRep.invariantsResMap φ (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (TopRep.invariantsResMap φ f) ((TopRep.invariantsFunctor k H).map g)

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRingGroupGroup