Theorems · Inductive type · commutative algebra

Localization.AtPrime.IsLiesOverAlgebra

{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)] → Prop

A predicate expressing that Localization.AtPrime P is an algebra over Localization.AtPrime p in the natural way when P lies over p.

Defined in

Mathlib.RingTheory.Localization.AtPrime.Basic

Cited by

23 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIdeal.IsPrimeIdeal.IsPrimeIdeal.LiesOverAlgebra