Theorems · Definition · group theory
Rep.invariantsFunctor
(k : Type u) →
(G : Type v) → [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (ModuleCat k)The functor sending a representation to its submodule of invariants.
- Defined in
- Mathlib.RepresentationTheory.Invariants
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- CategoryTheory.Functorstatement · cited by 16,252
- Groupstatement and proof · cited by 6,238
- LinearMap.compproof · cited by 1,642
- ModuleCatstatement · cited by 1,429
- Repstatement and proof · cited by 843
- Rep.Vproof · cited by 695
- ModuleCat.ofproof · cited by 594
- Submodule.subtypeproof · cited by 480
- Rep.ρproof · cited by 356
- ModuleCat.ofHomproof · cited by 200
Cited by11
Results whose statement or proof uses this declaration.
- Rep.invariantsAdjunctionstatement · cited by 4
- groupCohomology.map_id_comp_H0Iso_homstatement and proof · cited by 2
- Rep.invariantsFunctor_map_homstatement and proof · cited by 1
- Rep.quotientToInvariantsFunctorproof · cited by 1
- Rep.invariantsAdjunction_counit_appstatement · cited by 0
- Rep.invariantsAdjunction_homEquiv_apply_homstatement · cited by 0
- Rep.invariantsAdjunction_homEquiv_symm_apply_homstatement and proof · cited by 0
- Rep.invariantsAdjunction_unit_appstatement · cited by 0
- Rep.invariantsFunctor_obj_carrierstatement · cited by 0
- groupCohomology.map_id_comp_H0Iso_hom_applyproof · cited by 0
- groupCohomology.map_id_comp_H0Iso_hom_assocstatement and proof · cited by 0