PullbackCone

This file provides API for interacting with cones (resp. cocones) in the case of pullbacks (resp. pushouts).

Main definitions

• PullbackCone f g: Given morphisms f : X ⟶ Z and g : Y ⟶ Z, a term t : PullbackCone f g provides the data of a cone pictured as follows

  t.pt ---t.snd---> Y
    |               |
  t.fst            g
    |               |
    v               v
    X -----f------> Z
  

  The type PullbackCone f g is implemented as an abbreviation for Cone (cospan f g), so general results about cones are also available for PullbackCone f g.

• PushoutCone f g: Given morphisms f : X ⟶ Y and g : X ⟶ Z, a term t : PushoutCone f g provides the data of a cocone pictured as follows

    X -----f------> Y
    |               |
    g               t.inr
    |               |
    v               v
    Z ---t.inl---> t.pt
  

  Similar to PullbackCone, PushoutCone f g is implemented as an abbreviation for Cocone (span f g), so general results about cocones are also available for PushoutCone f g.

API

We summarize the most important parts of the API for pullback cones here. The dual notions for pushout cones is also available in this file.

Various ways of constructing pullback cones:

• PullbackCone.mk constructs a term of PullbackCone f g given morphisms fst and snd such that fst ≫ f = snd ≫ g.
• PullbackCone.flip is the PullbackCone obtained by flipping fst and snd.

Interaction with IsLimit:

• PullbackCone.isLimitAux and PullbackCone.isLimitAux' provide two convenient ways to show that a given PullbackCone is a limit cone.
• PullbackCone.isLimit.mk provides a convenient way to show that a PullbackCone constructed using PullbackCone.mk is a limit cone.
• PullbackCone.IsLimit.lift and PullbackCone.IsLimit.lift' provides convenient ways for constructing the morphisms to the point of a limit PullbackCone from the universal property.
• PullbackCone.IsLimit.hom_ext provides a convenient way to show that two morphisms to the point of a limit PullbackCone are equal.

References

• Stacks: Fibre products
• Stacks: Pushouts

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone {C : Type u} [Category.{v, u} 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, inline]

abbrev CategoryTheory.Limits.PullbackCone.fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.pt ⟶ X

The first projection of a pullback cone.

@[reducible, inline]

abbrev CategoryTheory.Limits.PullbackCone.snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.pt ⟶ Y

The second projection of a pullback cone.

theorem CategoryTheory.Limits.PullbackCone.π_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.π.app WalkingCospan.left = c.fst

theorem CategoryTheory.Limits.PullbackCone.π_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.π.app WalkingCospan.right = c.snd

@[simp]

theorem CategoryTheory.Limits.PullbackCone.condition_one {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.π.app WalkingCospan.one = CategoryStruct.comp t.fst f

def CategoryTheory.Limits.PullbackCone.mk {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : PullbackCone f 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.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_pt {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).pt = W

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_π_app {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) (j : WalkingCospan) : (mk fst snd eq).π.app j = Option.casesOn j (CategoryStruct.comp fst f) fun (j' : WalkingPair) => WalkingPair.casesOn j' fst snd

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_π_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).π.app WalkingCospan.left = fst

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_π_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).π.app WalkingCospan.right = snd

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_π_app_one {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).π.app WalkingCospan.one = CategoryStruct.comp fst f

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).fst = fst

@[simp]

theorem CategoryTheory.Limits.PullbackCone.mk_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X) (snd : W ⟶ Y) (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) : (mk fst snd eq).snd = snd

theorem CategoryTheory.Limits.PullbackCone.condition {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : CategoryStruct.comp t.fst f = CategoryStruct.comp t.snd g

theorem CategoryTheory.Limits.PullbackCone.condition_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp t.fst (CategoryStruct.comp f h) = CategoryStruct.comp t.snd (CategoryStruct.comp g h)

theorem CategoryTheory.Limits.PullbackCone.equalizer_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : CategoryStruct.comp k t.fst = CategoryStruct.comp l t.fst) (h₁ : CategoryStruct.comp k t.snd = CategoryStruct.comp l t.snd) (j : WalkingCospan) : CategoryStruct.comp k (t.π.app j) = CategoryStruct.comp l (t.π.app j)

