instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject

English

The full subcategory of Ind-objects in C is locally small.

Русский

Полная подкатегория Ind-объектов в C локально мала.

LaTeX

$$$\mathrm{LocallySmall}\big(\mathrm{ObjectProperty.FullSubcategory}(\mathrm{IsIndObject}(C))\big)$$$

Lean4

instance : LocallySmall.{v} (ObjectProperty.FullSubcategory (IsIndObject (C := C))) where
  hom_small X
    Y := by
    obtain ⟨⟨P⟩⟩ := X.2
    obtain ⟨⟨Q⟩⟩ := Y.2
    let e₁ := IsColimit.coconePointUniqueUpToIso (P.isColimit) (colimit.isColimit _)
    let e₂ := IsColimit.coconePointUniqueUpToIso (Q.isColimit) (colimit.isColimit _)
    let e₃ := Iso.homCongr e₁ e₂
    dsimp only [colimit.cocone_x] at e₃
    exact small_map e₃

Похожие утверждения