Theorems · Definition · category theory
TopCat.PrelocalPredicate.sheafify
{X : TopCat} → {T : ↑X → Type u_2} → TopCat.PrelocalPredicate T → TopCat.LocalPredicate TGiven a P : PrelocalPredicate, we can always construct a LocalPredicate
by asking that the condition from P holds locally near every point.
- Defined in
- Mathlib.Topology.Sheaves.LocalPredicate
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 74 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.
- DFunLike.coeproof · cited by 62,936
- Quiver.Homproof · cited by 32,603
- TopCat.carrierstatement and proof · cited by 3,184
- TopologicalSpace.Opensproof · cited by 2,040
- TopCatstatement and proof · cited by 1,889
- TopCat.PrelocalPredicate.predproof · cited by 56
- TopCat.PrelocalPredicatestatement and proof · cited by 15
- TopCat.LocalPredicatestatement · cited by 10
Cited by8
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFractionproof · cited by 20
- AlgebraicGeometry.StructureSheaf.isLocallyFractionproof · cited by 8
- TopCat.Presheaf.Sheafify.isLocallyGermproof · cited by 2
- TopCat.PrelocalPredicate.sheafifyOfstatement · cited by 1
- TopCat.PrelocalPredicate.sheafify_inductionOnstatement and proof · cited by 1
- TopCat.PrelocalPredicate.sheafify_inductionOn₂statement and proof · cited by 1
- TopCat.PrelocalPredicate.sheafify_inductionOn'statement and proof · cited by 0
- TopCat.PrelocalPredicate.sheafify_inductionOn₂'statement and proof · cited by 0