Theorems · Definition · Lie groups
TopRep.invariants
{k : Type u} →
[inst : TopologicalSpace k] → [inst_1 : Ring k] → {G : Type v} → [inst_2 : Group G] → TopRep k G → TopModuleCat kThe G-invariant topologicalsubmodule of a topological representation.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceRingGroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Ringstatement and proof · cited by 7,463
- Groupstatement and proof · cited by 6,238
- TopRepstatement and proof · cited by 54
- TopModuleCatstatement · cited by 45
- TopRep.Vproof · cited by 36
- TopRep.ρproof · cited by 34
- ContRepresentation.invariantsproof · cited by 11
- TopModuleCat.ofproof · cited by 4
Cited by6
Results whose statement or proof uses this declaration.
- TopRep.invariantsResMapstatement · cited by 4
- ContinuousCohomology.cochainsMap_idproof · cited by 2
- ContinuousCohomology.cochainsMap_fstatement · cited by 1
- TopRep.invariantsResMap_compstatement · cited by 0
- TopRep.invariantsResMap_map_compstatement · cited by 0
- ContinuousCohomology.cochainsMap_f_homstatement · cited by 0