componentwise_diagram_π_isIso — Mathlib

English

Each projection π_i in the gluing diagram is an isomorphism with inverse given by ιInvAppπEqMap in conjunction with ιInvApp.

Русский

Каждая проекция π_i в диаграмме сшивки является изоморфизмом; её обратная карта задаётся через ιInvAppπEqMap и ιInvApp.

LaTeX

$$$\pi_{OverOpen,U,i} : (D.diagramOverOpen U) \to ... \quad \text{isIso with inverse } D.ιInvAppπEqMap U \circ D.ιInvApp U$$$

Lean4

instance componentwise_diagram_π_isIso (i : D.J) (U : Opens (D.U i).carrier) : IsIso (D.diagramOverOpenπ U i) :=
  by
  use D.ιInvAppπEqMap U ≫ D.ιInvApp U
  constructor
  · apply π_ιInvApp_eq_id
  · rw [Category.assoc, (D.ιInvApp_π _).choose_spec]
    exact Iso.inv_hom_id ((D.U i).presheaf.mapIso (eqToIso _))

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