English
Let C be a category and W a morphism property. If F : ComposableArrows C n is a diagram of n+1 objects with every connecting map F.obj i.castSucc ⟶ F.obj i.succ lying in W, then the total morphism F.hom: F.left ⟶ F.right is a transfinite composition of shape Fin(n+1) of morphisms in W.
Русский
Пусть C - категория, W - свойство морфизмов. Пусть F : ComposableArrows C n задаёт диаграмму из n+1 объектов с тем, что каждый переходной морфизм F.obj i.castSucc ⟶ F.obj i.succ принадлежит W; тогда общий морфизм F.hom: F.left ⟶ F.right является трансфинитной композицией по форме Fin(n+1) из морфизмов из W.
LaTeX
$$$F\mathrm{.hom} \in W.\mathrm{TransfiniteCompositionOfShape}(\mathrm{Fin}(n+1))\, F.\mathrm{hom}$$$
Lean4
/-- If `F : ComposableArrows C n` and all maps `F.obj i.castSucc ⟶ F.obj i.succ`
are in `W`, then `F.hom : F.left ⟶ F.right` is a transfinite composition of
shape `Fin (n + 1)` of morphisms in `W`. -/
@[simps!]
def ofComposableArrows {n : ℕ} (F : ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (homOfLE i.castSucc_le_succ))) :
W.TransfiniteCompositionOfShape (Fin (n + 1)) F.hom
where
toTransfiniteCompositionOfShape := .ofComposableArrows F
map_mem j
hj := by
obtain ⟨j, rfl⟩ | rfl := j.eq_castSucc_or_eq_last
· replace hF := hF j
rw [← W.arrow_mk_mem_toSet_iff] at hF ⊢
have eq : Arrow.mk (homOfLE (Order.le_succ j.castSucc)) = Arrow.mk (homOfLE j.castSucc_le_succ) :=
Arrow.ext rfl j.orderSucc_castSucc rfl
replace eq := congr_arg F.mapArrow.obj eq
convert hF using 1
· rw [isMax_iff_eq_top] at hj
exact (hj rfl).elim
