Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-01 15:44 93cf56c5

View on Github →

feat(algebraic_geometry/*): The map F.stalk y ⟶ F.stalk x for x ⤳ y (#11144)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added theorem prime_spectrum.le_iff_specializes

added def prime_spectrum.localization_map_of_specializes

Modified src/algebraic_geometry/stalks.lean

added theorem algebraic_geometry.PresheafedSpace.stalk_map.stalk_specializes_stalk_map

Modified src/algebraic_geometry/structure_sheaf.lean

added theorem algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_specializes

added theorem algebraic_geometry.structure_sheaf.localization_to_stalk_stalk_to_fiber_ring_hom

added theorem algebraic_geometry.structure_sheaf.stalk_specializes_stalk_to_fiber

added theorem algebraic_geometry.structure_sheaf.stalk_to_fiber_ring_hom_localization_to_stalk

added theorem algebraic_geometry.structure_sheaf.to_stalk_stalk_specializes

Modified src/topology/sheaves/stalks.lean

added theorem Top.presheaf.germ_stalk_specializes'

added theorem Top.presheaf.germ_stalk_specializes

added def Top.presheaf.stalk_specializes

added theorem Top.presheaf.stalk_specializes_stalk_functor_map

added theorem Top.presheaf.stalk_specializes_stalk_pushforward