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').

structure CategoryTheory.Square (C : Type u) [Category.{v, u} C] : Type (max u v)

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 : CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryStruct.comp self.f₁₃ self.f₃₄

theorem CategoryTheory.Square.commSq {C : Type u} [Category.{v, u} C] (sq : Square C) : CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄

structure CategoryTheory.Square.Hom {C : Type u} [Category.{v, u} C] (sq₁ sq₂ : Square C) : Type v

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

• τ₁ : sq₁.X₁ ⟶ sq₂.X₁

  the top-left morphism

• τ₂ : sq₁.X₂ ⟶ sq₂.X₂

  the top-right morphism

• τ₃ : sq₁.X₃ ⟶ sq₂.X₃

  the bottom-left morphism

• τ₄ : sq₁.X₄ ⟶ sq₂.X₄

  the bottom-right morphism

• comm₁₂ : CategoryStruct.comp sq₁.f₁₂ self.τ₂ = CategoryStruct.comp self.τ₁ sq₂.f₁₂
• comm₁₃ : CategoryStruct.comp sq₁.f₁₃ self.τ₃ = CategoryStruct.comp self.τ₁ sq₂.f₁₃
• comm₂₄ : CategoryStruct.comp sq₁.f₂₄ self.τ₄ = CategoryStruct.comp self.τ₂ sq₂.f₂₄
• comm₃₄ : CategoryStruct.comp sq₁.f₃₄ self.τ₄ = CategoryStruct.comp self.τ₃ sq₂.f₃₄

theorem CategoryTheory.Square.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {sq₁ sq₂ : Square C} {x y : sq₁.Hom sq₂} : x = y ↔ x.τ₁ = y.τ₁ ∧ x.τ₂ = y.τ₂ ∧ x.τ₃ = y.τ₃ ∧ x.τ₄ = y.τ₄

theorem CategoryTheory.Square.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {sq₁ sq₂ : Square C} {x y : sq₁.Hom sq₂} (τ₁ : x.τ₁ = y.τ₁) (τ₂ : x.τ₂ = y.τ₂) (τ₃ : x.τ₃ = y.τ₃) (τ₄ : x.τ₄ = y.τ₄) : x = y

@[simp]

theorem CategoryTheory.Square.Hom.comm₂₄_assoc {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₄ ⟶ Z) : CategoryStruct.comp sq₁.f₂₄ (CategoryStruct.comp self.τ₄ h) = CategoryStruct.comp self.τ₂ (CategoryStruct.comp sq₂.f₂₄ h)

@[simp]

theorem CategoryTheory.Square.Hom.comm₃₄_assoc {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₄ ⟶ Z) : CategoryStruct.comp sq₁.f₃₄ (CategoryStruct.comp self.τ₄ h) = CategoryStruct.comp self.τ₃ (CategoryStruct.comp sq₂.f₃₄ h)

@[simp]

theorem CategoryTheory.Square.Hom.comm₁₃_assoc {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₃ ⟶ Z) : CategoryStruct.comp sq₁.f₁₃ (CategoryStruct.comp self.τ₃ h) = CategoryStruct.comp self.τ₁ (CategoryStruct.comp sq₂.f₁₃ h)

@[simp]

theorem CategoryTheory.Square.Hom.comm₁₂_assoc {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₂ ⟶ Z) : CategoryStruct.comp sq₁.f₁₂ (CategoryStruct.comp self.τ₂ h) = CategoryStruct.comp self.τ₁ (CategoryStruct.comp sq₂.f₁₂ h)

