English
Definition of mapping glue data along a functor F: it produces a new glue data on C' with components obtained by applying F to U,V,f,t and t'.
Русский
Определение отображения данных сцепления через функтор F: получается новое данные сцепления на C' со составляющими, получаемыми применением F к U,V,f,t и t'.
LaTeX
$$$\\text{mapGlueData}(D,F)$ is a GlueData on C' with components defined by $U_i' = F(U_i)$, $V_i' = F(V_i)$, $f_{i j}' = F(f_{i j})$, $t'_{i j k}' = \\mathrm{(inverse\; pullback\; iso)} \\circ F(t'_{i j k}) \\circ \\mathrm{(other\; iso)}$ and cocycle conditions transported along F.$$
Lean4
/-- If `F` preserves the gluing, we obtain an iso between the glued objects. -/
def gluedIso : F.obj D.glued ≅ (D.mapGlueData F).glued :=
haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
preservesColimitIso F D.diagram.multispan ≪≫ Limits.HasColimit.isoOfNatIso (D.diagramIso F)
