Module

TwoOpenGluing.lean

Nyll.SchemeTheory.FiniteEtale.TwoOpenGluing

4 declarations indexed from sourceView source ↗

Module documentation

Gluing finite étale covers over two open subschemes

An isomorphism over the actual intersection glues two finite étale covers. The glued scheme is the pushout of their open overlap; the Cartesian squares over the two base opens prove that its structural morphism is finite étale. This supplies the two-open gluing step in Stacks Project, Tag 0EY7.

Imports7

Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Mathlib.AlgebraicGeometry.Gluing
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.Restrict
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.CategoryTheory.MorphismProperty.Comma

Imported by4

theorem

pushout_jointly_surjective

L30 ↗

AlgebraicGeometry.FiniteEtale.pushout_jointly_surjective

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem pushout_jointly_surjective
    {W A B : Scheme.{u}} (f : W ⟶ A) (g : W ⟶ B)
    [IsOpenImmersion f] [IsOpenImmersion g] (x : ↑(pushout f g)) :
    (∃ a, pushout.inl f g a = x) ∨ (∃ b, pushout.inr f g b = x)

theorem

range_of_two_open_gluing

L43 ↗

AlgebraicGeometry.FiniteEtale.range_of_two_open_gluing

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem range_of_two_open_gluing
    {S U V O A B W Z : Scheme.{u}}
    (u : U ⟶ S) (v : V ⟶ S) (iU : O ⟶ U) (iV : O ⟶ V)
    (hO : IsPullback iU iV u v)
    (a : A ⟶ U) (b : B ⟶ V) (f : W ⟶ A) (g : W ⟶ B) (l : W ⟶ O)
    (hB : IsPullback g l b iV)
    (ia : A ⟶ Z) (ib : B ⟶ Z) (q : Z ⟶ S)
    (hab : f ≫ ia = g ≫ ib)
    (ha : ia ≫ q = a ≫ u) (hb : ib ≫ q = b ≫ v)
    (hc : ∀ z : Z, (∃ x, ia x = z) ∨ (∃ y, ib y = z)) :
    q ⁻¹' Set.range u = Set.range ia

theorem

exists_glued_of_isPullback

L72 ↗

AlgebraicGeometry.FiniteEtale.exists_glued_of_isPullback

Documentation

Two finite étale covers with an isomorphism over a Cartesian overlap glue over a jointly surjective pair of open immersions.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem exists_glued_of_isPullback
    {S U V O : Scheme.{u}} (u : U ⟶ S) (v : V ⟶ S)
    [IsOpenImmersion u] [IsOpenImmersion v]
    (hc : ∀ s : S, (∃ x, u x = s) ∨ (∃ y, v y = s))
    (iU : O ⟶ U) (iV : O ⟶ V) (hO : IsPullback iU iV u v)
    (A : FiniteEtale U) (B : FiniteEtale V)
    (e : (pullback iU).obj A ≅ (pullback iV).obj B) :
    ∃ Z : FiniteEtale S,
      Nonempty ((pullback u).obj Z ≅ A) ∧
      Nonempty ((pullback v).obj Z ≅ B)

theorem

exists_glued_over_sup

L165 ↗

AlgebraicGeometry.FiniteEtale.exists_glued_over_sup

Documentation

Finite étale covers on two opens glue over their union from an isomorphism between their restrictions to the intersection.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry.FiniteEtale
universe u

Lean source · statement

theorem exists_glued_over_sup
    (X : Scheme.{u}) (U N : X.Opens)
    (A : FiniteEtale U.toScheme) (B : FiniteEtale N.toScheme)
    (e : (pullback (X.homOfLE (inf_le_left : U ⊓ N ≤ U))).obj A ≅
      (pullback (X.homOfLE (inf_le_right : U ⊓ N ≤ N))).obj B) :
    ∃ Z : FiniteEtale (U ⊔ N).toScheme,
      Nonempty ((pullback (X.homOfLE (le_sup_left : U ≤ U ⊔ N))).obj Z ≅ A) ∧
      Nonempty ((pullback (X.homOfLE (le_sup_right : N ≤ U ⊔ N))).obj Z ≅ B)

Module documentation

Gluing finite étale covers over two open subschemes

Declarations

pushout_jointly_surjective

range_of_two_open_gluing

exists_glued_of_isPullback

exists_glued_over_sup