Documentation

Mathlib.CategoryTheory.Limits.Elements

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.

source
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 (CategoryTheory.Functor.Elements A)) :
CategoryTheory.Limits.limit (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A)) 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
    source
    @[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 (CategoryTheory.Functor.Elements A)) (i : I) :
    CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A)) A) i (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F) = (F.obj i).snd
    source
    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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
    A.obj (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (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
      source
      @[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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) (c : CategoryTheory.Limits.Cone F) :
      A.map (CategoryTheory.Limits.limit.lift (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A)) ((CategoryTheory.CategoryOfElements.π A).mapCone c)) c.pt.snd = CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
      source
      @[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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) (i : I) :
      A.map (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A)) i) (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F) = (F.obj i).snd
      source
      @[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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.snd = CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F
      source
      @[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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) (i : I) :
      ↑((CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).π.app i) = CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A)) i
      source
      @[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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F).pt.fst = CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π A))
      source
      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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
      CategoryTheory.Limits.Cone F

      (implementation) The constructured limit cone.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
        (CategoryTheory.CategoryOfElements.π A).mapCone (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F) ≅ CategoryTheory.Limits.limit.cone (CategoryTheory.Functor.comp F (CategoryTheory.CategoryOfElements.π 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
          source
          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] [CategoryTheory.Limits.HasLimitsOfShape I C] [CategoryTheory.Limits.PreservesLimitsOfShape I A] (F : CategoryTheory.Functor I (CategoryTheory.Functor.Elements A)) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F)

          (implementation) The constuctured limit cone is a limit cone.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitElementsCategoryOfElementsπ {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 (CategoryTheory.Functor.Elements A)) :
            CategoryTheory.CreatesLimit F (CategoryTheory.CategoryOfElements.π A)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsCategoryOfElementsπ {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.CreatesLimitsOfShape I (CategoryTheory.CategoryOfElements.π A)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            instance CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElementsCategoryOfElements {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 (CategoryTheory.Functor.Elements A)
            Equations
            • ⋯ = ⋯