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) : Prop

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 π))

  R consists of a finite collection of arrows that together induce an isomorphism from the coproduct of their sources.

instance CategoryTheory.instHasPairwisePullbacksOfExtensive {C : Type u_1} [Category.{v_1, u_1} C] [FinitaryPreExtensive C] {X : C} (S : Presieve X) [S.Extensive] : S.HasPairwisePullbacks

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] : Presieve.IsSheafFor F S

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] : (extensiveTopology C).Subcanonical

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)) : IsSheaf (extensiveTopology C) F ↔ Limits.PreservesFiniteProducts F

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) : IsSheaf (extensiveTopology C) F ↔ Limits.PreservesFiniteProducts F

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) : Limits.PreservesFiniteProducts F.obj