Pullback and pushout squares, and bi-Cartesian squares #
We provide another API for pullbacks and pushouts.
IsPullback 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 IsPushout
.)
We provide the glue to go back and forth to the usual IsLimit
API for pullbacks, and prove
IsPullback (pullback.fst f g) (pullback.snd f g) f g
for the usual pullback f g
provided by the HasLimit
API.
We don't attempt to restate everything we know about pullbacks in this language, but do restate the pasting lemmas.
We define bi-Cartesian squares, and show that the pullback and pushout squares for a biproduct are bi-Cartesian.
The (not necessarily limiting) PullbackCone h i
implicit in the statement
that we have CommSq f g h i
.
Equations
Instances For
The (not necessarily limiting) PushoutCocone f g
implicit in the statement
that we have CommSq f g h i
.
Equations
Instances For
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
Instances For
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
Instances For
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
Instances For
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
Instances For
The proposition that a square
P --fst--> X
| |
snd f
| |
v v
Y ---g---> Z
is a pullback square. (Also known as a fibered product or Cartesian square.)
- isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk fst snd ⋯))
the pullback cone is a limit
Instances For
The proposition that a square
Z ---f---> X
| |
g inl
| |
v v
Y --inr--> P
is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)
- isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk inl inr ⋯))
the pushout cocone is a colimit
Instances For
A bi-Cartesian square is a commutative square
W ---f---> X
| |
g h
| |
v v
Y ---i---> Z
that is both a pullback square and a pushout square.
- isLimit' : Nonempty (Limits.IsLimit (Limits.PullbackCone.mk f g ⋯))
- isColimit' : Nonempty (Limits.IsColimit (Limits.PushoutCocone.mk h i ⋯))
Instances For
We begin by providing some glue between IsPullback
and the IsLimit
and HasLimit
APIs.
(And similarly for IsPushout
.)
The (limiting) PullbackCone f g
implicit in the statement
that we have an IsPullback fst snd f g
.
Instances For
The cone obtained from IsPullback fst snd f g
is a limit cone.
Instances For
API for PullbackCone.IsLimit.lift for IsPullback
Equations
- hP.lift h k w = CategoryTheory.Limits.PullbackCone.IsLimit.lift hP.isLimit h k w
Instances For
If c
is a limiting pullback cone, then we have an IsPullback c.fst c.snd f g
.
A variant of of_isLimit
that is more useful with apply
.
Variant of of_isLimit
for an arbitrary cone on a diagram WalkingCospan ⥤ C
.
The pullback provided by HasPullback f g
fits into an IsPullback
.
If c
is a limiting binary product cone, and we have a terminal object,
then we have IsPullback c.fst c.snd 0 0
(where each 0
is the unique morphism to the terminal object).
A variant of of_is_product
that is more useful with apply
.
Any object at the top left of a pullback square is isomorphic to the object at the top left of any other pullback square with the same cospan.
Equations
Instances For
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the HasLimit
API.
Equations
- h.isoPullback = (CategoryTheory.Limits.limit.isoLimitCone { cone := h.cone, isLimit := h.isLimit }).symm
Instances For
The (colimiting) PushoutCocone f g
implicit in the statement
that we have an IsPushout f g inl inr
.
Instances For
The cocone obtained from IsPushout f g inl inr
is a colimit cocone.
Instances For
API for PushoutCocone.IsColimit.lift for IsPushout
Equations
- hP.desc h k w = CategoryTheory.Limits.PushoutCocone.IsColimit.desc hP.isColimit h k w
Instances For
If c
is a colimiting pushout cocone, then we have an IsPushout f g c.inl c.inr
.
A variant of of_isColimit
that is more useful with apply
.
Variant of of_isColimit
for an arbitrary cocone on a diagram WalkingSpan ⥤ C
.
The pushout provided by HasPushout f g
fits into an IsPushout
.
If c
is a colimiting binary coproduct cocone, and we have an initial object,
then we have IsPushout 0 0 c.inl c.inr
(where each 0
is the unique morphism from the initial object).
A variant of of_is_coproduct
that is more useful with apply
.
Any object at the bottom right of a pushout square is isomorphic to the object at the bottom right of any other pushout square with the same span.
Equations
Instances For
Any object at the top left of a pullback square is
isomorphic to the pullback provided by the HasLimit
API.
Equations
- h.isoPushout = (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := h.cocone, isColimit := h.isColimit }).symm
Instances For
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.
The square with 0 : 0 ⟶ 0
on the right and 𝟙 X
on the left is a pullback square.
The square with 0 : 0 ⟶ 0
on the bottom and 𝟙 X
on the top is a pullback square.
Paste two pullback squares "vertically" to obtain another pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
Paste two pullback squares "horizontally" to obtain another pullback square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
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.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
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 objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
Variant of IsPullback.of_right
where h₁₁
is induced from a morphism h₁₃ : X₁₁ ⟶ X₁₃
, and
the universal property of the right square.
The objects fit in the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
Variant of IsPullback.of_bot
, where v₁₁
is induced from a morphism v₃₁ : X₁₁ ⟶ X₃₁
, and
the universal property of the bottom square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pullback square.
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pullback square.
The pullback of biprod.inl
and biprod.inr
is the zero object.
Equations
- CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr = CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }
Instances For
The following diagram is a pullback
X --f--> Z
| |
id id
v v
X --f--> Z
The following diagram is a pullback
X --id--> X
| |
f f
v v
Z --id--> Z
In a category, given a morphism f : A ⟶ B
and an object X
,
this is the obvious pullback diagram:
A ⨯ X ⟶ A
| |
v v
B ⨯ X ⟶ B
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.
The square with 0 : 0 ⟶ 0
on the right left 𝟙 X
on the right is a pushout square.
The square with 0 : 0 ⟶ 0
on the top and 𝟙 X
on the bottom is a pushout square.
Paste two pushout squares "vertically" to obtain another pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
Paste two pushout squares "horizontally" to obtain another pushout square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
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.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
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.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
Variant of IsPushout.of_top
where v₂₂
is induced from a morphism v₁₃ : X₁₂ ⟶ X₃₂
, and
the universal property of the top square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
Variant of IsPushout.of_right
where h₂₂
is induced from a morphism h₂₃ : X₂₁ ⟶ X₂₃
, and
the universal property of the left square.
The objects in the statement fit into the following diagram:
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
The square
X --inl--> X ⊞ Y
| |
0 snd
| |
v v
0 ---0-----> Y
is a pushout square.
The square
Y --inr--> X ⊞ Y
| |
0 fst
| |
v v
0 ---0-----> X
is a pushout square.
The pushout of biprod.fst
and biprod.snd
is the zero object.
Equations
- CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd = CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ⋯.cocone, isColimit := ⋯.isColimit }
Instances For
The following diagram is a pullback
X --f--> Z
| |
id id
v v
X --f--> Z
The following diagram is a pullback
X --id--> X
| |
f f
v v
Z --id--> Z
In a category, given a morphism f : A ⟶ B
and an object X
,
this is the obvious pushout diagram:
A ⟶ A ⨿ X
| |
v v
B ⟶ B ⨿ X
If f : X ⟶ Y
, g g' : Y ⟶ Z
forms a pullback square, then f
is the equalizer of
g
and g'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f f' : X ⟶ Y
, g : Y ⟶ Z
forms a pushout square, then g
is the coequalizer of
f
and f'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bi-Cartesian square.
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bi-Cartesian square.
X ⊞ Y --fst--> X
| |
snd 0
| |
v v
Y -----0---> 0
is a bi-Cartesian square.
0 -----0---> X
| |
0 inl
| |
v v
Y --inr--> X ⊞ Y
is a bi-Cartesian square.
Alias of CategoryTheory.Functor.map_isPullback
.
Alias of CategoryTheory.Functor.map_isPushout
.