Module

PuncturedSpectrumFiniteEtaleDescent.lean

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumFiniteEtaleDescent

2 declarations indexed from sourceView source ↗

Module documentation

Finite-etale descent over the directed punctured-spectrum cover

A cartesian scheme diagram over the directed finite principal-open cover is already effective by relative gluing. This file proves that when its chart maps are finite etale, the resulting glued morphism is finite etale as well.

Imports1

Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumDirectedRefinement

Imported by1

Nyll.EtaleFundamentalGroups.Purity.All

theorem

isFiniteEtale_toBase_of_puncturedSpectrumRelativeGluingData

L29 ↗

AlgebraicGeometry.Scheme.isFiniteEtale_toBase_of_puncturedSpectrumRelativeGluingData

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable (R : Type u) [CommRing R] [IsLocalRing R]

/- A cartesian diagram of finite-etale morphisms on the directed principal
cover glues to a finite-etale morphism over the punctured spectrum. -/

Lean source · statement

theorem isFiniteEtale_toBase_of_puncturedSpectrumRelativeGluingData
    (d : Cover.RelativeGluingData
      (puncturedSpectrumDirectedOpenCover R))
    (hfinite : ∀ s, IsFiniteEtale (d.natTrans.app s)) :
    IsFiniteEtale d.toBase

def

finiteEtaleOfPuncturedSpectrumRelativeGluingData

L59 ↗

AlgebraicGeometry.Scheme.finiteEtaleOfPuncturedSpectrumRelativeGluingData

Documentation

The finite-etale cover obtained from an actual cartesian finite-etale diagram on the directed principal-open cover.