← all areas

Namespace IsLocalization 6 theorems

— 2 · AtPrime 3 · Away 1

directly in IsLocalization 2

• Generic fibre of a bijective base change widehat R⊗_R S→ T IsLocalization.exists_algEquiv_tensorProduct_and_injective_of_bijective_baseChange 0 below · cited by 1 · depth 26
• Kernel of localisation at a prime is killed by one element IsLocalization.exists_not_mem_forall_algebraMap_away_eq_zero_of_algebraMap_atPrime_eq_zero 0 below · cited by 1 · depth 36

IsLocalization.AtPrime 3

• Global-to-local map for a finite over-ring in K IsLocalization.AtPrime.surjective_and_ker_pi_span_mul_quotient_of_moduleFinite 0 below · cited by 1 · depth 30
• Adic completion commutes with localisation at a maximal ideal IsLocalization.AtPrime.exists_ringEquiv_adicCompletion_maximalIdeal 0 below · cited by 2 · depth 31
• Reduced Noetherian rings: integrality spreads to a basic open IsLocalization.AtPrime.exists_notMem_forall_isDomain_away_of_isReduced 0 below · cited by 1 · depth 34

IsLocalization.Away 1

• Refining a basic open cover through localisations away IsLocalization.Away.exists_span_range_mul_eq_top_of_span_eq_top 0 below · cited by 2 · depth 29