Theorems · Theorem · commutative algebra

Polynomial.isIntegral_isLocalization_polynomial_quotient

∀ {R : Type u_1} [inst : CommRing R] {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_1 : CommRing Rₘ] [inst_2 : CommRing Sₘ]
  (P : Ideal (Polynomial R)),
  ∀ pX ∈ P,
    ∀ [inst_3 : Algebra (R ⧸ Ideal.comap Polynomial.C P) Rₘ]
      [inst_4 :
        IsLocalization.Away (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ]
      [inst_5 : Algebra (Polynomial R ⧸ P) Sₘ]
      [inst_6 :
        IsLocalization
          (Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯)
            (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff))
          Sₘ],
      (IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral

If I is a prime ideal of R[X] and pX ∈ I is a non-constant polynomial, then the map R →+* R[x]/I descends to an integral map when localizing at pX.leadingCoeff. In particular X is integral because it satisfies pX, and constants are trivially integral, so integrality of the entire extension follows by closure under addition and multiplication.

Defined in

Mathlib.RingTheory.Jacobson.Ring

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraIsLocalization.AwayAlgebraIsLocalization