# 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, CommSq top left right bottom is the predicate that this square is commutative.

The structure CommSq is extended in CategoryTheory/Shapes/Limits/CommSq.lean as IsPullback and IsPushout in order to define pullback and pushout squares.

## Future work #

Refactor LiftStruct from Arrow.lean and lifting properties using CommSq.lean.

structure CategoryTheory.CommSq {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) :

The proposition that a square

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



is a commuting square.

• The square commutes.

Instances For
theorem CategoryTheory.CommSq.w {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (self : ) :

The square commutes.

theorem CategoryTheory.CommSq.w_assoc {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z✝} {i : Y Z✝} (self : ) {Z : C} (h : Z✝ Z) :
theorem CategoryTheory.CommSq.flip {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
theorem CategoryTheory.CommSq.of_arrow {C : Type u_1} [] {f : } {g : } (h : f g) :
CategoryTheory.CommSq f.hom h.left h.right g.hom
theorem CategoryTheory.CommSq.op {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
CategoryTheory.CommSq i.op h.op g.op f.op

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

theorem CategoryTheory.CommSq.unop {C : Type u_1} [] {W : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : ) :
CategoryTheory.CommSq i.unop h.unop g.unop f.unop

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

theorem CategoryTheory.CommSq.vert_inv {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {f : W X} {i : Y Z} {g : W Y} {h : X Z} (p : CategoryTheory.CommSq f g.hom h.hom i) :
CategoryTheory.CommSq i g.inv h.inv f
theorem CategoryTheory.CommSq.horiz_inv {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} {g : W Y} {h : X Z} {f : W X} {i : Y Z} (p : CategoryTheory.CommSq f.hom g h i.hom) :
CategoryTheory.CommSq f.inv h g i.inv
theorem CategoryTheory.CommSq.horiz_comp {C : Type u_1} [] {W : C} {X : C} {X' : C} {Y : C} {Z : C} {Z' : C} {f : W X} {f' : X X'} {g : W Y} {h : X Z} {h' : X' Z'} {i : Y Z} {i' : Z Z'} (hsq₁ : ) (hsq₂ : CategoryTheory.CommSq f' h h' i') :

The horizontal composition of two commutative squares as below is a commutative square.

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


theorem CategoryTheory.CommSq.vert_comp {C : Type u_1} [] {W : C} {X : C} {Y : C} {Y' : C} {Z : C} {Z' : C} {f : W X} {g : W Y} {g' : Y Y'} {h : X Z} {h' : Z Z'} {i : Y Z} {i' : Y' Z'} (hsq₁ : ) (hsq₂ : CategoryTheory.CommSq i g' h' i') :

The vertical composition of two commutative squares as below is a commutative square.

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


theorem CategoryTheory.Functor.map_commSq {C : Type u_1} [] {D : Type u_2} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
theorem CategoryTheory.CommSq.map {C : Type u_1} [] {D : Type u_2} [] (F : ) {W : C} {X : C} {Y : C} {Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : ) :
CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)

Alias of CategoryTheory.Functor.map_commSq.

theorem CategoryTheory.CommSq.LiftStruct.ext_iff {C : Type u_1} :
∀ {inst : } {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (x y : sq.LiftStruct), x = y x.l = y.l
theorem CategoryTheory.CommSq.LiftStruct.ext {C : Type u_1} :
∀ {inst : } {A B X Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (x y : sq.LiftStruct), x.l = y.lx = y
structure CategoryTheory.CommSq.LiftStruct {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
Type u_2

Now we consider a square:

  A ---f---> X
|          |
i          p
|          |
v          v
B ---g---> Y


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

• l : B X

The lift.

• fac_left : = f

The upper left triangle commutes.

• fac_right : = g

The lower right triangle commutes.

Instances For
theorem CategoryTheory.CommSq.LiftStruct.fac_left {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (self : sq.LiftStruct) :
= f

The upper left triangle commutes.

theorem CategoryTheory.CommSq.LiftStruct.fac_right {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (self : sq.LiftStruct) :
= g

The lower right triangle commutes.

@[simp]
theorem CategoryTheory.CommSq.LiftStruct.op_l {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (l : sq.LiftStruct) :
l.op.l = l.l.op
def CategoryTheory.CommSq.LiftStruct.op {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (l : sq.LiftStruct) :
.LiftStruct

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

Equations
• l.op = { l := l.l.op, fac_left := , fac_right := }
Instances For
@[simp]
theorem CategoryTheory.CommSq.LiftStruct.unop_l {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (l : sq.LiftStruct) :
l.unop.l = l.l.unop
def CategoryTheory.CommSq.LiftStruct.unop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (l : sq.LiftStruct) :
.LiftStruct

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

Equations
• l.unop = { l := l.l.unop, fac_left := , fac_right := }
Instances For
@[simp]
theorem CategoryTheory.CommSq.LiftStruct.opEquiv_apply {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) (l : sq.LiftStruct) :
= l.op
@[simp]
theorem CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) (l : .LiftStruct) :
.symm l = l.unop
def CategoryTheory.CommSq.LiftStruct.opEquiv {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
sq.LiftStruct .LiftStruct

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

Equations
• = { toFun := CategoryTheory.CommSq.LiftStruct.op, invFun := CategoryTheory.CommSq.LiftStruct.unop, left_inv := , right_inv := }
Instances For
def CategoryTheory.CommSq.LiftStruct.unopEquiv {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
sq.LiftStruct .LiftStruct

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

Equations
• = { toFun := CategoryTheory.CommSq.LiftStruct.unop, invFun := CategoryTheory.CommSq.LiftStruct.op, left_inv := , right_inv := }
Instances For
instance CategoryTheory.CommSq.subsingleton_liftStruct_of_epi {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
Subsingleton sq.LiftStruct
Equations
• =
instance CategoryTheory.CommSq.subsingleton_liftStruct_of_mono {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
Subsingleton sq.LiftStruct
Equations
• =
class CategoryTheory.CommSq.HasLift {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :

The assertion that a square has a LiftStruct.

• exists_lift : Nonempty sq.LiftStruct

Square has a LiftStruct.

Instances
theorem CategoryTheory.CommSq.HasLift.exists_lift {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } [self : sq.HasLift] :
Nonempty sq.LiftStruct

Square has a LiftStruct.

theorem CategoryTheory.CommSq.HasLift.mk' {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} {sq : } (l : sq.LiftStruct) :
sq.HasLift
theorem CategoryTheory.CommSq.HasLift.iff {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
sq.HasLift Nonempty sq.LiftStruct
theorem CategoryTheory.CommSq.HasLift.iff_op {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
sq.HasLift .HasLift
theorem CategoryTheory.CommSq.HasLift.iff_unop {C : Type u_1} [] {A : Cᵒᵖ} {B : Cᵒᵖ} {X : Cᵒᵖ} {Y : Cᵒᵖ} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) :
sq.HasLift .HasLift
noncomputable def CategoryTheory.CommSq.lift {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) [hsq : sq.HasLift] :
B X

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

Equations
• sq.lift = .some.l
Instances For
@[simp]
theorem CategoryTheory.CommSq.fac_left_assoc {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) [hsq : sq.HasLift] {Z : C} (h : X Z) :
@[simp]
theorem CategoryTheory.CommSq.fac_left {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) [hsq : sq.HasLift] :
= f
@[simp]
theorem CategoryTheory.CommSq.fac_right_assoc {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) [hsq : sq.HasLift] {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.CommSq.fac_right {C : Type u_1} [] {A : C} {B : C} {X : C} {Y : C} {f : A X} {i : A B} {p : X Y} {g : B Y} (sq : ) [hsq : sq.HasLift] :
= g