# Documentation

Mathlib.CategoryTheory.CommSq

# 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 square commutes.

The proposition that a square

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



is a commuting square.

Instances For
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.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 : ), 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 : ), 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
• l : B X

The lift.

• fac_left :

The upper left triangle commutes.

• fac_right :

The lower right triangle commutes.

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.

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

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

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

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

Instances For
@[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 : CategoryTheory.CommSq.LiftStruct (_ : CategoryTheory.CommSq g.op p.op i.op f.op)) :
@[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 : ) :
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 : ) :

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

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

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

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

Square has a LiftStruct.

The assertion that a square has a LiftStruct.

Instances
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 : ) :
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 : ) :
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 : ) :
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 : ) :
CategoryTheory.CommSq.HasLift (_ : CategoryTheory.CommSq g.unop p.unop i.unop f.unop)
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 : ] :
B X

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

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 : ] {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 : ] :
@[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 : ] {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 : ] :