English
Given a morphism F between arrows f ⟶ g in a category, there is a natural morphism of Čech conerves F: f.cechConerve ⟶ g.cechConerve whose nth component is constructed by the universal property of the wide pushout using F's left and right components.
Русский
Для морфизма F между стрелками f ⟶ g в категории существует естественный морфизм ČechConerve F: f.cechConerve ⟶ g.cechConerve, чьи компоненты на уровне n строятся с использованием универсального свойства широкого pushout через части F слева и справа.
LaTeX
$$$$ F: f \to g \quad\Rightarrow\quad f.cechConerve \to g.cechConerve, \; (F)_{\!n} = \text{WidePushout.desc}(F.left \circ \text{WidePushout.head}, \; i \mapsto F.right \circ \text{WidePushout.ι}^i). $$$$
Lean4
/-- The morphism between Čech conerves associated to a morphism of arrows. -/
@[simps]
def mapCechConerve {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.cechConerve ⟶ g.cechConerve where
app
n :=
WidePushout.desc (F.left ≫ WidePushout.head _) (fun i => F.right ≫ (by apply WidePushout.ι _ i))
(fun i => (by rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]))
