English
For a full subcategory determined by an object property P, if every outside object d has a connected CostructuredArrow P.ι d, then the inclusion P.ι is initial.
Русский
Для полной подсистемы, заданной свойством объекта P, если каждый внешний объект d имеет связанный CostructuredArrow P.ι d, то включение P.ι является начальником.
LaTeX
$$$P.\\iota.\\text{Initial}$ provided $\\forall d, \\lnot P(d) \\Rightarrow \\operatorname{IsConnected}(\\operatorname{CostructuredArrow} P.ι d)$$$
Lean4
/-- For the full subcategory induced by an object property `P` on `C`, to show initiality of
the inclusion functor it is enough to consider arrows to objects outside of the subcategory. -/
theorem initial_ι {C : Type u₁} [Category.{v₁} C] (P : ObjectProperty C)
(h : ∀ d, ¬P d → IsConnected (CostructuredArrow P.ι d)) : P.ι.Initial :=
.mk <| fun d => by
by_cases hd : P d
· have : Nonempty (CostructuredArrow P.ι d) := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩
refine
zigzag_isConnected fun ⟨c₁, ⟨⟨⟩⟩, g₁⟩ ⟨c₂, ⟨⟨⟩⟩, g₂⟩ =>
Zigzag.trans (j₂ := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩) (.of_hom ?_) (.of_inv ?_)
· apply CostructuredArrow.homMk g₁
· apply CostructuredArrow.homMk g₂
· exact h d hd
