Theorems · Theorem · algebraic geometry
AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
(f : ↑(X.presheaf.obj (Opposite.op U))),
IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) f)The restriction of a section f to the basic open of f is a unit.
- Defined in
- Mathlib.Geometry.RingedSpace.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 91 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.
- DFunLike.coestatement and proof · cited by 62,936
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- RingHomstatement · cited by 10,189
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- Oppositestatement · cited by 8,081
- CategoryTheory.ConcreteCategory.homstatement and proof · cited by 4,022
- Monoidproof · cited by 3,887
- 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
Cited by3
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.isLocalization_basicOpen_of_qcqsproof · cited by 3
- AlgebraicGeometry.LocallyRingedSpace.isUnit_res_toΓSpecMapBasicOpenproof · cited by 1
- AlgebraicGeometry.exists_isUnit_germ_eqproof · cited by 0