English
Let F: J ⥤ C be a diagram in a category C, c a colimit cocone of F, X and Y objects in C, p: X → Y a morphism, f: F.obj ⊥ ⟶ X and g: c.pt ⟶ Y. For a fixed index j in a linear ordered index J, and a SqStruct c p f g j, there is a commutative square connecting F.obj j to X and F.obj (succ j) to c.pt via the structure maps; this square witnesses a lifting property crucial for stability of left lifting properties under transfinite composition.
Русский
Пусть F: J ⥤ C—диаграмма в категории C, c — кокон-колимит к F, X и Y — объекты, p: X ⟶ Y — морфизм, f: F.obj ⊥ ⟶ X и g: c.pt ⟶ Y. Для фиксированного индекса j ∈ J и SqStruct c p f g j существует коммутативный квадрат между F.obj j → X и F.obj (succ j) → c.pt, построенный с помощью f', F.map(homOfLE(Order.le_succ j)) и г, доказывающий свойство лифтинга, необходимое для перехода к трансфинитной композиции.
LaTeX
$$$$ \;p \circ f' = (\\iota_{\\operatorname{succ}(j)} \\circ g) \\circ F(\\mathrm{homOfLE}(\\mathrm{Order.le\\_succ}(j))) $$$$
Lean4
/-- Given `sq' : SqStruct c p f g j`, this is the commutative square
```
sq'.f'
F.obj j --------------------> X
| |
| |p
v g v
F.obj (succ j) ---> c.pt ---> Y
```
(Using the lifting property for this square is the key ingredient
in the proof that the left lifting property with respect to `p`
is stable under transfinite composition.) -/
theorem sq [SuccOrder J] : CommSq sq'.f' (F.map (homOfLE (Order.le_succ j))) p (c.ι.app _ ≫ g) where w := by simp
