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.

@[simp]
theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) :
@[simp]
theorem CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.2 }) (i : CategoryTheory.Limits.Fork s t) (j : J) :
def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.2 }) (i : CategoryTheory.Limits.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
    def CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Fan F.obj} {c₂ : CategoryTheory.Limits.Fan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.2} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp s (c₂.app { as := f }) = CategoryTheory.CategoryStruct.comp (c₁.app { as := f.fst.1 }) (F.map f.snd)) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp t (c₂.app { as := f }) = c₁.app { as := f.fst.2 }) {i : CategoryTheory.Limits.Fork s t} (t₁ : CategoryTheory.Limits.IsLimit c₁) (t₂ : CategoryTheory.Limits.IsLimit c₂) (hi : CategoryTheory.Limits.IsLimit 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

      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.)

        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

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

          @[simp]
          theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) (j : J) :
          @[simp]
          theorem CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.1 }) (i : CategoryTheory.Limits.Cofork s t) :
          def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.1 }) (i : CategoryTheory.Limits.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
            def CategoryTheory.Limits.HasColimitOfHasCoproductsOfHasCoequalizers.buildIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type w} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J C} {c₁ : CategoryTheory.Limits.Cofan fun (f : (p : J × J) × (p.1 p.2)) => F.obj f.fst.1} {c₂ : CategoryTheory.Limits.Cofan F.obj} (s : c₁.pt c₂.pt) (t : c₁.pt c₂.pt) (hs : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) s = CategoryTheory.CategoryStruct.comp (F.map f.snd) (c₂.app { as := f.fst.2 })) (ht : ∀ (f : (p : J × J) × (p.1 p.2)), CategoryTheory.CategoryStruct.comp (c₁.app { as := f }) t = c₂.app { as := f.fst.1 }) {i : CategoryTheory.Limits.Cofork s t} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) (hi : CategoryTheory.Limits.IsColimit 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.)

                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