Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-07 08:32 4f785b62

View on Github →

feat(algebraic_geometry/Spec): (f∗ 𝒪ₛ)ₚ is just the localization Sₚ for affine f : Spec S ⟶ Spec R (#17471)

Estimated changes

Modified src/algebra/module/localized_module.lean

added theorem is_localized_module.mk_of_algebra

Modified src/algebraic_geometry/Spec.lean

added theorem algebraic_geometry.structure_sheaf.algebra_map_pushforward_stalk

added theorem algebraic_geometry.structure_sheaf.is_localized_module_to_pushforward_stalk_alg_hom_aux

added def algebraic_geometry.structure_sheaf.to_pushforward_stalk

added def algebraic_geometry.structure_sheaf.to_pushforward_stalk_alg_hom

added theorem algebraic_geometry.structure_sheaf.to_pushforward_stalk_comp