Module

UnramifiedNormalBase.lean

Nyll.EtaleFundamentalGroups.Normalization.UnramifiedNormalBase

1 declaration indexed from sourceView source ↗

Module documentation

Dominant unramified domains over normal domains

An unramified algebra which is a domain faithful over a normal domain is étale. The local structure of unramified algebras presents principal opens as quotients of standard étale algebras. Their dominant domain quotients are étale, and locality on the target gives the conclusion, including finite presentation.

Imports3

Nyll.EtaleFundamentalGroups.Normalization.EtaleDominantQuotient
Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.Unramified.LocalStructure

Imported by5

theorem

etale_of_unramified_of_domain_of_faithful

L30 ↗

EtaleFundamentalGroups.etale_of_unramified_of_domain_of_faithful

Documentation

An unramified domain faithful over a normal domain is étale. Finite presentation is obtained from the local standard étale quotient presentations, rather than assumed.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem etale_of_unramified_of_domain_of_faithful
    {R B : Type u}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing B] [IsDomain B] [Algebra R B] [FaithfulSMul R B]
    [Algebra.FiniteType R B] [Algebra.FormallyUnramified R B] :
    Algebra.Etale R B

Module documentation

Dominant unramified domains over normal domains

Declarations

etale_of_unramified_of_domain_of_faithful