Mathlib Changelog
v4
Changelog
About
Github
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