Theorems · Definition · algebraic geometry
AlgebraicGeometry.RingedSpace.basicOpen
(X : AlgebraicGeometry.RingedSpace) →
{U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace} →
↑(X.presheaf.obj (Opposite.op U)) → TopologicalSpace.Opens ↑↑X.toPresheafedSpaceThe basic open of a section f is the set of all points x, such that the germ of f at
x is a unit.
- Defined in
- Mathlib.Geometry.RingedSpace.Basic
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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.Functor.objstatement and proof · cited by 19,642
- Oppositestatement · cited by 8,081
- Set.ofPredproof · cited by 6,101
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- TopCat.carrierstatement and proof · cited by 3,184
- CommRingCatstatement · cited by 2,333
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- AlgebraicGeometry.PresheafedSpace.carrierstatement and proof · cited by 2,020
- AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement and proof · cited by 1,988
- IsUnitproof · cited by 1,602
- AlgebraicGeometry.PresheafedSpace.presheafstatement and proof · cited by 1,104
Cited by33
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.basicOpenproof · cited by 141
- AlgebraicGeometry.RingedSpace.mem_basicOpenstatement · cited by 8
- AlgebraicGeometry.exists_basicOpen_le_affine_interproof · cited by 7
- AlgebraicGeometry.RingedSpace.basicOpen_lestatement and proof · cited by 7
- AlgebraicGeometry.RingedSpace.zeroLocusproof · cited by 5
- AlgebraicGeometry.RingedSpace.basicOpen_resstatement and proof · cited by 4
- AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eqstatement · cited by 3
- AlgebraicGeometry.RingedSpace.isUnit_res_basicOpenstatement and proof · cited by 3
- AlgebraicGeometry.LocallyRingedSpace.basicOpen_zerostatement · cited by 2
- AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpenstatement · cited by 2
- AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpenproof · cited by 2
- AlgebraicGeometry.RingedSpace.basicOpen_mulstatement and proof · cited by 2