Documentation

Mathlib.CategoryTheory.Limits.Indization.LocallySmall

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.

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (w : F ≅ G) (j : J) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F✝] (x : carrier (limit F)) :
    (ConcreteCategory.hom (limit.π G j)) ((ConcreteCategory.hom (isoOfNatIso w).hom) x) = (ConcreteCategory.hom (w.hom.app j)) ((ConcreteCategory.hom (limit.π F j)) x)
    source
    @[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ᵒᵖ) :
    (ConcreteCategory.hom (Limits.limit.π (F.op.comp G) i)) ((colimitYonedaHomEquiv F G) η) = (ConcreteCategory.hom (η.app (Opposite.op (F.obj (Opposite.unop i))))) ((ConcreteCategory.hom ((Limits.colimit.ι (F.comp yoneda) (Opposite.unop i)).app (Opposite.op (F.obj (Opposite.unop i))))) (CategoryStruct.id (F.obj (Opposite.unop i))))
    source
    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)
    source
    instance CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject {C : Type u} [Category.{v, u} C] :
    LocallySmall.{v, max u v, max u (v + 1)} (ObjectProperty.FullSubcategory Limits.IsIndObject)