Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Pullbacks and monomorphisms #

This file provides some results about interactions between pullbacks and monomorphisms, as well as the dual statements between pushouts and epimorphisms.

Main results #

The dual notions for pushouts are also available.

Monomorphisms are stable under pullback in the first argument.

Monomorphisms are stable under pullback in the second argument.

The pullback cone (𝟙 X, 𝟙 X) for the pair (f, f) is a limit if f is a mono. The converse is shown in mono_of_pullback_is_id.

Equations
Instances For

    f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is given in PullbackCone.is_id_of_mono.

    Suppose f and g are two morphisms with a common codomain and s is a limit cone over the diagram formed by f and g. Suppose f and g both factor through a monomorphism h via x and y, respectively. Then s is also a limit cone over the diagram formed by x and y.

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

      If W is the pullback of f, g, it is also the pullback of f ≫ i, g ≫ i for any mono i.

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

        The pullback of a monomorphism is a monomorphism

        Equations
        • =

        The pullback of a monomorphism is a monomorphism

        Equations
        • =

        The pullback of f, g is also the pullback of f ≫ i, g ≫ i for any mono i.

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

          The pushout cocone (𝟙 X, 𝟙 X) for the pair (f, f) is a colimit if f is an epi. The converse is shown in epi_of_isColimit_mk_id_id.

          Equations
          Instances For

            f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f). The converse is given in PushoutCocone.isColimitMkIdId.

            def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : X W) [CategoryTheory.Epi h] (x : W Y) (y : W Z) (hhx : CategoryTheory.CategoryStruct.comp h x = f) (hhy : CategoryTheory.CategoryStruct.comp h y = g) (s : CategoryTheory.Limits.PushoutCocone f g) (hs : CategoryTheory.Limits.IsColimit s) :
            let_fun reassoc₁ := ; let_fun reassoc₂ := ; CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk s.inl s.inr )

            Suppose f and g are two morphisms with a common domain and s is a colimit cocone over the diagram formed by f and g. Suppose f and g both factor through an epimorphism h via x and y, respectively. Then s is also a colimit cocone over the diagram formed by x and y.

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

              If W is the pushout of f, g, it is also the pushout of h ≫ f, h ≫ g for any epi h.

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

                The pushout of an epimorphism is an epimorphism

                Equations
                • =

                The pushout of an epimorphism is an epimorphism

                Equations
                • =

                The pushout of f, g is also the pullback of h ≫ f, h ≫ g for any epi h.

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