Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.asOverProp
{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
(X S : AlgebraicGeometry.Scheme) → [inst : X.Over S] → P (X ↘ S) → P.Over ⊤ SBundle an S-scheme with P into an object of P.Over ⊤ S.
- Defined in
- Mathlib.AlgebraicGeometry.Cover.Over
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.MorphismProperty.Overstatement · cited by 94
- CategoryTheory.overstatement and proof · cited by 76
- CategoryTheory.OverClassstatement · cited by 68
- AlgebraicGeometry.Scheme.Overstatement and proof · cited by 35
- AlgebraicGeometry.Scheme.asOverproof · cited by 9
Cited by10
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.asOverPropstatement · cited by 7
- AlgebraicGeometry.Scheme.Cover.toPresieveOverPropproof · cited by 5
- AlgebraicGeometry.Scheme.ofArrows_mem_smallEtaleTopology_iffproof · cited by 1
- AlgebraicGeometry.Scheme.locallyCoverDense_of_leproof · cited by 1
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_Xstatement · cited by 0
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'_fstatement · cited by 0
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_Xstatement · cited by 0
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_fstatement · cited by 0
- AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopologyproof · cited by 0