Documentation

Mathlib.CategoryTheory.GlueData

Gluing data #

We define GlueData as a family of data needed to glue topological spaces, schemes, etc. We provide the API to realize it as a multispan diagram, and also states lemmas about its interaction with a functor that preserves certain pullbacks.

structure CategoryTheory.GlueData (C : Type u₁) [CategoryTheory.Category.{v, u₁} C] :
Type (max u₁ (v + 1))

A gluing datum consists of

  1. An index type J
  2. An object U i for each i : J.
  3. An object V i j for each i j : J.
  4. A monomorphism f i j : V i j ⟶ U i for each i j : J.
  5. A transition map t i j : V i j ⟶ V j i for each i j : J. such that
  6. f i i is an isomorphism.
  7. t i i is the identity.
  8. The pullback for f i j and f i k exists.
  9. 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.
  10. t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _.
Instances For
    theorem CategoryTheory.GlueData.t_fac_assoc {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J) (j : self.J) (k : self.J) {Z : C} (h : CategoryTheory.GlueData.V self (j, i) Z) :

    (Implementation) The disjoint union of U i.

    Instances For

      (Implementation) The diagram to take colimit of.

      Instances For

        The pullback cone spanned by V i j ⟶ U i and V i j ⟶ U j. This will often be a pullback diagram.

        Instances For

          A functor that preserves the pullbacks of f i j and f i k can map a family of glue data.

          Instances For

            If there is a forgetful functor into Type that preserves enough (co)limits, then D.ι will be jointly surjective.