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 #

@[reducible]

The type of objects for the diagram indexing a pullback, defined as a special case of wide_pullback_shape.

@[reducible]

The left point of the walking cospan.

@[reducible]

The right point of the walking cospan.

@[reducible]

The central point of the walking cospan.

@[reducible]

The type of objects for the diagram indexing a pushout, defined as a special case of wide_pushout_shape.

@[reducible]

The left point of the walking span.

@[reducible]

The right point of the walking span.

@[reducible]

The central point of the walking span.

@[reducible]

The type of arrows for the diagram indexing a pullback.

@[reducible]

The identity arrows of the walking cospan.

@[reducible]

The type of arrows for the diagram indexing a pushout.

@[reducible]

The identity arrows of the walking span.

To construct an isomorphism of cones over the walking cospan, it suffices to construct an isomorphism of the cone points and check it commutes with the legs to left and right.

Equations

To construct an isomorphism of cocones over the walking span, it suffices to construct an isomorphism of the cocone points and check it commutes with the legs from left and right.

Equations

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

Equations
Instances for category_theory.limits.cospan
def category_theory.limits.cospan_ext {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :

Construct an isomorphism of cospans from components.

Equations
@[simp]
theorem category_theory.limits.cospan_ext_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_app_one {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_hom_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_hom_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_hom_app_one {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_inv_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_inv_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.cospan_ext_inv_app_one {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : iX.hom f' = f iZ.hom) (wg : iY.hom g' = g iZ.hom) :
def category_theory.limits.span_ext {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :

Construct an isomorphism of spans from components.

Equations
@[simp]
theorem category_theory.limits.span_ext_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_app_one {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_hom_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_hom_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_hom_app_zero {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_inv_app_left {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_inv_app_right {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[simp]
theorem category_theory.limits.span_ext_inv_app_zero {C : Type u} [category_theory.category C] {X Y Z X' Y' Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : iX.hom f' = f iY.hom) (wg : iX.hom g' = g iZ.hom) :
@[reducible]
def category_theory.limits.pullback_cone {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Z) (g : 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.

@[reducible]
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.

@[reducible]
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.pullback_cone f g), s.X t.X) (fac_left : ∀ (s : category_theory.limits.pullback_cone f g), lift s t.fst = s.fst) (fac_right : ∀ (s : category_theory.limits.pullback_cone f g), lift s t.snd = s.snd) (uniq : ∀ (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) :

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) (create : Π (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}) :

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) (eq : fst f = snd g) :

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} (h₀ : k t.fst = l t.fst) (h₁ : k t.snd = l t.snd) :
k = l
def category_theory.limits.pullback_cone.ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} {s t : category_theory.limits.pullback_cone f g} (i : s.X t.X) (w₁ : s.fst = i.hom t.fst) (w₂ : s.snd = i.hom t.snd) :
s t

To construct an isomorphism of pullback cones, it suffices to construct an isomorphism of the cone points and check it commutes with fst and snd.

Equations
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) (w : 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) (fac_left : ∀ (s : category_theory.limits.pullback_cone f g), lift s fst = s.fst) (fac_right : ∀ (s : category_theory.limits.pullback_cone f g), lift s snd = s.snd) (uniq : ∀ (s : category_theory.limits.pullback_cone f g) (m : s.X W), m fst = s.fstm snd = s.sndm = lift s) :

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} (t : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk k h category_theory.limits.pullback_cone.flip_is_limit._proof_1)) :

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.

Suppose f and g are two morphisms with a common codomain and s is a limit cone over the diagram formed by f and g. Suppose f and g both factor through a monomorphism h via x and y, respectively. Then s is also a limit cone over the diagram formed by x and y.

Equations

If W is the pullback of f, g, it is also the pullback of f ≫ i, g ≫ i for any mono i.

Equations
@[reducible]
def category_theory.limits.pushout_cocone {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) (g : 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.

@[reducible]
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.

@[reducible]
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) (fac_left : ∀ (s : category_theory.limits.pushout_cocone f g), t.inl desc s = s.inl) (fac_right : ∀ (s : category_theory.limits.pushout_cocone f g), t.inr desc s = s.inr) (uniq : ∀ (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) :

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) (create : Π (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}) :

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) (eq : f inl = g inr) :

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} (h₀ : t.inl k = t.inl l) (h₁ : t.inr k = t.inr l) :
k = 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) (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.ext {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} {s t : category_theory.limits.pushout_cocone f g} (i : s.X t.X) (w₁ : s.inl i.hom = t.inl) (w₂ : s.inr i.hom = t.inr) :
s t

To construct an isomorphism of pushout cocones, it suffices to construct an isomorphism of the cocone points and check it commutes with inl and inr.

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) (fac_left : ∀ (s : category_theory.limits.pushout_cocone f g), inl desc s = s.inl) (fac_right : ∀ (s : category_theory.limits.pushout_cocone f g), inr desc s = s.inr) (uniq : ∀ (s : category_theory.limits.pushout_cocone f g) (m : W s.X), inl m = s.inlinr m = s.inrm = desc s) :

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} (t : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk k h category_theory.limits.pushout_cocone.flip_is_colimit._proof_1)) :

