Limits in the category of elements #
We show that if C
has limits of shape I
and A : C ⥤ Type w
preserves limits of shape I
, then
the category of elements of A
has limits of shape I
and the forgetful functor
π : A.Elements ⥤ C
creates them.
noncomputable def
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
:
CategoryTheory.Limits.limit ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A)
(implementation) A system (Fi, fi)_i
of elements induces an element in lim_i A(Fi)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
(i : I)
:
CategoryTheory.Limits.limit.π ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A) i
(CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F) = (F.obj i).snd
noncomputable def
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
A.obj (CategoryTheory.Limits.limit (F.comp (CategoryTheory.CategoryOfElements.π A)))
(implementation) A system (Fi, fi)_i
of elements induces an element in A(lim_i Fi)
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
(c : CategoryTheory.Limits.Cone F)
:
A.map
(CategoryTheory.Limits.limit.lift (F.comp (CategoryTheory.CategoryOfElements.π A))
((CategoryTheory.CategoryOfElements.π A).mapCone c))
c.pt.snd = CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
(i : I)
:
A.map (CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i)
(CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F) = (F.obj i).snd
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
(i : I)
:
↑((CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).π.app i) = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
@[simp]
theorem
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
noncomputable def
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
(implementation) The constructured limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.CategoryOfElements.CreatesLimitsAux.isValidLift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
(implementation) The constructed limit cone is a lift of the limit cone in C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.CategoryOfElements.CreatesLimitsAux.isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
(F : CategoryTheory.Functor I A.Elements)
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
(implementation) The constuctured limit cone is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
CategoryTheory.CategoryOfElements.instCreatesLimitElementsπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
(F : CategoryTheory.Functor I A.Elements)
:
Equations
- One or more equations did not get rendered due to their size.
noncomputable instance
CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
Equations
- CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ = { CreatesLimit := fun {K : CategoryTheory.Functor I A.Elements} => inferInstance }
instance
CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{A : CategoryTheory.Functor C (Type w)}
{I : Type u₁}
[CategoryTheory.Category.{v₁, u₁} I]
[Small.{w, u₁} I]
[CategoryTheory.Limits.HasLimitsOfShape I C]
[CategoryTheory.Limits.PreservesLimitsOfShape I A]
:
CategoryTheory.Limits.HasLimitsOfShape I A.Elements
Equations
- ⋯ = ⋯