Theorems · Theorem · commutative algebra

is_integral_localization_at_leadingCoeff

∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {Rₘ : Type u_3} {Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : CommRing Sₘ] [inst_5 : Algebra R Rₘ]
  [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
  {x : S} (p : Polynomial R),
  (Polynomial.aeval x) p = 0 →
    p.leadingCoeff ∈ M → (IsLocalization.map Sₘ (algebraMap R S) ⋯).IsIntegralElem ((algebraMap S Sₘ) x)

Given a particular witness to an element being algebraic over an algebra R → S, We can localize to a submonoid containing the leading coefficient to make it integral. Explicitly, the map between the localizations will be an integral ring morphism

Defined in

Mathlib.RingTheory.Localization.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraIsLocalizationAlgebraIsLocalization