Commit 2024-10-24 07:23 893b3a84

View on Github →

feat(Algebra/Category/ModuleCat): the free presheaf of modules on a presheaf of sets (#16755) This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib.lean

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

added theorem ModuleCat.adj_homEquiv

added theorem ModuleCat.freeDesc_apply

added def ModuleCat.freeHomEquiv

added theorem ModuleCat.free_hom_ext

added theorem ModuleCat.free_map_apply

Created Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

added theorem PresheafOfModules.freeAdjunction_homEquiv

added theorem PresheafOfModules.freeAdjunction_unit_app

added theorem PresheafOfModules.free_hom_ext

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

added theorem PresheafOfModules.sheafificationAdjunction_homEquiv_apply

deleted theorem PresheafOfModules.sheaififcationAdjunction_homEquiv_apply

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean