Theorems · Theorem · category theory
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
[inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.FinitaryPreExtensive C]
[CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ D),
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ↔
CategoryTheory.Limits.PreservesFiniteProducts FA presheaf on a category which is FinitaryExtensive is a sheaf iff it preserves finite products.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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.Functor.objproof · cited by 19,642
- CategoryTheory.Functorstatement and proof · cited by 16,252
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.Discreteproof · cited by 2,447
- CategoryTheory.Presheaf.IsSheafstatement and proof · cited by 991
- CategoryTheory.Limits.Coneproof · cited by 710
- CategoryTheory.Limits.IsLimitproof · cited by 664
- CategoryTheory.coyonedaproof · cited by 208
- CategoryTheory.Functor.mapConeproof · cited by 147
- CategoryTheory.Limits.isLimitOfPreservesproof · cited by 76
Cited by4
Results whose statement or proof uses this declaration.
- CategoryTheory.isSheaf_pointwiseColimitproof · cited by 0
- CategoryTheory.Presheaf.isSheaf_iff_extensiveSheaf_of_projectiveproof · cited by 0