Documentation

Mathlib.CategoryTheory.Limits.Pi

Limits in the category of indexed families of objects. #

Given a functor F : J β₯€ Ξ  i, C i into a category of indexed families,

  1. we can assemble a collection of cones over F β‹™ Pi.eval C i into a cone over F
  2. if all those cones are limit cones, the assembled cone is a limit cone, and
  3. if we have limits for each of F β‹™ Pi.eval C i, we can produce a HasLimit F instance
source
πŸ”Έ coverage
def CategoryTheory.pi.coneCompEval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} (c : Limits.Cone F) (i : I) :
Limits.Cone (F.comp (Pi.eval C i))

A cone over F : J β₯€ Ξ  i, C i has as its components cones over each of the F β‹™ Pi.eval C i.

Equations
    Instances For
      source
      πŸ”Έ coverage
      def CategoryTheory.pi.coconeCompEval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} (c : Limits.Cocone F) (i : I) :
      Limits.Cocone (F.comp (Pi.eval C i))

      A cocone over F : J β₯€ Ξ  i, C i has as its components cocones over each of the F β‹™ Pi.eval C i.

      Equations
        Instances For
          source
          πŸ”Έ coverage
          def CategoryTheory.pi.coneOfConeCompEval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} (c : (i : I) β†’ Limits.Cone (F.comp (Pi.eval C i))) :
          Limits.Cone F

          Given a family of cones over the F β‹™ Pi.eval C i, we can assemble these together as a Cone F.

          Equations
            Instances For
              source
              πŸ”Έ coverage
              def CategoryTheory.pi.coconeOfCoconeCompEval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} (c : (i : I) β†’ Limits.Cocone (F.comp (Pi.eval C i))) :
              Limits.Cocone F

              Given a family of cocones over the F β‹™ Pi.eval C i, we can assemble these together as a Cocone F.

              Equations
                Instances For
                  source
                  πŸ”Έ coverage
                  def CategoryTheory.pi.coneOfConeEvalIsLimit {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} {c : (i : I) β†’ Limits.Cone (F.comp (Pi.eval C i))} (P : (i : I) β†’ Limits.IsLimit (c i)) :
                  Limits.IsLimit (coneOfConeCompEval c)

                  Given a family of limit cones over the F β‹™ Pi.eval C i, assembling them together as a Cone F produces a limit cone.

                  Equations
                    Instances For
                      source
                      πŸ”Έ coverage
                      def CategoryTheory.pi.coconeOfCoconeEvalIsColimit {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} {c : (i : I) β†’ Limits.Cocone (F.comp (Pi.eval C i))} (P : (i : I) β†’ Limits.IsColimit (c i)) :
                      Limits.IsColimit (coconeOfCoconeCompEval c)

                      Given a family of colimit cocones over the F β‹™ Pi.eval C i, assembling them together as a Cocone F produces a colimit cocone.

                      Equations
                        Instances For
                          source
                          theorem CategoryTheory.pi.hasLimit_of_hasLimit_comp_eval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} [βˆ€ (i : I), Limits.HasLimit (F.comp (Pi.eval C i))] :
                          Limits.HasLimit F

                          If we have a functor F : J β₯€ Ξ  i, C i into a category of indexed families, and we have limits for each of the F β‹™ Pi.eval C i, then F has a limit.

                          source
                          theorem CategoryTheory.pi.hasColimit_of_hasColimit_comp_eval {I : Type v₁} {C : I β†’ Type u₁} [(i : I) β†’ Category.{v₁, u₁} (C i)] {J : Type v₁} [SmallCategory J] {F : Functor J ((i : I) β†’ C i)} [βˆ€ (i : I), Limits.HasColimit (F.comp (Pi.eval C i))] :
                          Limits.HasColimit F

                          If we have a functor F : J β₯€ Ξ  i, C i into a category of indexed families, and colimits exist for each of the F β‹™ Pi.eval C i, there is a colimit for F.

                          As an example, we can use this to construct particular shapes of limits in a category of indexed families.

                          With the addition of import CategoryTheory.Limits.Types.Products we can use:

                          attribute [local instance] hasLimit_of_hasLimit_comp_eval
example : hasBinaryProducts (I β†’ Type v₁) := ⟨by infer_instance⟩