Module

FiniteAffineCover.lean

Nyll.SchemeTheory.Etale.FiniteAffineCover

2 declarations indexed from sourceView source ↗

Module documentation

Finite affine refinements of étale covers

An étale cover of a quasi-compact scheme has a finite affine refinement by open subschemes of its members. Collapsing this finite cover to its disjoint union gives a single surjective étale morphism with affine source.

The refinement morphism is retained on the finite family: the disjoint union need not map to one fixed member of the original cover. Over an affine base, its map on global sections is faithfully flat and étale, providing the ring map needed for effective descent. No ground field, noetherianity, or quasi-separatedness of the base is assumed.

Imports11

Mathlib.AlgebraicGeometry.Cover.MorphismProperty
Mathlib.AlgebraicGeometry.Cover.QuasiCompact
Mathlib.AlgebraicGeometry.Cover.Sigma
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.RingTheory.RingHom.FaithfullyFlat

Imported by3

theorem

exists_finite_affine_etale_refinement

L47 ↗

AlgebraicGeometry.Scheme.Cover.exists_finite_affine_etale_refinement

Documentation

A finite affine refinement of an étale cover, together with its single affine, surjective, étale total-space morphism. The component maps to the original cover are open immersions. The underlying refinement hom allows the indexing universe of the original cover to differ from the scheme universe.

Source context 4 commands

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

@[expose] public noncomputable section
open CategoryTheory Limits
universe u v
namespace AlgebraicGeometry.Scheme.Cover

Lean source · full declaration

theorem exists_finite_affine_etale_refinement {X : Scheme.{u}} [CompactSpace X]
    (𝒰 : X.Cover.{v} (Scheme.precoverage (show MorphismProperty Scheme.{u} from @Etale))) :
    ∃ (𝒱 : Scheme.AffineCover.{u} (show MorphismProperty Scheme.{u} from @Etale) X)
      (e : 𝒱.cover.toPreZeroHypercover.Hom 𝒰.toPreZeroHypercover),
      Finite 𝒱.I₀ ∧ (∀ i : 𝒱.I₀, IsOpenImmersion (e.h₀ i)) ∧
      IsAffine (∐ fun i : 𝒱.I₀ => Spec (𝒱.X i)) ∧
      Etale (Sigma.desc 𝒱.f) ∧ Surjective (Sigma.desc 𝒱.f) := by
  let 𝒰' := 𝒰.ulift
  let a : 𝒰'.toPreZeroHypercover.Hom 𝒰.toPreZeroHypercover :=
    { s₀ := 𝒰.idx
      h₀ x := 𝟙 (𝒰.X (𝒰.idx x))
      w₀ x := Category.id_comp (𝒰.f (𝒰.idx x)) }
  let : QuasiCompactCover 𝒰'.toPreZeroHypercover :=
    QuasiCompactCover.of_isOpenMap (fun i => (𝒰'.f i).isOpenMap)
  obtain ⟨𝒱, e', hfinite, he'⟩ :
      ∃ (𝒱 : Scheme.AffineCover.{u} (show MorphismProperty Scheme.{u} from @Etale) X)
        (e : 𝒱.cover ⟶ 𝒰'), Finite 𝒱.I₀ ∧ ∀ i : 𝒱.I₀, IsOpenImmersion (e.h₀ i) :=
    QuasiCompactCover.exists_hom 𝒰'
  let e : 𝒱.cover.toPreZeroHypercover.Hom 𝒰.toPreZeroHypercover :=
    PreZeroHypercover.Hom.comp e' a
  have he (i : 𝒱.I₀) : IsOpenImmersion (e.h₀ i) := by
    have : IsOpenImmersion (e'.h₀ i) := he' i
    change IsOpenImmersion (e'.h₀ i ≫ 𝟙 _)
    infer_instance
  have : Finite 𝒱.I₀ := hfinite
  let : IsZariskiLocalAtSource (show MorphismProperty Scheme.{u} from @Etale) :=
    HasRingHomProperty.instIsZariskiLocalAtSource
  refine ⟨𝒱, e, hfinite, he, inferInstance, 𝒱.cover.sigma.map_prop default, ?_⟩
  constructor
  intro x
  obtain ⟨y, hy⟩ := 𝒱.covers x
  refine ⟨Sigma.ι (fun i : 𝒱.I₀ => Spec (𝒱.X i)) (𝒱.idx x) y, ?_⟩
  rw [← Scheme.Hom.comp_apply, Sigma.ι_comp_desc]
  exact hy

theorem

exists_finite_affine_etale_refinement_faithfullyFlat

L84 ↗

AlgebraicGeometry.Scheme.Cover.exists_finite_affine_etale_refinement_faithfullyFlat