Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-05 14:15 9fd7a02d

View on Github →

feat(category_theory/sites/left_exact): Sheafification is left exact. (#11252)

Estimated changes

Created src/category_theory/sites/left_exact.lean

added def category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation

added def category_theory.grothendieck_topology.lift_to_diagram_limit_obj

added def category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj

added theorem category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj_fac