Theorems · Definition · algebraic geometry
AlgebraicGeometry.targetAffineLocally
AlgebraicGeometry.AffineTargetMorphismProperty → CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
For a P : AffineTargetMorphismProperty, targetAffineLocally P holds for
f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of Y.
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- Set.Elemproof · cited by 7,166
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.MorphismPropertystatement · cited by 2,179
- AlgebraicGeometry.PresheafedSpace.Hom.baseproof · cited by 1,135
- AlgebraicGeometry.LocallyRingedSpace.Hom.toHomproof · cited by 995
- AlgebraicGeometry.Scheme.Hom.toLRSHom'proof · cited by 895
- TopologicalSpace.Opens.mapproof · cited by 645
- AlgebraicGeometry.Scheme.Opens.toSchemeproof · cited by 433
- AlgebraicGeometry.Scheme.affineOpensproof · cited by 220
- AlgebraicGeometry.morphismRestrictproof · cited by 90
Cited by15
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.affineLocallyproof · cited by 13
- AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocallystatement · cited by 10
- AlgebraicGeometry.targetAffineLocally_affineAnd_iffstatement · cited by 4
- AlgebraicGeometry.targetAffineLocally_affineAnd_iff'statement · cited by 2
- AlgebraicGeometry.of_targetAffineLocally_of_isPullbackstatement and proof · cited by 2
- AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally'statement · cited by 1
- AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocallystatement and proof · cited by 1
- AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocallystatement · cited by 1
- AlgebraicGeometry.targetAffineLocally_affineAnd_lestatement and proof · cited by 1
- AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTargetproof · cited by 1
- AlgebraicGeometry.HasAffineProperty.affineAnd_iffproof · cited by 0