To check whether two morphisms are equalized by the maps of a pullback cone, it suffices to check it for fst t and snd t

def CategoryTheory.Limits.PullbackCone.ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {s t : PullbackCone f g} (i : s.pt ≅ t.pt) (w₁ : s.fst = CategoryStruct.comp i.hom t.fst := by cat_disch) (w₂ : s.snd = CategoryStruct.comp i.hom t.snd := by cat_disch) : 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.

def CategoryTheory.Limits.PullbackCone.eta {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t ≅ mk t.fst t.snd ⋯

The natural isomorphism between a pullback cone and the corresponding pullback cone reconstructed using PullbackCone.mk.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.eta_inv_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.eta.inv.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.PullbackCone.eta_hom_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.eta.hom.hom = CategoryStruct.id t.pt

def CategoryTheory.Limits.PullbackCone.isLimitAux {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) (lift : (s : PullbackCone f g) → s.pt ⟶ t.pt) (fac_left : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) t.fst = s.fst) (fac_right : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) t.snd = s.snd) (uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ t.pt), (∀ (j : WalkingCospan), CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s) : IsLimit 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

def CategoryTheory.Limits.PullbackCone.isLimitAux' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) (create : (s : PullbackCone f g) → { l : s.pt ⟶ t.pt // CategoryStruct.comp l t.fst = s.fst ∧ CategoryStruct.comp l t.snd = s.snd ∧ ∀ {m : s.pt ⟶ t.pt}, CategoryStruct.comp m t.fst = s.fst → CategoryStruct.comp m t.snd = s.snd → m = l }) : IsLimit 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.

def CategoryTheory.Limits.PullbackCone.IsLimit.mk {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) (lift : (s : PullbackCone f g) → s.pt ⟶ W) (fac_left : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : PullbackCone f g) (m : s.pt ⟶ W), CategoryStruct.comp m fst = s.fst → CategoryStruct.comp m snd = s.snd → m = lift s) : IsLimit (PullbackCone.mk fst snd eq)

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

theorem CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} {k l : W ⟶ t.pt} (h₀ : CategoryStruct.comp k t.fst = CategoryStruct.comp l t.fst) (h₁ : CategoryStruct.comp k t.snd = CategoryStruct.comp l t.snd) : k = l

def CategoryTheory.Limits.PullbackCone.IsLimit.lift {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : W ⟶ t.pt

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 get l : W ⟶ t.pt, which satisfies l ≫ fst t = h and l ≫ snd t = k, see IsLimit.lift_fst and IsLimit.lift_snd.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift ht h k w) t.fst = h

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryStruct.comp (lift ht h k w) (CategoryStruct.comp t.fst h✝) = CategoryStruct.comp h h✝

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift ht h k w) t.snd = k

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryStruct.comp (lift ht h k w) (CategoryStruct.comp t.snd h✝) = CategoryStruct.comp k h✝

def CategoryTheory.Limits.PullbackCone.IsLimit.lift' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : { l : W ⟶ t.pt // CategoryStruct.comp l t.fst = h ∧ CategoryStruct.comp 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.pt satisfying l ≫ fst t = h and l ≫ snd t = k.

def CategoryTheory.Limits.PullbackCone.mkSelfIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) : IsLimit (mk t.fst t.snd ⋯)

The pullback cone reconstructed using PullbackCone.mk from a pullback cone that is a limit, is also a limit.

