Commit 2023-10-20 14:35 33e0d3e6

View on Github →

feat(Topology/Sheaves/Functors): Specialize pullback-pushforward adjunction to sheaves over topological spaces. (#7722) Port of https://github.com/leanprover-community/mathlib/pull/17561

Estimated changes

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Topology/Sheaves/Functors.lean

deleted theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.mapCocone

deleted theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.map_diagram

deleted theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.pushforward_sheaf_of_sheaf

added def TopCat.Sheaf.pullback

added def TopCat.Sheaf.pullbackIso

added def TopCat.Sheaf.pullbackPushforwardAdjunction

added theorem TopCat.Sheaf.pullback_eq

modified def TopCat.Sheaf.pushforward

added def TopCat.Sheaf.pushforwardForgetIso

added theorem TopCat.Sheaf.pushforward_forget

added theorem TopCat.Sheaf.pushforward_map

added theorem TopCat.Sheaf.pushforward_obj_val

modified theorem TopCat.Sheaf.pushforward_sheaf_of_sheaf

Modified Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

added theorem compatiblePreserving_opens_map

added theorem coverPreserving_opens_map