There are only v-many natural transformations between Ind-objects

We provide the instance LocallySmall.{v} (FullSubcategory (IsIndObject (C := C))), which will serve as the basis for our definition of the category of Ind-objects.

Future work

The equivalence established here serves as the basis for a well-known calculation of hom-sets of ind-objects as a limit of a colimit.

noncomputable def CategoryTheory.colimitYonedaHomEquiv {C : Type u} [Category.{v, u} C] {I : Type u₁} [Category.{v₁, u₁} I] [Limits.HasColimitsOfShape I (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : Functor I C) (G : Functor Cᵒᵖ (Type v)) : (Limits.colimit (F.comp yoneda) ⟶ G) ≃ Limits.limit (F.op.comp G)

Variant of colimitYonedaHomIsoLimitOp: natural transformations with domain colimit (F ⋙ yoneda) are equivalent to a limit in a lower universe.

@[simp]

theorem CategoryTheory.colimitYonedaHomEquiv_π_apply {C : Type u} [Category.{v, u} C] {I : Type u₁} [Category.{v₁, u₁} I] [Limits.HasColimitsOfShape I (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : Functor I C) (G : Functor Cᵒᵖ (Type v)) (η : Limits.colimit (F.comp yoneda) ⟶ G) (i : Iᵒᵖ) : Limits.limit.π (F.op.comp G) i ((colimitYonedaHomEquiv F G) η) = η.app (Opposite.op (F.obj (Opposite.unop i))) ((Limits.colimit.ι (F.comp yoneda) (Opposite.unop i)).app (Opposite.op (F.obj (Opposite.unop i))) (CategoryStruct.id (Opposite.unop (Opposite.op (F.obj (Opposite.unop i))))))

instance CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda {C : Type u} [Category.{v, u} C] {I : Type u₁} [Category.{v₁, u₁} I] [Limits.HasColimitsOfShape I (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : Functor I C) (G : Functor Cᵒᵖ (Type v)) : Small.{v, max u v} (Limits.colimit (F.comp yoneda) ⟶ G)

instance CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject {C : Type u} [Category.{v, u} C] : LocallySmall.{v, max u v, max u (v + 1)} (ObjectProperty.FullSubcategory Limits.IsIndObject)