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} [CategoryTheory.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

• CategoryTheory.Limits.PullbackCone f g = CategoryTheory.Limits.Cone (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

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

The first projection of a pullback cone.

Equations

• t.fst = t.π.app CategoryTheory.Limits.WalkingCospan.left

@[reducible, inline]

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

The second projection of a pullback cone.

Equations

• t.snd = t.π.app CategoryTheory.Limits.WalkingCospan.right

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem CategoryTheory.Limits.PullbackCone.equalizer_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : CategoryTheory.Limits.PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : CategoryTheory.CategoryStruct.comp k t.fst = CategoryTheory.CategoryStruct.comp l t.fst) (h₁ : CategoryTheory.CategoryStruct.comp k t.snd = CategoryTheory.CategoryStruct.comp l t.snd) (j : CategoryTheory.Limits.WalkingCospan) : CategoryTheory.CategoryStruct.comp k (t.π.app j) = CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {s t : CategoryTheory.Limits.PullbackCone f g} (i : s.pt ≅ t.pt) (w₁ : s.fst = CategoryTheory.CategoryStruct.comp i.hom t.fst := by aesop_cat) (w₂ : s.snd = CategoryTheory.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

• CategoryTheory.Limits.PullbackCone.ext i w₁ w₂ = CategoryTheory.Limits.WalkingCospan.ext i w₁ w₂

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

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

Equations

• t.eta = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl t.pt) ⋯ ⋯

@[simp]

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

@[simp]

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

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

Equations

• t.isLimitAux lift fac_left fac_right uniq = { lift := lift, fac := ⋯, uniq := uniq }

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

Equations

• t.isLimitAux' create = t.isLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f g) => ↑(create s)) ⋯ ⋯ ⋯

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

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

Equations

• CategoryTheory.Limits.PullbackCone.IsLimit.mk eq lift fac_left fac_right uniq = (CategoryTheory.Limits.PullbackCone.mk fst snd eq).isLimitAux lift fac_left fac_right ⋯

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

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

• CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w = ht.lift (CategoryTheory.Limits.PullbackCone.mk h k w)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Limits.PullbackCone.IsLimit.lift' ht h k w = ⟨CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w, ⋯⟩

def CategoryTheory.Limits.PullbackCone.mkSelfIsLimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.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

• CategoryTheory.Limits.PullbackCone.mkSelfIsLimit ht = ht.ofIsoLimit t.eta

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

The pullback cone obtained by flipping fst and snd.

Equations

• t.flip = CategoryTheory.Limits.PullbackCone.mk t.snd t.fst ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

Flipping a pullback cone twice gives an isomorphic cone.

Equations

• t.flipFlipIso = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl t.flip.flip.pt) ⋯ ⋯

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

The flip of a pullback square is a pullback square.

Equations

• CategoryTheory.Limits.PullbackCone.flipIsLimit ht = CategoryTheory.Limits.PullbackCone.IsLimit.mk ⋯ (fun (s : CategoryTheory.Limits.PullbackCone g f) => ht.lift s.flip) ⋯ ⋯ ⋯

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

A square is a pullback square if its flip is.

Equations

• CategoryTheory.Limits.PullbackCone.isLimitOfFlip ht = (CategoryTheory.Limits.PullbackCone.flipIsLimit ht).ofIsoLimit t.flipFlipIso

def CategoryTheory.Limits.Cone.ofPullbackCone {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr)) : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.Cone.ofPullbackCone t = { pt := t.pt, π := CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).inv }

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.PullbackCone.ofCone {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) (F.map CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.PullbackCone.ofCone t = { pt := t.pt, π := CategoryTheory.CategoryStruct.comp t.π (CategoryTheory.Limits.diagramIsoCospan F).hom }

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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

@[reducible, inline]

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

• CategoryTheory.Limits.PushoutCocone f g = CategoryTheory.Limits.Cocone (CategoryTheory.Limits.span f g)

@[reducible, inline]

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

The first inclusion of a pushout cocone.

Equations

• t.inl = t.ι.app CategoryTheory.Limits.WalkingSpan.left

@[reducible, inline]

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

The second inclusion of a pushout cocone.

Equations

• t.inr = t.ι.app CategoryTheory.Limits.WalkingSpan.right

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

• CategoryTheory.Limits.PushoutCocone.ext i w₁ w₂ = CategoryTheory.Limits.WalkingSpan.ext i w₁ w₂

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

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

Equations

• t.eta = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl t.pt) ⋯ ⋯

@[simp]

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

@[simp]

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

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

Equations

• t.isColimitAux desc fac_left fac_right uniq = { desc := desc, fac := ⋯, uniq := uniq }

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

Equations

• t.isColimitAux' create = t.isColimitAux (fun (s : CategoryTheory.Limits.PushoutCocone f g) => ↑(create s)) ⋯ ⋯ ⋯

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

def CategoryTheory.Limits.PushoutCocone.IsColimit.desc {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.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

• CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w = ht.desc (CategoryTheory.Limits.PushoutCocone.mk h k w)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.Limits.PushoutCocone.IsColimit.desc' ht h k w = ⟨CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w, ⋯⟩

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

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

Equations

• CategoryTheory.Limits.PushoutCocone.IsColimit.mk eq desc fac_left fac_right uniq = (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).isColimitAux desc fac_left fac_right ⋯

def CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.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

• CategoryTheory.Limits.PushoutCocone.mkSelfIsColimit ht = ht.ofIsoColimit t.eta

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

The pushout cocone obtained by flipping inl and inr.

Equations

• t.flip = CategoryTheory.Limits.PushoutCocone.mk t.inr t.inl ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

Flipping a pushout cocone twice gives an isomorphic cocone.

Equations

• t.flipFlipIso = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl t.flip.flip.pt) ⋯ ⋯

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

The flip of a pushout square is a pushout square.

Equations

• CategoryTheory.Limits.PushoutCocone.flipIsColimit ht = CategoryTheory.Limits.PushoutCocone.IsColimit.mk ⋯ (fun (s : CategoryTheory.Limits.PushoutCocone g f) => ht.desc s.flip) ⋯ ⋯ ⋯

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

A square is a pushout square if its flip is.

Equations

• CategoryTheory.Limits.PushoutCocone.isColimitOfFlip ht = (CategoryTheory.Limits.PushoutCocone.flipIsColimit ht).ofIsoColimit t.flipFlipIso

def CategoryTheory.Limits.Cocone.ofPushoutCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)) : CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.Cocone.ofPushoutCocone t = { pt := t.pt, ι := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).hom t.ι }

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.PushoutCocone.ofCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} (t : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst) (F.map CategoryTheory.Limits.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.

Equations

• CategoryTheory.Limits.PushoutCocone.ofCocone t = { pt := t.pt, ι := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagramIsoSpan F).inv t.ι }

@[simp]

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

@[simp]

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

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

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.

@[simp]

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

@[simp]

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