English
There is a construction equivalenceLeftToRight which, given a morphism G: F.augmentedCechConerve ⟶ X, produces a morphism F ⟶ Augmented.toArrow.obj X with left part G.left and a certain right part determined by G.right and X.
Русский
Существует конструкция equivalenceLeftToRight, которая, заданная морфизмом G: F.augmentedCechConerve ⟶ X, получает морфизм F ⟶ Augmented.toArrow.obj X с левой частью G.left и правой частью, определяемой G.right и X.
LaTeX
$$$\\text{equivalenceLeftToRight}(F,X,G) : F \\to \\mathrm{Augmented.toArrow}(X)\\quad \\text{with } \\text{left} = G.left$, $\\text{right} = \\text{(неочередной состав с G.right и X)}$$$
Lean4
/-- A helper function used in defining the Čech conerve adjunction. -/
@[simps]
def equivalenceLeftToRight (F : Arrow C) (X : CosimplicialObject.Augmented C) (G : F.augmentedCechConerve ⟶ X) :
F ⟶ Augmented.toArrow.obj X where
left := G.left
right := (WidePushout.ι _ 0 ≫ G.right.app ⦋0⦌ :)
w := by
dsimp
rw [@WidePushout.arrow_ι_assoc _ _ _ _ _ (fun (_ : Fin 1) => F.hom) (by dsimp; infer_instance)]
exact congr_app G.w ⦋0⦌
