Theorems · Theorem · commutative algebra

exists_derivative_mul_eq_and_isIntegral_coeff

∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {φ : Polynomial S →ₐ[R] B},
  Function.Surjective ⇑φ →
    ∀ {f : Polynomial S},
      f.Monic →
        (∀ (i : ℕ), IsIntegral R (f.coeff i)) →
          RingHom.ker φ.toRingHom = Ideal.span {f} →
            ∀ {y : B}, IsIntegral R y → ∃ g, φ (Polynomial.derivative f) * y = φ g ∧ ∀ (i : ℕ), IsIntegral R (g.coeff i)

Let S be an R-algebra and f : S[X] be a monic polynomial with R-integral coefficients. Suppose y in B = S[X]/f is R-integral, then f' * y is the image of some g : S[X] with R-integral coefficients.

Defined in

Mathlib.RingTheory.Smooth.IntegralClosure

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebra