English
Let J be a linear order and F : J → C a diagram which is IsWellOrderContinuous. For any j ∈ J, restrict F to the upper set Ici(j) and compose with the inclusion, obtaining a diagram on the subposet (Subtype.mono_coe(Set.Ici j)) → J → C; this restricted diagram is again IsWellOrderContinuous.
Русский
Пусть J — линейный порядок, F: J → C диаграмма с IsWellOrderContinuous. Для любого j∈J ограничим F на верхнее множество Ici(j) и получим диаграмму на подчасти; эта ограниченная диаграмма также имеет IsWellOrderContinuous.
LaTeX
$$$\\operatorname{IsWellOrderContinuous} \\big( (\\mathrm{Subtype}.mono\\_coe(\\mathrm{Set.Ici}(j)) \\right) .\\text{functor} \\; \\circ F \\big)$ for each $j$.$$
Lean4
instance restriction_setIci {J : Type w} [LinearOrder J] {F : J ⥤ C} [F.IsWellOrderContinuous] (j : J) :
((Subtype.mono_coe (Set.Ici j)).functor ⋙ F).IsWellOrderContinuous where
nonempty_isColimit m
hm :=
⟨by
let f : Set.Iio m → Set.Iio m.1 := fun ⟨⟨a, ha⟩, ha'⟩ ↦ ⟨a, ha'⟩
have hf : Monotone f := fun _ _ h ↦ h
have : hf.functor.Final := by
rw [Monotone.final_functor_iff]
rintro ⟨j', hj'⟩
simp only [Set.mem_Iio] at hj'
dsimp only [f]
by_cases h : j' ≤ j
· refine ⟨⟨⟨j, le_refl j⟩, ?_⟩, h⟩
by_contra!
simp only [Set.mem_Iio, not_lt] at this
apply hm.1
rintro ⟨k, hk⟩ hkm
exact this.trans hk
· simp only [not_le] at h
exact ⟨⟨⟨j', h.le⟩, hj'⟩, by rfl⟩
exact
(Functor.Final.isColimitWhiskerEquiv (F := hf.functor) _).2
(F.isColimitOfIsWellOrderContinuous m.1 (Set.Ici.isSuccLimit_coe m hm))⟩
