Theorems · Definition · commutative algebra

Localization.localAlgHom

{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

For an R-algebra homomorphism f : S →ₐ[R] P and prime ideals I = f⁻¹(J), the induced R-algebra homomorphism from the localization of S at I to the localization of P at J. See localAlgHom' for a variant where the base ring R is also localized.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrime