Documentation

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Multi-(co)equalizers #

A multiequalizer is an equalizer of two morphisms between two products. Since both products and equalizers are limits, such an object is again a limit. This file provides the diagram whose limit is indeed such an object. In fact, it is well-known that any limit can be obtained as a multiequalizer. The dual construction (multicoequalizers) is also provided.

Projects #

Prove that a multiequalizer can be identified with an equalizer between products (and analogously for multicoequalizers).

Prove that the limit of any diagram is a multiequalizer (and similarly for colimits).

inductive CategoryTheory.Limits.WalkingMulticospan {L : Type w} {R : Type w} (fst : RL) (snd : RL) :

The type underlying the multiequalizer diagram.

Instances For
    inductive CategoryTheory.Limits.WalkingMultispan {L : Type w} {R : Type w} (fst : LR) (snd : LR) :

    The type underlying the multiecoqualizer diagram.

    Instances For

      This is a structure encapsulating the data necessary to define a Multicospan.

      Instances For
        structure CategoryTheory.Limits.MultispanIndex (C : Type u) [CategoryTheory.Category.{v, u} C] :
        Type (max (max u v) (w + 1))

        This is a structure encapsulating the data necessary to define a Multispan.

        Instances For

          Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over the two morphsims ∏ I.left ⇉ ∏ I.right. This is the diagram of the latter.

          Instances For
            @[inline, reducible]

            Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over the two morphsims ∐ I.left ⇉ ∐ I.right. This is the diagram of the latter.

            Instances For
              @[inline, reducible]

              A multifork is a cone over a multicospan.

              Instances For
                @[inline, reducible]

                A multicofork is a cocone over a multispan.

                Instances For

                  The maps from the cone point of a multifork to the objects on the left.

                  Instances For

                    The category of multiforks is equivalent to the category of forks over ∏ I.left ⇉ ∏ I.right. It then follows from CategoryTheory.IsLimit.ofPreservesConeTerminal (or reflects) that it preserves and reflects limit cones.

                    Instances For

                      The maps to the cocone point of a multicofork from the objects on the right.

                      Instances For

                        The category of multicoforks is equivalent to the category of coforks over ∐ I.left ⇉ ∐ I.right. It then follows from CategoryTheory.IsColimit.ofPreservesCoconeInitial (or reflects) that it preserves and reflects colimit cocones.

                        Instances For
                          @[inline, reducible]

                          For I : MulticospanIndex C, we say that it has a multiequalizer if the associated multicospan has a limit.

                          Instances For
                            @[inline, reducible]

                            For I : MultispanIndex C, we say that it has a multicoequalizer if the associated multicospan has a limit.

                            Instances For