Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.forget
CategoryTheory.Functor AlgebraicGeometry.Scheme (Type u)
The forgetful functor from Scheme to Type.
- Defined in
- Mathlib.AlgebraicGeometry.Scheme
- Cited by
- 78 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Functorstatement · cited by 16,252
- CategoryTheory.Functor.compproof · cited by 6,529
- AlgebraicGeometry.Schemestatement · cited by 2,540
- TopCatproof · cited by 1,889
- CategoryTheory.forgetproof · cited by 418
- AlgebraicGeometry.Scheme.forgetToTopproof · cited by 13
Cited by96
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.normalizationCoprodIsostatement · cited by 15
- AlgebraicGeometry.coprodSpecstatement · cited by 7
- AlgebraicGeometry.sigmaSpecstatement · cited by 7
- AlgebraicGeometry.coprodMkstatement · cited by 6
- AlgebraicGeometry.Scheme.coprodPresheafObjIsostatement · cited by 5
- AlgebraicGeometry.Scheme.IsLocallyDirected.openCoverstatement and proof · cited by 5
- AlgebraicGeometry.isCompl_range_inl_inrstatement · cited by 4
- AlgebraicGeometry.sigmaOpenCoverstatement · cited by 4
- AlgebraicGeometry.Scheme.IsLocallyDirected.tAuxstatement and proof · cited by 4
- AlgebraicGeometry.ι_sigmaSpecstatement · cited by 4
- AlgebraicGeometry.coprodMk_inlstatement · cited by 3
- AlgebraicGeometry.coprodMk_inrstatement · cited by 3