cechConerveEquiv — Mathlib

English

There is a canonical equivalence between morphisms from the augmented Čech conerve of F to X and morphisms from F to Augmented.toArrow.obj X.

Русский

Существует каноническая эквивалентность между отображениями из faugmentedCechConerve в X и из F в Augmented.toArrow.obj X.

LaTeX

$$$ (\\mathrm{cechConerveEquiv} \\, F \, X) : (F.augmentedCechConerve \\to X) \\simeq (F \\to \\mathrm{Augmented.toArrow.obj} \\, X) $$$

Lean4

/-- A helper function used in defining the Čech conerve adjunction. -/
@[simps]
def cechConerveEquiv (F : Arrow C) (X : CosimplicialObject.Augmented C) :
    (F.augmentedCechConerve ⟶ X) ≃ (F ⟶ Augmented.toArrow.obj X)
    where
  toFun := equivalenceLeftToRight _ _
  invFun := equivalenceRightToLeft _ _
  left_inv := by
    intro A
    ext x : 2
    · rfl
    · refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_
      · dsimp
        simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right,
          SimplexCategory.len_mk, Arrow.cechConerve_map, colimit.ι_desc, WidePushoutShape.mkCocone_ι_app,
          colimit.ι_desc_assoc]
        rfl
      · dsimp
        rw [colimit.ι_desc]
        exact congr_app A.w x
  right_inv := by
    intro A
    ext
    · rfl
    · dsimp
      rw [WidePushout.ι_desc]
      nth_rw 2 [← Category.comp_id A.right]
      congr 1
      convert X.right.map_id _
      ext ⟨a, ha⟩
      simp

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