Module

AffineFinitePresentationRefinement.lean

Nyll.SchemeTheory.Etale.AffineFinitePresentationRefinement

2 declarations indexed from sourceView source ↗

Module documentation

Finite-FP refinements of étale covers over affine bases

The integral refinement of a surjective étale cover over an affine base has an affine source. Its actual isoSpec and the native Spec.preimage map supply the integral algebra to which finite-FP local-factor descent applies. Thus the finite refinement is constructed from the original cover, without a local-factorization or limit premise in the final statement.

This proves the affine-base case of the finite-presentation refinement in Stacks Project, Tag 09Z0. Arbitrary qcqs-base globalization and proper base change are separate remaining steps.

Imports10

Nyll.SchemeTheory.Etale.AffineLocalFactorDescent
Nyll.SchemeTheory.Etale.IntegralRefinement
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Mathlib.AlgebraicGeometry.Morphisms.Affine
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Restrict
Mathlib.RingTheory.IntegralClosure.Algebra.Defs

Imported by1

Nyll.SchemeTheory.Etale.All

theorem

locally_factors_precomp

L41 ↗

AlgebraicGeometry.locally_factors_precomp

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite Algebra
namespace AlgebraicGeometry

Lean source · statement

theorem locally_factors_precomp {S T U X : Scheme.{u}}
    {g : T ⟶ X} {f : U ⟶ X} (h : g.ZariskiLocallyFactorsThrough f) (k : S ⟶ T) :
    (k ≫ g).ZariskiLocallyFactorsThrough f

theorem

exists_finitePresentation_refinement_spec

L60 ↗

AlgebraicGeometry.Etale.exists_finitePresentation_refinement_spec

Documentation

A surjective étale cover of an arbitrary affine scheme has a finite, finitely presented surjective refinement which Zariski locally factors through that cover. No compactness or separatedness of the cover source is required.