Theorems · Theorem · category theory
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts_of_projective
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
[inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A)
[inst_2 : CategoryTheory.Preregular C] [inst_3 : CategoryTheory.FinitaryExtensive C]
[∀ (X : C), CategoryTheory.Projective X],
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
CategoryTheory.Limits.PreservesFiniteProducts F- Cited by
- 3 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
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.Functorstatement and proof · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.Presheaf.IsSheafstatement · cited by 991
- CategoryTheory.coherentTopologystatement · cited by 141
- CategoryTheory.Projectivestatement and proof · cited by 78
- CategoryTheory.Limits.PreservesFiniteProductsstatement and proof · cited by 75
- CategoryTheory.Preregularstatement and proof · cited by 52
- CategoryTheory.FinitaryExtensivestatement and proof · cited by 38
- CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProductsproof · cited by 4
- CategoryTheory.Presheaf.isSheaf_coherent_iff_regular_and_extensiveproof · cited by 2
- CategoryTheory.regularTopology.isSheaf_of_projectiveproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projectiveproof · cited by 0
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_compproof · cited by 0
- CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_compproof · cited by 0