equivalenceRightToLeft — Mathlib

English

There is a construction equivalenceRightToLeft which, given a morphism G: F ⟶ Augmented.toArrow.obj X, produces a morphism F.augmentedCechConerve ⟶ X with left part G.left and a right part defined by G.right and X.

Русский

Существует конструкция equivalenceRightToLeft, которая, заданная морфизмом G: F ⟶ Augmented.toArrow.obj X, образует морфизм F.augmentedCechConerve ⟶ X с левой частью G.left и правой частью, заданной через G.right и X.

LaTeX

$$$\\text{equivalenceRightToLeft}(F,X,G) : F.augmentedCechConerve \\to X\\;\\text{ with left }=G.left$ and a right component defined by G.right$$$

Lean4

/-- A helper function used in defining the Čech conerve adjunction. -/
@[simps!]
def equivalenceRightToLeft (F : Arrow C) (X : CosimplicialObject.Augmented C) (G : F ⟶ Augmented.toArrow.obj X) :
    F.augmentedCechConerve ⟶ X where
  left := G.left
  right :=
    { app := fun x =>
        Limits.WidePushout.desc (G.left ≫ X.hom.app _) (fun i => G.right ≫ X.right.map (SimplexCategory.const _ x i))
          (by
            rintro j
            rw [← Arrow.w_assoc G]
            have t := X.hom.naturality (SimplexCategory.const ⦋0⦌ x j)
            dsimp at t ⊢
            simp only [Category.id_comp] at t
            rw [← t])
      naturality := by
        intro x y f
        dsimp
        ext
        · dsimp
          simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]
          rw [Category.assoc, ← X.right.map_comp]
          rfl
        · simp [← NatTrans.naturality] }

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