Theorems · Definition · algebraic geometry
AlgebraicGeometry.LocallyRingedSpace.toTopCat
AlgebraicGeometry.LocallyRingedSpace → TopCat
The underlying topological space of a locally ringed space.
- Cited by
- 128 results in Mathlib
- Foundations
- Depth 22 from the axioms, rests on 192 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AlgebraicGeometry.PresheafedSpace.carrierproof · cited by 2,020
- AlgebraicGeometry.SheafedSpace.toPresheafedSpaceproof · cited by 1,988
- AlgebraicGeometry.LocallyRingedSpace.toSheafedSpaceproof · cited by 1,892
- TopCatstatement · cited by 1,889
- AlgebraicGeometry.LocallyRingedSpacestatement and proof · cited by 205
Cited by160
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.affineCoverproof · cited by 61
- AlgebraicGeometry.LocallyRingedSpace.restrictstatement and proof · cited by 55
- AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMapstatement and proof · cited by 34
- AlgebraicGeometry.LocallyRingedSpace.residueFieldstatement and proof · cited by 16
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctorstatement · cited by 13
- AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invAppstatement and proof · cited by 12
- AlgebraicGeometry.LocallyRingedSpace.ofRestrictstatement and proof · cited by 10
- AlgebraicGeometry.LocallyRingedSpace.residueFieldMapstatement and proof · cited by 10
- AlgebraicGeometry.LocallyRingedSpace.restrictStalkIsostatement and proof · cited by 10
- AlgebraicGeometry.Scheme.affineOpenCoverproof · cited by 8
- AlgebraicGeometry.LocallyRingedSpace.toΓSpecBasestatement · cited by 8
- AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpenstatement · cited by 7