ι_gluedIso_hom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem ι_gluedIso_hom (i : D.J) : F.map (D.ι i) ≫ (D.gluedIso F).hom = (D.mapGlueData F).ι i :=
  by
  haveI : HasColimit (MultispanIndex.multispan (diagram (mapGlueData D F))) := inferInstance
  erw [ι_preservesColimitIso_hom_assoc]
  rw [HasColimit.isoOfNatIso_ι_hom]
  erw [Category.id_comp]
  rfl

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