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 #

@[reducible, inline]

The image of a pullback cone by a functor.

Equations
Instances For

    The map (as a cone) of a pullback cone is limit iff the map (as a pullback cone) is limit.

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

      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
      Instances For

        The property of preserving pullbacks expressed in terms of binary fans.

        Equations
        • One or more equations did not get rendered due to their size.
        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
              def CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (c : CategoryTheory.Limits.PullbackCone f g) :
              CategoryTheory.Limits.IsLimit c ((X_1 : Cᵒᵖ) → CategoryTheory.Limits.IsLimit (c.map (CategoryTheory.coyoneda.obj X_1)))

              A pullback cone in C is limit iff if it is so after the application of coyoneda.obj X for all X : Cᵒᵖ.

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

                The image of a pullback cone by a functor.

                Equations
                Instances For

                  The map (as a cocone) of a pushout cocone is colimit iff the map (as a pushout cocone) is limit.

                  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 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
                              def CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                              CategoryTheory.Limits.IsColimit c ((X_1 : C) → CategoryTheory.Limits.IsLimit (c.op.map (CategoryTheory.yoneda.obj X_1)))

                              A pushout cocone in C is colimit iff it becomes limit after the application of yoneda.obj X for all X : C.

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