def CategoryTheory.Square.Hom.id {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.Hom sq

The identity of a commutative square.

@[simp]

theorem CategoryTheory.Square.Hom.id_τ₃ {C : Type u} [Category.{v, u} C] (sq : Square C) : (id sq).τ₃ = CategoryStruct.id sq.X₃

@[simp]

theorem CategoryTheory.Square.Hom.id_τ₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : (id sq).τ₄ = CategoryStruct.id sq.X₄

@[simp]

theorem CategoryTheory.Square.Hom.id_τ₁ {C : Type u} [Category.{v, u} C] (sq : Square C) : (id sq).τ₁ = CategoryStruct.id sq.X₁

@[simp]

theorem CategoryTheory.Square.Hom.id_τ₂ {C : Type u} [Category.{v, u} C] (sq : Square C) : (id sq).τ₂ = CategoryStruct.id sq.X₂

def CategoryTheory.Square.Hom.comp {C : Type u} [Category.{v, u} C] {sq₁ sq₂ sq₃ : Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : sq₁.Hom sq₃

The composition of morphisms of squares.

@[simp]

theorem CategoryTheory.Square.Hom.comp_τ₂ {C : Type u} [Category.{v, u} C] {sq₁ sq₂ sq₃ : Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₂ = CategoryStruct.comp f.τ₂ g.τ₂

@[simp]

theorem CategoryTheory.Square.Hom.comp_τ₁ {C : Type u} [Category.{v, u} C] {sq₁ sq₂ sq₃ : Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₁ = CategoryStruct.comp f.τ₁ g.τ₁

@[simp]

theorem CategoryTheory.Square.Hom.comp_τ₃ {C : Type u} [Category.{v, u} C] {sq₁ sq₂ sq₃ : Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₃ = CategoryStruct.comp f.τ₃ g.τ₃

@[simp]

theorem CategoryTheory.Square.Hom.comp_τ₄ {C : Type u} [Category.{v, u} C] {sq₁ sq₂ sq₃ : Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₄ = CategoryStruct.comp f.τ₄ g.τ₄

instance CategoryTheory.Square.category {C : Type u} [Category.{v, u} C] : Category.{v, max u v} (Square C)

@[simp]

theorem CategoryTheory.Square.category_comp_τ₄ {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).τ₄ = CategoryStruct.comp f.τ₄ g.τ₄

@[simp]

theorem CategoryTheory.Square.category_id_τ₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : (CategoryStruct.id sq).τ₄ = CategoryStruct.id sq.X₄

@[simp]

theorem CategoryTheory.Square.category_id_τ₂ {C : Type u} [Category.{v, u} C] (sq : Square C) : (CategoryStruct.id sq).τ₂ = CategoryStruct.id sq.X₂

@[simp]

theorem CategoryTheory.Square.category_comp_τ₁ {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).τ₁ = CategoryStruct.comp f.τ₁ g.τ₁

@[simp]

theorem CategoryTheory.Square.category_id_τ₃ {C : Type u} [Category.{v, u} C] (sq : Square C) : (CategoryStruct.id sq).τ₃ = CategoryStruct.id sq.X₃

@[simp]

theorem CategoryTheory.Square.category_comp_τ₃ {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).τ₃ = CategoryStruct.comp f.τ₃ g.τ₃

@[simp]

theorem CategoryTheory.Square.category_id_τ₁ {C : Type u} [Category.{v, u} C] (sq : Square C) : (CategoryStruct.id sq).τ₁ = CategoryStruct.id sq.X₁

@[simp]

theorem CategoryTheory.Square.category_comp_τ₂ {C : Type u} [Category.{v, u} C] {X✝ Y✝ Z✝ : Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).τ₂ = CategoryStruct.comp f.τ₂ g.τ₂

theorem CategoryTheory.Square.hom_ext {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} {f g : sq₁ ⟶ sq₂} (h₁ : f.τ₁ = g.τ₁) (h₂ : f.τ₂ = g.τ₂) (h₃ : f.τ₃ = g.τ₃) (h₄ : f.τ₄ = g.τ₄) : f = g

theorem CategoryTheory.Square.hom_ext_iff {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} {f g : sq₁ ⟶ sq₂} : f = g ↔ f.τ₁ = g.τ₁ ∧ f.τ₂ = g.τ₂ ∧ f.τ₃ = g.τ₃ ∧ f.τ₄ = g.τ₄

def CategoryTheory.Square.isoMk {C : Type u} [Category.{v, u} C] {sq₁ sq₂ : Square C} (e₁ : sq₁.X₁ ≅ sq₂.X₁) (e₂ : sq₁.X₂ ≅ sq₂.X₂) (e₃ : sq₁.X₃ ≅ sq₂.X₃) (e₄ : sq₁.X₄ ≅ sq₂.X₄) (comm₁₂ : CategoryStruct.comp sq₁.f₁₂ e₂.hom = CategoryStruct.comp e₁.hom sq₂.f₁₂) (comm₁₃ : CategoryStruct.comp sq₁.f₁₃ e₃.hom = CategoryStruct.comp e₁.hom sq₂.f₁₃) (comm₂₄ : CategoryStruct.comp sq₁.f₂₄ e₄.hom = CategoryStruct.comp e₂.hom sq₂.f₂₄) (comm₃₄ : CategoryStruct.comp sq₁.f₃₄ e₄.hom = CategoryStruct.comp e₃.hom sq₂.f₃₄) : sq₁ ≅ sq₂

Constructor for isomorphisms in Square c

def CategoryTheory.Square.flip {C : Type u} [Category.{v, u} C] (sq : Square C) : Square C

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

@[simp]

theorem CategoryTheory.Square.flip_f₁₂ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.f₁₂ = sq.f₁₃

@[simp]

theorem CategoryTheory.Square.flip_f₁₃ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.f₁₃ = sq.f₁₂

@[simp]

theorem CategoryTheory.Square.flip_f₃₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.f₃₄ = sq.f₂₄

@[simp]

theorem CategoryTheory.Square.flip_f₂₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.f₂₄ = sq.f₃₄

@[simp]

theorem CategoryTheory.Square.flip_X₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.X₄ = sq.X₄

@[simp]

theorem CategoryTheory.Square.flip_X₁ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.X₁ = sq.X₁

@[simp]

theorem CategoryTheory.Square.flip_X₂ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.X₂ = sq.X₃

@[simp]

theorem CategoryTheory.Square.flip_X₃ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.flip.X₃ = sq.X₂

def CategoryTheory.Square.flipFunctor {C : Type u} [Category.{v, u} C] : Functor (Square C) (Square C)

The functor which flips commutative squares.

@[simp]

theorem CategoryTheory.Square.flipFunctor_map_τ₂ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (flipFunctor.map φ).τ₂ = φ.τ₃

@[simp]

theorem CategoryTheory.Square.flipFunctor_map_τ₄ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (flipFunctor.map φ).τ₄ = φ.τ₄

@[simp]

theorem CategoryTheory.Square.flipFunctor_map_τ₃ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (flipFunctor.map φ).τ₃ = φ.τ₂

@[simp]

theorem CategoryTheory.Square.flipFunctor_obj {C : Type u} [Category.{v, u} C] (sq : Square C) : flipFunctor.obj sq = sq.flip

@[simp]

theorem CategoryTheory.Square.flipFunctor_map_τ₁ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (flipFunctor.map φ).τ₁ = φ.τ₁

def CategoryTheory.Square.flipEquivalence {C : Type u} [Category.{v, u} C] : Square C ≌ Square C

Flipping commutative squares is an auto-equivalence.

@[simp]

theorem CategoryTheory.Square.flipEquivalence_counitIso {C : Type u} [Category.{v, u} C] : flipEquivalence.counitIso = Iso.refl (flipFunctor.comp flipFunctor)

@[simp]

theorem CategoryTheory.Square.flipEquivalence_functor {C : Type u} [Category.{v, u} C] : flipEquivalence.functor = flipFunctor

@[simp]

theorem CategoryTheory.Square.flipEquivalence_inverse {C : Type u} [Category.{v, u} C] : flipEquivalence.inverse = flipFunctor

@[simp]

theorem CategoryTheory.Square.flipEquivalence_unitIso {C : Type u} [Category.{v, u} C] : flipEquivalence.unitIso = Iso.refl (Functor.id (Square C))

def CategoryTheory.Square.toArrowArrowFunctor {C : Type u} [Category.{v, u} C] : Functor (Square C) (Arrow (Arrow C))

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.

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).right.left = sq.X₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).left.right = sq.X₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_map_left_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor.map φ).left.right = φ.τ₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_map_left_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor.map φ).left.left = φ.τ₁

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).left.left = sq.X₁

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_map_right_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor.map φ).right.right = φ.τ₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_hom_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).hom.left = sq.f₁₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_map_right_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor.map φ).right.left = φ.τ₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_left_hom {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).left.hom = sq.f₁₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_hom_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).hom.right = sq.f₃₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_hom {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).right.hom = sq.f₂₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor_obj_right_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor.obj sq).right.right = sq.X₄

