English
A morphism f: X → Y lies in ind(P) if and only if its corresponding object in the under category Under.mk f lies in ObjectProperty.ind of P.underObj.
Русский
Морфизм f: X → Y принадлежит ind(P) тогда и только тогда, когда соответствующий объект в категории Under.mk f принадлежит ObjectProperty.ind(P.underObj).
LaTeX
$$$ \mathrm{ind}\, f \;\leftrightarrow\; \mathrm{ObjectProperty}.\mathrm{ind} \; (P.underObj) \; (\mathrm{Under.mk} f)$$$
Lean4
theorem ind_iff_ind_underMk {X Y : C} (f : X ⟶ Y) :
ind.{w} P f ↔ ObjectProperty.ind.{w} P.underObj (CategoryTheory.Under.mk f) :=
by
refine ⟨fun ⟨J, _, _, D, t, s, hs, hst⟩ ↦ ?_, fun ⟨J, _, _, pres, hpres⟩ ↦ ?_⟩
· refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
· exact { app j := CategoryTheory.Under.homMk (s.app j) (by simp [hst]) }
· have : Nonempty J := IsFiltered.nonempty
exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs
· simp [underObj, hst]
· refine ⟨J, ‹_›, ‹_›, pres.diag ⋙ CategoryTheory.Under.forget _, ?_, ?_, ?_, fun j ↦ ⟨?_, ?_⟩⟩
· exact { app j := (pres.diag.obj j).hom }
· exact Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)
· exact isColimitOfPreserves (CategoryTheory.Under.forget _) pres.isColimit
· exact hpres j
· simp
