Pullbacks
We define a category walking_cospan (resp. walking_span), which is the index category
for the given data for a pullback (resp. pushout) diagram. Convenience methods cospan f g
and span f g construct functors from the walking (co)span, hitting the given morphisms.
We define pullback f g and pushout f g as limits and colimits of such functors.
References
The type of objects for the diagram indexing a pullback, defined as a special case of
wide_pullback_shape.
The left point of the walking cospan.
The right point of the walking cospan.
The central point of the walking cospan.
The type of objects for the diagram indexing a pushout, defined as a special case of
wide_pushout_shape.
The left point of the walking span.
The right point of the walking span.
The central point of the walking span.
The type of arrows for the diagram indexing a pullback.
The left arrow of the walking cospan.
The right arrow of the walking cospan.
The identity arrows of the walking cospan.
The type of arrows for the diagram indexing a pushout.
The left arrow of the walking span.
The right arrow of the walking span.
The identity arrows of the walking span.
cospan f g is the functor from the walking cospan hitting f and g.
Equations
- category_theory.limits.cospan f g = category_theory.limits.wide_pullback_shape.wide_cospan Z (λ (j : category_theory.limits.walking_pair), j.cases_on X Y) (λ (j : category_theory.limits.walking_pair), j.cases_on f g)
span f g is the functor from the walking span hitting f and g.
Equations
- category_theory.limits.span f g = category_theory.limits.wide_pushout_shape.wide_span X (λ (j : category_theory.limits.walking_pair), j.cases_on Y Z) (λ (j : category_theory.limits.walking_pair), j.cases_on f g)
Every diagram indexing an pullback is naturally isomorphic (actually, equal) to a cospan
Every diagram indexing a pushout is naturally isomorphic (actually, equal) to a span
A pullback cone is just a cone on the cospan formed by two morphisms f : X ⟶ Z and
g : Y ⟶ Z.
The first projection of a pullback cone.
The second projection of a pullback cone.
This is a slightly more convenient method to verify that a pullback cone is a limit cone. It only asks for a proof of facts that carry any mathematical content
This is another convenient method to verify that a pullback cone is a limit cone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Equations
- t.is_limit_aux' create = t.is_limit_aux (λ (s : category_theory.limits.cone (category_theory.limits.cospan f g)), (create s).val) _ _ _
A pullback cone on f and g is determined by morphisms fst : W ⟶ X and snd : W ⟶ Y
such that fst ≫ f = snd ≫ g.
Equations
- category_theory.limits.pullback_cone.mk fst snd eq = {X := W, π := {app := λ (j : category_theory.limits.walking_cospan), option.cases_on j (fst ≫ f) (λ (j' : category_theory.limits.walking_pair), j'.cases_on fst snd), naturality' := _}}
To check whether a morphism is equalized by the maps of a pullback cone, it suffices to check
it for fst t and snd t
If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that
h ≫ f = k ≫ g, then we have l : W ⟶ t.X satisfying l ≫ fst t = h and l ≫ snd t = k.
Equations
- category_theory.limits.pullback_cone.is_limit.lift' ht h k w = ⟨ht.lift (category_theory.limits.pullback_cone.mk h k w), _⟩
This is a more convenient formulation to show that a pullback_cone constructed using
pullback_cone.mk is a limit cone.
Equations
- category_theory.limits.pullback_cone.is_limit.mk fst snd eq lift fac_left fac_right uniq = (category_theory.limits.pullback_cone.mk fst snd eq).is_limit_aux lift fac_left fac_right _
The flip of a pullback square is a pullback square.
Equations
- category_theory.limits.pullback_cone.flip_is_limit t = (category_theory.limits.pullback_cone.mk h k comm).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨(category_theory.limits.pullback_cone.is_limit.lift' t s.snd s.fst _).val, _⟩)
A pushout cocone is just a cocone on the span formed by two morphisms f : X ⟶ Y and
g : X ⟶ Z.
The first inclusion of a pushout cocone.
The second inclusion of a pushout cocone.
This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone. It only asks for a proof of facts that carry any mathematical content
This is another convenient method to verify that a pushout cocone is a colimit cocone. It
only asks for a proof of facts that carry any mathematical content, and allows access to the
same s for all parts.
Equations
- t.is_colimit_aux' create = t.is_colimit_aux (λ (s : category_theory.limits.pushout_cocone f g), (create s).val) _ _ _
A pushout cocone on f and g is determined by morphisms inl : Y ⟶ W and inr : Z ⟶ W such
that f ≫ inl = g ↠ inr.
Equations
- category_theory.limits.pushout_cocone.mk inl inr eq = {X := W, ι := {app := λ (j : category_theory.limits.walking_span), option.cases_on j (f ≫ inl) (λ (j' : category_theory.limits.walking_pair), j'.cases_on inl inr), naturality' := _}}
To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check
it for inl t and inr t
If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are
morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.X ⟶ W such that
inl t ≫ l = h and inr t ≫ l = k.
Equations
- category_theory.limits.pushout_cocone.is_colimit.desc' ht h k w = ⟨ht.desc (category_theory.limits.pushout_cocone.mk h k w), _⟩
This is a more convenient formulation to show that a pushout_cocone constructed using
pushout_cocone.mk is a colimit cocone.
Equations
- category_theory.limits.pushout_cocone.is_colimit.mk inl inr eq desc fac_left fac_right uniq = (category_theory.limits.pushout_cocone.mk inl inr eq).is_colimit_aux desc fac_left fac_right _
The flip of a pushout square is a pushout square.
Equations
This is a helper construction that can be useful when verifying that a category has all
pullbacks. Given F : walking_cospan ⥤ C, which is really the same as
cospan (F.map inl) (F.map inr), and a pullback cone on F.map inl and F.map inr, we
get a cone on F.
If you're thinking about using this, have a look at has_pullbacks_of_has_limit_cospan,
which you may find to be an easier way of achieving your goal.
Equations
- category_theory.limits.cone.of_pullback_cone t = {X := t.X, π := t.π ≫ (category_theory.limits.diagram_iso_cospan F).inv}
This is a helper construction that can be useful when verifying that a category has all
pushout. Given F : walking_span ⥤ C, which is really the same as
span (F.map fst) (F.mal snd), and a pushout cocone on F.map fst and F.map snd,
we get a cocone on F.
If you're thinking about using this, have a look at has_pushouts_of_has_colimit_span, which
you may find to be an easiery way of achieving your goal.
Equations
- category_theory.limits.cocone.of_pushout_cocone t = {X := t.X, ι := (category_theory.limits.diagram_iso_span F).hom ≫ t.ι}
Given F : walking_cospan ⥤ C, which is really the same as cospan (F.map inl) (F.map inr),
and a cone on F, we get a pullback cone on F.map inl and F.map inr.
Equations
- category_theory.limits.pullback_cone.of_cone t = {X := t.X, π := t.π ≫ (category_theory.limits.diagram_iso_cospan F).hom}
Given F : walking_span ⥤ C, which is really the same as span (F.map fst) (F.map snd),
and a cocone on F, we get a pushout cocone on F.map fst and F.map snd.
Equations
- category_theory.limits.pushout_cocone.of_cocone t = {X := t.X, ι := (category_theory.limits.diagram_iso_span F).inv ≫ t.ι}
has_pullback f g represents a particular choice of limiting cone
for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.
has_pushout f g represents a particular choice of colimiting cocone
for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.
pullback f g computes the pullback of a pair of morphisms with the same target.
pushout f g computes the pushout of a pair of morphisms with the same source.
The first projection of the pullback of f and g.
The second projection of the pullback of f and g.
The first inclusion into the pushout of f and g.
The second inclusion into the pushout of f and g.
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
pullback.lift : W ⟶ pullback f g.
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
pushout.desc : pushout f g ⟶ W.
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
l : W ⟶ pullback f g such that l ≫ pullback.fst = h and l ≫ pullback.snd = k.
Equations
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
l : pushout f g ⟶ W such that pushout.inl ≫ l = h and pushout.inr ≫ l = k.
Equations
Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal
The pullback of a monomorphism is a monomorphism
The pullback of a monomorphism is a monomorphism
Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal
The pushout of an epimorphism is an epimorphism
The pushout of an epimorphism is an epimorphism
has_pullbacks represents a choice of pullback for every pair of morphisms
See https://stacks.math.columbia.edu/tag/001W.
has_pushouts represents a choice of pushout for every pair of morphisms
If C has all limits of diagrams cospan f g, then it has all pullbacks
If C has all colimits of diagrams span f g, then it has all pushouts