mathlib documentation

category_theory.sites.left_exact

Left exactness of sheafification #

In this file we show that sheafification commutes with finite limits.

An auxiliary definition to be used in the proof of the fact that J.diagram_functor D X preserves limits.

An auxiliary definition to be used in the proof that J.plus_functor D commutes with finite limits.

Equations
@[protected, instance]
Equations