← all areas

Namespace Localization 6 theorems

— 1 · AtPrime 3 · Away 2

directly in Localization 1

• Localisation at a prime of a surjective ring map Localization.localRingHom_surjective_and_ker_eq_map_of_surjective 0 below · cited by 1 · depth 30

Localization.AtPrime 3

• Localisation at a height-one prime of a normal Noetherian domain is a DVR Localization.AtPrime.isDiscreteValuationRing_of_height_eq_one 0 below · cited by 18 · depth 16
• Local-unit criterion and valuation dichotomy over a place of ℚ̄ Localization.AtPrime.mem_range_of_forall_comap_eq_bot_and_valuation_dichotomy_tensorProduct_valuationSubring_of_liesOverPrime 3 below · cited by 5 · depth 27
• Regularity along several branches over a place above p Localization.AtPrime.mem_range_of_forall_branch_of_forall_comap_eq_bot_and_valuation_dichotomy_of_map_eq_iInf_tensorProduct_valuationSubring_of_liesOverPrime 3 below · cited by 1 · depth 28

Localization.Away 2

• ℤ[1/M] is a characteristic-zero domain embedding in any field of characteristic 0 Localization.Away.isDomain_and_charZero_and_isUnit_and_exists_injective_of_charZero 0 below · cited by 4 · depth 26
• Gluing ring elements along a standard open cover Localization.Away.existsUnique_forall_algebraMap_eq_of_span_eq_top 0 below · cited by 3 · depth 29