Module

FiniteEtaleQuotientBaseChange.lean

Nyll.EtaleFundamentalGroups.Purity.FiniteEtaleQuotientBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Essential surjectivity of finite-etale base change to a quotient

For a complete Noetherian local ring, every finite-etale algebra over a quotient by an ideal in the maximal ideal comes by base change from the original ring. This file packages the algebraic lifting theorem as the canonical categorical EssSurj statement for finite-etale algebras.

Imports2

Nyll.EtaleFundamentalGroups.Purity.FiniteEtaleQuotientLift
Mathlib.RingTheory.Etale.Finite

Imported by3

theorem

finiteEtale_baseChange_essSurj_of_quotient

L30 ↗

EtaleFundamentalGroups.finiteEtale_baseChange_essSurj_of_quotient

Documentation

Finite-etale base change from a complete Noetherian local ring to any quotient by an ideal contained in the maximal ideal is essentially surjective.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open CategoryTheory IsLocalRing
universe u

Lean source · statement

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

Module documentation

Essential surjectivity of finite-etale base change to a quotient

Declarations

finiteEtale_baseChange_essSurj_of_quotient