Documentation

TauCeti.RingTheory.IntegralClosure.PowRelation

Integrality as an explicit monic relation of positive degree #

IsIntegral S x says a monic polynomial over S kills x. For arguments that adjust the coefficients one at a time it is more convenient to have the relation written out, and written so that its degree is visibly positive:

x ^ (n + 1) + ∑ i ∈ Finset.range (n + 1), c i * x ^ i = 0,   with `c i ∈ S` for `i < n + 1`.

This file gives that form and its converse. Both directions are pure ring theory — no topology appears — and they are stated for a subring of an arbitrary commutative ring.

Writing the degree as n + 1 rather than carrying a separate 0 < p.natDegree hypothesis is what lets a caller perturb the constant coefficient without disturbing the leading one, which is the shape Huber's approximation arguments need.

Main results #

source
theorem TauCeti.exists_pow_add_sum_eq_zero_of_isIntegral {R : Type u_1} [CommRing R] {S : Subring R} {x : R} (hx : IsIntegral (↥S) x) :
∃ (n : ℕ) (c : ℕ → R), (∀ i < n + 1, c i ∈ S) ∧ x ^ (n + 1) + ∑ i ∈ Finset.range (n + 1), c i * x ^ i = 0

An element integral over a subring S satisfies a monic relation of positive degree whose coefficients lie in S. Membership is asserted only on i < n + 1, the range the relation sums over; a caller reading off coefficients gets no promise about the tail and needs none. Writing the degree as n + 1 builds the positivity into the shape, which is what lets the constant coefficient be adjusted without disturbing the leading one.

source
theorem TauCeti.isIntegral_of_pow_add_sum_eq_zero {R : Type u_1} [CommRing R] {S : Subring R} {x : R} {n : ℕ} {c : ℕ → R} (hcS : ∀ i < n + 1, c i ∈ S) (h : x ^ (n + 1) + ∑ i ∈ Finset.range (n + 1), c i * x ^ i = 0) :
IsIntegral (↥S) x

The converse of TauCeti.exists_pow_add_sum_eq_zero_of_isIntegral: a monic relation of positive degree with coefficients in a subring S exhibits its root as integral over S. Only the coefficients actually summed over, i < n + 1, are required to lie in S.