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} [CategoryTheory.Category.{u_3, u_1} 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_1} [CategoryTheory.Category.{u_3, u_1} 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_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] {X : C} (S : CategoryTheory.Presieve X) [S.Extensive] : S.hasPullbacks

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.extensiveTopology.isSheaf_yoneda_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] (W : C) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) (CategoryTheory.yoneda.obj W)

Every Yoneda-presheaf is a sheaf for the extensive topology.

theorem CategoryTheory.extensiveTopology.subcanonical {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] : CategoryTheory.Sheaf.Subcanonical (CategoryTheory.extensiveTopology C)

The extensive topology on a finitary pre-extensive category is subcanonical.

theorem CategoryTheory.Presieve.isSheaf_iff_preservesFiniteProducts {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) : CategoryTheory.Presieve.IsSheaf (CategoryTheory.extensiveTopology C) F ↔ Nonempty (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C) F ↔ Nonempty (CategoryTheory.Limits.PreservesFiniteProducts F)

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

noncomputable instance CategoryTheory.instPreservesFiniteProductsOppositeVal {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.FinitaryExtensive C] (F : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) D) : CategoryTheory.Limits.PreservesFiniteProducts F.val

Equations

• CategoryTheory.instPreservesFiniteProductsOppositeVal F = ⋯.some