Commit 2026-03-03 19:57 777aaa61

View on Github →

refactor(Topology/Sheaves): harmonize names (#36074) Make the name of the pullback/pushforward adjunction for presheaves Presheaf.pullbackPushforwardAdjunction, so it follows the same convention as the name of the similar adjunction for sheaves.

Estimated changes

Modified Mathlib/Topology/Sheaves/Presheaf.lean

added def TopCat.Presheaf.pullbackPushforwardAdjunction

deleted def TopCat.Presheaf.pushforwardPullbackAdjunction

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.pullbackPushforwardAdjunction_unit_app_app_germToPullbackStalk

added theorem TopCat.Presheaf.pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk

deleted theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_app_app_germToPullbackStalk

deleted theorem TopCat.Presheaf.pushforwardPullbackAdjunction_unit_pullback_map_germToPullbackStalk