English
Inductive construction of morphisms between consecutive length-(n+1) composable arrows: given α on the first vertex and β on δ₀, with a compatibility condition, produce a morphism F ⟶ G.
Русский
Индуктивное построение морфизмов между соседними последовательностями длины (n+1): заданы α и β и совместимость, образуется морфизм F ⟶ G.
LaTeX
$$$$ \\text{homMkSucc}:\\ α:\\ F.obj'0 \\to G.obj'0,\\ β:\\ F.δ_0 \\to G.δ_0,\\ w: F.map' 0 1 \\circ app' β 0 = α \\circ G.map' 0 1 \\Rightarrow F \\to G $$$$
Lean4
/-- Inductive construction of morphisms in `ComposableArrows C (n + 1)`: in order to construct
a morphism `F ⟶ G`, it suffices to provide `α : F.obj' 0 ⟶ G.obj' 0` and `β : F.δ₀ ⟶ G.δ₀`
such that `F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1`. -/
def homMkSucc (α : F.obj' 0 ⟶ G.obj' 0) (β : F.δ₀ ⟶ G.δ₀) (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1) : F ⟶ G :=
homMk
(fun i =>
match i with
| ⟨0, _⟩ => α
| ⟨i + 1, hi⟩ => app' β i)
(fun i hi => by
obtain _ | i := i
· exact w
· exact naturality' β i (i + 1))
