Theorems · Definition · commutative algebra

Localization.localAlgEquiv

{R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              [inst_4 : Algebra R P] →
                (I : Ideal S) →
                  [inst_5 : I.IsPrime] →
                    (J : Ideal P) →
                      [inst_6 : J.IsPrime] →
                        (f : S ≃ₐ[R] P) → I = Ideal.comap f J → Localization.AtPrime I ≃ₐ[R] Localization.AtPrime J

Isomorphic algebras have isomorphic localizations. See localAlgEquiv' for a variant where the base ring is also localized.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

3 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrime