Theorems · Definition · group theory
Rep.invariantsAdjunction
(k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Group G] → Rep.trivialFunctor k G ⊣ Rep.invariantsFunctor k G
The adjunction between the functor equipping a module with the trivial representation, and the functor sending a representation to its submodule of invariants.
- Defined in
- Mathlib.RepresentationTheory.Invariants
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functor.objproof · cited by 19,642
- CommRingstatement and proof · cited by 17,173
- Groupstatement and proof · cited by 6,238
- ModuleCatstatement and proof · cited by 1,429
- Repstatement and proof · cited by 843
- LinearMap.idproof · cited by 625
- CategoryTheory.Adjunctionstatement · cited by 524
- Submodule.subtypeproof · cited by 480
- Rep.ρproof · cited by 356
- ModuleCat.ofHomproof · cited by 200
- LinearMap.codRestrictproof · cited by 61
- Representation.invariantsproof · cited by 49
Cited by4
Results whose statement or proof uses this declaration.
- Rep.invariantsAdjunction_counit_appstatement and proof · cited by 0
- Rep.invariantsAdjunction_homEquiv_apply_homstatement · cited by 0
- Rep.invariantsAdjunction_homEquiv_symm_apply_homstatement · cited by 0
- Rep.invariantsAdjunction_unit_appstatement and proof · cited by 0