Theorems · Inductive type · algebraic geometry
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal
AlgebraicGeometry.AffineTargetMorphismProperty → Prop
We say that P : AffineTargetMorphismProperty is a local property if
1. P respects isomorphisms.
2. If P holds for f : X ⟶ Y, then P holds for f ∣_ Y.basicOpen r for any
global section r.
3. If P holds for f ∣_ Y.basicOpen r for all r in a spanning set of the global sections,
then P holds for f.
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AlgebraicGeometry.AffineTargetMorphismPropertystatement · cited by 31
Cited by21
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.HasAffineProperty.iff_of_isAffineproof · cited by 21
- AlgebraicGeometry.HasAffineProperty.isLocal_affinePropertystatement · cited by 10
- AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChangeproof · cited by 3
- AlgebraicGeometry.HasAffineProperty.of_iSup_eq_topproof · cited by 3
- AlgebraicGeometry.HasAffineProperty.diagonal_of_openCoverproof · cited by 2
- AlgebraicGeometry.affineAnd_isLocalstatement · cited by 2
- AlgebraicGeometry.of_targetAffineLocally_of_isPullbackstatement and proof · cited by 2
- AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChangeproof · cited by 1
- AlgebraicGeometry.HasAffineProperty.diagonal_iffproof · cited by 1
- AlgebraicGeometry.HasAffineProperty.diagonal_of_diagonal_of_isPullbackproof · cited by 1
- AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.of_basicOpenCoverstatement and proof · cited by 1
- AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.to_basicOpenstatement and proof · cited by 1