Pullback and pushout squares #
We provide another API for pullbacks and pushouts.
is_pullback fst snd f g
is the proposition that
P --fst--> X
| |
snd f
| |
v v
Y ---g---> Z
is a pullback square.
(And similarly for is_pushout
.)
We provide the glue to go back and forth to the usual is_limit
API for pullbacks, and prove
is_pullback (pullback.fst : pullback f g ⟶ X) (pullback.snd : pullback f g ⟶ Y) f g
for the usual pullback f g
provided by the has_limit
API.
We don't attempt to restate everything we know about pullbacks in this language, but do restate the pasting lemmas.
Future work #
Bicartesian squares, and show that the pullback and pushout squares for a biproduct are bicartesian.
The (not necessarily limiting) pullback_cone h i
implicit in the statement
that we have comm_sq f g h i
.
Equations
The (not necessarily limiting) pushout_cocone f g
implicit in the statement
that we have comm_sq f g h i
.
Equations
The pushout cocone in the opposite category associated to the cone of a commutative square identifies to the cocone of the flipped commutative square in the opposite category
Equations
The pullback cone in the opposite category associated to the cocone of a commutative square identifies to the cone of the flipped commutative square in the opposite category
Equations
The pushout cocone obtained from the pullback cone associated to a commutative square in the opposite category identifies to the cocone associated to the flipped square.
Equations
The pullback cone obtained from the pushout cone associated to a commutative square in the opposite category identifies to the cone associated to the flipped square.
Equations
- to_comm_sq : category_theory.comm_sq fst snd f g
- is_limit' : nonempty (category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk fst snd _))
The proposition that a square
P --fst--> X
| |
snd f
| |
v v
Y ---g---> Z
is a pullback square.
- to_comm_sq : category_theory.comm_sq f g inl inr
- is_colimit' : nonempty (category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk inl inr _))
The proposition that a square
Z ---f---> X
| |
g inl
| |
v v
Y --inr--> P
is a pushout square.
We begin by providing some glue between is_pullback
and the is_limit
and has_limit
APIs.
(And similarly for is_pushout
.)
The (limiting) pullback_cone f g
implicit in the statement
that we have a is_pullback fst snd f g
.
The cone obtained from is_pullback fst snd f g
is a limit cone.
If c
is a limiting pullback cone, then we have a is_pullback c.fst c.snd f g
.
A variant of of_is_limit
that is more useful with apply
.
The pullback provided by has_pullback f g
fits into a is_pullback
.
If c
is a limiting binary product cone, and we have a terminal object,
then we have is_pullback c.fst c.snd 0 0
(where each 0
is the unique morphism to the terminal object).
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the has_limit
API.
Equations
- h.iso_pullback = (category_theory.limits.limit.iso_limit_cone {cone := h.cone, is_limit := h.is_limit}).symm
The (colimiting) pushout_cocone f g
implicit in the statement
that we have a is_pushout f g inl inr
.
The cocone obtained from is_pushout f g inl inr
is a colimit cocone.
Equations
- h.is_colimit = _.some
If c
is a colimiting pushout cocone, then we have a is_pushout f g c.inl c.inr
.
A variant of of_is_colimit
that is more useful with apply
.
The pushout provided by has_pushout f g
fits into a is_pushout
.
If c
is a colimiting binary coproduct cocone, and we have an initial object,
then we have is_pushout 0 0 c.inl c.inr
(where each 0
is the unique morphism from the initial object).
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the has_limit
API.
Equations
The square with 0 : 0 ⟶ 0
on the left and 𝟙 X
on the right is a pullback square.
The square with 0 : 0 ⟶ 0
on the top and 𝟙 X
on the bottom is a pullback square.
Paste two pullback squares "vertically" to obtain another pullback square.
Paste two pullback squares "horizontally" to obtain another pullback square.
Given a pullback square assembled from a commuting square on the top and a pullback square on the bottom, the top square is a pullback square.
Given a pullback square assembled from a commuting square on the left and a pullback square on the right, the left square is a pullback square.
The square with 0 : 0 ⟶ 0
on the right and 𝟙 X
on the left is a pushout square.
The square with 0 : 0 ⟶ 0
on the bottom and 𝟙 X
on the top is a pushout square.
Paste two pushout squares "vertically" to obtain another pushout square.
Paste two pushout squares "horizontally" to obtain another pushout square.
Given a pushout square assembled from a pushout square on the top and a commuting square on the bottom, the bottom square is a pushout square.
Given a pushout square assembled from a pushout square on the left and a commuting square on the right, the right square is a pushout square.
Alias of category_theory.functor.map_is_pullback
.
Alias of category_theory.functor.map_is_pushout
.