Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-02 12:47 3e72feb3

View on Github →

feat(ring_theory/localization): The localization of a localization is a localization. (#10456) Also provides an easy consequence : the map of Spec M⁻¹R ⟶ Spec R is isomorphic on stalks.

Estimated changes

Modified src/algebraic_geometry/Spec.lean

added theorem algebraic_geometry.Spec_map_localization_is_iso

Modified src/ring_theory/localization.lean

added theorem is_localization.is_localization_is_localization_at_prime_is_localization

added def is_localization.localization_localization_at_prime_iso_localization

added theorem is_localization.localization_localization_eq_iff_exists

added theorem is_localization.localization_localization_is_localization

added theorem is_localization.localization_localization_is_localization_of_has_all_units

added theorem is_localization.localization_localization_map_units

added def is_localization.localization_localization_submodule

added theorem is_localization.localization_localization_surj

added theorem is_localization.mem_localization_localization_submodule