Commit 2025-11-16 17:26 48d5afee

View on Github →

feat(CategoryTheory/Sites): categories of sheaves on Over categories, as a pseudofunctor (#31087) Given a Grothendieck topology J on a category C and a category A, we define the pseudofunctor J.pseudofunctorOver A : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat which sends X : C to the category of sheaves on Over X with values in A. In order to do this, we expand the API for pushforward of sheaves for continuous functors. We add a few pseudofunctor-like definitions for these pushforwards.

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.Over.mapCongr_rfl

modified def CategoryTheory.Over.mapId

Modified Mathlib/CategoryTheory/Sites/Continuous.lean

added def CategoryTheory.Functor.sheafPushforwardContinuousComp'

added def CategoryTheory.Functor.sheafPushforwardContinuousComp

added def CategoryTheory.Functor.sheafPushforwardContinuousId'

added def CategoryTheory.Functor.sheafPushforwardContinuousId

added def CategoryTheory.Functor.sheafPushforwardContinuousIso

added def CategoryTheory.Functor.sheafPushforwardContinuousNatTrans

Modified Mathlib/CategoryTheory/Sites/Over.lean

added def CategoryTheory.GrothendieckTopology.overMapPullbackComp

added def CategoryTheory.GrothendieckTopology.overMapPullbackCongr

added theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso

added def CategoryTheory.GrothendieckTopology.overMapPullbackId

added theorem CategoryTheory.GrothendieckTopology.overMapPullback_assoc

added theorem CategoryTheory.GrothendieckTopology.overMapPullback_comp_id

added theorem CategoryTheory.GrothendieckTopology.overMapPullback_id_comp

Created Mathlib/CategoryTheory/Sites/PseudofunctorSheafOver.lean

added def CategoryTheory.GrothendieckTopology.pseudofunctorOver