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}
[CategoryTheory.Category.{u_2, u_1} C]
{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.
theorem
CategoryTheory.CommSq.w
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(self : CategoryTheory.CommSq f g h i)
:
The square commutes.
theorem
CategoryTheory.CommSq.w_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z✝}
{i : Y ⟶ Z✝}
(self : CategoryTheory.CommSq f g h✝ i)
{Z : C}
(h : Z✝ ⟶ Z)
:
theorem
CategoryTheory.CommSq.flip
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CategoryTheory.CommSq f g h i)
:
CategoryTheory.CommSq g f i h
theorem
CategoryTheory.CommSq.of_arrow
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{f : CategoryTheory.Arrow C}
{g : CategoryTheory.Arrow C}
(h : f ⟶ g)
:
CategoryTheory.CommSq f.hom h.left h.right g.hom
theorem
CategoryTheory.CommSq.op
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CategoryTheory.CommSq f g h i)
:
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}
[CategoryTheory.Category.{u_2, u_1} C]
{W : Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{Z : Cᵒᵖ}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(p : CategoryTheory.CommSq f g h i)
:
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}
[CategoryTheory.Category.{u_2, u_1} C]
{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}
[CategoryTheory.Category.{u_2, u_1} C]
{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}
[CategoryTheory.Category.{u_2, u_1} C]
{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₁ : CategoryTheory.CommSq f g h i)
(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}
[CategoryTheory.Category.{u_2, u_1} C]
{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₁ : CategoryTheory.CommSq f g h i)
(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.CommSq.eq_of_mono
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{f : W ⟶ X}
{g : W ⟶ X}
{i : X ⟶ Y}
[CategoryTheory.Mono i]
(sq : CategoryTheory.CommSq f g i i)
:
f = g
theorem
CategoryTheory.CommSq.eq_of_epi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{W : C}
{X : C}
{Y : C}
{f : W ⟶ X}
{h : X ⟶ Y}
{i : X ⟶ Y}
[CategoryTheory.Epi f]
(sq : CategoryTheory.CommSq f f h i)
:
h = i
theorem
CategoryTheory.Functor.map_commSq
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : CategoryTheory.CommSq f g h i)
:
CategoryTheory.CommSq (F.map f) (F.map g) (F.map h) (F.map i)
theorem
CategoryTheory.CommSq.map
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : W ⟶ X}
{g : W ⟶ Y}
{h : X ⟶ Z}
{i : Y ⟶ Z}
(s : CategoryTheory.CommSq f g h i)
:
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
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g} {x y : sq.LiftStruct}, x.l = y.l → x = y
theorem
CategoryTheory.CommSq.LiftStruct.ext_iff
{C : Type u_1}
:
∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g} {x y : sq.LiftStruct}, x = y ↔ x.l = y.l
structure
CategoryTheory.CommSq.LiftStruct
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
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 : CategoryTheory.CategoryStruct.comp i self.l = f
The upper left triangle commutes.
- fac_right : CategoryTheory.CategoryStruct.comp self.l p = g
The lower right triangle commutes.
theorem
CategoryTheory.CommSq.LiftStruct.fac_left
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(self : sq.LiftStruct)
:
CategoryTheory.CategoryStruct.comp i self.l = f
The upper left triangle commutes.
theorem
CategoryTheory.CommSq.LiftStruct.fac_right
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(self : sq.LiftStruct)
:
CategoryTheory.CategoryStruct.comp self.l p = g
The lower right triangle commutes.
@[simp]
theorem
CategoryTheory.CommSq.LiftStruct.op_l
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(l : sq.LiftStruct)
:
l.op.l = l.l.op
def
CategoryTheory.CommSq.LiftStruct.op
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(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 := ⋯ }
@[simp]
theorem
CategoryTheory.CommSq.LiftStruct.unop_l
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(l : sq.LiftStruct)
:
l.unop.l = l.l.unop
def
CategoryTheory.CommSq.LiftStruct.unop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(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 := ⋯ }
@[simp]
theorem
CategoryTheory.CommSq.LiftStruct.opEquiv_symm_apply
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
(l : ⋯.LiftStruct)
:
(CategoryTheory.CommSq.LiftStruct.opEquiv sq).symm l = l.unop
@[simp]
theorem
CategoryTheory.CommSq.LiftStruct.opEquiv_apply
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
(l : sq.LiftStruct)
:
(CategoryTheory.CommSq.LiftStruct.opEquiv sq) l = l.op
def
CategoryTheory.CommSq.LiftStruct.opEquiv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
sq.LiftStruct ≃ ⋯.LiftStruct
Equivalences of LiftStruct for a square and the corresponding square
in the opposite category.
Equations
- CategoryTheory.CommSq.LiftStruct.opEquiv sq = { toFun := CategoryTheory.CommSq.LiftStruct.op, invFun := CategoryTheory.CommSq.LiftStruct.unop, left_inv := ⋯, right_inv := ⋯ }
def
CategoryTheory.CommSq.LiftStruct.unopEquiv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
sq.LiftStruct ≃ ⋯.LiftStruct
Equivalences of LiftStruct for a square in the oppositive category and
the corresponding square in the original category.
Equations
- CategoryTheory.CommSq.LiftStruct.unopEquiv sq = { toFun := CategoryTheory.CommSq.LiftStruct.unop, invFun := CategoryTheory.CommSq.LiftStruct.op, left_inv := ⋯, right_inv := ⋯ }
instance
CategoryTheory.CommSq.subsingleton_liftStruct_of_epi
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[CategoryTheory.Epi i]
:
Subsingleton sq.LiftStruct
Equations
- ⋯ = ⋯
instance
CategoryTheory.CommSq.subsingleton_liftStruct_of_mono
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[CategoryTheory.Mono p]
:
Subsingleton sq.LiftStruct
Equations
- ⋯ = ⋯
class
CategoryTheory.CommSq.HasLift
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
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}
:
∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g} [self : sq.HasLift], Nonempty sq.LiftStruct
Square has a LiftStruct.
theorem
CategoryTheory.CommSq.HasLift.mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
{sq : CategoryTheory.CommSq f i p g}
(l : sq.LiftStruct)
:
sq.HasLift
theorem
CategoryTheory.CommSq.HasLift.iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
theorem
CategoryTheory.CommSq.HasLift.iff_op
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
sq.HasLift ↔ ⋯.HasLift
theorem
CategoryTheory.CommSq.HasLift.iff_unop
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : Cᵒᵖ}
{B : Cᵒᵖ}
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
:
sq.HasLift ↔ ⋯.HasLift
noncomputable def
CategoryTheory.CommSq.lift
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[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
@[simp]
theorem
CategoryTheory.CommSq.fac_left_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[hsq : sq.HasLift]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.CommSq.fac_left
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[hsq : sq.HasLift]
:
CategoryTheory.CategoryStruct.comp i sq.lift = f
@[simp]
theorem
CategoryTheory.CommSq.fac_right_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[hsq : sq.HasLift]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.CommSq.fac_right
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{X : C}
{Y : C}
{f : A ⟶ X}
{i : A ⟶ B}
{p : X ⟶ Y}
{g : B ⟶ Y}
(sq : CategoryTheory.CommSq f i p g)
[hsq : sq.HasLift]
:
CategoryTheory.CategoryStruct.comp sq.lift p = g