English
When j is a limit element, the limit extension is formed by lifting from prior stages and using compatibility to glue in the limit.
Русский
Когда j лимитный элемент, расширение через предел строится поднимая с предыдущих стадий и используя совместимость для склейки на пределе.
LaTeX
$$$\\text{limit}(j, \\text{Order.IsSuccLimit}, e)$$$
Lean4
/-- The element in `d.Extension val₀ (Order.succ j)` obtained by extending
an element in `d.Extension val₀ j` when `j` is not maximal. -/
def succ {j : J} (e : d.Extension val₀ j) (hj : ¬IsMax j) : d.Extension val₀ (Order.succ j)
where
val := d.succ j hj e.val
map_zero := by
simp only [← e.map_zero]
conv_rhs => rw [← d.map_succ j hj e.val]
rw [← FunctorToTypes.map_comp_apply]
rfl
map_succ i
hi := by
obtain hij | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq
·
rw [← homOfLE_comp ((Order.lt_succ_iff_of_not_isMax hj).mp hi) (Order.le_succ j), op_comp,
FunctorToTypes.map_comp_apply, d.map_succ, ← e.map_succ i hij, ←
homOfLE_comp (Order.succ_le_of_lt hij) (Order.le_succ j), op_comp, FunctorToTypes.map_comp_apply, d.map_succ]
· simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, homOfLE_leOfHom, d.map_succ]
map_limit i hi
hij := by
obtain hij | rfl := hij.lt_or_eq
· have hij' : i ≤ j := (Order.lt_succ_iff_of_not_isMax hj).mp hij
have := congr_arg (F.map (homOfLE hij').op) (d.map_succ j hj e.val)
rw [e.map_limit i hi, ← FunctorToTypes.map_comp_apply, ← op_comp, homOfLE_comp] at this
rw [this]
congr
ext ⟨⟨l, hl⟩⟩
dsimp
conv_lhs => rw [← d.map_succ j hj e.val]
rw [← FunctorToTypes.map_comp_apply]
rfl
· exfalso
exact hj hi.isMax
