Theorems · Theorem · commutative algebra
isIntegral_localization
∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
{Rₘ : Type u_3} {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
[inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[Algebra.IsIntegral R S], (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralIf R → S is an integral extension, M is a submonoid of R,
Rₘ is the localization of R at M,
and Sₘ is the localization of S at the image of M under the extension map,
then the induced map Rₘ → Sₘ is also an integral extension
- Defined in
- Mathlib.RingTheory.Localization.Integral
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites28
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomstatement and proof · cited by 10,189
- SetLike.coeproof · cited by 8,199
- Polynomialproof · cited by 5,681
- Algebra.algebraMapstatement and proof · cited by 4,706
- Submonoidstatement and proof · cited by 3,086
- map_mulproof · cited by 1,137
- map_oneproof · cited by 861
- IsLocalizationstatement and proof · cited by 636
- Polynomial.Monicproof · cited by 461
Cited by4
Results whose statement or proof uses this declaration.
- Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomainproof · cited by 2
- IsLocalization.OverPrime.mem_normalizedFactors_of_isPrimeproof · cited by 1
- Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐproof · cited by 1
- isIntegral_localization'proof · cited by 0