def CategoryTheory.Square.fromArrowArrowFunctor {C : Type u} [Category.{v, u} C] : Functor (Arrow (Arrow C)) (Square C)

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.

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₂ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).X₂ = f.right.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₄ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor.map φ).τ₄ = φ.right.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₃₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).f₃₄ = f.hom.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₂ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor.map φ).τ₂ = φ.right.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₁ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).X₁ = f.left.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₂ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).f₁₂ = f.hom.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₁ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor.map φ).τ₁ = φ.left.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₃ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).X₃ = f.left.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_map_τ₃ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor.map φ).τ₃ = φ.left.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₂₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).f₂₄ = f.right.hom

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₃ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).f₁₃ = f.left.hom

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor_obj_X₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor.obj f).X₄ = f.right.right

def CategoryTheory.Square.arrowArrowEquivalence {C : Type u} [Category.{v, u} C] : Square C ≌ Arrow (Arrow C)

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.

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence_counitIso {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence.counitIso = Iso.refl (fromArrowArrowFunctor.comp toArrowArrowFunctor)

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence_functor {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence.functor = toArrowArrowFunctor

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence_unitIso {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence.unitIso = Iso.refl (Functor.id (Square C))

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence_inverse {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence.inverse = fromArrowArrowFunctor

def CategoryTheory.Square.toArrowArrowFunctor' {C : Type u} [Category.{v, u} C] : Functor (Square C) (Arrow (Arrow C))

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.

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_map_right_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor'.map φ).right.right = φ.τ₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_map_left_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor'.map φ).left.left = φ.τ₁

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_map_right_left {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor'.map φ).right.left = φ.τ₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_hom {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).right.hom = sq.f₃₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).left.left = sq.X₁

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).right.left = sq.X₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_hom {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).left.hom = sq.f₁₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_left_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).left.right = sq.X₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_right_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).right.right = sq.X₄

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_left {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).hom.left = sq.f₁₃

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_map_left_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (toArrowArrowFunctor'.map φ).left.right = φ.τ₂

@[simp]

theorem CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_right {C : Type u} [Category.{v, u} C] (sq : Square C) : (toArrowArrowFunctor'.obj sq).hom.right = sq.f₂₄

def CategoryTheory.Square.fromArrowArrowFunctor' {C : Type u} [Category.{v, u} C] : Functor (Arrow (Arrow C)) (Square C)

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.

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₂ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).X₂ = f.left.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₃ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).f₁₃ = f.hom.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₁ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor'.map φ).τ₁ = φ.left.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₂₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).f₂₄ = f.hom.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₃ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor'.map φ).τ₃ = φ.right.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₃₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).f₃₄ = f.right.hom

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₁ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).X₁ = f.left.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₃ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).X₃ = f.right.left

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₂ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor'.map φ).τ₂ = φ.left.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₄ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).X₄ = f.right.right

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₂ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) : (fromArrowArrowFunctor'.obj f).f₁₂ = f.left.hom

@[simp]

theorem CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₄ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Arrow (Arrow C)} (φ : X✝ ⟶ Y✝) : (fromArrowArrowFunctor'.map φ).τ₄ = φ.right.right

def CategoryTheory.Square.arrowArrowEquivalence' {C : Type u} [Category.{v, u} C] : Square C ≌ Arrow (Arrow C)

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.

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence'_inverse {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence'.inverse = fromArrowArrowFunctor'

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence'_unitIso {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence'.unitIso = Iso.refl (Functor.id (Square C))

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence'_counitIso {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence'.counitIso = Iso.refl (fromArrowArrowFunctor'.comp toArrowArrowFunctor')

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence'_functor {C : Type u} [Category.{v, u} C] : arrowArrowEquivalence'.functor = toArrowArrowFunctor'

def CategoryTheory.Square.evaluation₁ {C : Type u} [Category.{v, u} C] : Functor (Square C) C

The top-left evaluation Square C ⥤ C.

@[simp]

theorem CategoryTheory.Square.evaluation₁_obj {C : Type u} [Category.{v, u} C] (sq : Square C) : evaluation₁.obj sq = sq.X₁

@[simp]

theorem CategoryTheory.Square.evaluation₁_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : evaluation₁.map φ = φ.τ₁

def CategoryTheory.Square.evaluation₂ {C : Type u} [Category.{v, u} C] : Functor (Square C) C

The top-right evaluation Square C ⥤ C.

@[simp]

theorem CategoryTheory.Square.evaluation₂_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : evaluation₂.map φ = φ.τ₂

@[simp]

theorem CategoryTheory.Square.evaluation₂_obj {C : Type u} [Category.{v, u} C] (sq : Square C) : evaluation₂.obj sq = sq.X₂

def CategoryTheory.Square.evaluation₃ {C : Type u} [Category.{v, u} C] : Functor (Square C) C

The bottom-left evaluation Square C ⥤ C.

@[simp]

theorem CategoryTheory.Square.evaluation₃_obj {C : Type u} [Category.{v, u} C] (sq : Square C) : evaluation₃.obj sq = sq.X₃

@[simp]

theorem CategoryTheory.Square.evaluation₃_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : evaluation₃.map φ = φ.τ₃

def CategoryTheory.Square.evaluation₄ {C : Type u} [Category.{v, u} C] : Functor (Square C) C

The bottom-right evaluation Square C ⥤ C.

@[simp]

theorem CategoryTheory.Square.evaluation₄_obj {C : Type u} [Category.{v, u} C] (sq : Square C) : evaluation₄.obj sq = sq.X₄

@[simp]

theorem CategoryTheory.Square.evaluation₄_map {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : evaluation₄.map φ = φ.τ₄

def CategoryTheory.Square.op {C : Type u} [Category.{v, u} C] (sq : Square C) : Square Cᵒᵖ

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

@[simp]

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

@[simp]

theorem CategoryTheory.Square.op_X₄ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.op.X₄ = Opposite.op sq.X₁

@[simp]

theorem CategoryTheory.Square.op_X₃ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.op.X₃ = Opposite.op sq.X₃

@[simp]

theorem CategoryTheory.Square.op_X₁ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.op.X₁ = Opposite.op sq.X₄

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Square.op_X₂ {C : Type u} [Category.{v, u} C] (sq : Square C) : sq.op.X₂ = Opposite.op sq.X₂

def CategoryTheory.Square.unop {C : Type u} [Category.{v, u} C] (sq : Square Cᵒᵖ) : Square C

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Square.unop_X₃ {C : Type u} [Category.{v, u} C] (sq : Square Cᵒᵖ) : sq.unop.X₃ = Opposite.unop sq.X₃

@[simp]

theorem CategoryTheory.Square.unop_X₄ {C : Type u} [Category.{v, u} C] (sq : Square Cᵒᵖ) : sq.unop.X₄ = Opposite.unop sq.X₁

@[simp]

theorem CategoryTheory.Square.unop_X₂ {C : Type u} [Category.{v, u} C] (sq : Square Cᵒᵖ) : sq.unop.X₂ = Opposite.unop sq.X₂

@[simp]

theorem CategoryTheory.Square.unop_X₁ {C : Type u} [Category.{v, u} C] (sq : Square Cᵒᵖ) : sq.unop.X₁ = Opposite.unop sq.X₄

@[simp]

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

def CategoryTheory.Square.opFunctor {C : Type u} [Category.{v, u} C] : Functor (Square C)ᵒᵖ (Square Cᵒᵖ)

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

@[simp]

theorem CategoryTheory.Square.opFunctor_map_τ₁ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : (Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (opFunctor.map φ).τ₁ = φ.unop.τ₄.op

@[simp]

theorem CategoryTheory.Square.opFunctor_obj {C : Type u} [Category.{v, u} C] (sq : (Square C)ᵒᵖ) : opFunctor.obj sq = (Opposite.unop sq).op

@[simp]

theorem CategoryTheory.Square.opFunctor_map_τ₃ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : (Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (opFunctor.map φ).τ₃ = φ.unop.τ₃.op

@[simp]

theorem CategoryTheory.Square.opFunctor_map_τ₂ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : (Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (opFunctor.map φ).τ₂ = φ.unop.τ₂.op

@[simp]

theorem CategoryTheory.Square.opFunctor_map_τ₄ {C : Type u} [Category.{v, u} C] {X✝ Y✝ : (Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (opFunctor.map φ).τ₄ = φ.unop.τ₁.op

def CategoryTheory.Square.unopFunctor {C : Type u} [Category.{v, u} C] : Functor (Square Cᵒᵖ)ᵒᵖ (Square C)

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

def CategoryTheory.Square.opEquivalence {C : Type u} [Category.{v, u} C] : (Square C)ᵒᵖ ≌ Square Cᵒᵖ

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

def CategoryTheory.Square.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : Square D

The image of a commutative square by a functor.

@[simp]

theorem CategoryTheory.Square.map_X₃ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).X₃ = F.obj sq.X₃

@[simp]

theorem CategoryTheory.Square.map_X₂ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).X₂ = F.obj sq.X₂

@[simp]

theorem CategoryTheory.Square.map_f₂₄ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).f₂₄ = F.map sq.f₂₄

@[simp]

theorem CategoryTheory.Square.map_f₁₂ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).f₁₂ = F.map sq.f₁₂

@[simp]

theorem CategoryTheory.Square.map_X₁ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).X₁ = F.obj sq.X₁

@[simp]

theorem CategoryTheory.Square.map_f₁₃ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).f₁₃ = F.map sq.f₁₃

@[simp]

theorem CategoryTheory.Square.map_X₄ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).X₄ = F.obj sq.X₄

