Module

FiniteProduct.lean

Nyll.SchemeTheory.Normalization.IntegralClosure.FiniteProduct

5 declarations indexed from sourceView source ↗

Module documentation

Integral closure in a finite product

Completion of a finite separable field extension splits its generic fibre as a finite product of completed fields. To aggregate local normalization statements one needs the corresponding integral closure to split coordinatewise. This file proves that comparison directly from monic equations. For a reduced Artinian algebra, its canonical product of maximal-ideal quotients then gives the corresponding product decomposition of its integral closure.

Imports7

Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.Polynomial.Monic
Mathlib.RingTheory.Artinian.Module
Mathlib.RingTheory.Etale.Pi
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Mathlib.RingTheory.Spectrum.Maximal.Basic

Imported by5

theorem

isIntegral_pi_iff

L35 ↗

EtaleFundamentalGroups.isIntegral_pi_iff

Documentation

An element of a finite product is integral exactly when all of its coordinates are integral. The reverse implication uses the product of one monic annihilating polynomial for each coordinate.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uI uA

Lean source · statement

theorem isIntegral_pi_iff
    {R : Type uR} {I : Type uI} {A : I → Type uA}
    [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [Finite I] (x : ∀ i, A i) :
    IsIntegral R x ↔ ∀ i, IsIntegral R (x i)

def

integralClosurePiAlgEquiv

L60 ↗

EtaleFundamentalGroups.integralClosurePiAlgEquiv

Documentation

Integral closure commutes with finite products, with the canonical coordinate maps on the nose.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uI uA

Lean source · statement

def integralClosurePiAlgEquiv
    {R : Type uR} {I : Type uI} (A : I → Type uA)
    [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [Finite I] :
    integralClosure R (∀ i, A i) ≃ₐ[R]
      (∀ i, integralClosure R (A i))

theorem

integralClosurePiAlgEquiv_apply

L88 ↗

EtaleFundamentalGroups.integralClosurePiAlgEquiv_apply

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uI uA

Lean source · statement

theorem integralClosurePiAlgEquiv_apply
    {R : Type uR} {I : Type uI} (A : I → Type uA)
    [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [Finite I] (x : integralClosure R (∀ i, A i)) (i : I) :
    ((integralClosurePiAlgEquiv A x i : integralClosure R (A i)) : A i) =
      (x : ∀ i, A i) i

theorem

integralClosure_pi_etale

L98 ↗

EtaleFundamentalGroups.integralClosure_pi_etale

Documentation

If every completed field factor has étale normalization, then the normalization in their finite product is étale as well.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uI uA

Lean source · statement

theorem integralClosure_pi_etale
    {R : Type uR} {I : Type uI} (A : I → Type uA)
    [CommRing R] [∀ i, CommRing (A i)] [∀ i, Algebra R (A i)]
    [Finite I]
    [∀ i, Algebra.Etale R (integralClosure R (A i))] :
    Algebra.Etale R (integralClosure R (∀ i, A i))

def

integralClosureFactorsEquiv

L117 ↗

SchemeTheory.integralClosureFactorsEquiv

Documentation

The normalization of a reduced Artinian algebra is the product of the normalizations in its actual maximal-ideal quotients. The algebra structures are the canonical quotient and coordinatewise structures, with scalars restricted from the Artinian algebra to the original base ring.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u v

Lean source · statement

def integralClosureFactorsEquiv
    (R : Type u) (A : Type v) [CommRing R] [CommRing A] [Algebra R A]
    [IsArtinianRing A] [IsReduced A] :
    integralClosure R A ≃ₐ[R]
      ∀ m : MaximalSpectrum A, integralClosure R (A ⧸ m.asIdeal)

Module documentation

Integral closure in a finite product

Declarations

isIntegral_pi_iff

integralClosurePiAlgEquiv

integralClosurePiAlgEquiv_apply

integralClosure_pi_etale

integralClosureFactorsEquiv