English
The limit operation preserves the inductive structure and respects the order-theoretic bounds.
Русский
Ограничение сохраняет индуктивную структуру и учитывает порядковые границы.
LaTeX
$$$\\text{limit}_{j}(\\cdot)\\text{ satisfies compatibility and bounds}$$$
Lean4
/-- When `j` is a limit element, this is the extension to `d.Extension val₀ j`
of a family of elements in `d.Extension val₀ i` for all `i < j`. -/
def limit (j : J) (hj : Order.IsSuccLimit j) (e : ∀ (i : J) (_ : i < j), d.Extension val₀ i) : d.Extension val₀ j
where
val :=
d.lift j hj
{ val := fun ⟨i, hi⟩ ↦ (e i hi).val
property := fun f ↦ by apply compatibility }
map_zero := by
rw [d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)]
simpa only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply] using
(e ⊥ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)).map_zero
map_succ i
hi :=
by
convert
(e (Order.succ i) ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)).map_succ i
(by
simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
exact ⟨_, hi⟩) using
1
· dsimp
rw [FunctorToTypes.map_id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr hi)]
· congr
rw [d.map_lift _ _ _ _ hi]
symm
apply compatibility
map_limit i hi
hij := by
obtain hij' | rfl := hij.lt_or_eq
· have := (e i hij').map_limit i hi (by rfl)
dsimp at this ⊢
rw [FunctorToTypes.map_id_apply] at this
rw [d.map_lift _ _ _ _ hij']
dsimp
rw [this]
congr
dsimp
ext ⟨⟨l, hl⟩⟩
rw [map_lift _ _ _ _ _ (hl.trans hij')]
apply compatibility
· dsimp
rw [FunctorToTypes.map_id_apply]
congr
ext ⟨⟨l, hl⟩⟩
rw [d.map_lift _ _ _ _ hl]
