# mathlibdocumentation

category_theory.comm_sq

# Commutative squares #

This file provide an API for commutative squares in categories. If top, left, right and bottom are four morphisms which are the edges of a square, comm_sq top left right bottom is the predicate that this square is commutative.

The structure comm_sq is extended in category_theory/shapes/limits/comm_sq.lean as is_pullback and is_pushout in order to define pullback and pushout squares.

## Future work #

Refactor lift_struct from arrow.lean and lifting properties using comm_sq.lean.

structure category_theory.comm_sq {C : Type u_1} {W X Y Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) :
Prop

The proposition that a square

  W ---f---> X
|          |
g          h
|          |
v          v
Y ---i---> Z


is a commuting square.

theorem category_theory.comm_sq.w_assoc {C : Type u_1} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (self : i) {X' : C} (f' : Z X') :
f h f' = g i f'
theorem category_theory.comm_sq.flip {C : Type u_1} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : i) :
h
theorem category_theory.comm_sq.of_arrow {C : Type u_1} {f g : category_theory.arrow C} (h : f g) :
g.hom
theorem category_theory.comm_sq.op {C : Type u_1} {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : i) :
g.op f.op

The commutative square in the opposite category associated to a commutative square.

theorem category_theory.comm_sq.unop {C : Type u_1} {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : i) :
f.unop

The commutative square associated to a commutative square in the opposite category.

theorem category_theory.functor.map_comm_sq {C : Type u_1} {D : Type u_3} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(F.map g) (F.map h) (F.map i)
theorem category_theory.comm_sq.map {C : Type u_1} {D : Type u_3} (F : C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : i) :
(F.map g) (F.map h) (F.map i)

Alias of category_theory.functor.map_comm_sq.

theorem category_theory.comm_sq.lift_struct.ext_iff {C : Type u_1} {_inst_1 : category_theory.category C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (x y : sq.lift_struct) :
x = y x.l = y.l
@[nolint, ext]
structure category_theory.comm_sq.lift_struct {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :
Type u_2
• l : B X
• fac_left' : i self.l = f
• fac_right' : self.l p = g

The datum of a lift in a commutative square, i.e. a up-right-diagonal morphism which makes both triangles commute.

Instances for category_theory.comm_sq.lift_struct
theorem category_theory.comm_sq.lift_struct.ext {C : Type u_1} {_inst_1 : category_theory.category C} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (x y : sq.lift_struct) (h : x.l = y.l) :
x = y
theorem category_theory.comm_sq.lift_struct.fac_left {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (self : sq.lift_struct) :
i self.l = f
theorem category_theory.comm_sq.lift_struct.fac_right {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (self : sq.lift_struct) :
self.l p = g
def category_theory.comm_sq.lift_struct.op {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (l : sq.lift_struct) :

A lift_struct for a commutative square gives a lift_struct for the corresponding square in the opposite category.

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.op_l {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (l : sq.lift_struct) :
l.op.l = l.l.op
def category_theory.comm_sq.lift_struct.unop {C : Type u_1} {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (l : sq.lift_struct) :

A lift_struct for a commutative square in the opposite category gives a lift_struct for the corresponding square in the original category.

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.unop_l {C : Type u_1} {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (l : sq.lift_struct) :
l.unop.l = l.l.unop
def category_theory.comm_sq.lift_struct.op_equiv {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :

Equivalences of lift_struct for a square and the corresponding square in the opposite category.

Equations
@[simp]
theorem category_theory.comm_sq.lift_struct.op_equiv_symm_apply {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) (l : _.lift_struct) :
@[simp]
theorem category_theory.comm_sq.lift_struct.op_equiv_apply {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) (l : sq.lift_struct) :
def category_theory.comm_sq.lift_struct.unop_equiv {C : Type u_1} {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :

Equivalences of lift_struct for a square in the oppositive category and the corresponding square in the original category.

Equations
@[protected, instance]
def category_theory.comm_sq.subsingleton_lift_struct_of_epi {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g)  :
@[protected, instance]
def category_theory.comm_sq.subsingleton_lift_struct_of_mono {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g)  :
@[class]
structure category_theory.comm_sq.has_lift {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :
Prop
• exists_lift :

The assertion that a square has a lift_struct.

Instances of this typeclass
theorem category_theory.comm_sq.has_lift.mk' {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : g} (l : sq.lift_struct) :
theorem category_theory.comm_sq.has_lift.iff {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :
theorem category_theory.comm_sq.has_lift.iff_op {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :
theorem category_theory.comm_sq.has_lift.iff_unop {C : Type u_1} {A B X Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) :
noncomputable def category_theory.comm_sq.lift {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) [hsq : sq.has_lift] :
B X

A choice of a diagonal morphism that is part of a lift_struct when the square has a lift.

Equations
@[simp]
theorem category_theory.comm_sq.fac_left {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) [hsq : sq.has_lift] :
i sq.lift = f
@[simp]
theorem category_theory.comm_sq.fac_left_assoc {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) [hsq : sq.has_lift] {X' : C} (f' : X X') :
i sq.lift f' = f f'
@[simp]
theorem category_theory.comm_sq.fac_right {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) [hsq : sq.has_lift] :
sq.lift p = g
@[simp]
theorem category_theory.comm_sq.fac_right_assoc {C : Type u_1} {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : g) [hsq : sq.has_lift] {X' : C} (f' : Y X') :
sq.lift p f' = g f'