Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

Commutative squares that are pushout or pullback squares #

In this file, we translate the IsPushout and IsPullback API for the objects of the category Square C of commutative squares in a category C. We also obtain lemmas which states in this language that a pullback of a monomorphism is a monomorphism (and similarly for pushouts of epimorphisms).

source
@[reducible, inline]
abbrev CategoryTheory.Square.pullbackCone {C : Type u} [Category.{v, u} C] (sq : Square C) :
Limits.PullbackCone sq.f₂₄ sq.f₃₄

The pullback cone attached to a commutative square.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev CategoryTheory.Square.pushoutCocone {C : Type u} [Category.{v, u} C] (sq : Square C) :
    Limits.PushoutCocone sq.f₁₂ sq.f₁₃

    The pushout cocone attached to a commutative square.

    Equations
    Instances For
      source
      def CategoryTheory.Square.IsPullback {C : Type u} [Category.{v, u} C] (sq : Square C) :
      Prop

      The condition that a commutative square is a pullback square.

      Equations
      Instances For
        source
        def CategoryTheory.Square.IsPushout {C : Type u} [Category.{v, u} C] (sq : Square C) :
        Prop

        The condition that a commutative square is a pushout square.

        Equations
        Instances For
          source
          theorem CategoryTheory.Square.isPullback_iff {C : Type u} [Category.{v, u} C] (sq : Square C) :
          sq.IsPullback ↔ Nonempty (Limits.IsLimit sq.pullbackCone)
          source
          theorem CategoryTheory.Square.isPushout_iff {C : Type u} [Category.{v, u} C] (sq : Square C) :
          sq.IsPushout ↔ Nonempty (Limits.IsColimit sq.pushoutCocone)
          source
          theorem CategoryTheory.Square.IsPullback.mk {C : Type u} [Category.{v, u} C] (sq : Square C) (h : Limits.IsLimit sq.pullbackCone) :
          sq.IsPullback
          source
          theorem CategoryTheory.Square.IsPushout.mk {C : Type u} [Category.{v, u} C] (sq : Square C) (h : Limits.IsColimit sq.pushoutCocone) :
          sq.IsPushout
          source
          noncomputable def CategoryTheory.Square.IsPullback.isLimit {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPullback) :
          Limits.IsLimit sq.pullbackCone

          If a commutative square sq is a pullback square, then sq.pullbackCone is limit.

          Equations
          Instances For
            source
            noncomputable def CategoryTheory.Square.IsPushout.isColimit {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPushout) :
            Limits.IsColimit sq.pushoutCocone

            If a commutative square sq is a pushout square, then sq.pushoutCocone is colimit.

            Equations
            Instances For
              source
              theorem CategoryTheory.Square.IsPullback.of_iso {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (h : sq₁.IsPullback) (e : sq₁ ≅ sq₂) :
              sq₂.IsPullback
              source
              theorem CategoryTheory.Square.IsPullback.iff_of_iso {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
              sq₁.IsPullback ↔ sq₂.IsPullback
              source
              theorem CategoryTheory.Square.IsPushout.of_iso {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (h : sq₁.IsPushout) (e : sq₁ ≅ sq₂) :
              sq₂.IsPushout
              source
              theorem CategoryTheory.Square.IsPushout.iff_of_iso {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
              sq₁.IsPushout ↔ sq₂.IsPushout
              source
              theorem CategoryTheory.Square.IsPushout.op {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPushout) :
              sq.op.IsPullback
              source
              theorem CategoryTheory.Square.IsPushout.unop {C : Type u} [Category.{v, u} C] {sq : Square Cᵒᵖ} (h : sq.IsPushout) :
              sq.unop.IsPullback
              source
              theorem CategoryTheory.Square.IsPullback.op {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPullback) :
              sq.op.IsPushout
              source
              theorem CategoryTheory.Square.IsPullback.unop {C : Type u} [Category.{v, u} C] {sq : Square Cᵒᵖ} (h : sq.IsPullback) :
              sq.unop.IsPushout
              source
              theorem CategoryTheory.Square.IsPullback.flip {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPullback) :
              sq.flip.IsPullback
              source
              theorem CategoryTheory.Square.IsPullback.mono_f₁₃ {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPullback) [Mono sq.f₂₄] :
              Mono sq.f₁₃
              source
              theorem CategoryTheory.Square.IsPullback.mono_f₁₂ {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPullback) [Mono sq.f₃₄] :
              Mono sq.f₁₂
              source
              theorem CategoryTheory.Square.IsPushout.flip {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPushout) :
              sq.flip.IsPushout
              source
              theorem CategoryTheory.Square.IsPushout.epi_f₂₄ {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPushout) [Epi sq.f₁₃] :
              Epi sq.f₂₄
              source
              theorem CategoryTheory.Square.IsPushout.epi_f₃₄ {C : Type u} [Category.{v, u} C] {sq : Square C} (h : sq.IsPushout) [Epi sq.f₁₂] :
              Epi sq.f₃₄