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} [CategoryTheory.Category.{v, u} C] {X : C} (R : CategoryTheory.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 = CategoryTheory.Presieve.ofArrows Z π ∧ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π))

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

theorem CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {R : CategoryTheory.Presieve X} [self : R.Extensive] : ∃ (α : Type) (_ : Finite α) (Z : α → C) (π : (a : α) → Z a ⟶ X), R = CategoryTheory.Presieve.ofArrows Z π ∧ Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.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.instHasPullbacksOfExtensive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [S.Extensive] : S.hasPullbacks

Equations

• ⋯ = ⋯

theorem CategoryTheory.isSheafFor_extensive_of_preservesFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [S.Extensive] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) [CategoryTheory.Limits.PreservesFiniteProducts F] : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] {α : Type} [Finite α] (Z : α → C) : (CategoryTheory.Presieve.ofArrows Z fun (i : α) => CategoryTheory.Limits.Sigma.ι Z i).Extensive

Equations

• ⋯ = ⋯

theorem CategoryTheory.isSheaf_iff_preservesFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (CategoryTheory.extensiveCoverage C)) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)

A presheaf on a category which is FinitaryExtensive is a sheaf iff it preserves finite products.