English
A morphism between arrows induces a morphism between augmented Čech nerves with left part mapCechNerve and right part the right component.
Русский
Морфизм между стрелами порождает морфизм между дополненными Čech нервами: левый компонент — mapCechNerve, правый — F.right.
LaTeX
$$$ (F : f ⟶ g) : f.augmentedCechNerve ⟶ g.augmentedCechNerve \\;\\text{with } left = mapCechNerve F, right = F.right $$$
Lean4
/-- The morphism between augmented Čech nerve associated to a morphism of arrows. -/
@[simps]
def mapAugmentedCechNerve {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.augmentedCechNerve ⟶ g.augmentedCechNerve
where
left := mapCechNerve F
right := F.right
