Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

PullbackCone #

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

Main definitions #

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.

  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:

Interaction with IsLimit:

References #

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

Equations
@[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.

Equations
@[simp]
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) :
@[simp]
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) :
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) :

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
  • One or more equations did not get rendered due to their size.
@[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_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_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) :
@[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.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) :

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 aesop_cat) (w₂ : s.snd = CategoryStruct.comp i.hom t.snd := by aesop_cat) :
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 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.

Equations
@[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) :
@[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) :
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) :

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
  • t.isLimitAux lift fac_left fac_right uniq = { lift := lift, fac := , uniq := uniq }
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.fstCategoryStruct.comp m 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 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.fstCategoryStruct.comp m snd = s.sndm = lift s) :

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

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

Equations
@[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✝) :
@[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✝) :
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) :

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.

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

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

The pullback cone obtained by flipping fst and snd.

Equations
@[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) :
@[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) :
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) :

Flipping a pullback cone twice gives an isomorphic cone.

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

The flip of a pullback square is a pullback square.

Equations

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.

Equations

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.

Equations

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

Equations
  • One or more equations did not get rendered due to their size.
@[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.

Equations
@[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.

Equations
@[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.

Equations
@[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) :
@[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) :
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) :

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
  • One or more equations did not get rendered due to their size.
@[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 {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_ι_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) :
@[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.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) :

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 aesop_cat) (w₂ : CategoryStruct.comp s.inr i.hom = t.inr := by aesop_cat) :
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 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.

Equations
@[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) :
@[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) :
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) :

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
  • t.isColimitAux desc fac_left fac_right uniq = { desc := desc, fac := , uniq := uniq }
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.inlCategoryStruct.comp t.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
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.

Equations
@[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✝) :
@[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✝) :
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) :

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.

Equations
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.inlCategoryStruct.comp inr m = s.inrm = desc s) :

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

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

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

The pushout cocone obtained by flipping inl and inr.

Equations
@[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) :
@[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) :
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) :

Flipping a pushout cocone twice gives an isomorphic cocone.

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

The flip of a pushout square is a pushout square.

Equations

This is a helper construction that can be useful when verifying that a category has all 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.

Equations

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.

Equations

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

Equations
  • One or more equations did not get rendered due to their size.