English
Same idempotence for ind-ind under the same hypothesis as 78053.
Русский
Та же идемпотентность для ind-ind при той же гипотезе, что и в 78053.
LaTeX
$$$\mathrm{ind}(\mathrm{ind}(P)) = \mathrm{ind}(P) \quad \text{if } P \leq \mathrm{isFinitelyPresentable}(C).$$$
Lean4
/-- `ind` is idempotent if `P` implies finitely presentable. -/
theorem ind_ind (h : P ≤ isFinitelyPresentable.{w} C) [LocallySmall.{w} C] : ind.{w} (ind.{w} P) = ind.{w} P :=
by
refine le_antisymm (fun X h ↦ ?_) (le_ind P.ind)
choose J Jc Jf pres K Kc Kf pres' hp using h
have (j : J) (i : K j) : IsFinitelyPresentable ((pres' j).diag.obj i) := h _ (hp _ _)
have := IsFiltered.of_equivalence (ShrinkHoms.equivalence (ColimitPresentation.Total pres'))
exact
⟨_, inferInstance, inferInstance, (pres.bind pres').reindex (ShrinkHoms.equivalence _).inverse, fun k ↦ by
simp [hp]⟩
