Commit 2024-06-10 19:57 14040d47

View on Github →

feat: the category of sheaves of modules is abelian (#13455)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/ChangeOfRings.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

added theorem SheafOfModules.add_val

Created Mathlib/Algebra/Category/ModuleCat/Sheaf/Abelian.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/ChangeOfRings.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Limits.lean

Modified Mathlib/AlgebraicGeometry/Modules/Sheaf.lean

Modified Mathlib/CategoryTheory/Functor/ReflectsIso.lean

added theorem CategoryTheory.reflectsIsomorphisms_of_comp