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.
- J : Type v
- U : s.J → C
- V : s.J × s.J → C
- f : (i j : s.J) → CategoryTheory.GlueData.V s (i, j) ⟶ CategoryTheory.GlueData.U s i
- f_mono : ∀ (i j : s.J), CategoryTheory.Mono (CategoryTheory.GlueData.f s i j)
- f_hasPullback : ∀ (i j k : s.J), CategoryTheory.Limits.HasPullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k)
- f_id : ∀ (i : s.J), CategoryTheory.IsIso (CategoryTheory.GlueData.f s i i)
- t : (i j : s.J) → CategoryTheory.GlueData.V s (i, j) ⟶ CategoryTheory.GlueData.V s (j, i)
- t_id : ∀ (i : s.J), CategoryTheory.GlueData.t s i i = CategoryTheory.CategoryStruct.id (CategoryTheory.GlueData.V s (i, i))
- t' : (i j k : s.J) → CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k) ⟶ CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s j k) (CategoryTheory.GlueData.f s j i)
- t_fac : ∀ (i j k : s.J), CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s i j k) CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.GlueData.t s i j)
- cocycle : ∀ (i j k : s.J), CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GlueData.t' s j k i) (CategoryTheory.GlueData.t' s k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (CategoryTheory.GlueData.f s i j) (CategoryTheory.GlueData.f s i k))
A gluing datum consists of
- An index type
J
- An object
U i
for eachi : J
. - An object
V i j
for eachi j : J
. - A monomorphism
f i j : V i j ⟶ U i
for eachi j : J
. - A transition map
t i j : V i j ⟶ V j i
for eachi j : J
. such that f i i
is an isomorphism.t i i
is the identity.- The pullback for
f i j
andf i k
exists. V i j ×[U i] V i k ⟶ V i j ⟶ V j i
factors throughV j k ×[U j] V j i ⟶ V j i
via somet' : V i j ×[U i] V i k ⟶ V j k ×[U j] V j i
.t' i j k ≫ t' j k i ≫ t' k i j = 𝟙 _
.
Instances For
(Implementation) The disjoint union of U i
.
Instances For
(Implementation) The diagram to take colimit of.
Instances For
The glued object given a family of gluing data.
Instances For
The map D.U i ⟶ D.glued
for each i
.
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
The projection ∐ D.U ⟶ D.glued
given by the colimit.
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
The diagram of the image of a GlueData
under a functor F
is naturally isomorphic to the
original diagram of the GlueData
via F
.
Instances For
If F
preserves the gluing, we obtain an iso between the glued objects.
Instances For
If F
preserves the gluing, and reflects the pullback of U i ⟶ glued
and U j ⟶ glued
,
then F
reflects the fact that V_pullback_cone
is a pullback.
Instances For
If there is a forgetful functor into Type
that preserves enough (co)limits, then D.ι
will
be jointly surjective.