Commit 2025-12-18 09:28 1dad9693

View on Github →

feat(Algebra/Category/ModuleCat/Sheaf/Quasicoherent): construction of Presentation (#32437) We construct presentation of sheaf of module by sequence and add Presentation.map. This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025.

Estimated changes

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

added theorem SheafOfModules.map_ιFree_mapFree_hom

added theorem SheafOfModules.ιFree_mapFree_inv

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

added def SheafOfModules.Presentation.isColimit

added def SheafOfModules.Presentation.map

added def SheafOfModules.Presentation.mapGenerators

added def SheafOfModules.Presentation.mapRelations

added theorem SheafOfModules.Presentation.mapRelations_mapGenerators

added theorem SheafOfModules.Presentation.map_π_eq

added def SheafOfModules.generatorsOfIsCokernelFree

added theorem SheafOfModules.generatorsOfIsCokernelFree_π

added def SheafOfModules.presentationOfIsCokernelFree

added def SheafOfModules.relationsOfIsCokernelFree

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

added def CategoryTheory.Limits.parallelPairHomMk

added def CategoryTheory.Limits.parallelPairIso

added def CategoryTheory.Limits.parallelPairIsoMk