Rigid coverage (source code)

= Rigid coverage

A <coverage on a category> is rigid when each object is covered by the sieve generated by arrows from <J-irreducible objects of a site>. Restriction to their full subcategory identifies the <sheaves on a site> with its <presheaf category>. A presheaf on that subcategory extends by the right Kan extension $C\mapsto\operatorname{Nat}(yC|_{\mathcal D},F)$: every covering sieve restricts to the full representable on $\mathcal D$, which proves the sheaf condition directly.