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} [CategoryTheory.Category.{v, u} C] {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] [CategoryTheory.Limits.HasColimitsOfShape I (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C) (G : CategoryTheory.Functor Cᵒᵖ (Type v)) :
(CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G) ≃ CategoryTheory.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
    @[simp]
    theorem CategoryTheory.colimitYonedaHomEquiv_π_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] [CategoryTheory.Limits.HasColimitsOfShape I (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C) (G : CategoryTheory.Functor Cᵒᵖ (Type v)) (η : CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G) (i : Iᵒᵖ) :
    CategoryTheory.Limits.limit.π (F.op.comp G) i ((CategoryTheory.colimitYonedaHomEquiv F G) η) = η.app (Opposite.op (F.obj (Opposite.unop i))) ((CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.yoneda) (Opposite.unop i)).app (Opposite.op (F.obj (Opposite.unop i))) (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op (F.obj (Opposite.unop i))))))
    source
    instance CategoryTheory.instSmallHomFunctorOppositeTypeColimitCompYoneda {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u₁} [CategoryTheory.Category.{v₁, u₁} I] [CategoryTheory.Limits.HasColimitsOfShape I (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C) (G : CategoryTheory.Functor Cᵒᵖ (Type v)) :
    Small.{v, max u v} (CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G)
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject {C : Type u} [CategoryTheory.Category.{v, u} C] :
    CategoryTheory.LocallySmall.{v, max u v, max u (v + 1)} (CategoryTheory.FullSubcategory CategoryTheory.Limits.IsIndObject)
    Equations
    • ⋯ = ⋯