Documentation

Mathlib.CategoryTheory.Square

The category of commutative squares #

In this file, we define a bundled version of CommSq which allows to consider commutative squares as objects in a category Square C.

The four objects in a commutative square are numbered as follows:

X₁ --> X₂
|      |
v      v
X₃ --> X₄

We define the flip functor, and two equivalences with the category Arrow (Arrow C), depending on whether we consider a commutative square as a horizontal morphism between two vertical maps (arrowArrowEquivalence) or a vertical morphism between two horizontal maps (arrowArrowEquivalence').

The category of commutative squares in a category.

  • X₁ : C

    the top-left object

  • X₂ : C

    the top-right object

  • X₃ : C

    the bottom-left object

  • X₄ : C

    the bottom-right object

  • f₁₂ : self.X₁ self.X₂

    the top morphism

  • f₁₃ : self.X₁ self.X₃

    the left morphism

  • f₂₄ : self.X₂ self.X₄

    the right morphism

  • f₃₄ : self.X₃ self.X₄

    the bottom morphism

  • fac : CategoryTheory.CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryTheory.CategoryStruct.comp self.f₁₃ self.f₃₄
Instances For
    theorem CategoryTheory.Square.commSq {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
    CategoryTheory.CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
    theorem CategoryTheory.Square.Hom.ext {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂}, x.τ₁ = y.τ₁x.τ₂ = y.τ₂x.τ₃ = y.τ₃x.τ₄ = y.τ₄x = y
    theorem CategoryTheory.Square.Hom.ext_iff {C : Type u} :
    ∀ {inst : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂}, x = y x.τ₁ = y.τ₁ x.τ₂ = y.τ₂ x.τ₃ = y.τ₃ x.τ₄ = y.τ₄

    A morphism between two commutative squares consists of 4 morphisms which extend these two squares into a commuting cube.

    Instances For
      @[simp]
      theorem CategoryTheory.Square.Hom.comm₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) :
      CategoryTheory.CategoryStruct.comp sq₁.f₁₂ self.τ₂ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₂
      @[simp]
      theorem CategoryTheory.Square.Hom.comm₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) :
      CategoryTheory.CategoryStruct.comp sq₁.f₁₃ self.τ₃ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₃
      @[simp]
      theorem CategoryTheory.Square.Hom.comm₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) :
      CategoryTheory.CategoryStruct.comp sq₁.f₂₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₂ sq₂.f₂₄
      @[simp]
      theorem CategoryTheory.Square.Hom.comm₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) :
      CategoryTheory.CategoryStruct.comp sq₁.f₃₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₃ sq₂.f₃₄

      The identity of a commutative square.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.Square.Hom.comp_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) :
        (f.comp g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
        @[simp]
        theorem CategoryTheory.Square.Hom.comp_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) :
        (f.comp g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
        @[simp]
        theorem CategoryTheory.Square.Hom.comp_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) :
        (f.comp g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
        @[simp]
        theorem CategoryTheory.Square.Hom.comp_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) :
        (f.comp g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
        def CategoryTheory.Square.Hom.comp {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) :
        sq₁.Hom sq₃

        The composition of morphisms of squares.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem CategoryTheory.Square.hom_ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {f : sq₁ sq₂} {g : sq₁ sq₂} :
          f = g f.τ₁ = g.τ₁ f.τ₂ = g.τ₂ f.τ₃ = g.τ₃ f.τ₄ = g.τ₄
          theorem CategoryTheory.Square.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} {f : sq₁ sq₂} {g : sq₁ sq₂} (h₁ : f.τ₁ = g.τ₁) (h₂ : f.τ₂ = g.τ₂) (h₃ : f.τ₃ = g.τ₃) (h₄ : f.τ₄ = g.τ₄) :
          f = g
          def CategoryTheory.Square.isoMk {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {sq₂ : CategoryTheory.Square C} (e₁ : sq₁.X₁ sq₂.X₁) (e₂ : sq₁.X₂ sq₂.X₂) (e₃ : sq₁.X₃ sq₂.X₃) (e₄ : sq₁.X₄ sq₂.X₄) (comm₁₂ : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₂) (comm₁₃ : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₃) (comm₂₄ : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom sq₂.f₂₄) (comm₃₄ : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom sq₂.f₃₄) :
          sq₁ sq₂

          Constructor for isomorphisms in Square c

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            @[simp]
            @[simp]
            theorem CategoryTheory.Square.flip_f₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
            sq.flip.f₁₂ = sq.f₁₃
            @[simp]
            @[simp]
            theorem CategoryTheory.Square.flip_f₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
            sq.flip.f₂₄ = sq.f₃₄
            @[simp]
            theorem CategoryTheory.Square.flip_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
            sq.flip.f₁₃ = sq.f₁₂
            @[simp]
            theorem CategoryTheory.Square.flip_f₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
            sq.flip.f₃₄ = sq.f₂₄
            @[simp]

            Flipping a square by switching the top-right and the bottom-left objects.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Square.flipFunctor_map_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] :
              ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.flipFunctor.map φ).τ₂ = φ.τ₃
              @[simp]
              theorem CategoryTheory.Square.flipFunctor_map_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] :
              ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.flipFunctor.map φ).τ₄ = φ.τ₄
              @[simp]
              theorem CategoryTheory.Square.flipFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
              CategoryTheory.Square.flipFunctor.obj sq = sq.flip
              @[simp]
              theorem CategoryTheory.Square.flipFunctor_map_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] :
              ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.flipFunctor.map φ).τ₃ = φ.τ₂
              @[simp]
              theorem CategoryTheory.Square.flipFunctor_map_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] :
              ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.flipFunctor.map φ).τ₁ = φ.τ₁

              The functor which flips commutative squares.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Square.flipEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.Square.flipEquivalence.inverse = CategoryTheory.Square.flipFunctor
                @[simp]
                theorem CategoryTheory.Square.flipEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.Square.flipEquivalence.functor = CategoryTheory.Square.flipFunctor
                @[simp]
                theorem CategoryTheory.Square.flipEquivalence_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
                CategoryTheory.Square.flipEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.flipFunctor.comp CategoryTheory.Square.flipFunctor)

                Flipping commutative squares is an auto-equivalence.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_map_left_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.right = φ.τ₃
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.right = sq.X₃
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.hom = sq.f₁₃
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.hom = sq.f₂₄
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.left = sq.X₁
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_hom_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.right = sq.f₃₄
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_hom_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.left = sq.f₁₂
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.right = sq.X₄
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_map_right_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.left = φ.τ₂
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_map_right_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.right = φ.τ₄
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_map_left_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.left = φ.τ₁
                  @[simp]
                  theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.left = sq.X₂

                  The functor Square C ⥤ Arrow (Arrow C) which sends a commutative square sq to the obvious arrow from the left morphism of sq to the right morphism of sq.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₁ = f.left.left
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                    ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₄ = φ.right.right
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                    ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₃ = φ.left.right
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₃ = f.left.hom
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₂₄ = f.right.hom
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₂ = f.right.left
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                    ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₁ = φ.left.left
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₃₄ = f.hom.right
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₂ = f.hom.left
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₄ = f.right.right
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                    ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₂ = φ.right.left
                    @[simp]
                    theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                    (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₃ = f.left.right

                    The functor Arrow (Arrow C) ⥤ Square C which sends a morphism Arrow.mk f ⟶ Arrow.mk g to the commutative square with f on the left side and g on the right side.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Square.arrowArrowEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] :
                      CategoryTheory.Square.arrowArrowEquivalence.inverse = CategoryTheory.Square.fromArrowArrowFunctor
                      @[simp]
                      theorem CategoryTheory.Square.arrowArrowEquivalence_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
                      CategoryTheory.Square.arrowArrowEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor.comp CategoryTheory.Square.toArrowArrowFunctor)
                      @[simp]
                      theorem CategoryTheory.Square.arrowArrowEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] :
                      CategoryTheory.Square.arrowArrowEquivalence.functor = CategoryTheory.Square.toArrowArrowFunctor

                      The equivalence Square C ≌ Arrow (Arrow C) which sends a commutative square sq to the obvious arrow from the left morphism of sq to the right morphism of sq.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.left = sq.X₁
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.left = sq.f₁₃
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.right = sq.X₂
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_map_left_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                        ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.right = φ.τ₂
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_map_left_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                        ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.left = φ.τ₁
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.hom = sq.f₃₄
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_map_right_right {C : Type u} [CategoryTheory.Category.{v, u} C] :
                        ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.right = φ.τ₄
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_left {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.left = sq.X₃
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_map_right_left {C : Type u} [CategoryTheory.Category.{v, u} C] :
                        ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.left = φ.τ₃
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.right = sq.f₂₄
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_right {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.right = sq.X₄
                        @[simp]
                        theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                        (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.hom = sq.f₁₂

                        The functor Square C ⥤ Arrow (Arrow C) which sends a commutative square sq to the obvious arrow from the top morphism of sq to the bottom morphism of sq.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                          ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₁ = φ.left.left
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₁ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₁ = f.left.left
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                          ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₄ = φ.right.right
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₂₄ = f.hom.right
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₃₄ = f.right.hom
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                          ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₃ = φ.right.left
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                          ∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₂ = φ.left.right
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₂ = f.left.right
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₃ = f.hom.left
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₄ = f.right.right
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₃ = f.right.left
                          @[simp]
                          theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) :
                          (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₂ = f.left.hom

                          The functor Arrow (Arrow C) ⥤ Square C which sends a morphism Arrow.mk f ⟶ Arrow.mk g to the commutative square with f on the top side and g on the bottom side.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Square.arrowArrowEquivalence'_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] :
                            CategoryTheory.Square.arrowArrowEquivalence'.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor'.comp CategoryTheory.Square.toArrowArrowFunctor')
                            @[simp]
                            theorem CategoryTheory.Square.arrowArrowEquivalence'_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] :
                            CategoryTheory.Square.arrowArrowEquivalence'.inverse = CategoryTheory.Square.fromArrowArrowFunctor'
                            @[simp]
                            theorem CategoryTheory.Square.arrowArrowEquivalence'_functor {C : Type u} [CategoryTheory.Category.{v, u} C] :
                            CategoryTheory.Square.arrowArrowEquivalence'.functor = CategoryTheory.Square.toArrowArrowFunctor'

                            The equivalence Square C ≌ Arrow (Arrow C) which sends a commutative square sq to the obvious arrow from the top morphism of sq to the bottom morphism of sq.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Square.evaluation₁_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                              CategoryTheory.Square.evaluation₁.obj sq = sq.X₁
                              @[simp]
                              theorem CategoryTheory.Square.evaluation₁_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                              ∀ {X Y : CategoryTheory.Square C} (φ : X Y), CategoryTheory.Square.evaluation₁.map φ = φ.τ₁

                              The top-left evaluation Square C ⥤ C.

                              Equations
                              Instances For
                                @[simp]
                                theorem CategoryTheory.Square.evaluation₂_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                ∀ {X Y : CategoryTheory.Square C} (φ : X Y), CategoryTheory.Square.evaluation₂.map φ = φ.τ₂
                                @[simp]
                                theorem CategoryTheory.Square.evaluation₂_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                CategoryTheory.Square.evaluation₂.obj sq = sq.X₂

                                The top-right evaluation Square C ⥤ C.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Square.evaluation₃_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                  CategoryTheory.Square.evaluation₃.obj sq = sq.X₃
                                  @[simp]
                                  theorem CategoryTheory.Square.evaluation₃_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), CategoryTheory.Square.evaluation₃.map φ = φ.τ₃

                                  The bottom-left evaluation Square C ⥤ C.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Square.evaluation₄_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                    CategoryTheory.Square.evaluation₄.obj sq = sq.X₄
                                    @[simp]
                                    theorem CategoryTheory.Square.evaluation₄_map {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                    ∀ {X Y : CategoryTheory.Square C} (φ : X Y), CategoryTheory.Square.evaluation₄.map φ = φ.τ₄

                                    The bottom-right evaluation Square C ⥤ C.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.Square.op_f₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                      sq.op.f₃₄ = sq.f₁₃.op
                                      @[simp]
                                      theorem CategoryTheory.Square.op_f₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                      sq.op.f₂₄ = sq.f₁₂.op
                                      @[simp]
                                      theorem CategoryTheory.Square.op_f₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                      sq.op.f₁₂ = sq.f₂₄.op
                                      @[simp]
                                      theorem CategoryTheory.Square.op_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) :
                                      sq.op.f₁₃ = sq.f₃₄.op

                                      The map Square C → Square Cᵒᵖ which switches X₁ and X₃, but does not move X₂ and X₃.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.Square.unop_f₁₃ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) :
                                        sq.unop.f₁₃ = sq.f₃₄.unop
                                        @[simp]
                                        theorem CategoryTheory.Square.unop_f₁₂ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) :
                                        sq.unop.f₁₂ = sq.f₂₄.unop
                                        @[simp]
                                        theorem CategoryTheory.Square.unop_f₂₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) :
                                        sq.unop.f₂₄ = sq.f₁₂.unop
                                        @[simp]
                                        theorem CategoryTheory.Square.unop_f₃₄ {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) :
                                        sq.unop.f₃₄ = sq.f₁₃.unop

                                        The map Square Cᵒᵖ → Square C which switches X₁ and X₃, but does not move X₂ and X₃.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Square.opFunctor_map_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                          ∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X Y), (CategoryTheory.Square.opFunctor.map φ).τ₂ = φ.unop.τ₂.op
                                          @[simp]
                                          theorem CategoryTheory.Square.opFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] (sq : (CategoryTheory.Square C)ᵒᵖ) :
                                          CategoryTheory.Square.opFunctor.obj sq = (Opposite.unop sq).op
                                          @[simp]
                                          theorem CategoryTheory.Square.opFunctor_map_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                          ∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X Y), (CategoryTheory.Square.opFunctor.map φ).τ₃ = φ.unop.τ₃.op
                                          @[simp]
                                          theorem CategoryTheory.Square.opFunctor_map_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                          ∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X Y), (CategoryTheory.Square.opFunctor.map φ).τ₄ = φ.unop.τ₁.op
                                          @[simp]
                                          theorem CategoryTheory.Square.opFunctor_map_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] :
                                          ∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X Y), (CategoryTheory.Square.opFunctor.map φ).τ₁ = φ.unop.τ₄.op

                                          The functor (Square C)ᵒᵖ ⥤ Square Cᵒᵖ.

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

                                            The functor (Square Cᵒᵖ)ᵒᵖ ⥤ Square Cᵒᵖ.

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

                                              The equivalence (Square C)ᵒᵖ ≌ Square Cᵒᵖ.

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

                                                The image of a commutative square by a functor.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapSquare_map_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) :
                                                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (F.mapSquare.map φ).τ₂ = F.map φ.τ₂
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapSquare_map_τ₄ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) :
                                                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (F.mapSquare.map φ).τ₄ = F.map φ.τ₄
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapSquare_map_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) :
                                                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (F.mapSquare.map φ).τ₃ = F.map φ.τ₃
                                                  @[simp]
                                                  theorem CategoryTheory.Functor.mapSquare_map_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) :
                                                  ∀ {X Y : CategoryTheory.Square C} (φ : X Y), (F.mapSquare.map φ).τ₁ = F.map φ.τ₁

                                                  The functor Square C ⥤ Square D induced by a functor C ⥤ D.

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

                                                    The natural transformation F.mapSquare ⟶ G.mapSquare induces by a natural transformation F ⟶ G.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.Square.mapFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] :
                                                      ∀ {X Y : CategoryTheory.Functor C D} (τ : X Y), CategoryTheory.Square.mapFunctor.map τ = CategoryTheory.NatTrans.mapSquare τ
                                                      @[simp]
                                                      theorem CategoryTheory.Square.mapFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) :
                                                      CategoryTheory.Square.mapFunctor.obj F = F.mapSquare

                                                      The functor (C ⥤ D) ⥤ Square C ⥤ Square D.

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