NYLL
Module

FiniteRefinement.lean

Nyll.SchemeTheory.Etale.FiniteRefinement
1 declaration indexed from sourceView source ↗

Module documentation

Finite surjective refinements over a qcqs base

Start with the original surjective étale morphism. Its integral refinement supplies both the actual integral cover and its local factorizations. On finitely many affine base charts, finite subalgebras inside its actual direct-image algebra retain these factorizations. The proved finite quasicoherent submodule theorem contains all these actual section modules at once. Its generated relative algebra gives the finite model.

The original integral source maps to this model, proving surjectivity. The literal chart subalgebra inclusions transfer the local factorizations to the model's native open cover. No finite-presentation conclusion is asserted or required for this finite refinement.

Imports15
Imported by2

Declarations

theorem

exists_finite_refinement

L50 ↗
AlgebraicGeometry.Etale.exists_finite_refinement
Documentation

A surjective étale morphism over a quasi-compact quasi-separated scheme has a finite surjective refinement which Zariski locally factors through the original cover. The cover source need not be quasi-compact or separated.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite TopologicalSpace
namespace AlgebraicGeometry
Lean source · statement
theorem Etale.exists_finite_refinement
    {U X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (f : U ⟶ X) [Etale f] [Surjective f] :
    ∃ (Y : Scheme.{u}) (q : Y ⟶ X),
      IsFinite q ∧ Surjective q ∧ q.ZariskiLocallyFactorsThrough f

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