Theorems · Inductive type · category theory
CategoryTheory.Precoherent
(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → PropThe condition Precoherent C is essentially the minimal condition required to define the
coherent coverage on C.
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
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.
- CategoryTheory.Categorystatement · cited by 32,673
Cited by32
Results whose statement or proof uses this declaration.
- CategoryTheory.coherentTopologystatement and proof · cited by 141
- CategoryTheory.Equivalence.sheafCongrPrecoherentstatement and proof · cited by 11
- CategoryTheory.Equivalence.precoherentstatement and proof · cited by 11
- CategoryTheory.coherentCoveragestatement and proof · cited by 6
- CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamilystatement and proof · cited by 3
- CategoryTheory.Functor.reflects_precoherentstatement and proof · cited by 3
- CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamilystatement and proof · cited by 2
- CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_inducedstatement and proof · cited by 1
- CategoryTheory.coherentTopology.isSheaf_yoneda_objstatement and proof · cited by 1
- CategoryTheory.Precoherent.pullbackstatement and proof · cited by 1
- CategoryTheory.EffectiveEpiFamily.transitive_of_finitestatement and proof · cited by 1
- CategoryTheory.Equivalence.precoherent_isSheaf_iffstatement and proof · cited by 1