English
Let J be a linear order with a succ-limit structure and f an initial segment of a monotone structure; then α-shaped colimits exist in C.
Русский
Пусть J — линейный порядок с succ-граничной структурой; пусть f задаёт начальный сегмент монотонной структуры; тогда существуют колимиты формы α в C.
LaTeX
$$$\text{HasColimitsOfShape}(\alpha, C)$$$
Lean4
theorem hasColimitsOfShape_of_initialSeg {α : Type*} [PartialOrder α] (f : α ≤i J) [Nonempty α] :
HasColimitsOfShape α C := by
by_cases hf : Function.Surjective f
·
exact
hasColimitsOfShape_of_equivalence (OrderIso.ofRelIsoLT (RelIso.ofSurjective f.toRelEmbedding hf)).equivalence.symm
· let s := f.toPrincipalSeg hf
obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩
induction i using SuccOrder.limitRecOn with
| isMin i hi =>
subst hi₀
exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
| succ i hi
_ =>
obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
have : OrderTop α :=
{ top := a
le_top
b := by
rw [← s.le_iff_le]
exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
infer_instance
| isSuccLimit i hi =>
subst hi₀
exact hasColimitsOfShape_of_isSuccLimit' C s hi
