equivalenceLeftToRight — Mathlib

English

First component of the equivalence proof for the Čech nerve isomorphism.

Русский

Первая часть доказательства эквивалентности для изоморфности Čech нерва.

LaTeX

$$$ cechNerveEquiv._proof_1 \\;: \\; \\text{Eq } (CategoryTheory. Arrow.mapCechNerve ...) (CategoryTheory.SimplicialObject ...) $$$

Lean4

/-- A helper function used in defining the Čech adjunction. -/
@[simps]
def equivalenceLeftToRight (X : SimplicialObject.Augmented C) (F : Arrow C) (G : Augmented.toArrow.obj X ⟶ F) :
    X ⟶ F.augmentedCechNerve
    where
  left :=
    { app := fun x =>
        Limits.WidePullback.lift (X.hom.app _ ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const _ x.unop i).op ≫ G.left) fun i => by simp
      naturality := by
        intro x y f
        dsimp
        ext
        · simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]
          rfl
        · simp }
  right := G.right

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