English
For each i and U, the componentwise projection π_i is an isomorphism between the diagram over Open U and the component in the gluing diagram.
Русский
Для каждого i и U проекция π_i является изоморфизмом между диаграммой над открытым множеством U и компонентой в диаграмме сшивки.
LaTeX
$$$(D.\mathrm{diagramOverOpen}\,U)_i \cong (D.diagramOverOpen U).obj(\mathrm{op}\,i)$$$
Lean4
/-- `ιInvApp` is the inverse of `D.ι i` on `U`. -/
theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) :
D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 _ :=
by
ext j
induction j with
| op j => ?_
rcases j with (⟨j, k⟩ | ⟨j⟩)
· rw [← limit.w (componentwiseDiagram 𝖣.diagram.multispan _) (Quiver.Hom.op (WalkingMultispan.Hom.fst (j, k))), ←
Category.assoc, Category.id_comp]
congr 1
simp_rw [Category.assoc]
apply π_ιInvApp_π
· simp_rw [Category.assoc]
rw [Category.id_comp]
apply π_ιInvApp_π