English
For every index j, the restricted functor to Set.Iic j has a nonempty object at every stage, ensuring a nonempty iteration construction exists at each limit stage.
Русский
Для каждого индекса j ограниченный функтор до Set.Iic j имеет ненулевой объект на каждом этапе, что обеспечивает существование неисчерпаемой итерации на каждом предельном этапе.
LaTeX
$$$\\forall j, \\exists X: (Set.Iic j).Elem,\\; X \\mapsto\\text{iteration}$$$
Lean4
/-- When `j : J` is not maximal, this is the extension in `Φ.Iteration (Order.succ j)`
of any `iter : Φ.Iteration j`. -/
noncomputable def mkOfSucc {j : J} (hj : ¬IsMax j) (iter : Φ.Iteration j) : Φ.Iteration (Order.succ j)
where
F := extendToSucc hj iter.F (Φ.toSucc _)
obj_bot := by rw [extendToSucc_obj_eq _ _ _ _ bot_le, obj_bot]
arrowSucc_eq i
hi₁ := by
rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁
obtain hi₁ | rfl := hi₁.lt_or_eq
·
rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁), ← arrowSucc_def _ _ hi₁,
iter.arrowSucc_eq i hi₁, extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]
· rw [arrowSucc_extendToSucc, toSuccArrow, extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]
arrowMap_limit i hi hij k
hk := by
have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij
rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk]
congr 1
apply Arrow.functor_ext
rintro ⟨k₁, h₁⟩ ⟨k₂, h₂⟩ f
dsimp
rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc]
rfl
