mathlib3 documentation

category_theory.sites.left_exact

Left exactness of sheafification #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file we show that sheafification commutes with finite limits.

@[reducible]

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