Theorems · Definition · algebraic geometry
AlgebraicGeometry.modulesSpecToSheaf
{R : CommRingCat} →
CategoryTheory.Functor (AlgebraicGeometry.Spec R).Modules
(TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace)The forgetful functor from 𝒪_{Spec R} modules to sheaves of R-modules.
- Defined in
- Mathlib.AlgebraicGeometry.Modules.Tilde
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- Top.topproof · cited by 9,680
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.Iso.invproof · cited by 6,514
- TopCat.carrierproof · cited by 3,184
- CommRingCatstatement and proof · cited by 2,333
- AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
- AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988
- AlgebraicGeometry.LocallyRingedSpace.toSheafedSpacestatement and proof · cited by 1,892
- AlgebraicGeometry.Scheme.toLocallyRingedSpacestatement and proof · cited by 1,734
- ModuleCatstatement · cited by 1,429
- CommRingCat.carrierstatement · cited by 1,096
Cited by25
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.tilde.toOpenstatement · cited by 10
- AlgebraicGeometry.Scheme.Modules.fromTildeΓstatement and proof · cited by 9
- AlgebraicGeometry.tilde.toOpen_resstatement · cited by 4
- AlgebraicGeometry.moduleSpecΓFunctorproof · cited by 3
- AlgebraicGeometry.tilde.modulesSpecToSheafIsostatement and proof · cited by 2
- AlgebraicGeometry.Scheme.Modules.toOpen_fromTildeΓ_appstatement and proof · cited by 2
- AlgebraicGeometry.isLocalizing_pushforward_of_isLocalizingstatement and proof · cited by 1
- AlgebraicGeometry.isLocalizing_tildestatement and proof · cited by 1
- AlgebraicGeometry.pushforwardCompModulesSpecToSheafIsostatement · cited by 1
- AlgebraicGeometry.tilde.isoTopstatement · cited by 1
- AlgebraicGeometry.tilde.toOpen_map_appstatement · cited by 1
- AlgebraicGeometry.isIso_fromTildeΓ_iffstatement · cited by 1