Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Preserving (co)equalizers #

Constructions to relate the notions of preserving (co)equalizers and reflecting (co)equalizers to concrete (co)forks.

In particular, we show that equalizerComparison f g G is an isomorphism iff G preserves the limit of the parallel pair f,g, as well as the dual result.

The map of a fork is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute Fork.ofι with Functor.mapCone.

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

    If the equalizer comparison map for G at (f,g) is an isomorphism, then G preserves the equalizer of (f,g).

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

      If G preserves the equalizer of (f,g), then the equalizer comparison map for G at (f,g) is an isomorphism.

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

        The map of a cofork is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute Cofork.ofπ with Functor.mapCocone.

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

          If the coequalizer comparison map for G at (f,g) is an isomorphism, then G preserves the coequalizer of (f,g).

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

            If G preserves the coequalizer of (f,g), then the coequalizer comparison map for G at (f,g) is an isomorphism.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[instance 1]

              Any functor preserves coequalizers of split pairs.

              Equations
              • One or more equations did not get rendered due to their size.
              @[instance 1]
              Equations
              • One or more equations did not get rendered due to their size.