English
There is a natural morphism between augmented Čech conerves induced by a morphism of arrows; namely, for f ⟶ g there exists a morphism f.augmentedCechConerve ⟶ g.augmentedCechConerve with left part given by F.left and right part given by mapCechConerve F.
Русский
Существует естественный морфизм между дополненными Čech-конвервами, индуцируемый морфизмом стрелок; для f ⟶ g существует морфизм f.augmentedCechConerve ⟶ g.augmentedCechConerve с левой компонентой F.left и правой компонентой mapCechConerve F.
LaTeX
$$$\\exists \\Phi : f.augmentedCechConerve \\to g.augmentedCechConerve\\;\\big(\\Phi.left = F.left \\;\\land\\; \\Phi.right = \\mathrm{mapCechConerve}(F)\\big)$$$
Lean4
/-- The morphism between augmented Čech conerves associated to a morphism of arrows. -/
@[simps]
def mapAugmentedCechConerve {f g : Arrow C}
[∀ n : ℕ, HasWidePushout f.left (fun _ : Fin (n + 1) => f.right) fun _ => f.hom]
[∀ n : ℕ, HasWidePushout g.left (fun _ : Fin (n + 1) => g.right) fun _ => g.hom] (F : f ⟶ g) :
f.augmentedCechConerve ⟶ g.augmentedCechConerve
where
left := F.left
right := mapCechConerve F
