NYLL
Module

EtaleLocalDomainOfIntegralNormalExtension.lean

Nyll.SchemeTheory.RingTheory.Descent.EtaleLocalDomainOfIntegralNormalExtension
2 declarations indexed from sourceView source ↗

Module documentation

Domains in local étale neighborhoods of a geometrically unibranch ring

The algebraic input is an actual injective integral local map into a normal local domain, with purely inseparable residue field extension. Base change of that extension along a local étale neighborhood is local. It is also a localization of an étale algebra over the normal domain, hence a domain. Flatness embeds the original local étale neighborhood into that domain.

For a reduced geometrically unibranch local ring, the integral closure in its fraction field supplies exactly these inputs. No domain assertion about the étale neighborhood or geometric stalk is assumed.

Imports4
Imported by3

Declarations

theorem

isDomain_of_etale_of_local_localization

L37 ↗
SchemeTheory.isDomain_of_etale_of_local_localization
Documentation

A localization of an étale algebra over a normal domain is a domain whenever that localization is a local ring.

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 isDomain_of_etale_of_local_localization
    (R C D : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing C] [Algebra R C] [Algebra.Etale R C]
    [CommRing D] [Algebra C D] [IsLocalRing D]
    (M : Submonoid C) [IsLocalization M D] : IsDomain D
theorem

isDomain_atPrime_of_etale_of_integral_normal_extension

L58 ↗
SchemeTheory.isDomain_atPrime_of_etale_of_integral_normal_extension
Documentation

An actual local étale neighborhood is a domain if the local base embeds integrally into a normal local domain with purely inseparable residue field.

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 isDomain_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)]
    (hinj : Function.Injective (algebraMap R N))
    [CommRing C] [Algebra R C] [Algebra.Etale R C]
    (q : Ideal C) [q.IsPrime]
    [IsLocalHom (algebraMap R (Localization.AtPrime q))] :
    IsDomain (Localization.AtPrime q)

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