mathlib documentation

category_theory.limits.shapes.pullbacks

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 type of objects for the diagram indexing a pushout, defined as a special case of wide_pushout_shape.

The type of arrows for the diagram indexing a pullback.

The identity arrows of the walking cospan.

The type of arrows for the diagram indexing a pushout.

The identity arrows of the walking span.

cospan f g is the functor from the walking cospan hitting f and g.

Equations
def category_theory.limits.span {C : Type u} [category_theory.category C] {X Y Z : C} :

span f g is the functor from the walking span hitting f and g.

Equations
def category_theory.limits.pullback_cone {C : Type u} [category_theory.category C] {X Y Z : C} :
(X Z)(Y Z)Type (max u v)

A pullback cone is just a cone on the cospan formed by two morphisms f : X ⟶ Z and g : Y ⟶ Z.

def category_theory.limits.pullback_cone.fst {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) :
t.X X

The first projection of a pullback cone.

def category_theory.limits.pullback_cone.snd {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) :
t.X Y

The second projection of a pullback cone.

def category_theory.limits.pullback_cone.is_limit_aux {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) (lift : Π (s : category_theory.limits.cone (category_theory.limits.cospan f g)), s.X t.X) :
(∀ (s : category_theory.limits.pullback_cone f g), lift s t.fst = s.fst)(∀ (s : category_theory.limits.pullback_cone f g), lift s t.snd = s.snd)(∀ (s : category_theory.limits.pullback_cone f g) (m : s.X t.X), (∀ (j : category_theory.limits.walking_cospan), m t.π.app j = s.π.app j)m = lift s)category_theory.limits.is_limit t

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