The flip of a pushout square is a pushout square.

Equations

The pushout cocone (𝟙 X, 𝟙 X) for the pair (f, f) is a colimit if f is an epi. The converse is shown in epi_of_is_colimit_mk_id_id.

Equations

f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f). The converse is given in pushout_cocone.is_colimit_mk_id_id.

Suppose f and g are two morphisms with a common domain and s is a colimit cocone over the diagram formed by f and g. Suppose f and g both factor through an epimorphism h via x and y, respectively. Then s is also a colimit cocone over the diagram formed by x and y.

Equations

If W is the pushout of f, g, it is also the pushout of h ≫ f, h ≫ g for any epi h.

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

@[reducible]
def category_theory.limits.has_pushout {C : Type u} [category_theory.category C] {X Y Z : C} (f : X Y) (g : 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.

@[reducible]
noncomputable 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.

@[reducible]
noncomputable 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.

@[reducible]
noncomputable def category_theory.limits.pullback.fst {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} [category_theory.limits.has_pullback f g] :

The first projection of the pullback of f and g.

@[reducible]
noncomputable def category_theory.limits.pullback.snd {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Z} {g : Y Z} [category_theory.limits.has_pullback f g] :

The second projection of the pullback of f and g.

@[reducible]
noncomputable def category_theory.limits.pushout.inl {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] :

The first inclusion into the pushout of f and g.

@[reducible]
noncomputable def category_theory.limits.pushout.inr {C : Type u} [category_theory.category C] {X Y Z : C} {f : X Y} {g : X Z} [category_theory.limits.has_pushout f g] :

The second inclusion into the pushout of f and g.

@[reducible]
noncomputable 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) (w : h f = k 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.

@[reducible]
noncomputable 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) (w : f h = g k) :

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]
noncomputable 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) (w : h f = k g) :

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
noncomputable 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) (w : f h = g k) :

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
@[reducible]
noncomputable def category_theory.limits.pullback.map {C : Type u} [category_theory.category C] {W X Y Z S T : C} (f₁ : W S) (f₂ : X S) [category_theory.limits.has_pullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [category_theory.limits.has_pullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) :

Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.

W    Y
        
    S    T
        
X    Z
@[reducible]
noncomputable def category_theory.limits.pushout.map {C : Type u} [category_theory.category C] {W X Y Z S T : C} (f₁ : S W) (f₂ : S X) [category_theory.limits.has_pushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [category_theory.limits.has_pushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : f₁ i₁ = i₃ g₁) (eq₂ : f₂ i₂ = i₃ g₂) :

Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.

    W    Y
        
S    T
        
    X    Z
@[ext]

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

@[protected, instance]

The pullback of a monomorphism is a monomorphism

@[protected, 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

@[protected, instance]

The pushout of an epimorphism is an epimorphism

@[protected, instance]

The pushout of an epimorphism is an epimorphism

@[protected, instance]
def category_theory.limits.pullback.map_is_iso {C : Type u} [category_theory.category C] {W X Y Z S T : C} (f₁ : W S) (f₂ : X S) [category_theory.limits.has_pullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [category_theory.limits.has_pullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : f₁ i₃ = i₁ g₁) (eq₂ : f₂ i₃ = i₂ g₂) [category_theory.is_iso i₁] [category_theory.is_iso i₂] [category_theory.is_iso i₃] :
category_theory.is_iso (category_theory.limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
noncomputable def category_theory.limits.pullback.congr_hom {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pullback f₁ g₁] [category_theory.limits.has_pullback f₂ g₂] :

If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂

Equations
@[simp]
theorem category_theory.limits.pullback.congr_hom_hom {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pullback f₁ g₁] [category_theory.limits.has_pullback f₂ g₂] :
@[simp]
theorem category_theory.limits.pullback.congr_hom_inv {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Z} {g₁ g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pullback f₁ g₁] [category_theory.limits.has_pullback f₂ g₂] :
@[protected, instance]
def category_theory.limits.pushout.map_is_iso {C : Type u} [category_theory.category C] {W X Y Z S T : C} (f₁ : S W) (f₂ : S X) [category_theory.limits.has_pushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [category_theory.limits.has_pushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : f₁ i₁ = i₃ g₁) (eq₂ : f₂ i₂ = i₃ g₂) [category_theory.is_iso i₁] [category_theory.is_iso i₂] [category_theory.is_iso i₃] :
category_theory.is_iso (category_theory.limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
@[simp]
theorem category_theory.limits.pushout.congr_hom_hom {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pushout f₁ g₁] [category_theory.limits.has_pushout f₂ g₂] :
noncomputable def category_theory.limits.pushout.congr_hom {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pushout f₁ g₁] [category_theory.limits.has_pushout f₂ g₂] :

If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂

Equations
@[simp]
theorem category_theory.limits.pushout.congr_hom_inv {C : Type u} [category_theory.category C] {X Y Z : C} {f₁ f₂ : X Y} {g₁ g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [category_theory.limits.has_pushout f₁ g₁] [category_theory.limits.has_pushout f₂ g₂] :

The comparison morphism for the pullback of f,g. This is an isomorphism iff G preserves the pullback of f,g; see category_theory/limits/preserves/shapes/pullbacks.lean

Equations
Instances for category_theory.limits.pullback_comparison
@[simp]

The comparison morphism for the pushout of f,g. This is an isomorphism iff G preserves the pushout of f,g; see category_theory/limits/preserves/shapes/pullbacks.lean

Equations
Instances for category_theory.limits.pushout_comparison
@[simp]
theorem category_theory.limits.pushout_comparison_map_desc_assoc {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] {X Y Z : C} (G : C D) (f : X Y) (g : X Z) [category_theory.limits.has_pushout f g] [category_theory.limits.has_pushout (G.map f) (G.map g)] {W : C} {h : Y W} {k : Z W} (w : f h = g k) {X' : D} (f' : G.obj W X') :

Making this a global instance would make the typeclass seach go in an infinite loop.

Making this a global instance would make the typeclass seach go in an infinite loop.

@[protected, instance]

If f : X ⟶ Z is iso, then X ×[Z] Y ≅ Y. This is the explicit limit cone.

Equations

If g : Y ⟶ Z is iso, then X ×[Z] Y ≅ X. This is the explicit limit cone.

Equations
@[protected, instance]
@[protected, instance]

If f : X ⟶ Y is iso, then Y ⨿[X] Z ≅ Z. This is the explicit colimit cocone.

Equations
@[protected, instance]

If f : X ⟶ Z is iso, then Y ⨿[X] Z ≅ Y. This is the explicit colimit cocone.

Equations
@[protected, instance]
def category_theory.limits.big_square_is_pullback {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : i₁ g₁ = f₁ i₂) (h₂ : i₂ g₂ = f₂ i₃) (H : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₂ f₂ h₂)) (H' : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₁ f₁ h₁)) :

Given

X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the big square is a pullback if both the small squares are.

Equations
def category_theory.limits.big_square_is_pushout {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : i₁ g₁ = f₁ i₂) (h₂ : i₂ g₂ = f₂ i₃) (H : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₂ i₃ h₂)) (H' : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁)) :

Given

X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the big square is a pushout if both the small squares are.

Equations
def category_theory.limits.left_square_is_pullback {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : i₁ g₁ = f₁ i₂) (h₂ : i₂ g₂ = f₂ i₃) (H : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₂ f₂ h₂)) (H' : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk i₁ (f₁ f₂) _)) :

Given

X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the left square is a pullback if the right square and the big square are.

Equations
def category_theory.limits.right_square_is_pushout {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : i₁ g₁ = f₁ i₂) (h₂ : i₂ g₂ = f₂ i₃) (H : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk g₁ i₂ h₁)) (H' : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (g₁ g₂) i₃ _)) :

Given

X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

Then the right square is a pushout if the left square and the big square are.

Equations

(X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

Equations
theorem category_theory.limits.has_pullback_assoc {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [category_theory.limits.has_pullback f₁ f₂] [category_theory.limits.has_pullback f₃ f₄] [category_theory.limits.has_pullback (category_theory.limits.pullback.snd f₃) f₄] :

X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).

Equations

The canonical isomorphism (X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

Equations

(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).

Equations
theorem category_theory.limits.has_pushout_assoc {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [category_theory.limits.has_pushout g₁ g₂] [category_theory.limits.has_pushout g₃ g₄] [category_theory.limits.has_pushout (g₃ category_theory.limits.pushout.inr) g₄] :

X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃.

Equations
theorem category_theory.limits.has_pushout_assoc_symm {C : Type u} [category_theory.category C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [category_theory.limits.has_pushout g₁ g₂] [category_theory.limits.has_pushout g₃ g₄] [category_theory.limits.has_pushout g₁ (g₂ category_theory.limits.pushout.inl)] :

The canonical isomorphism (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).

Equations
@[reducible]

has_pullbacks represents a choice of pullback for every pair of morphisms

See https://stacks.math.columbia.edu/tag/001W

@[reducible]

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

@[protected, instance]

Having wide pullback at any universe level implies having binary pullbacks.

Given a morphism f : X ⟶ Y, we can take morphisms over Y to morphisms over X via pullbacks. This is right adjoint to over.map (TODO)

Equations