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.

The functor between two walking_cospans in different universes.

Equations

The functor between two walking_spans in different universes.

Equations

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) :
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.

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.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
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.

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) (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
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.

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.

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.

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.

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.

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.

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.

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.

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.

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
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
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]