Module

FiniteEtaleNilpotentEquivalence.lean

Nyll.EtaleFundamentalGroups.Purity.FiniteEtaleNilpotentEquivalence

2 declarations indexed from sourceView source ↗

Module documentation

Finite-etale equivalence across a nilpotent quotient

Over a complete Noetherian local ring, finite-etale algebras lift from every quotient by an ideal in the maximal ideal. For a nilpotent ideal, formal etaleness also lifts every morphism uniquely. Together these statements make finite-etale base change an equivalence of categories.

Imports2

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

finiteEtale_baseChange_isEquivalence_of_isNilpotent

L29 ↗

EtaleFundamentalGroups.finiteEtale_baseChange_isEquivalence_of_isNilpotent

Documentation

Finite-etale base change from a complete Noetherian local ring to a nilpotent quotient is an equivalence of categories.

Source context 4 commands

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

noncomputable section
open CategoryTheory IsLocalRing
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem finiteEtale_baseChange_isEquivalence_of_isNilpotent
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : IsNilpotent I) :
    (CommAlgCat.FiniteEtale.baseChange.{u} R (R ⧸ I)).IsEquivalence

def

finiteEtale_baseChange_equivalence_of_isNilpotent

L49 ↗

EtaleFundamentalGroups.finiteEtale_baseChange_equivalence_of_isNilpotent