pairwiseCoconeIso — Mathlib

English

The functor pairwiseToOpensLeCover maps Pairwise objects to OpensLeCover objects by sending a single i to Ui and a pair i,j to Ui ∩ Uj.

Русский

Функтор pairwiseToOpensLeCover переводит пары объектов в OpensLeCover: одиночный i идёт в Ui, пара i,j идёт в Ui ∩ Uj.

LaTeX

$$$\text{pairwiseToOpensLeCoverObj } U (\text{single } i)= Ui$, $\text{pairwiseToOpensLeCoverObj } U (\text{pair } i j)= Ui \cap Uj$$$

Lean4

/-- The cocone `Pairwise.cocone U` with cocone point `iSup U` over `Pairwise.diagram U` is isomorphic
to the cocone `opensLeCoverCocone U` (with the same cocone point)
after appropriate whiskering and postcomposition.
-/
def pairwiseCoconeIso :
    (Pairwise.cocone U).op ≅
      (Cones.postcomposeEquivalence (NatIso.op (pairwiseDiagramIso U :) :)).functor.obj
        ((opensLeCoverCocone U).op.whisker (pairwiseToOpensLeCover U).op) :=
  Cones.ext (Iso.refl _) (by cat_disch)

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