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

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) :

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 {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_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.τ₄

@[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.

Equations

One or more equations did not get rendered due to their size.

@[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.

Equations

One or more equations did not get rendered due to their size.

@[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)

Equations

One or more equations did not get rendered due to their size.

@[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_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_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

Equations

One or more equations did not get rendered due to their size.

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

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

Equations

sq.flip = { X₁ := sq.X₁, X₂ := sq.X₃, X₃ := sq.X₂, X₄ := sq.X₄, f₁₂ := sq.f₁₃, f₁₃ := sq.f₁₂, f₂₄ := sq.f₃₄, f₃₄ := sq.f₂₄, fac := ⋯ }

@[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_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₃

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

Functor (Square C) (Square C)

The functor which flips commutative squares.

Equations

One or more equations did not get rendered due to their size.

@[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 φ).τ₄ = φ.τ₄

@[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 φ).τ₁ = φ.τ₁

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

Square C ≌ Square C

Flipping commutative squares is an auto-equivalence.

Equations

One or more equations did not get rendered due to their size.

@[simp]

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

flipEquivalence.inverse = flipFunctor

@[simp]

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

flipEquivalence.functor = flipFunctor

@[simp]

theorem CategoryTheory.Square.flipEquivalence_unitIso {C : Type u} [Category.{v, u} C] :

flipEquivalence.unitIso = Iso.refl (Functor.id (Square C))

@[simp]

theorem CategoryTheory.Square.flipEquivalence_counitIso {C : Type u} [Category.{v, u} C] :

flipEquivalence.counitIso = Iso.refl (flipFunctor.comp flipFunctor)

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.

Equations

One or more equations did not get rendered due to their size.

@[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_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_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_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_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_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_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_right {C : Type u} [Category.{v, u} C] {X✝ Y✝ : Square C} (φ : X✝ ⟶ Y✝) :

(toArrowArrowFunctor.map φ).right.right = φ.τ₄

@[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_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.

Equations

One or more equations did not get rendered due to their size.

@[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.hom.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.left.hom

@[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 φ).τ₁ = φ.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.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.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_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

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.

Equations

One or more equations did not get rendered due to their size.

@[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_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))

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.

Equations

One or more equations did not get rendered due to their size.

@[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_hom_left {C : Type u} [Category.{v, u} C] (sq : Square C) :

(toArrowArrowFunctor'.obj sq).hom.left = 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'_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_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_left {C : Type u} [Category.{v, u} C] (sq : Square C) :

(toArrowArrowFunctor'.obj sq).right.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'_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_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_right {C : Type u} [Category.{v, u} C] (sq : Square C) :

(toArrowArrowFunctor'.obj sq).right.right = 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₁₂

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.

Equations

One or more equations did not get rendered due to their size.

@[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_X₁ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) :

(fromArrowArrowFunctor'.obj f).X₁ = f.left.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.right.hom

@[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.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'_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'_obj_X₃ {C : Type u} [Category.{v, u} C] (f : Arrow (Arrow C)) :

(fromArrowArrowFunctor'.obj f).X₃ = f.right.left

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.

Equations

One or more equations did not get rendered due to their size.

@[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'_functor {C : Type u} [Category.{v, u} C] :

arrowArrowEquivalence'.functor = toArrowArrowFunctor'

@[simp]

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

arrowArrowEquivalence'.inverse = fromArrowArrowFunctor'

@[simp]

theorem CategoryTheory.Square.arrowArrowEquivalence'_counitIso {C : Type u} [Category.{v, u} C] :

arrowArrowEquivalence'.counitIso = Iso.refl (fromArrowArrowFunctor'.comp toArrowArrowFunctor')

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

Functor (Square C) C

The top-left evaluation Square C ⥤ C.

Equations

CategoryTheory.Square.evaluation₁ = { obj := fun (sq : CategoryTheory.Square C) => sq.X₁, map := fun {X Y : CategoryTheory.Square C} (φ : X ⟶ Y) => φ.τ₁, map_id := ⋯, map_comp := ⋯ }

@[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.

Equations

CategoryTheory.Square.evaluation₂ = { obj := fun (sq : CategoryTheory.Square C) => sq.X₂, map := fun {X Y : CategoryTheory.Square C} (φ : X ⟶ Y) => φ.τ₂, map_id := ⋯, map_comp := ⋯ }

@[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.

Equations

CategoryTheory.Square.evaluation₃ = { obj := fun (sq : CategoryTheory.Square C) => sq.X₃, map := fun {X Y : CategoryTheory.Square C} (φ : X ⟶ Y) => φ.τ₃, map_id := ⋯, map_comp := ⋯ }

@[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.

Equations

CategoryTheory.Square.evaluation₄ = { obj := fun (sq : CategoryTheory.Square C) => sq.X₄, map := fun {X Y : CategoryTheory.Square C} (φ : X ⟶ Y) => φ.τ₄, map_id := ⋯, map_comp := ⋯ }

@[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) :

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

Equations

sq.op = { X₁ := Opposite.op sq.X₄, X₂ := Opposite.op sq.X₂, X₃ := Opposite.op sq.X₃, X₄ := Opposite.op sq.X₁, f₁₂ := sq.f₂₄.op, f₁₃ := sq.f₃₄.op, f₂₄ := sq.f₁₂.op, f₃₄ := sq.f₁₃.op, fac := ⋯ }

@[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_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

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

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

Equations

One or more equations did not get rendered due to their size.

@[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

@[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_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

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

Functor (Square C)ᵒᵖ (Square Cᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

@[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

@[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

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

Functor (Square Cᵒᵖ)ᵒᵖ (Square C)

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

Equations

One or more equations did not get rendered due to their size.

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

(Square C)ᵒᵖ ≌ Square Cᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

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) :

The image of a commutative square by a functor.

Equations

sq.map F = { X₁ := F.obj sq.X₁, X₂ := F.obj sq.X₂, X₃ := F.obj sq.X₃, X₄ := F.obj sq.X₄, f₁₂ := F.map sq.f₁₂, f₁₃ := F.map sq.f₁₃, f₂₄ := F.map sq.f₂₄, f₃₄ := F.map sq.f₃₄, fac := ⋯ }

@[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_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_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₁

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.

Equations

One or more equations did not get rendered due to their size.

@[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_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 φ.τ₃

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.

Equations

One or more equations did not get rendered due to their size.

@[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.

Equations

One or more equations did not get rendered due to their size.

@[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 τ