NYLL
Module

AffinizationExtension.lean

Nyll.SchemeTheory.FiniteEtale.AffinizationExtension
2 declarations indexed from sourceView source ↗

Module documentation

Finite étale extension by affinization

A finite étale cover of an open subscheme is the restriction of its affinization once that affinization is an open immersion and its section algebra is finite étale. Density of the canonical affinization and properness of the comparison with the restricted finite cover prove surjectivity.

Imports8
Imported by3

Declarations

theorem

exists_finiteEtale_extension_of_open_affinization

L35 ↗
AlgebraicGeometry.exists_finiteEtale_extension_of_open_affinization
Documentation

Finite étale sections and an open affinization produce an actual extension of a finite étale cover across the ambient affine scheme.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem exists_finiteEtale_extension_of_open_affinization
    {S W : Scheme.{u}} [IsAffine S] [CompactSpace W]
    (U : S.Opens) (f : W ⟶ U) [IsFiniteEtale f]
    [IsOpenImmersion W.toSpecΓ]
    (h : (f ≫ U.ι).appTop.hom.FiniteEtale) :
    ∃ V : FiniteEtale S,
      Nonempty ((FiniteEtale.pullback U.ι).obj V ≅ FiniteEtale.mk f)
theorem

exists_finiteEtale_extension_of_flat_baseChange

L78 ↗
AlgebraicGeometry.exists_finiteEtale_extension_of_flat_baseChange
Documentation

An extension after affine faithfully flat base change descends when the extending open immersion preserves global sections.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem exists_finiteEtale_extension_of_flat_baseChange
    {S T W V : Scheme.{u}} [IsAffine S] [IsAffine T] [CompactSpace W]
    (U : S.Opens) [QuasiCompact U.ι]
    (f : W ⟶ U) [IsFiniteEtale f]
    (g : T ⟶ S) [Flat g] [Surjective g]
    (p : V ⟶ T) [IsFiniteEtale p]
    (j : pullback (f ≫ U.ι) g ⟶ V) [IsOpenImmersion j] [IsIso j.appTop]
    (hj : j ≫ p = pullback.snd (f ≫ U.ι) g) :
    ∃ Z : FiniteEtale S,
      Nonempty ((FiniteEtale.pullback U.ι).obj Z ≅ FiniteEtale.mk f)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.