Integrally closed algebras and subrings

For a field k and a nontrivial commutative k-algebra A, being integrally closed in A means every element of A algebraic over k is a constant. An algebraically closed field is integrally closed in every domain algebra.

If R is integrally closed in A, divisibility in R can be tested on n-th powers by any element of R that becomes a unit in A: a quotient b / a in A whose n-th power lies in R is integral over R. This is the non-domain form of Mathlib's IsIntegrallyClosed.pow_dvd_pow_iff.

If x ∈ R is a nonzerodivisor and R ⧸ (x) is reduced, then R is integrally closed in its localization R[1/x]: if a / x is integral over R then a ^ n is divisible by x, so a is, and one removes the powers of x from a denominator one at a time. For instance, this applies to the root y of A[y] ⧸ (y ^ e - f) for e ≥ 1, a nonzerodivisor f and a reduced A ⧸ (f): the quotient by y is A ⧸ (f).

If a subring S of B is integrally closed in B, then its preimage under a ring homomorphism f : A → B is integrally closed in A: an element of A integral over the preimage is sent by f to an element integral over S, which therefore lies in S. Conversely, a surjective ring homomorphism carries an integrally closed subring containing its kernel to an integrally closed subring: lift a monic integral equation, whose evaluation then lies in the kernel.

Main results

• TauCeti.isIntegrallyClosedIn_iff_forall_isAlgebraic: the elementwise criterion for a field to be integrally closed in a nontrivial commutative algebra.
• IsIntegrallyClosedIn.transcendental_of_notMem_span_one: if a field is integrally closed in a nontrivial algebra, every element outside the line spanned by 1 is transcendental.
• TauCeti.isIntegrallyClosedIn_of_isAlgClosed: an algebraically closed field is integrally closed in every domain algebra.
• IsIntegrallyClosedIn.pow_dvd_pow_iff: for a ∈ R invertible in A and n ≠ 0, a ^ n ∣ b ^ n ↔ a ∣ b in R.
• IsIntegrallyClosedIn.of_ringEquiv: transport along a semilinear ring isomorphism.
• IsIntegrallyClosedIn.of_isLocalization_of_le_powers: R is integrally closed in its localization at any submonoid of the powers of a nonzerodivisor x with R ⧸ (x) reduced.
• IsIntegrallyClosedIn.of_isLocalization_away: the case of the localization R[1/x].
• Subring.isIntegrallyClosedIn_comap: the preimage of an integrally closed subring is integrally closed.
• Subring.isIntegrallyClosedIn_map_of_ker_le: a surjective ring homomorphism carries an integrally closed subring containing its kernel to an integrally closed subring.
• Subring.mem_of_pow_mem_of_isIntegrallyClosedIn: a subring integrally closed in A contains every element some positive power of which it contains.

theorem TauCeti.isIntegrallyClosedIn_iff_forall_isAlgebraic {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] [Nontrivial A] : IsIntegrallyClosedIn k A ↔ ∀ (x : A), IsAlgebraic k x → ∃ (c : k), (algebraMap k A) c = x

A field k is integrally closed in a nontrivial commutative k-algebra A exactly when every element of A algebraic over k lies in the image of k.

theorem TauCeti.isIntegrallyClosedIn_of_isAlgClosed {k : Type u_1} {A : Type u_2} [Field k] [CommRing A] [Algebra k A] [IsAlgClosed k] [IsDomain A] : IsIntegrallyClosedIn k A

An algebraically closed field is integrally closed in every domain algebra.

theorem IsIntegrallyClosedIn.pow_dvd_pow_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] {n : ℕ} (hn : n ≠ 0) {a b : R} (ha : IsUnit ((algebraMap R A) a)) : a ^ n ∣ b ^ n ↔ a ∣ b

If R is integrally closed in A and a ∈ R is a unit in A, then for n ≠ 0, a ^ n divides b ^ n in R exactly when a divides b in R. Compare IsIntegrallyClosed.pow_dvd_pow_iff, which asks R to be a domain integrally closed in its fraction field.

theorem IsIntegrallyClosedIn.transcendental_of_notMem_span_one {K : Type u_3} {B : Type u_4} [Field K] [CommRing B] [Algebra K B] [Nontrivial B] (hex : IsIntegrallyClosedIn K B) {u : B} (hu : u ∉ K ∙ 1) : Transcendental K u

If k is integrally closed in A, an element of A outside the line k ∙ 1 is transcendental over k.

theorem IsIntegrallyClosedIn.of_ringEquiv {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {S : Type u_3} {B : Type u_4} [CommRing S] [CommRing B] [Algebra S B] (h : IsIntegrallyClosedIn R A) (σ : R ≃+* S) (τ : A ≃+* B) (hτ : ∀ (r : R), τ ((algebraMap R A) r) = (algebraMap S B) (σ r)) : IsIntegrallyClosedIn S B

Integral closedness is invariant under semilinear isomorphisms: if τ : A ≃+* B carries the image of R onto the image of S along σ : R ≃+* S, and R is integrally closed in A, then S is integrally closed in B. Over the identity of R this is AlgEquiv.isIntegrallyClosedIn.

theorem IsIntegrallyClosedIn.of_isLocalization_of_le_powers {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : R} (hx : x ∈ nonZeroDivisors R) [IsReduced (R ⧸ Ideal.span {x})] (M : Submonoid R) (hM : M ≤ Submonoid.powers x) [IsLocalization M A] : IsIntegrallyClosedIn R A

A ring is integrally closed in its localization at a nonzerodivisor with reduced quotient. If x ∈ R is a nonzerodivisor and R ⧸ (x) is reduced, then R is integrally closed in its localization A at any submonoid M of the powers of x, such as the powers of x ^ e.

theorem IsIntegrallyClosedIn.of_isLocalization_away {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {x : R} (hx : x ∈ nonZeroDivisors R) [IsReduced (R ⧸ Ideal.span {x})] [IsLocalization.Away x A] : IsIntegrallyClosedIn R A

If x ∈ R is a nonzerodivisor and R ⧸ (x) is reduced, then R is integrally closed in its localization away from x.

instance Subring.isIntegrallyClosedIn_comap {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (f : A →+* B) (S : Subring B) [IsIntegrallyClosedIn (↥S) B] : IsIntegrallyClosedIn (↥(comap f S)) A

The preimage of an integrally closed subring is integrally closed: if S is integrally closed in B, then S.comap f is integrally closed in A for every ring homomorphism f : A →+* B.

theorem Subring.mem_of_pow_mem_of_isIntegrallyClosedIn {A : Type u_1} [CommRing A] {S : Subring A} [IsIntegrallyClosedIn (↥S) A] {a : A} {n : ℕ} (hn : 0 < n) (ha : a ^ n ∈ S) : a ∈ S

A subring S integrally closed in A contains every element a some positive power of which lies in S, as a is then integral over S.

theorem Subring.isIntegrallyClosedIn_map_of_ker_le {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] (S : Subring A) [IsIntegrallyClosedIn (↥S) A] (f : A →+* B) (hf : Function.Surjective ⇑f) (hker : ↑(RingHom.ker f) ⊆ ↑S) : IsIntegrallyClosedIn (↥(map f S)) B

A surjective ring homomorphism carries an integrally closed subring to an integrally closed subring if its kernel is contained in that subring.