@[simp]

theorem CategoryTheory.Square.map_f₃₄ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (sq : Square C) (F : Functor C D) : (sq.map F).f₃₄ = F.map sq.f₃₄

def CategoryTheory.Functor.mapSquare {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : Functor (Square C) (Square D)

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

@[simp]

theorem CategoryTheory.Functor.mapSquare_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) (sq : Square C) : F.mapSquare.obj sq = sq.map F

@[simp]

theorem CategoryTheory.Functor.mapSquare_map_τ₂ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₂ = F.map φ.τ₂

@[simp]

theorem CategoryTheory.Functor.mapSquare_map_τ₁ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₁ = F.map φ.τ₁

@[simp]

theorem CategoryTheory.Functor.mapSquare_map_τ₃ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₃ = F.map φ.τ₃

@[simp]

theorem CategoryTheory.Functor.mapSquare_map_τ₄ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₄ = F.map φ.τ₄

def CategoryTheory.NatTrans.mapSquare {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) : F.mapSquare ⟶ G.mapSquare

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

@[simp]

theorem CategoryTheory.NatTrans.mapSquare_app_τ₂ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) (sq : Square C) : ((mapSquare τ).app sq).τ₂ = τ.app sq.X₂

@[simp]

theorem CategoryTheory.NatTrans.mapSquare_app_τ₃ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) (sq : Square C) : ((mapSquare τ).app sq).τ₃ = τ.app sq.X₃

@[simp]

theorem CategoryTheory.NatTrans.mapSquare_app_τ₄ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) (sq : Square C) : ((mapSquare τ).app sq).τ₄ = τ.app sq.X₄

@[simp]

theorem CategoryTheory.NatTrans.mapSquare_app_τ₁ {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {F G : Functor C D} (τ : F ⟶ G) (sq : Square C) : ((mapSquare τ).app sq).τ₁ = τ.app sq.X₁

def CategoryTheory.Square.mapFunctor {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] : Functor (Functor C D) (Functor (Square C) (Square D))

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

@[simp]

theorem CategoryTheory.Square.mapFunctor_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : mapFunctor.obj F = F.mapSquare

@[simp]

theorem CategoryTheory.Square.mapFunctor_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {X✝ Y✝ : Functor C D} (τ : X✝ ⟶ Y✝) : mapFunctor.map τ = NatTrans.mapSquare τ