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

    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.