Documentation

Mathlib.CategoryTheory.Sites.LeftExact

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.diagramFunctor D X preserves limits.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[reducible, inline]

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For