Theorems · Definition · commutative algebra

Localization.AtPrime.algebra_localization_localization

{R : Type u_1} →
  (S : Type u_2) →
    (T : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              {P : Ideal R} →
                [inst_4 : P.IsPrime] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : Algebra R T] →
                      [IsScalarTower R S T] →
                        Algebra (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
                          (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

Let R ⊆ S ⊆ T be a tower of rings. Let Sₚ and Tₚ denote the localizations of S and T at the prime ideal P of R. Then Tₚ is a Sₚ-algebra. This cannot be an instance since it creates a diamond when S = T.

Defined in

Mathlib.RingTheory.DedekindDomain.Instances

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraIdeal.IsPrimeAlgebraAlgebraIsScalarTower