Theorems · Definition · Lie groups

TopRep.resFunctor

{k : Type u} →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] →
      {G : Type v} →
        [inst_2 : Group G] →
          {H : Type u_1} → [inst_3 : Monoid H] → (H →* G) → CategoryTheory.Functor (TopRep k G) (TopRep k H)

The functor taking a topological G-representation to a topological H-representation along a monoid homomorphism φ : H →* G.

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

7 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRingGroupMonoid