Sheaves for the extensive topology #
This file characterises sheaves for the extensive topology.
Main result #
isSheaf_iff_preservesFiniteProducts: In a finitary extensive category, the sheaves for the extensive topology are precisely those preserving finite products.
class
CategoryTheory.Presieve.Extensive
{C : Type u_1}
[Category.{v_1, u_1} C]
{X : C}
(R : Presieve X)
:
A presieve is extensive if it is finite and its arrows induce an isomorphism from the coproduct to the target.
- arrows_nonempty_isColimit : ∃ (α : Type) (_ : Finite α) (Z : α → C) (π : (a : α) → Z a ⟶ X), R = ofArrows Z π ∧ Nonempty (Limits.IsColimit (Limits.Cofan.mk X π))
Rconsists of a finite collection of arrows that together induce an isomorphism from the coproduct of their sources.
Instances
instance
CategoryTheory.instHasPairwisePullbacksOfExtensive
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
{X : C}
(S : Presieve X)
[S.Extensive]
:
theorem
CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
{X : C}
(S : Presieve X)
[S.Extensive]
(F : Functor Cᵒᵖ (Type w))
[Limits.PreservesFiniteProducts F]
:
A finite-product-preserving presheaf is a sheaf for the extensive topology on a category which is
FinitaryPreExtensive.
instance
CategoryTheory.instExtensiveOfArrowsι
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
{α : Type}
[Finite α]
(Z : α → C)
:
(Presieve.ofArrows Z fun (i : α) => Limits.Sigma.ι Z i).Extensive
theorem
CategoryTheory.extensiveTopology.isSheaf_yoneda_obj
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
(W : C)
:
Presieve.IsSheaf (extensiveTopology C) (yoneda.obj W)
Every Yoneda-presheaf is a sheaf for the extensive topology.
instance
CategoryTheory.extensiveTopology.subcanonical
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
:
The extensive topology on a finitary pre-extensive category is subcanonical.
theorem
CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts
{C : Type u_1}
[Category.{v_1, u_1} C]
[FinitaryPreExtensive C]
[FinitaryExtensive C]
(F : Functor Cᵒᵖ (Type w))
:
A presheaf of sets on a category which is FinitaryExtensive is a sheaf iff it preserves finite
products.
theorem
CategoryTheory.Presheaf.isSheaf_iff_preservesFiniteProducts
{C : Type u_1}
[Category.{v_1, u_1} C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[FinitaryPreExtensive C]
[FinitaryExtensive C]
(F : Functor Cᵒᵖ D)
:
A presheaf on a category which is FinitaryExtensive is a sheaf iff it preserves finite products.
instance
CategoryTheory.instPreservesFiniteProductsOppositeObjFunctorIsSheafExtensiveTopology
{C : Type u_1}
[Category.{v_1, u_1} C]
{D : Type u_2}
[Category.{v_2, u_2} D]
[FinitaryPreExtensive C]
[FinitaryExtensive C]
(F : Sheaf (extensiveTopology C) D)
: