Module

EtaleLocalNormality.lean

Nyll.SchemeTheory.RingTheory.Descent.EtaleLocalNormality

1 declaration indexed from sourceView source ↗

Module documentation

Local normality under an etale algebra

Only the local ring of the base at the contracted prime is assumed normal. Localizing the etale algebra over that ring and then at the lifted prime gives the original local ring, through the actual localization comparison.

Imports4

Nyll.SchemeTheory.RingTheory.Descent.EtaleAtPrimeNormality
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Localization.LocalizationLocalization

Imported by2

theorem

isDomain_and_isIntegrallyClosed_atPrime_of_etale

L28 ↗

SchemeTheory.isDomain_and_isIntegrallyClosed_atPrime_of_etale

Documentation

Normality of the base local ring ascends to the local ring of an etale algebra. The original base ring need not be a domain or normal.

Source context 3 commands

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

noncomputable section
namespace SchemeTheory
universe u

Lean source · statement

theorem isDomain_and_isIntegrallyClosed_atPrime_of_etale
    (R C : Type u) [CommRing R] [CommRing C] [Algebra R C] [Algebra.Etale R C]
    (q : Ideal C) [q.IsPrime]
    [IsDomain (Localization.AtPrime (q.under R))]
    [IsIntegrallyClosed (Localization.AtPrime (q.under R))] :
    IsDomain (Localization.AtPrime q) ∧ IsIntegrallyClosed (Localization.AtPrime q)

Module documentation

Local normality under an etale algebra

Declarations

isDomain_and_isIntegrallyClosed_atPrime_of_etale