Commit 2023-06-01 12:32 0165a5b6

View on Github →

feat: port AlgebraicGeometry.Stalks (#4498)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PresheafedSpace.lean

Created Mathlib/AlgebraicGeometry/Stalks.lean

added def AlgebraicGeometry.PresheafedSpace.restrictStalkIso

added theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ

added theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ

added theorem AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.comp

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.congr_point

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.id

added def AlgebraicGeometry.PresheafedSpace.stalkMap.stalkIso

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap

added def AlgebraicGeometry.PresheafedSpace.stalkMap

added theorem AlgebraicGeometry.PresheafedSpace.stalkMap_germ