English
If e ∈ d.Extension val₀ j, and from i ≤ j you consider e.ofLE, then its image under F.map equals the image at i of e; i.e., F.map (homOfLE h).op e.val = e'.val where e' = e.ofLE h.
Русский
Если e ∈ d.Extension val₀ j, то e образ по маппингу через h совпадает с образцом на i через e.ofLE.
LaTeX
$$$F.map (homOfLE h).op e.val = e'.val$$$
Lean4
instance [WellFoundedLT J] (j : J) : Subsingleton (d.Extension val₀ j) := by
induction j using SuccOrder.limitRecOn with
| isMin i hi =>
obtain rfl : i = ⊥ := by simpa using hi
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
have h₁ := e₁.map_zero
have h₂ := e₂.map_zero
simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply] at h₁ h₂
rw [h₁, h₂]
| succ i hi hi' =>
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, homOfLE_leOfHom] at h₁ h₂
rw [h₁, h₂]
congr
exact congr_arg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))
| isSuccLimit i hi hi' =>
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
have h₁ := e₁.map_limit i hi (by rfl)
have h₂ := e₂.map_limit i hi (by rfl)
simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, OrderHom.Subtype.val_coe, comp_obj, op_obj,
Monotone.functor_obj, homOfLE_leOfHom] at h₁ h₂
rw [h₁, h₂]
congr
ext ⟨⟨l, hl⟩⟩
have := hi' l hl
exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))
