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 #

source

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

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

Instances For

source

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

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

Instances For

source

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

Equations

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

Instances For

source

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

source

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

source

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

source

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.

Equations

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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.

Equations

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

Instances For

source

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

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

Instances For

source

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

source

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

source

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

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

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 ⋯

Instances For

source

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

source

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

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

Instances For

source

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

source

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

source

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

source

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

source

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.

Equations

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

Instances For

source

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

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

Instances For

source

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.

Equations

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

Instances For

source

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

source

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

source

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

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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

source

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

source

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.

Equations

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

Instances For

source

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

source

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

source

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.

Equations

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

Instances For

source

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

source

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

source

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

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

Instances For

source

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

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

Instances For

source

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

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

Instances For

source

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

source

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

source

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

source

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.

Equations

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

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

source

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.

Equations

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

Instances For

source

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

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

Instances For

source

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

source

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

source

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

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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

source

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

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

Instances For

source

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

source

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

source

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

source

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

source

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 }

Equations

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

Instances For

source

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.

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 ⋯

Instances For

source

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

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

Instances For

source

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.

Equations

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

Instances For

source

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

source

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

source

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

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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.

Equations

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

Instances For

source

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

source

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

source

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.

Equations