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.
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.
Equations
- _ = _
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.
Equations
- _ = _
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
Equations
The pullback of a monomorphism is a monomorphism
Equations
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
Equations
The pushout of an epimorphism is an epimorphism
Equations
has_pullbacks represents a choice of pullback for every pair of morphisms
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