Commit 2026-02-12 12:31 cb07be6e

View on Github →

feat(Algebra/Category): IsQuasicoherent from a cover (#35168)

Estimated changes

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

added theorem SheafOfModules.GeneratingSections.ofEpi_π

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

added def SheafOfModules.pushforwardPushforwardEquivalence

added theorem SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app

added theorem SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app

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

added theorem SheafOfModules.IsQuasicoherent.of_coversTop

added theorem SheafOfModules.QuasicoherentData.isQuasicoherent

added def SheafOfModules.QuasicoherentData.shrink

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added theorem CategoryTheory.Sieve.functorPushforward_ofObjects_le

added theorem CategoryTheory.Sieve.ofObjects_mono

added theorem CategoryTheory.Sieve.pullback_ofObjects