pairwiseDiagramIso — Mathlib

English

The comparison between pairwise and opensLeCover diagrams is an isomorphism after postcomposition with an appropriate equivalence.

Русский

Сравнение между диаграммами pairwise и opensLeCover является изоморфизмом после посткомпозиции через соответствующее эквивалентное отображение.

LaTeX

$$$\text{pairwiseCoconeIso} : \text{Pairwise} \Rightarrow \text{OpensLeCover}$ is an isomorphism after postcompose.$$

Lean4

/-- The diagram in `Opens X` indexed by pairwise intersections from `U` is isomorphic
(in fact, equal) to the diagram factored through `OpensLeCover U`.
-/
def pairwiseDiagramIso : Pairwise.diagram U ≅ pairwiseToOpensLeCover U ⋙ ObjectProperty.ι _
    where
  hom := { app := by rintro (i | ⟨i, j⟩) <;> exact 𝟙 _ }
  inv := { app := by rintro (i | ⟨i, j⟩) <;> exact 𝟙 _ }

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