English
Given an object family obj : Fin (n+1) → C and maps mapSucc between successive indices, there exists F and e with F.obj i = obj i and F.map' i (i+1) = mapSucc i.
Русский
При заданном семействе объектов obj и отображений между соседними индексами существует F и e такими, что F.obj i = obj i и F.map' i (i+1) = mapSucc i.
LaTeX
$$$\exists F : ComposableArrows C n\;\exists e : \forall i, F.obj i ≅ obj i, \forall i< n, mapSucc ⟨i,i+1⟩ = e ⟨i,⊢⟩^{-1} \circ F.map' i (i+1) \circ e ⟨i+1,⊢⟩.hom$$$
Lean4
theorem mkOfObjOfMapSucc_exists :
∃ (F : ComposableArrows C n) (e : ∀ i, F.obj i ≅ obj i),
∀ (i : ℕ) (hi : i < n), mapSucc ⟨i, hi⟩ = (e ⟨i, _⟩).inv ≫ F.map' i (i + 1) ≫ (e ⟨i + 1, _⟩).hom :=
by
induction n with
| zero => exact ⟨mk₀ (obj 0), fun 0 => Iso.refl _, fun i hi => by simp at hi⟩
| succ n hn =>
obtain ⟨F, e, h⟩ := hn (fun i => obj i.succ) (fun i => mapSucc i.succ)
refine
⟨F.precomp (mapSucc 0 ≫ (e 0).inv), fun i =>
match i with
| 0 => Iso.refl _
| ⟨i + 1, hi⟩ => e _,
fun i hi => ?_⟩
obtain _ | i := i
· simp
· exact h i (by valid)
