Theorems · Definition · category theory
PresheafOfModules.toPresheaf
{C : Type u₁} →
[inst : CategoryTheory.Category.{v₁, u₁} C] →
(R : CategoryTheory.Functor Cᵒᵖ RingCat) →
CategoryTheory.Functor (PresheafOfModules R) (CategoryTheory.Functor Cᵒᵖ Ab)The forgetful functor PresheafOfModules R ⥤ Cᵒᵖ ⥤ Ab.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- RingCatstatement and proof · cited by 473
- PresheafOfModulesstatement and proof · cited by 247
- Abstatement · cited by 198
- PresheafOfModules.Hom.appproof · cited by 88
- PresheafOfModules.presheafproof · cited by 85
- AddCommGrpCat.ofHomproof · cited by 72
Cited by45
Results whose statement or proof uses this declaration.
- PresheafOfModules.sheafificationproof · cited by 9
- PresheafOfModules.Elementsproof · cited by 6
- SheafOfModules.toSheafproof · cited by 6
- PresheafOfModules.ModuleColimit.homEquivproof · cited by 6
- AlgebraicGeometry.Scheme.Modules.toPresheafproof · cited by 5
- PresheafOfModules.ModuleColimit.mapproof · cited by 5
- PresheafOfModules.sheafifyMapstatement and proof · cited by 3
- PresheafOfModules.ModuleColimit.map_applyproof · cited by 3
- PresheafOfModules.homEquivOfIsLocallyBijectiveproof · cited by 2
- PresheafOfModules.IsLocallyInjectiveproof · cited by 2
- PresheafOfModules.IsLocallySurjectiveproof · cited by 2
- PresheafOfModules.freeAdjunctionstatement · cited by 2