Module

AffineCompleteBaseChange.lean

Nyll.EtaleFundamentalGroups.Purity.AffineCompleteBaseChange

2 declarations indexed from sourceView source ↗

Module documentation

Finite étale covers under complete affine base change

Quotient base change for finite étale algebras over a complete Noetherian local ring is transported across the affine finite étale equivalence. This gives the corresponding equivalence for finite étale covers of affine schemes.

Imports2

Imported by2

theorem

finiteEtale_pullback_isEquivalence_of_complete_quotient

L28 ↗

EtaleFundamentalGroups.finiteEtale_pullback_isEquivalence_of_complete_quotient

Documentation

Pullback along Spec (R ⧸ I) ⟶ Spec R is an equivalence on finite étale covers when R is a complete Noetherian local ring and I is contained in its maximal ideal.

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_pullback_isEquivalence_of_complete_quotient
    {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    [IsAdicComplete (maximalIdeal R) R]
    (I : Ideal R) (hI : I ≤ maximalIdeal R) :
    (AlgebraicGeometry.FiniteEtale.pullback
      (AlgebraicGeometry.Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk I)))).IsEquivalence

def

finiteEtale_pullback_equivalence_of_complete_quotient

L58 ↗

EtaleFundamentalGroups.finiteEtale_pullback_equivalence_of_complete_quotient