Integral closure in a finite product

An element of a finite product of algebras is integral exactly when each coordinate is integral. Consequently, integral closure commutes with finite products. This comparison allows normalization and étaleness questions for finite products of fields to be checked on the individual field factors.

The finiteness assumption is essential: the integral equations for infinitely many coordinates need not have a common degree or common coefficients.

@[simp]

theorem TauCeti.isIntegral_pi_iff {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] {B : ι → Type u_3} [(i : ι) → Ring (B i)] [(i : ι) → Algebra R (B i)] {x : (i : ι) → B i} : IsIntegral R x ↔ ∀ (i : ι), IsIntegral R (x i)

A tuple in a finite product of algebras is integral if and only if every coordinate is integral. A common monic equation is the product of the coordinate equations.

def TauCeti.integralClosurePiAlgEquiv (R : Type u_1) [CommRing R] {ι : Type u_2} [Finite ι] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [(i : ι) → Algebra R (B i)] : ↥(integralClosure R ((i : ι) → B i)) ≃ₐ[R] (i : ι) → ↥(integralClosure R (B i))

Integral closure commutes with finite products, by taking coordinates of integral tuples.

@[simp]

theorem TauCeti.integralClosurePiAlgEquiv_apply (R : Type u_1) [CommRing R] {ι : Type u_2} [Finite ι] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [(i : ι) → Algebra R (B i)] (x : ↥(integralClosure R ((i : ι) → B i))) (i : ι) : ↑((integralClosurePiAlgEquiv R B) x i) = ↑x i

The product comparison takes an integral tuple to its coordinates.

@[simp]

theorem TauCeti.integralClosurePiAlgEquiv_symm_apply (R : Type u_1) [CommRing R] {ι : Type u_2} [Finite ι] (B : ι → Type u_3) [(i : ι) → CommRing (B i)] [(i : ι) → Algebra R (B i)] (x : (i : ι) → ↥(integralClosure R (B i))) (i : ι) : ↑((integralClosurePiAlgEquiv R B).symm x) i = ↑(x i)

The inverse product comparison assembles the coordinates into an integral tuple.