English
Relates objD under cosimplicialSimplicialEquiv by unop: objD X n = (AlternatingFaceMapComplex.objD (cosimplicialSimplicialEquiv C).functor.obj (op X)) n unop.
Русский
Соотносит objD X через cosimplicialSimplicialEquiv: objD X n = objD ∘ (cosimplicialSimplicialEquiv C).functor.obj (op X) unop.
LaTeX
$$$\text{objD } X n = (\text{AlternatingFaceMapComplex.objD} ((\cosimplicialSimplicialEquiv C).functor.obj (\mathrm{op} X)) n).unop$$$
Lean4
/-- The morphism between Čech nerves associated to a morphism of arrows. -/
@[simps]
def mapCechNerve {f g : Arrow C} [∀ n : ℕ, HasWidePullback f.right (fun _ : Fin (n + 1) => f.left) fun _ => f.hom]
[∀ n : ℕ, HasWidePullback g.right (fun _ : Fin (n + 1) => g.left) fun _ => g.hom] (F : f ⟶ g) :
f.cechNerve ⟶ g.cechNerve where
app n := WidePullback.lift (WidePullback.base _ ≫ F.right) (fun i => WidePullback.π _ i ≫ F.left) fun j => by simp
