Documentation

Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Constructing limits from products and equalizers. #

If a category has all products, and all equalizers, then it has all limits. Similarly, if it has all finite products, and all equalizers, then it has all finite limits.

If a functor preserves all products and equalizers, then it preserves all limits. Similarly, if it preserves all finite products and equalizers, then it preserves all finite limits.

TODO #

Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.

def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Fan F.obj} {c₂ : Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : Fork s t) :

(Implementation) Given the appropriate product and equalizer cones, build the cone for F which is limiting if the given cones are also.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Fan F.obj} {c₂ : Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : Fork s t) :
    (buildLimit s t hs ht i).pt = i.pt
    @[simp]
    theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Fan F.obj} {c₂ : Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) (i : Fork s t) (x✝ : J) :
    (buildLimit s t hs ht i).π.app x✝ = CategoryStruct.comp i.ι (c₁.π.app { as := x✝ })
    def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Fan F.obj} {c₂ : Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp s (c₂.π.app { as := f }) = CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) {i : Fork s t} (t₁ : IsLimit c₁) (t₂ : IsLimit c₂) (hi : IsLimit i) :
    IsLimit (buildLimit s t hs ht i)

    (Implementation) Show the cone constructed in buildLimit is limiting, provided the cones used in its construction are.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def CategoryTheory.Limits.limitConeOfEqualizerAndProduct {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] (F : Functor J C) [HasLimit (Discrete.functor F.obj)] [HasLimit (Discrete.functor fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2)] [HasEqualizers C] :

      Given the existence of the appropriate (possibly finite) products and equalizers, we can construct a limit cone for F. (This assumes the existence of all equalizers, which is technically stronger than needed.)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Given the existence of the appropriate (possibly finite) products and equalizers, we know a limit of F exists. (This assumes the existence of all equalizers, which is technically stronger than needed.)

        noncomputable def CategoryTheory.Limits.limitSubobjectProduct {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [HasLimitsOfSize.{w, w, v, u} C] (F : Functor J C) :
        limit F ∏ᶜ fun (j : J) => F.obj j

        A limit can be realised as a subobject of a product.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Any category with finite products and equalizers has all finite limits.

          Stacks Tag 002O

          If a functor preserves equalizers and the appropriate products, it preserves limits.

          If a functor creates equalizers and the appropriate products, it creates limits.

          We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating limits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            If a functor creates equalizers and finite products, it creates finite limits.

            We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating limits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              If a functor creates equalizers and products, it creates limits.

              We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating limits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                If a functor creates terminal objects and pullbacks, it creates finite limits.

                We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating limits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  We now dualize the above constructions, resorting to copy-paste.

                  def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : Cofan F.obj} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : Cofork s t) :

                  (Implementation) Given the appropriate coproduct and coequalizer cocones, build the cocone for F which is colimiting if the given cocones are also.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : Cofan F.obj} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : Cofork s t) (x✝ : J) :
                    (buildColimit s t hs ht i).ι.app x✝ = CategoryStruct.comp (c₂.ι.app { as := x✝ }) i.π
                    @[simp]
                    theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : Cofan F.obj} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) (i : Cofork s t) :
                    (buildColimit s t hs ht i).pt = i.pt
                    def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] {F : Functor J C} {c₁ : Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : Cofan F.obj} (s t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) s = CategoryStruct.comp (F.map f.snd) (c₂.ι.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryStruct.comp (c₁.ι.app { as := f }) t = c₂.ι.app { as := f.fst.1 }) {i : Cofork s t} (t₁ : IsColimit c₁) (t₂ : IsColimit c₂) (hi : IsColimit i) :
                    IsColimit (buildColimit s t hs ht i)

                    (Implementation) Show the cocone constructed in buildColimit is colimiting, provided the cocones used in its construction are.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Given the existence of the appropriate (possibly finite) coproducts and coequalizers, we can construct a colimit cocone for F. (This assumes the existence of all coequalizers, which is technically stronger than needed.)

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Given the existence of the appropriate (possibly finite) coproducts and coequalizers, we know a colimit of F exists. (This assumes the existence of all coequalizers, which is technically stronger than needed.)

                        noncomputable def CategoryTheory.Limits.colimitQuotientCoproduct {C : Type u} [Category.{v, u} C] {J : Type w} [SmallCategory J] [HasColimitsOfSize.{w, w, v, u} C] (F : Functor J C) :
                        ( fun (j : J) => F.obj j) colimit F

                        A colimit can be realised as a quotient of a coproduct.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits.

                          If a functor creates coequalizers and the appropriate coproducts, it creates colimits.

                          We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating colimits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            If a functor creates coequalizers and finite coproducts, it creates finite colimits.

                            We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating colimits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              If a functor creates coequalizers and coproducts, it creates colimits.

                              We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating colimits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For

                                If a functor creates initial objects and pushouts, it creates finite colimits.

                                We additionally require the rather strong condition that the functor reflects isomorphisms. It is unclear whether the statement remains true without this condition. There are various definitions of "creating colimits" in the literature, and whether or not the condition can be dropped seems to depend on the specific definition that is used.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For