Theorems · Definition · commutative algebra

Localization.AtPrime.algebraOfLiesOver

{A : Type u_4} →
  {B : Type u_5} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        [inst_2 : Algebra A B] →
          (p : Ideal A) →
            [inst_3 : p.IsPrime] →
              (P : Ideal B) →
                [inst_4 : P.IsPrime] → [P.LiesOver p] → Algebra (Localization.AtPrime p) (Localization.AtPrime P)

If P lies over p, then Localization.AtPrime P is an algebra over Localization.AtPrime p. This is not an instance for performance reasons and to avoid diamonds in the situation where the top ring is already an algebra over Localization.AtPrime p (e.g., this happens for Ideal.Fiber).

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

30 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOver