NYLL
Module

RegularLocalCompletionDescent.lean

Nyll.EtaleFundamentalGroups.Purity.Local.RegularLocalCompletionDescent
1 declaration indexed from sourceView source ↗

Module documentation

Punctured purity descends from the maximal-adic completion

The completed extension preserves global sections by the prime-pair Hartogs theorem. Flat base change then descends its finite étale section algebra and the open immersion into its affinization. The original cover is recovered as the restriction of this finite étale affinization.

Imports10
Imported by3

Declarations

theorem

hasPuncturedPurity_of_isRegularLocalRing

L36 ↗
EtaleFundamentalGroups.hasPuncturedPurity_of_isRegularLocalRing
Documentation

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

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits AlgebraicGeometry IsLocalRing TopologicalSpace
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem hasPuncturedPurity_of_isRegularLocalRing
    (R : Type u) [CommRing R] [IsRegularLocalRing R]
    (hdim : 2 ≤ ringKrullDim R) : FiniteEtale.HasPuncturedPurity R

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