Module

RelativeGluing.lean

Nyll.SchemeTheory.FiniteEtale.RelativeGluing

1 declaration indexed from sourceView source ↗

Module documentation

The range and open-immersion lifting arguments below adapt Christian Merten's RelativeGluingData.preimage_toBase_eq_range_ι and RelativeGluingData.isPullback_natTrans_ι_toBase from Mathlib: https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/AlgebraicGeometry/RelativeGluing.lean The present construction works with actual pairwise overlaps of arbitrary open covers, without a locally directed structure on the cover index.

Imports4

Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Morphisms.Basic
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic

Imported by3

theorem

exists_finiteEtale_gluedToBase

L28 ↗

AlgebraicGeometry.Scheme.GlueData.exists_finiteEtale_gluedToBase

Documentation

Gluing finite étale pieces over their actual pairwise overlaps constructs a finite étale scheme over the covered base, together with all local pullback squares.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory Limits AlgebraicGeometry
namespace AlgebraicGeometry.Scheme.GlueData

Lean source · statement

theorem exists_finiteEtale_gluedToBase
    (D : Scheme.GlueData.{u}) (S : Scheme.{u})
    (U : D.J → Scheme.{u}) (u : ∀ i, U i ⟶ S)
    [∀ i, IsOpenImmersion (u i)]
    (hu : ∀ s : S, ∃ (i : D.J) (x : U i), u i x = s)
    (y : ∀ i, D.U i ⟶ U i) [∀ i, IsFiniteEtale (y i)]
    (ℓ : ∀ i j, D.V (i, j) ⟶ U j)
    (hV : ∀ i j, IsPullback (D.f i j) (ℓ i j) (y i ≫ u i) (u j))
    (ht : ∀ i j, D.t i j ≫ D.f j i ≫ y j = ℓ i j) :
    ∃ q : D.glued ⟶ S, IsFiniteEtale q ∧
      ∀ i, IsPullback (y i) (D.ι i) (u i) q

Module documentation

Declarations

exists_finiteEtale_gluedToBase