Commit 2026-02-11 08:51 77a710a9

View on Github →

feat(AlgebraicGeometry): Presentation.isQuasicoherent (#34282) Given a sheaf of R-modules M and a Presentation M, then M is quasicoherent. 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

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

added def SheafOfModules.overPushforwardOverAdj

added def SheafOfModules.pushforwardOver

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

added theorem SheafOfModules.Presentation.isQuasicoherent

added def SheafOfModules.Presentation.quasicoherentData

Modified Mathlib/CategoryTheory/Comma/Over/Pullback.lean

added theorem CategoryTheory.Over.forgetAdjStar_counit_app

added theorem CategoryTheory.Over.forgetAdjStar_unit_app_left

Modified Mathlib/CategoryTheory/Equivalence.lean

added theorem CategoryTheory.Equivalence.symm_counit

added theorem CategoryTheory.Equivalence.symm_unit

Modified Mathlib/CategoryTheory/Sites/CoverPreserving.lean

modified theorem CategoryTheory.compatiblePreservingOfFlat

Modified Mathlib/CategoryTheory/Sites/Over.lean

added theorem CategoryTheory.GrothendieckTopology.coverPreserving_over_star