Theorems · Theorem · Lie groups

TopRep.invariantsResMap_map_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 X' : TopRep k G} {Y : TopRep k H} (φ : H →* G) (f : X ⟶ X') (g : TopRep.res φ X' ⟶ Y),
  TopRep.invariantsResMap φ (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor φ).map f) g) =
    CategoryTheory.CategoryStruct.comp ((TopRep.invariantsFunctor k G).map f) (TopRep.invariantsResMap φ 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