Module

IntegralClosureSplitProduct.lean

Nyll.SchemeTheory.RingTheory.IntegralClosureSplitProduct

2 declarations indexed from sourceView source ↗

Module documentation

Normalization of a split finite generic algebra

If the base ring is integrally closed in an ambient algebra, its integral closure in a finite product of copies of that algebra is the same finite product of the base ring. Coordinate evaluation supplies every integral coordinate; conversely a finite product of copies of the base is finite, so all of its elements are integral. This also proves that this actual integral closure is étale over the base.

Imports5

Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Mathlib.Algebra.Algebra.Pi
Mathlib.RingTheory.Finiteness.Prod
Mathlib.RingTheory.Etale.Pi

Imported by2

def

integralClosureSplitProductEquiv

L31 ↗

SchemeTheory.integralClosureSplitProductEquiv

Documentation

Normalize a split finite product by normalizing each actual coordinate.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace SchemeTheory
universe u v w

Lean source · statement

def integralClosureSplitProductEquiv
    (R : Type u) (K : Type v) (ι : Type w)
    [CommRing R] [CommRing K] [Algebra R K]
    [IsIntegrallyClosedIn R K] [Finite ι] :
    integralClosure R (ι → K) ≃ₐ[R] (ι → R)

theorem

integralClosure_splitProduct_etale

L55 ↗

SchemeTheory.integralClosure_splitProduct_etale