Mathlib Map

Theorems · Definition · Lie groups

TopRep.invariantsFunctor

(k : Type u) →
  [inst : TopologicalSpace k] →
    [inst_1 : Ring k] → (G : Type v) → [inst_2 : Group G] → CategoryTheory.Functor (TopRep k G) (TopModuleCat k)

The functor taking an R-linear G-representation to its G-invariant submodule.

Defined in
Mathlib.RepresentationTheory.Continuous.TopRep
Cited by
3 results in Mathlib
Foundations
Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceRingGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TopRep.homogeneousCochains · cited by 13TopRep.homogeneousCochainsTopRep.homogeneousCochains.d_eq · cited by 1homogeneousCochains.d_eqTopRep.invariantsResMap_comp · cited by 0TopRep.invariantsResMap_c…TopRep.invariantsResMap_map_comp · cited by 0TopRep.invariantsResMap_m…Quiver.Hom · cited by 32603Quiver.HomTopologicalSpace · cited by 24529TopologicalSpaceCategoryTheory.Functor · cited by 16252CategoryTheory.FunctorRing · cited by 7463RingGroup · cited by 6238GroupTopRep · cited by 54TopRepTopModuleCat · cited by 45TopModuleCatTopRep.V · cited by 36TopRep.VTopRep.ρ · cited by 34TopRep.ρTopRep.Hom.hom · cited by 33Hom.homContRepresentation.invariants · cited by 11ContRepresentation.invari…TopModuleCat.of · cited by 4TopModuleCat.ofTopModuleCat.ofHom · cited by 4TopModuleCat.ofHomContIntertwiningMap.mapInvariants · cited by 3ContIntertwiningMap.mapIn…TopRep.invariantsFunctorCITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.