mapGlueData — Mathlib

English

There is a natural isomorphism between the image of the glue data under F and the diagram of the mapped glue data.

Русский

Существует естественное изоморфизм между изображением даных сцепления под F и диаграммой отображённых данных сцепления.

LaTeX

$$$\\mathrm{diagramIso}: D.diagram.multispan \\circ F \\cong (D.mapGlueData F).diagram.multispan$$$

Lean4

/-- A functor that preserves the pullbacks of `f i j` and `f i k` can map a family of glue data. -/
@[simps]
def mapGlueData : GlueData C' where
  J := D.J
  U i := F.obj (D.U i)
  V i := F.obj (D.V i)
  f i j := F.map (D.f i j)
  f_mono _ _ := preserves_mono_of_preservesLimit _ _
  f_id _ := inferInstance
  t i j := F.map (D.t i j)
  t_id i := by simp
  t' i j
    k :=
    (PreservesPullback.iso F (D.f i j) (D.f i k)).inv ≫
      F.map (D.t' i j k) ≫ (PreservesPullback.iso F (D.f j k) (D.f j i)).hom
  t_fac i j k := by simpa [Iso.inv_comp_eq] using congr_arg (fun f => F.map f) (D.t_fac i j k)
  cocycle i j
    k := by
    simp only [Category.assoc, Iso.hom_inv_id_assoc, ← Functor.map_comp_assoc, D.cocycle, Iso.inv_hom_id,
      CategoryTheory.Functor.map_id, Category.id_comp]

Похожие утверждения