def CategoryTheory.Limits.PullbackCone.flip {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : PullbackCone g f

The pullback cone obtained by flipping fst and snd.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.flip_pt {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.flip.pt = t.pt

@[simp]

theorem CategoryTheory.Limits.PullbackCone.flip_fst {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.flip.fst = t.snd

@[simp]

theorem CategoryTheory.Limits.PullbackCone.flip_snd {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.flip.snd = t.fst

def CategoryTheory.Limits.PullbackCone.flipFlipIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) : t.flip.flip ≅ t

Flipping a pullback cone twice gives an isomorphic cone.

def CategoryTheory.Limits.PullbackCone.flipIsLimit {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t) : IsLimit t.flip

The flip of a pullback square is a pullback square.

def CategoryTheory.Limits.PullbackCone.isLimitOfFlip {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsLimit t.flip) : IsLimit t

A square is a pullback square if its flip is.

def CategoryTheory.Limits.Cone.ofPullbackCone {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : PullbackCone (F.map WalkingCospan.Hom.inl) (F.map WalkingCospan.Hom.inr)) : Cone F

This is a helper construction that can be useful when verifying that a category has all pullbacks. Given F : WalkingCospan ⥤ 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 hasPullbacks_of_hasLimit_cospan, which you may find to be an easier way of achieving your goal.

@[simp]

theorem CategoryTheory.Limits.Cone.ofPullbackCone_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : PullbackCone (F.map WalkingCospan.Hom.inl) (F.map WalkingCospan.Hom.inr)) : (ofPullbackCone t).π = CategoryStruct.comp t.π (diagramIsoCospan F).inv

@[simp]

theorem CategoryTheory.Limits.Cone.ofPullbackCone_pt {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : PullbackCone (F.map WalkingCospan.Hom.inl) (F.map WalkingCospan.Hom.inr)) : (ofPullbackCone t).pt = t.pt

def CategoryTheory.Limits.PullbackCone.ofCone {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : PullbackCone (F.map WalkingCospan.Hom.inl) (F.map WalkingCospan.Hom.inr)

Given F : WalkingCospan ⥤ 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.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.ofCone_pt {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : (ofCone t).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.PullbackCone.ofCone_π {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : (ofCone t).π = CategoryStruct.comp t.π (diagramIsoCospan F).hom

def CategoryTheory.Limits.PullbackCone.isoMk {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : (Cones.postcompose (diagramIsoCospan F).hom).obj t ≅ mk (t.π.app WalkingCospan.left) (t.π.app WalkingCospan.right) ⋯

A diagram WalkingCospan ⥤ C is isomorphic to some PullbackCone.mk after composing with diagramIsoCospan.

@[simp]

theorem CategoryTheory.Limits.PullbackCone.isoMk_hom_hom {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : (isoMk t).hom.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.PullbackCone.isoMk_inv_hom {C : Type u} [Category.{v, u} C] {F : Functor WalkingCospan C} (t : Cone F) : (isoMk t).inv.hom = CategoryStruct.id t.pt

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone {C : Type u} [Category.{v, u} 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, inline]

abbrev CategoryTheory.Limits.PushoutCocone.inl {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : Y ⟶ t.pt

The first inclusion of a pushout cocone.

@[reducible, inline]

abbrev CategoryTheory.Limits.PushoutCocone.inr {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : Z ⟶ t.pt

The second inclusion of a pushout cocone.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.ι_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.ι.app WalkingSpan.left = c.inl

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.ι_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.ι.app WalkingSpan.right = c.inr

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.condition_zero {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.ι.app WalkingSpan.zero = CategoryStruct.comp f t.inl

def CategoryTheory.Limits.PushoutCocone.mk {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : PushoutCocone f g

A pushout cocone on f and g is determined by morphisms inl : Y ⟶ W and inr : Z ⟶ W such that f ≫ inl = g ↠ inr.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) (j : WalkingSpan) : (mk inl inr eq).ι.app j = Option.casesOn j (CategoryStruct.comp f inl) fun (j' : WalkingPair) => WalkingPair.casesOn j' inl inr

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_pt {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).pt = W

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_left {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).ι.app WalkingSpan.left = inl

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_right {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).ι.app WalkingSpan.right = inr

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).ι.app WalkingSpan.zero = CategoryStruct.comp f inl

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_inl {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).inl = inl

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.mk_inr {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W) (inr : Z ⟶ W) (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) : (mk inl inr eq).inr = inr

theorem CategoryTheory.Limits.PushoutCocone.condition {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : CategoryStruct.comp f t.inl = CategoryStruct.comp g t.inr

theorem CategoryTheory.Limits.PushoutCocone.condition_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) {Z✝ : C} (h : t.pt ⟶ Z✝) : CategoryStruct.comp f (CategoryStruct.comp t.inl h) = CategoryStruct.comp g (CategoryStruct.comp t.inr h)

theorem CategoryTheory.Limits.PushoutCocone.coequalizer_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) {W : C} {k l : t.pt ⟶ W} (h₀ : CategoryStruct.comp t.inl k = CategoryStruct.comp t.inl l) (h₁ : CategoryStruct.comp t.inr k = CategoryStruct.comp t.inr l) (j : WalkingSpan) : CategoryStruct.comp (t.ι.app j) k = CategoryStruct.comp (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

def CategoryTheory.Limits.PushoutCocone.ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {s t : PushoutCocone f g} (i : s.pt ≅ t.pt) (w₁ : CategoryStruct.comp s.inl i.hom = t.inl := by cat_disch) (w₂ : CategoryStruct.comp s.inr i.hom = t.inr := by cat_disch) : 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.

def CategoryTheory.Limits.PushoutCocone.eta {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t ≅ mk t.inl t.inr ⋯

The natural isomorphism between a pushout cocone and the corresponding pushout cocone reconstructed using PushoutCocone.mk.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.eta_inv_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.eta.inv.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.eta_hom_hom {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.eta.hom.hom = CategoryStruct.id t.pt

def CategoryTheory.Limits.PushoutCocone.isColimitAux {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) (desc : (s : PushoutCocone f g) → t.pt ⟶ s.pt) (fac_left : ∀ (s : PushoutCocone f g), CategoryStruct.comp t.inl (desc s) = s.inl) (fac_right : ∀ (s : PushoutCocone f g), CategoryStruct.comp t.inr (desc s) = s.inr) (uniq : ∀ (s : PushoutCocone f g) (m : t.pt ⟶ s.pt), (∀ (j : WalkingSpan), CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s) : IsColimit 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

def CategoryTheory.Limits.PushoutCocone.isColimitAux' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) (create : (s : PushoutCocone f g) → { l : t.pt ⟶ s.pt // CategoryStruct.comp t.inl l = s.inl ∧ CategoryStruct.comp t.inr l = s.inr ∧ ∀ {m : t.pt ⟶ s.pt}, CategoryStruct.comp t.inl m = s.inl → CategoryStruct.comp t.inr m = s.inr → m = l }) : IsColimit 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.

theorem CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} {k l : t.pt ⟶ W} (h₀ : CategoryStruct.comp t.inl k = CategoryStruct.comp t.inl l) (h₁ : CategoryStruct.comp t.inr k = CategoryStruct.comp t.inr l) : k = l

def CategoryTheory.Limits.PushoutCocone.IsColimit.desc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) : t.pt ⟶ W

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.pt ⟶ W such that inl t ≫ l = h and inr t ≫ l = k, see IsColimit.inl_desc and IsColimit.inr_desc.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) : CategoryStruct.comp t.inl (desc ht h k w) = h

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryStruct.comp t.inl (CategoryStruct.comp (desc ht h k w) h✝) = CategoryStruct.comp h h✝

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) : CategoryStruct.comp t.inr (desc ht h k w) = k

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryStruct.comp t.inr (CategoryStruct.comp (desc ht h k w) h✝) = CategoryStruct.comp k h✝

def CategoryTheory.Limits.PushoutCocone.IsColimit.desc' {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) : { l : t.pt ⟶ W // CategoryStruct.comp t.inl l = h ∧ CategoryStruct.comp 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.pt ⟶ W such that inl t ≫ l = h and inr t ≫ l = k.

def CategoryTheory.Limits.PushoutCocone.IsColimit.mk {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} {inl : Y ⟶ W} {inr : Z ⟶ W} (eq : CategoryStruct.comp f inl = CategoryStruct.comp g inr) (desc : (s : PushoutCocone f g) → W ⟶ s.pt) (fac_left : ∀ (s : PushoutCocone f g), CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : PushoutCocone f g), CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : PushoutCocone f g) (m : W ⟶ s.pt), CategoryStruct.comp inl m = s.inl → CategoryStruct.comp inr m = s.inr → m = desc s) : IsColimit (PushoutCocone.mk inl inr eq)

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

def CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) : IsColimit (mk t.inl t.inr ⋯)

The pushout cocone reconstructed using PushoutCocone.mk from a pushout cocone that is a colimit, is also a colimit.

def CategoryTheory.Limits.PushoutCocone.flip {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : PushoutCocone g f

The pushout cocone obtained by flipping inl and inr.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.flip_pt {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.flip.pt = t.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.flip_inl {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.flip.inl = t.inr

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.flip_inr {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.flip.inr = t.inl

def CategoryTheory.Limits.PushoutCocone.flipFlipIso {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (t : PushoutCocone f g) : t.flip.flip ≅ t

Flipping a pushout cocone twice gives an isomorphic cocone.

def CategoryTheory.Limits.PushoutCocone.flipIsColimit {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t) : IsColimit t.flip

The flip of a pushout square is a pushout square.

def CategoryTheory.Limits.PushoutCocone.isColimitOfFlip {C : Type u} [Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : PushoutCocone f g} (ht : IsColimit t.flip) : IsColimit t

A square is a pushout square if its flip is.

def CategoryTheory.Limits.Cocone.ofPushoutCocone {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : PushoutCocone (F.map WalkingSpan.Hom.fst) (F.map WalkingSpan.Hom.snd)) : Cocone F

This is a helper construction that can be useful when verifying that a category has all pushout. Given F : WalkingSpan ⥤ C, which is really the same as span (F.map fst) (F.map 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 hasPushouts_of_hasColimit_span, which you may find to be an easier way of achieving your goal.

@[simp]

theorem CategoryTheory.Limits.Cocone.ofPushoutCocone_pt {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : PushoutCocone (F.map WalkingSpan.Hom.fst) (F.map WalkingSpan.Hom.snd)) : (ofPushoutCocone t).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.Cocone.ofPushoutCocone_ι {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : PushoutCocone (F.map WalkingSpan.Hom.fst) (F.map WalkingSpan.Hom.snd)) : (ofPushoutCocone t).ι = CategoryStruct.comp (diagramIsoSpan F).hom t.ι

def CategoryTheory.Limits.PushoutCocone.ofCocone {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : PushoutCocone (F.map WalkingSpan.Hom.fst) (F.map WalkingSpan.Hom.snd)

Given F : WalkingSpan ⥤ 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.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.ofCocone_pt {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : (ofCocone t).pt = t.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.ofCocone_ι {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : (ofCocone t).ι = CategoryStruct.comp (diagramIsoSpan F).inv t.ι

def CategoryTheory.Limits.PushoutCocone.isoMk {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : (Cocones.precompose (diagramIsoSpan F).inv).obj t ≅ mk (t.ι.app WalkingSpan.left) (t.ι.app WalkingSpan.right) ⋯

A diagram WalkingSpan ⥤ C is isomorphic to some PushoutCocone.mk after composing with diagramIsoSpan.

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.isoMk_hom_hom {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : (isoMk t).hom.hom = CategoryStruct.id t.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.isoMk_inv_hom {C : Type u} [Category.{v, u} C] {F : Functor WalkingSpan C} (t : Cocone F) : (isoMk t).inv.hom = CategoryStruct.id t.pt