Equations
def category_theory.limits.pullback_cone.is_limit_aux' {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) :
(Π (s : category_theory.limits.pullback_cone f g), {l // l t.fst = s.fst l t.snd = s.snd ∀ {m : s.X t.X}, m t.fst = s.fstm t.snd = s.sndm = l})category_theory.limits.is_limit t

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
def category_theory.limits.pullback_cone.mk {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) :

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
@[simp]
theorem category_theory.limits.pullback_cone.mk_X {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

@[simp]
theorem category_theory.limits.pullback_cone.mk_π_app {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) (j : category_theory.limits.walking_cospan) :
(category_theory.limits.pullback_cone.mk fst snd eq).π.app j = option.cases_on j (fst f) (λ (j' : category_theory.limits.walking_pair), j'.cases_on fst snd)

@[simp]
theorem category_theory.limits.pullback_cone.mk_π_app_left {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

@[simp]
theorem category_theory.limits.pullback_cone.mk_π_app_right {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

@[simp]
theorem category_theory.limits.pullback_cone.mk_π_app_one {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

@[simp]
theorem category_theory.limits.pullback_cone.mk_fst {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

@[simp]
theorem category_theory.limits.pullback_cone.mk_snd {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) :

theorem category_theory.limits.pullback_cone.condition {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) :
t.fst f = t.snd g

theorem category_theory.limits.pullback_cone.condition_assoc {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) {X' : C} (f' : Z X') :
t.fst f f' = t.snd g f'

theorem category_theory.limits.pullback_cone.equalizer_ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} (t : category_theory.limits.pullback_cone f g) {W : C} {k l : W t.X} (h₀ : k t.fst = l t.fst) (h₁ : k t.snd = l t.snd) (j : category_theory.limits.walking_cospan) :
k t.π.app j = l t.π.app j

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

theorem category_theory.limits.pullback_cone.is_limit.hom_ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {t : category_theory.limits.pullback_cone f g} (ht : category_theory.limits.is_limit t) {W : C} {k l : W t.X} :
k t.fst = l t.fstk t.snd = l t.sndk = l

def category_theory.limits.pullback_cone.is_limit.lift' {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {t : category_theory.limits.pullback_cone f g} (ht : category_theory.limits.is_limit t) {W : C} (h : W X) (k : W Y) :
h f = k g{l // l t.fst = h l t.snd = k}

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
def category_theory.limits.pullback_cone.is_limit.mk {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : fst f = snd g) (lift : Π (s : category_theory.limits.pullback_cone f g), s.X W) :
(∀ (s : category_theory.limits.pullback_cone f g), lift s fst = s.fst)(∀ (s : category_theory.limits.pullback_cone f g), lift s snd = s.snd)(∀ (s : category_theory.limits.pullback_cone f g) (m : s.X W), m fst = s.fstm snd = s.sndm = lift s)category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk fst snd eq)

This is a more convenient formulation to show that a pullback_cone constructed using pullback_cone.mk is a limit cone.

Equations
def category_theory.limits.pullback_cone.flip_is_limit {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {W : C} {h : W X} {k : W Y} {comm : h f = k g} :

The flip of a pullback square is a pullback square.

Equations

The pullback cone (𝟙 X, 𝟙 X) for the pair (f, f) is a limit if f is a mono. The converse is shown in mono_of_pullback_is_id.

Equations

f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is given in pullback_cone.is_id_of_mono.

def category_theory.limits.pushout_cocone {C : Type u} [category_theory.category C] {X Y Z : C} :
(X Y)(X Z)Type (max u v)

A pushout cocone is just a cocone on the span formed by two morphisms f : X ⟶ Y and g : X ⟶ Z.

def category_theory.limits.pushout_cocone.inl {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) :
Y t.X

The first inclusion of a pushout cocone.

def category_theory.limits.pushout_cocone.inr {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) :
Z t.X

The second inclusion of a pushout cocone.

def category_theory.limits.pushout_cocone.is_colimit_aux {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) (desc : Π (s : category_theory.limits.pushout_cocone f g), t.X s.X) :
(∀ (s : category_theory.limits.pushout_cocone f g), t.inl desc s = s.inl)(∀ (s : category_theory.limits.pushout_cocone f g), t.inr desc s = s.inr)(∀ (s : category_theory.limits.pushout_cocone f g) (m : t.X s.X), (∀ (j : category_theory.limits.walking_span), t.ι.app j m = s.ι.app j)m = desc s)category_theory.limits.is_colimit t

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

Equations
def category_theory.limits.pushout_cocone.is_colimit_aux' {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) :
(Π (s : category_theory.limits.pushout_cocone f g), {l // t.inl l = s.inl t.inr l = s.inr ∀ {m : t.X s.X}, t.inl m = s.inlt.inr m = s.inrm = l})category_theory.limits.is_colimit t

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
@[simp]
theorem category_theory.limits.pushout_cocone.mk_ι_app {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) (j : category_theory.limits.walking_span) :
(category_theory.limits.pushout_cocone.mk inl inr eq).ι.app j = option.cases_on j (f inl) (λ (j' : category_theory.limits.walking_pair), j'.cases_on inl inr)

def category_theory.limits.pushout_cocone.mk {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) :

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
@[simp]
theorem category_theory.limits.pushout_cocone.mk_X {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

@[simp]
theorem category_theory.limits.pushout_cocone.mk_ι_app_left {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

@[simp]
theorem category_theory.limits.pushout_cocone.mk_ι_app_right {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

@[simp]
theorem category_theory.limits.pushout_cocone.mk_ι_app_zero {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

@[simp]
theorem category_theory.limits.pushout_cocone.mk_inl {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

@[simp]
theorem category_theory.limits.pushout_cocone.mk_inr {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) :

theorem category_theory.limits.pushout_cocone.condition_assoc {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) {X' : C} (f' : t.X X') :
f t.inl f' = g t.inr f'

theorem category_theory.limits.pushout_cocone.condition {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) :
f t.inl = g t.inr

theorem category_theory.limits.pushout_cocone.coequalizer_ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} (t : category_theory.limits.pushout_cocone f g) {W : C} {k l : t.X W} (h₀ : t.inl k = t.inl l) (h₁ : t.inr k = t.inr l) (j : category_theory.limits.walking_span) :
t.ι.app j k = t.ι.app j l

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

theorem category_theory.limits.pushout_cocone.is_colimit.hom_ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {t : category_theory.limits.pushout_cocone f g} (ht : category_theory.limits.is_colimit t) {W : C} {k l : t.X W} :
t.inl k = t.inl lt.inr k = t.inr lk = l

def category_theory.limits.pushout_cocone.is_colimit.desc' {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {t : category_theory.limits.pushout_cocone f g} (ht : category_theory.limits.is_colimit t) {W : C} (h : Y W) (k : Z W) :
f h = g k{l // t.inl l = h t.inr l = k}

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
def category_theory.limits.pushout_cocone.is_colimit.mk {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : f inl = g inr) (desc : Π (s : category_theory.limits.pushout_cocone f g), W s.X) :
(∀ (s : category_theory.limits.pushout_cocone f g), inl desc s = s.inl)(∀ (s : category_theory.limits.pushout_cocone f g), inr desc s = s.inr)(∀ (s : category_theory.limits.pushout_cocone f g) (m : W s.X), inl m = s.inlinr m = s.inrm = desc s)category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk inl inr eq)

This is a more convenient formulation to show that a pushout_cocone constructed using pushout_cocone.mk is a colimit cocone.

Equations
def category_theory.limits.pushout_cocone.flip_is_colimit {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {W : C} {h : Y W} {k : Z W} {comm : f h = g k} :

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

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

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

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
def category_theory.limits.has_pullback {C : Type u} [category_theory.category C] {X Y Z : C} :
(X Z)(Y Z) → Prop

has_pullback f g represents a particular choice of limiting cone for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.

def category_theory.limits.has_pushout {C : Type u} [category_theory.category C] {X Y Z : C} :
(X Y)(X Z) → Prop

has_pushout f g represents a particular choice of colimiting cocone for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.

def category_theory.limits.pullback {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Z) (g : Y Z) [category_theory.limits.has_pullback f g] :
C

pullback f g computes the pullback of a pair of morphisms with the same target.

def category_theory.limits.pushout {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) (g : X Z) [category_theory.limits.has_pushout f g] :
C

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.

def category_theory.limits.pullback.lift {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Z} {g : Y Z} [category_theory.limits.has_pullback f g] (h : W X) (k : W Y) :

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.

def category_theory.limits.pushout.desc {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] (h : Y W) (k : Z W) :

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.

@[simp]
theorem category_theory.limits.pullback.lift_fst_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Z} {g : Y Z} [category_theory.limits.has_pullback f g] (h : W X) (k : W Y) (w : h f = k g) {X' : C} (f' : X X') :

@[simp]

@[simp]

@[simp]
theorem category_theory.limits.pullback.lift_snd_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Z} {g : Y Z} [category_theory.limits.has_pullback f g] (h : W X) (k : W Y) (w : h f = k g) {X' : C} (f' : Y X') :

@[simp]
theorem category_theory.limits.pushout.inl_desc_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] (h : Y W) (k : Z W) (w : f h = g k) {X' : C} (f' : W X') :

@[simp]

@[simp]
theorem category_theory.limits.pushout.inr_desc_assoc {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] (h : Y W) (k : Z W) (w : f h = g k) {X' : C} (f' : W X') :

@[simp]

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
def category_theory.limits.pullback.desc' {C : Type u} [category_theory.category C] {W X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] (h : Y W) (k : Z W) :

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
@[ext]

Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal

@[instance]

The pullback of a monomorphism is a monomorphism

@[instance]

The pullback of a monomorphism is a monomorphism

@[ext]

Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal

@[instance]

The pushout of an epimorphism is an epimorphism

@[instance]

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