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} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) :
Limits.limit ((F.comp (π A)).comp A)

(implementation) A system (Fi, fi)_i of elements induces an element in lim_i A(Fi).

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.π_liftedConeElement' {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) (i : I) :
      Limits.limit.π ((F.comp (π A)).comp A) i (liftedConeElement' F) = (F.obj i).snd
      source
      noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
      A.obj (Limits.limit (F.comp (π A)))

      (implementation) A system (Fi, fi)_i of elements induces an element in A(lim_i Fi).

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_lift_mapCone {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (c : Limits.Cone F) :
          A.map (Limits.limit.lift (F.comp (π A)) ((π A).mapCone c)) c.pt.snd = liftedConeElement F
          source
          @[simp]
          theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (i : I) :
          A.map (Limits.limit.π (F.comp (π A)) i) (liftedConeElement F) = (F.obj i).snd
          source
          noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
          Limits.Cone F

          (implementation) The constructed limit cone.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_π_app_coe {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (i : I) :
              ↑((liftedCone F).π.app i) = Limits.limit.π (F.comp (π A)) i
              source
              @[simp]
              theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_snd {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
              (liftedCone F).pt.snd = liftedConeElement F
              source
              @[simp]
              theorem CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone_pt_fst {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
              (liftedCone F).pt.fst = Limits.limit (F.comp (π A))
              source
              noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.isValidLift {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
              (π A).mapCone (liftedCone F) ≅ Limits.limit.cone (F.comp (π A))

              (implementation) The constructed limit cone is a lift of the limit cone in C.

              Equations
                Instances For
                  source
                  noncomputable def CategoryTheory.CategoryOfElements.CreatesLimitsAux.isLimit {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] (F : Functor I A.Elements) [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
                  Limits.IsLimit (liftedCone F)

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

                  Equations
                    Instances For
                      source
                      noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitElementsπ {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] (F : Functor I A.Elements) :
                      CreatesLimit F (π A)
                      Equations
                        source
                        noncomputable instance CategoryTheory.CategoryOfElements.instCreatesLimitsOfShapeElementsπ {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
                        CreatesLimitsOfShape I (π A)
                        Equations
                          source
                          instance CategoryTheory.CategoryOfElements.instHasLimitsOfShapeElements {C : Type u} [Category.{v, u} C] {A : Functor C (Type w)} {I : Type u₁} [Category.{v₁, u₁} I] [Small.{w, u₁} I] [Limits.HasLimitsOfShape I C] [Limits.PreservesLimitsOfShape I A] :
                          Limits.HasLimitsOfShape I A.Elements