Commit 2023-05-01 22:19 e8b2eac0

View on Github →

feat: port CategoryTheory.Sites.LeftExact (#3706)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/LeftExact.lean

added def CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation

added def CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj

added theorem CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac

Modified Mathlib/CategoryTheory/Sites/Sheafification.lean

added def CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf