Integrality over an algebra, tested on quotients

A failure of x : R to be integral over A is already a failure modulo a prime ideal of R. That is what this file proves, together with the elementary description of integrality in a quotient that the argument runs on: x becomes integral over A in R ⧸ J exactly when some monic polynomial over A sends x into J.

The point of reaching a prime is that R ⧸ J is then a domain. So a theorem about integral elements proved only for domains extends to an arbitrary commutative ring, as long as its hypothesis survives pulling back along Ideal.Quotient.mk J. The valuative criterion TauCeti.isIntegral_of_forall_valuation_le_one — the hard direction of Wedhorn's Proposition 7.18 — is such a theorem, and is what this file was written for.

Main results

• TauCeti.isIntegral_quotient_iff : integrality of x over A after passing to R ⧸ J is the statement that some monic polynomial over A sends x into J.
• TauCeti.isIntegral_of_forall_isPrime : if x becomes integral over A in every prime quotient of R, then it is integral over A.
• TauCeti.isIntegral_of_forall_isPrime_map : the same for a subring B ⊆ R, phrased with the image subring B.map (Ideal.Quotient.mk J) that a criterion quantifying over subrings of R ⧸ J needs.

The first of these needs only a ring and a two-sided ideal; commutativity enters with the prime, so the other two ask for it.

Mathlib's integrality-in-a-quotient lemmas, RingHom.IsIntegral.quotient and isIntegral_quotientMap_iff, say that a ring hom is integral, with source and target both quotiented. The criterion here is about a single element, keeps A unquotiented, and hands back the monic witness, which is what the argument below consumes.

Method

The statement is the positive one — integral in every prime quotient implies integral — and the argument runs on its contrapositive, which is where the prime comes from.

The values f(x) of monic polynomials f over A form a submonoid of R: monic polynomials are closed under multiplication and evaluation is multiplicative, and f = 1 gives the unit. Non-integrality of x says exactly that 0 is not one of those values — that the zero ideal is disjoint from the submonoid. Ideal.exists_le_prime_disjoint then supplies a prime ideal still disjoint from it, and isIntegral_quotient_iff reads that disjointness back as non-integrality in the quotient.

Packaging the monic values as a submonoid is the whole trick: the multiplicative closure Mathlib's Zorn argument needs is precisely "a product of monic polynomials is monic", so no bespoke maximality argument is required here, and no finiteness or noetherian hypothesis on R appears.

The subring form is a corollary rather than a separate argument. Only one direction of the comparison is needed — that integrality over the image subring implies integrality over B — and it holds because B surjects onto that image, so a monic polynomial over the image lifts to a monic polynomial over B.

Integrality after passing to a quotient

theorem TauCeti.isIntegral_quotient_iff {A : Type u_1} {R : Type u_2} [CommRing A] [Ring R] [Algebra A R] (x : R) (J : Ideal R) [J.IsTwoSided] : IsIntegral A ((Ideal.Quotient.mk J) x) ↔ ∃ (f : Polynomial A), f.Monic ∧ Polynomial.eval₂ (algebraMap A R) x f ∈ J

Integrality in a quotient is a monic polynomial landing in the ideal. The reduction of x is integral over A in R ⧸ J exactly when some monic polynomial over A sends x into J.

Non-integrality is witnessed modulo a prime

theorem TauCeti.isIntegral_of_forall_isPrime {A : Type u_1} {R : Type u_2} [CommRing A] [CommRing R] [Algebra A R] {x : R} (h : ∀ (J : Ideal R), J.IsPrime → IsIntegral A ((Ideal.Quotient.mk J) x)) : IsIntegral A x

Integrality is detected in the prime quotients. If the reduction of x is integral over A in R ⧸ J for every prime ideal J of R, then x is integral over A.

This is what lets a criterion for integrality that has been proved only for domains be applied to an arbitrary commutative ring: every R ⧸ J here is a domain, so the criterion supplies exactly the hypotheses this lemma consumes.

The subring form

theorem TauCeti.isIntegral_of_forall_isPrime_map {R : Type u_1} [CommRing R] {B : Subring R} {x : R} (h : ∀ (J : Ideal R), J.IsPrime → IsIntegral (↥(Subring.map (Ideal.Quotient.mk J) B)) ((Ideal.Quotient.mk J) x)) : IsIntegral (↥B) x

The subring form of isIntegral_of_forall_isPrime. If the reduction of x is integral over the image subring B.map (Ideal.Quotient.mk J) for every prime J of R, then x is integral over the subring B itself. The image subring is the shape a criterion that quantifies over subrings of R ⧸ J produces.