Module

IntegralRefinement.lean

Nyll.SchemeTheory.Etale.IntegralRefinement

6 declarations indexed from sourceView source ↗

Module documentation

Integral refinements of étale covers

This file proves the integral-refinement assertion of Stacks Project, Tag 09Z0, by induction on the actual uniform geometric-fiber bound. The recursive refinement is produced by the strict degree decrease of the normalization remainder. Its integral normalization extension is joined to the actual reduced closed complement, using native scheme coproducts.

The result is an integral surjective morphism which Zariski locally factors through the original étale cover. The later strengthening to a finite morphism of finite presentation is not asserted here.

Imports21

Nyll.SchemeTheory.Etale.FiniteAffineCover
Nyll.SchemeTheory.Etale.GeometricFiberBound
Nyll.SchemeTheory.Etale.NormalizationRemainderDegree
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Nyll.SchemeTheory.Morphisms.QuasiFinite
Nyll.SchemeTheory.Normalization.IntegralOpen
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Integral
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.ResidueField
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
Mathlib.FieldTheory.IsSepClosed
Mathlib.SetTheory.Cardinal.Finite
Mathlib.Topology.Compactness.Compact

Imported by7

def

ZariskiLocallyFactorsThrough

L53 ↗

AlgebraicGeometry.Scheme.Hom.ZariskiLocallyFactorsThrough

Documentation

A map to X factors through f on a Zariski neighborhood of each source point.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

def Scheme.Hom.ZariskiLocallyFactorsThrough {T U X : Scheme.{u}}
    (g : T ⟶ X) (f : U ⟶ X) : Prop

theorem

local_factor_on_open_image

L58 ↗

AlgebraicGeometry.local_factor_on_open_image

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem local_factor_on_open_image
    {A T U X : Scheme.{u}} (g : T ⟶ X) (f : U ⟶ X)
    (i : A ⟶ T) [IsOpenImmersion i] (a : A ⟶ U)
    (ha : a ≫ f = i ≫ g) (x : A) :
    ∃ V : T.Opens, i x ∈ V ∧ ∃ b : V.toScheme ⟶ U, b ≫ f = V.ι ≫ g

theorem

integral_refinement_glue

L75 ↗

AlgebraicGeometry.integral_refinement_glue

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem integral_refinement_glue
    {U X Y Z : Scheme.{u}} (f : U ⟶ X) (π : Y ⟶ X)
    [IsIntegralHom π] [Surjective π] (j : U ⟶ Y) [IsOpenImmersion j]
    (hj : j ≫ π = f) (V : Y.Opens) [QuasiCompact V.ι]
    (hcover : (Set.range j)ᶜ ⊆ (V : Set Y))
    (p : Z ⟶ V.toScheme) [IsIntegralHom p] [Surjective p]
    (hlocal : (p ≫ V.ι ≫ π).ZariskiLocallyFactorsThrough f) :
    ∃ (T : Scheme.{u}) (g : T ⟶ X),
      IsIntegralHom g ∧ Surjective g ∧ g.ZariskiLocallyFactorsThrough f

theorem

integral_refinement_of_bound

L198 ↗

AlgebraicGeometry.integral_refinement_of_bound

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem integral_refinement_of_bound (n : ℕ) :
    ∀ {U X : Scheme.{u}} [CompactSpace U] [QuasiSeparatedSpace X]
      (f : U ⟶ X) [Etale f] [IsSeparated f] [Surjective f],
      (∀ (Ω : Type u) [Field Ω] [IsSepClosed Ω]
        (s : Spec (CommRingCat.of Ω) ⟶ X),
        Finite (pullback f s : Scheme.{u}) ∧ Nat.card (pullback f s : Scheme.{u}) ≤ n) →
      ∃ (T : Scheme.{u}) (g : T ⟶ X),
        IsIntegralHom g ∧ Surjective g ∧ g.ZariskiLocallyFactorsThrough f

theorem

exists_integral_refinement_of_compactSource

L330 ↗

AlgebraicGeometry.Etale.exists_integral_refinement_of_compactSource

Documentation

A compact separated étale cover has an integral surjective refinement which locally factors through the original cover. The recursive local factorizations are constructed by induction on the actual fiber bound.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.exists_integral_refinement_of_compactSource
    {U X : Scheme.{u}} [CompactSpace U] [QuasiSeparatedSpace X]
    (f : U ⟶ X) [Etale f] [IsSeparated f] [Surjective f] :
    ∃ (T : Scheme.{u}) (g : T ⟶ X),
      IsIntegralHom g ∧ Surjective g ∧ g.ZariskiLocallyFactorsThrough f

theorem

exists_integral_refinement

L342 ↗

AlgebraicGeometry.Etale.exists_integral_refinement

Documentation

The integral-refinement assertion of Stacks, Tag 09Z0. A surjective étale cover of a quasi-compact quasi-separated scheme is Zariski locally dominated by an actual integral surjective morphism. Finite presentation of the refinement is a separate, later assertion.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry

Lean source · statement

theorem Etale.exists_integral_refinement
    {U X : Scheme.{u}} [CompactSpace X] [QuasiSeparatedSpace X]
    (f : U ⟶ X) [Etale f] [Surjective f] :
    ∃ (T : Scheme.{u}) (g : T ⟶ X),
      IsIntegralHom g ∧ Surjective g ∧ g.ZariskiLocallyFactorsThrough f

Module documentation

Integral refinements of étale covers

Declarations

ZariskiLocallyFactorsThrough

local_factor_on_open_image

integral_refinement_glue

integral_refinement_of_bound

exists_integral_refinement_of_compactSource

exists_integral_refinement