mathlib3 documentation

algebraic_geometry.presheafed_space.gluing

Gluing Structured spaces #

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

Given a family of gluing data of structured spaces (presheafed spaces, sheafed spaces, or locally ringed spaces), we may glue them together.

The construction should be "sealed" and considered as a black box, while only using the API provided.

Main definitions #

Main results #

Analogous results are also provided for SheafedSpace and LocallyRingedSpace.

Implementation details #

Almost the whole file is dedicated to showing tht ι i is an open immersion. The fact that this is an open embedding of topological spaces follows from topology.gluing.lean, and it remains to construct Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, ι i '' U) for each U ⊆ U i. Since Γ(𝒪_X, ι i '' U) is the the limit of diagram_over_open, the components of the structure sheafs of the spaces in the gluing diagram, we need to construct a map ι_inv_app_π_app : Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V) for each V in the gluing diagram.

We will refer to this diagram in the following doc strings. The X is the glued space, and the dotted arrow is a partial inverse guaranteed by the fact that it is an open immersion. The map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, _) is given by the composition of the red arrows, and the map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{V_{jk}}, _) is given by the composition of the blue arrows. To lift this into a map from Γ(𝒪_X, ι i '' U), we also need to show that these commute with the maps in the diagram (the green arrows), which is just a lengthy diagram-chasing.

@[nolint]

A family of gluing data consists of

  1. An index type J
  2. A presheafed space U i for each i : J.
  3. A presheafed space V i j for each i j : J. (Note that this is J × J → PresheafedSpace C rather than J → J → PresheafedSpace C 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 spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

Instances for algebraic_geometry.PresheafedSpace.glue_data
  • algebraic_geometry.PresheafedSpace.glue_data.has_sizeof_inst
@[reducible]

The glue data of topological spaces associated to a family of glue data of PresheafedSpaces.

@[reducible]

(Implementation) Given an open subset of one of the spaces U ⊆ Uᵢ, the sheaf component of the image ι '' U in the glued space is the limit of this diagram.

(Implementation) We construct the map Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V) for each V in the gluing diagram. We will lift these maps into ι_inv_app.

Equations
@[nolint]

A family of gluing data consists of

  1. An index type J
  2. A sheafed space U i for each i : J.
  3. A sheafed space V i j for each i j : J. (Note that this is J × J → SheafedSpace C rather than J → J → SheafedSpace C 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 spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

Instances for algebraic_geometry.SheafedSpace.glue_data
  • algebraic_geometry.SheafedSpace.glue_data.has_sizeof_inst
@[reducible]

The glue data of presheafed spaces associated to a family of glue data of sheafed spaces.

@[nolint]

A family of gluing data consists of

  1. An index type J
  2. A locally ringed space U i for each i : J.
  3. A locally ringed space V i j for each i j : J. (Note that this is J × J → LocallyRingedSpace rather than J → J → LocallyRingedSpace 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 spaces U i together by identifying V i j with V j i, such that the U i's are open subspaces of the glued space.

Instances for algebraic_geometry.LocallyRingedSpace.glue_data
  • algebraic_geometry.LocallyRingedSpace.glue_data.has_sizeof_inst
@[reducible]

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

@[reducible]

The gluing as locally ringed spaces is isomorphic to the gluing as ringed spaces.