NYLL
Module

EtaleLocalIrreducibilityOfIntegralNormalExtension.lean

Nyll.SchemeTheory.RingTheory.Descent.EtaleLocalIrreducibilityOfIntegralNormalExtension
1 declaration indexed from sourceView source ↗

Module documentation

Irreducibility of local étale neighborhoods from normalization data

The same actual normal base change used in the domain theorem also handles nonreduced local rings. Flatness carries a nilpotent kernel to a nilpotent kernel; embedding modulo that kernel into the constructed normal domain proves that the nilradical of the original local étale neighborhood is prime.

Imports6
Imported by2

Declarations

theorem

nilradical_isPrime_atPrime_of_etale_of_integral_normal_extension

L35 ↗
SchemeTheory.nilradical_isPrime_atPrime_of_etale_of_integral_normal_extension
Documentation

A local étale neighborhood has a prime nilradical when the base maps integrally and locally to a normal local domain with purely inseparable residue field and a kernel consisting of nilpotents.

Source context 5 commands

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

noncomputable section
open scoped TensorProduct
open IsLocalRing
namespace SchemeTheory
universe u
Lean source · statement
theorem nilradical_isPrime_atPrime_of_etale_of_integral_normal_extension
    (R N C : Type u)
    [CommRing R] [IsLocalRing R]
    [CommRing N] [IsLocalRing N] [IsDomain N] [IsIntegrallyClosed N]
    [Algebra R N] [Algebra.IsIntegral R N] [IsLocalHom (algebraMap R N)]
    [IsPurelyInseparable (ResidueField R) (ResidueField N)]
    (hker : RingHom.ker (algebraMap R N) ≤ nilradical R)
    [CommRing C] [Algebra R C] [Algebra.Etale R C]
    (q : Ideal C) [q.IsPrime]
    [IsLocalHom (algebraMap R (Localization.AtPrime q))] :
    (nilradical (Localization.AtPrime q)).IsPrime

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.