Theorems · Definition · category theory
CategoryTheory.Coverage.toPrecoverage
{C : Type u_1} →
[inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Coverage C → CategoryTheory.Precoverage C- Defined in
- Mathlib.CategoryTheory.Sites.Coverage
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Precoveragestatement · cited by 204
- CategoryTheory.Coveragestatement and proof · cited by 31
Cited by37
Results whose statement or proof uses this declaration.
- CategoryTheory.Coverage.toGrothendieckproof · cited by 15
- CategoryTheory.Presieve.isSheaf_coveragestatement and proof · cited by 8
- CategoryTheory.Coverage.toGrothendieck_toPrecoveragestatement and proof · cited by 4
- CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpiproof · cited by 4
- CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamilyproof · cited by 3
- CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forgetproof · cited by 3
- CategoryTheory.Coverage.mem_toGrothendieck_sieves_of_supersetstatement and proof · cited by 2
- CategoryTheory.Coverage.pullbackstatement · cited by 2
- CategoryTheory.extensive_regular_generate_coherentproof · cited by 2
- CategoryTheory.Precoverage.toCoverage_toPrecoveragestatement and proof · cited by 1
- CategoryTheory.Presheaf.isSheaf_iff_isLimit_coveragestatement and proof · cited by 1