Module

Thickening.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.Thickening

2 declarations indexed from sourceView source ↗

Module documentation

Invariance of finite étale covers under thickenings

A thickening is a surjective closed immersion. The affine equivalence for nil ideals supplies unique local lifts of maps and finite étale objects. Gluing on the directed affine cover gives the equivalence for arbitrary schemes, without a uniform nilpotence bound or a quasicompactness assumption.

Imports3

Nyll.SchemeTheory.FiniteEtale.ThickeningFullyFaithful
Nyll.SchemeTheory.FiniteEtale.ThickeningGluing
Mathlib.CategoryTheory.Equivalence

Imported by2

instance

finiteEtaleInfStableUnderBaseChangeThickeningExport

L30 ↗

AlgebraicGeometry.FiniteEtale.finiteEtaleInfStableUnderBaseChangeThickeningExport

Source context 4 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale

Lean source · statement

instance finiteEtaleInfStableUnderBaseChangeThickeningExport :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale)

theorem

pullback_isEquivalence_of_surjective_closedImmersion

L37 ↗

AlgebraicGeometry.FiniteEtale.pullback_isEquivalence_of_surjective_closedImmersion

Documentation

Pullback across any thickening is an equivalence on finite étale covers.

Source context 5 commands

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

@[expose] public section
open CategoryTheory
universe u
namespace AlgebraicGeometry.FiniteEtale
local instance finiteEtaleInfStableUnderBaseChangeThickeningExport :
    MorphismProperty.IsStableUnderBaseChange
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) :=
  MorphismProperty.IsStableUnderBaseChange.inf

Lean source · full declaration

theorem pullback_isEquivalence_of_surjective_closedImmersion
    {X Y : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i] [Surjective i] :
    (MorphismProperty.Over.pullback
      ((@IsFinite : MorphismProperty Scheme.{u}) ⊓ @Etale) ⊤ i).IsEquivalence where
  faithful := pullback_faithful_of_surjective_closedImmersion i
  full := pullback_full_of_surjective_closedImmersion i
  essSurj := pullback_essSurj_of_surjective_closedImmersion i

Module documentation

Invariance of finite étale covers under thickenings

Declarations

finiteEtaleInfStableUnderBaseChangeThickeningExport

pullback_isEquivalence_of_surjective_closedImmersion