Module

CompleteRegularLocalPurity.lean

Nyll.EtaleFundamentalGroups.Purity.Local.CompleteRegularLocalPurity

1 declaration indexed from sourceView source ↗

Module documentation

Purity for complete regular local rings

Regularity supplies both integral closedness and a generating regular system of parameters, giving punctured purity without either as an extra hypothesis.

Imports3

Imported by2

theorem

hasPuncturedPurity_of_complete_isRegularLocalRing

L25 ↗

EtaleFundamentalGroups.hasPuncturedPurity_of_complete_isRegularLocalRing

Documentation

A complete regular local ring of dimension at least two has punctured purity.

Source context 3 commands

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

namespace EtaleFundamentalGroups
open IsLocalRing
universe u

Lean source · statement

theorem hasPuncturedPurity_of_complete_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (hdim : 2 ≤ ringKrullDim R) :
    AlgebraicGeometry.FiniteEtale.HasPuncturedPurity R

Module documentation

Purity for complete regular local rings

Declarations

hasPuncturedPurity_of_complete_isRegularLocalRing