mathlib3 documentation


Gluing Schemes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a family of gluing data of schemes, we may glue them together.

Main definitions #

Main results #

Implementation details #

All the hard work is done in algebraic_geometry/presheafed_space/gluing.lean where we glue presheafed spaces, sheafed spaces, and locally ringed spaces.


A family of gluing data consists of

  1. An index type J
  2. An scheme U i for each i : J.
  3. An scheme V i j for each i j : J. (Note that this is J × J → Scheme rather than J → J → Scheme to connect to the limits library easier.)
  4. An open immersion f i j : V i j ⟶ U i for each i j : ι.
  5. A transition map t i j : V i j ⟶ V j i for each i j : ι. such that
  6. f i i is an isomorphism.
  7. t i i is the identity.
  8. V i j ×[U i] V i k ⟶ V i j ⟶ V j i factors through V j k ×[U j] V j i ⟶ V j i via some t' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i.
  9. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.

We can then glue the schemes U i together by identifying V i j with V j i, such that the U i's are open subschemes of the glued space.

Instances for algebraic_geometry.Scheme.glue_data
  • algebraic_geometry.Scheme.glue_data.has_sizeof_inst

The glue data of locally ringed spaces spaces associated to a family of glue data of schemes.

(Implementation). The glued scheme of a glue data. This should not be used outside this file. Use Scheme.glue_data.glued instead.


The glued scheme of a glued space.


The immersion from D.U i into the glued space.


The gluing as sheafed spaces is isomorphic to the gluing as presheafed spaces.

The pullback cone spanned by V i j ⟶ U i and V i j ⟶ U j. This is a pullback diagram (V_pullback_cone_is_limit).


An equivalence relation on Σ i, D.U i that holds iff 𝖣 .ι i x = 𝖣 .ι j y. See Scheme.gluing_data.ι_eq_iff.


The open cover of the glued space given by the glue data.

theorem algebraic_geometry.Scheme.open_cover.glued_cover_to_glue_data_V {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) (_x : 𝒰.J × 𝒰.J) :
𝒰.glued_cover.to_glue_data.V _x = algebraic_geometry.Scheme.open_cover.glued_cover._match_1 𝒰 _x

The glue data associated with an open cover. The canonical isomorphism 𝒰.glued_cover.glued ⟶ X is provided by 𝒰.from_glued.


The canonical morphism from the gluing of an open cover of X into X. This is an isomorphism, as witnessed by an is_iso instance.

Instances for algebraic_geometry.Scheme.open_cover.from_glued

Given an open cover of X, and a morphism 𝒰.obj x ⟶ Y for each open subscheme in the cover, such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms together into a morphism X ⟶ Y.

Note: If X is exactly (defeq to) the gluing of U i, then using multicoequalizer.desc suffices.

theorem algebraic_geometry.Scheme.open_cover.hom_ext {X : algebraic_geometry.Scheme} (𝒰 : X.open_cover) {Y : algebraic_geometry.Scheme} (f₁ f₂ : X Y) (h : (x : 𝒰.J), 𝒰.map x f₁ = 𝒰.map x f₂) :
f₁ = f₂