English
If C is locally small, WellPowered, has limits of size w, and 𝒢 is small and coseparating, then C has an initial object.
Русский
Если C локально малый, хорошо порождаемая, имеет пределы определенного размера w, и 𝒢 является маленьким и косепарирующим, тогда у C есть начальный объект.
LaTeX
$$$[LocallySmall(C)] [WellPowered(C)] [HasLimitsOfSize(C)] {𝒢: Set C} [Small 𝒢] \Rightarrow IsCoseparating(𝒢) \Rightarrow HasInitial C$$$
Lean4
/-- An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered
category with a small coseparating set has an initial object.
In fact, it follows from the Special Adjoint Functor Theorem that `C` is already cocomplete,
see `hasColimits_of_hasLimits_of_isCoseparating`. -/
theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C] [HasLimitsOfSize.{w, w} C] {𝒢 : Set C}
[Small.{w} 𝒢] (h𝒢 : IsCoseparating 𝒢) : HasInitial C :=
by
have := hasFiniteLimits_of_hasLimitsOfSize C
haveI : HasProductsOfShape 𝒢 C := hasProductsOfShape_of_small C 𝒢
haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : 𝒢, A ⟶ (G : C))
letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : 𝒢 → C)))
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) ⟶ A) by
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)
refine fun A => ⟨⟨?_⟩, fun f => ?_⟩
· let s := Pi.lift fun f : Σ G : 𝒢, A ⟶ (G : C) => id (Pi.π (Subtype.val : 𝒢 → C)) f.1
let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))
haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A
exact Subobject.ofLEMk _ (pullback.fst _ _ : pullback s t ⟶ _) bot_le ≫ pullback.snd _ _
· suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by apply this
intro g
suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
exact
IsSplitEpi.mk'
⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le,
by
ext
simp⟩
