Commit 2023-04-13 11:38 c35e8093

View on Github →

feat: port CategoryTheory.Sites.Sheafification (#3387)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Created Mathlib/CategoryTheory/Sites/Sheafification.lean

added theorem CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_exists

added theorem CategoryTheory.GrothendieckTopology.Plus.exists_of_sep

added theorem CategoryTheory.GrothendieckTopology.Plus.exists_rep

added theorem CategoryTheory.GrothendieckTopology.Plus.inj_of_sep

added theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_of_sep

added theorem CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus

added def CategoryTheory.GrothendieckTopology.Plus.meqOfSep

added def CategoryTheory.GrothendieckTopology.Plus.mk

added theorem CategoryTheory.GrothendieckTopology.Plus.res_mk_eq_mk_pullback

added theorem CategoryTheory.GrothendieckTopology.Plus.sep

added theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_apply

added theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_eq_mk

added theorem CategoryTheory.GrothendieckTopology.Plus.toPlus_mk

added theorem CategoryTheory.GrothendieckTopology.isIso_toSheafify

added theorem CategoryTheory.GrothendieckTopology.isoSheafify_hom

added theorem CategoryTheory.GrothendieckTopology.isoSheafify_inv

added theorem CategoryTheory.GrothendieckTopology.sheafification_map

added theorem CategoryTheory.GrothendieckTopology.sheafification_obj

added theorem CategoryTheory.GrothendieckTopology.sheafifyLift_unique

added theorem CategoryTheory.GrothendieckTopology.sheafifyMap_comp

added theorem CategoryTheory.GrothendieckTopology.sheafifyMap_id

added theorem CategoryTheory.GrothendieckTopology.sheafifyMap_sheafifyLift

added theorem CategoryTheory.GrothendieckTopology.sheafify_hom_ext

added theorem CategoryTheory.GrothendieckTopology.sheafify_isSheaf

added theorem CategoryTheory.GrothendieckTopology.toSheafification_app

added theorem CategoryTheory.GrothendieckTopology.toSheafify_naturality

added theorem CategoryTheory.GrothendieckTopology.toSheafify_sheafifyLift

added theorem CategoryTheory.Meq.condition

added theorem CategoryTheory.Meq.equiv_apply

added theorem CategoryTheory.Meq.equiv_symm_eq_apply

added theorem CategoryTheory.Meq.ext

added def CategoryTheory.Meq.mk

added theorem CategoryTheory.Meq.mk_apply

added def CategoryTheory.Meq.pullback

added theorem CategoryTheory.Meq.pullback_apply

added theorem CategoryTheory.Meq.pullback_refine

added def CategoryTheory.Meq.refine

added theorem CategoryTheory.Meq.refine_apply

added def CategoryTheory.Meq

added theorem CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono