Commit 2026-06-03 16:18 6b169127

View on Github →

feat(Algebra/CategoryTheory/ModuleCat): Locally Free Sheaves (#39399) This PR gives a definition of locally free sheaves in terms of first defining a predicate IsLocallyFree for SheafOfModules.LocalGeneratorsData.

Estimated changes

Modified Mathlib.lean

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

added def SheafOfModules.GeneratingSections.localGeneratorsData

added def SheafOfModules.GeneratingSections.map

added def SheafOfModules.GeneratingSections.mapFreeHom

added theorem SheafOfModules.GeneratingSections.map_π_eq

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

added theorem SheafOfModules.LocalGeneratorsData.isLocallyFree

added def SheafOfModules.LocalGeneratorsData.quasiCoherentData

added theorem SheafOfModules.LocalGeneratorsData.quasiCoherentData_localGeneratorsData

added def SheafOfModules.free.generatingSections

added theorem SheafOfModules.free.generatingSections_π

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

deleted def SheafOfModules.Presentation.mapGenerators

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.ofObjects_id