equivalenceRightToLeft — Mathlib

English

The equivalence between arrows and their Čech nerves: a pseudo-inverse given by equivalenceLeftToRight and equivalenceRightToLeft.

Русский

Эквивалентность между стрелками и их Čech нервами: псевдообратная пара equivalenceLeftToRight и equivalenceRightToLeft.

LaTeX

$$$ cechNerveEquiv(X,F): (Augmented.toArrow.obj X ⟶ F) \\cong (X ⟶ F.augmentedCechNerve) $$$

Lean4

/-- A helper function used in defining the Čech adjunction. -/
@[simps]
def equivalenceRightToLeft (X : SimplicialObject.Augmented C) (F : Arrow C) (G : X ⟶ F.augmentedCechNerve) :
    Augmented.toArrow.obj X ⟶ F where
  left := G.left.app _ ≫ WidePullback.π _ 0
  right := G.right
  w := by
    have := G.w
    apply_fun fun e => e.app (Opposite.op ⦋0⦌) at this
    simpa using this

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