Commit 2024-07-29 18:29 a01f1cc5

View on Github →

refactor(AlgebraicGeometry): stalk maps (#15070) Introduces Scheme.Hom.stalkMap and LocallyRingedSpace.Hom.stalkMap with the API copied from presheafed spaces. Removes LocallyRingedSpace.stalk and LocallyRingedSpace.ΓToStalk. Instead uses Presheaf.stalk and Presheaf.germ directly.

Estimated changes

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

added def AlgebraicGeometry.Scheme.arrowStalkMapSpecIso

added theorem AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso

Modified Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

deleted def AlgebraicGeometry.LocallyRingedSpace.ΓToStalk

deleted theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap

deleted theorem AlgebraicGeometry.LocallyRingedSpace.ΓToStalk_stalkMap_apply

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

Modified Mathlib/AlgebraicGeometry/Properties.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

added theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom'

added theorem AlgebraicGeometry.Scheme.Opens.germ_stalkIso_inv

Modified Mathlib/AlgebraicGeometry/Scheme.lean

added def AlgebraicGeometry.Scheme.Hom.stalkMap

added theorem AlgebraicGeometry.Scheme.iso_hom_val_base_inv_val_base

added theorem AlgebraicGeometry.Scheme.iso_hom_val_base_inv_val_base_apply

added theorem AlgebraicGeometry.Scheme.iso_inv_val_base_hom_val_base

added theorem AlgebraicGeometry.Scheme.iso_inv_val_base_hom_val_base_apply

added theorem AlgebraicGeometry.Scheme.stalkMap_comp

added theorem AlgebraicGeometry.Scheme.stalkMap_congr

added theorem AlgebraicGeometry.Scheme.stalkMap_congr_hom

added theorem AlgebraicGeometry.Scheme.stalkMap_congr_point

added theorem AlgebraicGeometry.Scheme.stalkMap_germ'

added theorem AlgebraicGeometry.Scheme.stalkMap_germ'_apply

added theorem AlgebraicGeometry.Scheme.stalkMap_germ

added theorem AlgebraicGeometry.Scheme.stalkMap_germ_apply

added theorem AlgebraicGeometry.Scheme.stalkMap_hom_inv

added theorem AlgebraicGeometry.Scheme.stalkMap_hom_inv_apply

added theorem AlgebraicGeometry.Scheme.stalkMap_id

added theorem AlgebraicGeometry.Scheme.stalkMap_inv_hom

added theorem AlgebraicGeometry.Scheme.stalkMap_inv_hom_apply

added theorem AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap

added theorem AlgebraicGeometry.Scheme.stalkSpecializes_stalkMap_apply

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/AlgebraicGeometry/Stalk.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

added theorem AlgebraicGeometry.LocallyRingedSpace.iso_hom_val_base_inv_val_base

added theorem AlgebraicGeometry.LocallyRingedSpace.iso_hom_val_base_inv_val_base_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.iso_inv_val_base_hom_val_base

added theorem AlgebraicGeometry.LocallyRingedSpace.iso_inv_val_base_hom_val_base_apply

added def AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso

added theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ

added theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ

added theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_ofRestrict

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ'_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_id

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap

added theorem AlgebraicGeometry.LocallyRingedSpace.stalkSpecializes_stalkMap_apply

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean

Modified Mathlib/Geometry/RingedSpace/OpenImmersion.lean

Modified Mathlib/Geometry/RingedSpace/Stalks.lean

added def AlgebraicGeometry.PresheafedSpace.Hom.stalkMap

deleted def AlgebraicGeometry.PresheafedSpace.stalkMap

Modified Mathlib/Topology/Sheaves/Stalks.lean

added theorem TopCat.Presheaf.map_germ_eq_Γgerm

added def TopCat.Presheaf.Γgerm

added theorem TopCat.Presheaf.Γgerm_res_apply