Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Preserving pullbacks #

Constructions to relate the notions of preserving pullbacks and reflecting pullbacks to concrete pullback cones.

In particular, we show that pullbackComparison G f g is an isomorphism iff G preserves the pullback of f and g.

The dual is also given.

TODO #

The map of a pullback cone is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute PullbackCone.mk with Functor.mapCone.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G] [i : CategoryTheory.Limits.HasPullback f g] :
    let_fun this := ; CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (G.map CategoryTheory.Limits.pullback.fst) (G.map CategoryTheory.Limits.pullback.snd) this)

    If G preserves pullbacks and C has them, then the pullback cone constructed of the mapped morphisms of the pullback cone is a limit.

    Equations
    Instances For

      If F preserves the pullback of f, g, it also preserves the pullback of g, f.

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

        If G preserves the pullback of (f,g), then the pullback 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 pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute PushoutCocone.mk with Functor.mapCocone.

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

            If G preserves pushouts and C has them, then the pushout cocone constructed of the mapped morphisms of the pushout cocone is a colimit.

            Equations
            Instances For

              If F preserves the pushout of f, g, it also preserves the pushout of g, f.

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

                If G preserves the pushout of (f,g), then the pushout 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

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

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

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

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