Theorems · Definition · category theory
RingCat.moduleCatRestrictScalarsPseudofunctor
CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete RingCatᵒᵖ) CategoryTheory.Cat
The pseudofunctor from LocallyDiscrete RingCatᵒᵖ to Cat which sends a ring R
to its category of modules. The functoriality is given by the restriction of scalars.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 39 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- Oppositestatement and proof · cited by 8,081
- Opposite.unopproof · cited by 2,231
- ModuleCatproof · cited by 1,429
- Quiver.Hom.unopproof · cited by 903
- CategoryTheory.Catstatement · cited by 884
- CategoryTheory.Pseudofunctorstatement · cited by 571
- RingCatstatement and proof · cited by 473
- CategoryTheory.LocallyDiscretestatement · cited by 318
- RingCat.carrierproof · cited by 279
- CategoryTheory.Cat.ofproof · cited by 189
- ModuleCat.restrictScalarsproof · cited by 148
Cited by4
Results whose statement or proof uses this declaration.
- RingCat.moduleCatRestrictScalarsPseudofunctor_mapstatement and proof · cited by 0
- RingCat.moduleCatRestrictScalarsPseudofunctor_mapCompstatement and proof · cited by 0
- RingCat.moduleCatRestrictScalarsPseudofunctor_mapIdstatement and proof · cited by 0
- RingCat.moduleCatRestrictScalarsPseudofunctor_objstatement and proof · cited by 0