π_ιInvApp_eq_id — Mathlib

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_π

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