English
The transfinite iteration functor Φ.iterationFunctor J is well-order continuous, i.e., it preserves the directed limits along the well-order J in the appropriate sense.
Русский
У трансфинитной итерационной функцийтора Φ.итерационнаяФункctor J есть свойство непрерывности по хорошо упорядочению: он сохраняет соответствующие пределы вдоль порядка J.
LaTeX
$$$(Φ.iterationFunctor J).IsWellOrderContinuous$$$
Lean4
instance : (Φ.iterationFunctor J).IsWellOrderContinuous where
nonempty_isColimit i
hi :=
⟨by
let e :
(Set.principalSegIio i).monotone.functor ⋙ (Φ.iterationFunctor J) ≅ restrictionLT (Φ.iter i).F (by simp) :=
NatIso.ofComponents (fun _ ↦ eqToIso (Φ.iterationFunctor_obj _ _ _))
(by
rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f
apply Arrow.mk_injective
simpa using Φ.arrowMk_iterationFunctor_map k₁ k₂ (leOfHom f) (Φ.iter i) h₂.le)
refine (IsColimit.precomposeInvEquiv e _).1 ?_
refine IsColimit.ofIsoColimit ((Φ.iter i).isColimit i hi (by simp)) ?_
refine Cocones.ext (eqToIso (Φ.iterationFunctor_obj i (Φ.iter i) (by simp)).symm) ?_
rintro ⟨k, hk⟩
apply Arrow.mk_injective
simp [Φ.arrowMk_iterationFunctor_map k i hk.le (Φ.iter i) (by simp), e]⟩
