PullbackCone #
This file provides API for interacting with cones (resp. cocones) in the case of pullbacks (resp. pushouts).
Main definitions #
PullbackCone f g: Given morphismsf : X ⟶ Zandg : Y ⟶ Z, a termt : PullbackCone f gprovides 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 morphismsf : X ⟶ Yandg : X ⟶ Z, a termt : PushoutCone f gprovides 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.mkconstructs a term ofPullbackCone f ggiven morphismsfstandsndsuch thatfst ≫ f = snd ≫ g.PullbackCone.flipis thePullbackConeobtained by flippingfstandsnd.
Interaction with IsLimit:
PullbackCone.isLimitAuxandPullbackCone.isLimitAux'provide two convenient ways to show that a givenPullbackConeis a limit cone.PullbackCone.isLimit.mkprovides a convenient way to show that aPullbackConeconstructed usingPullbackCone.mkis a limit cone.PullbackCone.IsLimit.liftandPullbackCone.IsLimit.lift'provides convenient ways for constructing the morphisms to the point of a limitPullbackConefrom the universal property.PullbackCone.IsLimit.hom_extprovides a convenient way to show that two morphisms to the point of a limitPullbackConeare equal.
References #
@[reducible, inline]
abbrev
CategoryTheory.Limits.PullbackCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
Type (max (max 0 u) v)
A pullback cone is just a cone on the cospan formed by two morphisms f : X ⟶ Z and
g : Y ⟶ Z.
@[reducible, inline]
abbrev
CategoryTheory.Limits.PullbackCone.fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.mk_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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
def
CategoryTheory.Limits.PullbackCone.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
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_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
(t : CategoryTheory.Limits.PullbackCone f g)
{Z : C}
(h : Z✝ ⟶ Z)
:
theorem
CategoryTheory.Limits.PullbackCone.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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.equalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
{W : C}
{k : W ⟶ t.pt}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{s : CategoryTheory.Limits.PullbackCone f g}
{t : CategoryTheory.Limits.PullbackCone f g}
(i : s.pt ≅ t.pt)
(w₁ : autoParam (s.fst = CategoryTheory.CategoryStruct.comp i.hom t.fst) _auto✝)
(w₂ : autoParam (s.snd = CategoryTheory.CategoryStruct.comp i.hom t.snd) _auto✝)
:
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
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.eta_hom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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.eta
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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) ⋯ ⋯
def
CategoryTheory.Limits.PullbackCone.isLimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
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 : C}
{Y : C}
{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 })
:
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 : C}
{Y : C}
{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)
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
{W : C}
{k : W ⟶ t.pt}
{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 : C}
{Y : C}
{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_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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
def
CategoryTheory.Limits.PullbackCone.IsLimit.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(t : CategoryTheory.Limits.PullbackCone f g)
:
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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t)
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(ht : CategoryTheory.Limits.IsLimit t.flip)
:
A square is a pullback square if its flip is.
Equations
- CategoryTheory.Limits.PullbackCone.isLimitOfFlip ht = (CategoryTheory.Limits.PullbackCone.flipIsLimit ht).ofIsoLimit t.flipFlipIso
@[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
@[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))
:
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))
:
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.PullbackCone.ofCone_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
(t : CategoryTheory.Limits.Cone F)
:
@[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
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)
:
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.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
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)
:
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}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
Type (max (max 0 u) v)
A pushout cocone is just a cocone on the span formed by two morphisms f : X ⟶ Y and
g : X ⟶ Z.
@[reducible, inline]
abbrev
CategoryTheory.Limits.PushoutCocone.inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.mk_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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
def
CategoryTheory.Limits.PushoutCocone.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
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_ι_app_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z✝}
(t : CategoryTheory.Limits.PushoutCocone f g)
{Z : C}
(h : t.pt ⟶ Z)
:
theorem
CategoryTheory.Limits.PushoutCocone.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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.coequalizer_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
{W : C}
{k : t.pt ⟶ W}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{s : CategoryTheory.Limits.PushoutCocone f g}
{t : CategoryTheory.Limits.PushoutCocone f g}
(i : s.pt ≅ t.pt)
(w₁ : autoParam (CategoryTheory.CategoryStruct.comp s.inl i.hom = t.inl) _auto✝)
(w₂ : autoParam (CategoryTheory.CategoryStruct.comp s.inr i.hom = t.inr) _auto✝)
:
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
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.eta_inv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
t.eta.inv.hom = CategoryTheory.CategoryStruct.id t.pt
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.eta_hom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
t.eta.hom.hom = CategoryTheory.CategoryStruct.id t.pt
def
CategoryTheory.Limits.PushoutCocone.eta
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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) ⋯ ⋯
def
CategoryTheory.Limits.PushoutCocone.isColimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
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 : C}
{Y : C}
{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 })
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
{W : C}
{k : t.pt ⟶ W}
{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 : C}
{Y : C}
{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_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
def
CategoryTheory.Limits.PushoutCocone.IsColimit.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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
def
CategoryTheory.Limits.PushoutCocone.IsColimit.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{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)
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(t : CategoryTheory.Limits.PushoutCocone f g)
:
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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t)
:
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 : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{t : CategoryTheory.Limits.PushoutCocone f g}
(ht : CategoryTheory.Limits.IsColimit t.flip)
:
A square is a pushout square if its flip is.
Equations
- CategoryTheory.Limits.PushoutCocone.isColimitOfFlip ht = (CategoryTheory.Limits.PushoutCocone.flipIsColimit ht).ofIsoColimit t.flipFlipIso
@[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
@[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))
:
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))
:
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.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)
:
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)
:
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.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
@[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
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)
:
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.