Documentation

Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Sheaves for the extensive topology #

This file characterises sheaves for the extensive topology.

Main result #

A presieve is extensive if it is finite and its arrows induce an isomorphism from the coproduct to the target.

Instances
    theorem CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit {C : Type u_1} :
    ∀ {inst : 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.

    A finite product preserving presheaf is a sheaf for the extensive topology on a category which is FinitaryPreExtensive.

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