HasPullback #
HasPullback f g and pullback f g provides API for HasLimit and limit in the case of
pullacks.
Main definitions #
HasPullback f g: this is an abbreviation forHasLimit (cospan f g), and is a typeclass used to express the fact that a given pair of morphisms has a pullback.HasPullbacks: expresses the fact thatCadmits all pullbacks, it is implemented as an abbreviation forHasLimitsOfShape WalkingCospan Cpullback f g: Given aHasPullback f ginstance, this function returns the choice of a limit object corresponding to the pullback offandg. It fits into the following diagram:
pullback f g ---pullback.snd f g---> Y
| |
| |
pullback.snd f g g
| |
v v
X --------------f--------------> Z
HasPushout f g: this is an abbreviation forHasColimit (span f g), and is a typeclass used to express the fact that a given pair of morphisms has a pushout.HasPushouts: expresses the fact thatCadmits all pushouts, it is implemented as an abbreviation forHasColimitsOfShape WalkingSpan Cpushout f g: Given aHasPushout f ginstance, this function returns the choice of a colimit object corresponding to the pushout offandg. It fits into the following diagram:
X --------------f--------------> Y
| |
g pushout.inr f g
| |
v v
Z ---pushout.inl f g---> pushout f g
Main results & API #
The following API is available for using the universal property of
pullback f g:lift,lift_fst,lift_snd,lift',hom_ext(for uniqueness).pullback.mapis the induced map between pullbacksW ×ₛ X ⟶ Y ×ₜ Zgiven pointwise (compatible) mapsW ⟶ Y,X ⟶ ZandS ⟶ T.pullbackComparison: Given a functorG, this is the natural morphismG.obj (pullback f g) ⟶ pullback (G.map f) (G.map g)pullbackSymmetryprovides the natural isomorphismpullback f g ≅ pullback g f
(The dual results for pushouts are also available)
References #
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
HasPullback f g represents a particular choice of limiting cone
for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.
@[reducible, inline]
abbrev
CategoryTheory.Limits.HasPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
HasPushout f g represents a particular choice of colimiting cocone
for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
C
pullback f g computes the pullback of a pair of morphisms with the same target.
Equations
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.cone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The cone associated to the pullback of f and g
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
C
pushout f g computes the pushout of a pair of morphisms with the same source.
Equations
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The cocone associated to the pullback of f and g
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The first projection of the pullback of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The second projection of the pullback of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.inl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The first inclusion into the pushout of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.inr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The second inclusion into the pushout of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
pullback.lift : W ⟶ pullback f g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
pushout.desc : pushout f g ⟶ W.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The cone associated to a pullback is a limit cone.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The cocone associated to a pushout is a colimit cone.
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.fst_limit_cone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.snd_limit_cone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
theorem
CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
theorem
CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
theorem
CategoryTheory.Limits.pullback.lift_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h✝ f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : X ⟶ Z)
:
theorem
CategoryTheory.Limits.pullback.lift_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.pullback.lift_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h✝ f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : Y ⟶ Z)
:
theorem
CategoryTheory.Limits.pullback.lift_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.pushout.inl_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z✝}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z✝ ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h✝ = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
theorem
CategoryTheory.Limits.pushout.inl_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
theorem
CategoryTheory.Limits.pushout.inr_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z✝}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z✝ ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h✝ = CategoryTheory.CategoryStruct.comp g k)
{Z : C}
(h : W ⟶ Z)
:
theorem
CategoryTheory.Limits.pushout.inr_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
def
CategoryTheory.Limits.pullback.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
{ l : W ⟶ CategoryTheory.Limits.pullback f g //
CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) = h ∧ CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g) = k }
A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism
l : W ⟶ pullback f g such that l ≫ pullback.fst = h and l ≫ pullback.snd = k.
Equations
- CategoryTheory.Limits.pullback.lift' h k w = ⟨CategoryTheory.Limits.pullback.lift h k w, ⋯⟩
def
CategoryTheory.Limits.pullback.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
{ l : CategoryTheory.Limits.pushout f g ⟶ W //
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l = h ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l = k }
A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism
l : pushout f g ⟶ W such that pushout.inl _ _ ≫ l = h and pushout.inr _ _ ≫ l = k.
Equations
- CategoryTheory.Limits.pullback.desc' h k w = ⟨CategoryTheory.Limits.pushout.desc h k w, ⋯⟩
theorem
CategoryTheory.Limits.pullback.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : Z✝ ⟶ Z)
:
theorem
CategoryTheory.Limits.pullback.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
:
theorem
CategoryTheory.Limits.pushout.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z✝}
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout f g ⟶ Z)
:
theorem
CategoryTheory.Limits.pushout.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
:
theorem
CategoryTheory.Limits.pullback.hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
{W : C}
{k : W ⟶ CategoryTheory.Limits.pullback f g}
{l : W ⟶ CategoryTheory.Limits.pullback f g}
:
k = l ↔ CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) ∧ CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g)
theorem
CategoryTheory.Limits.pullback.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
{W : C}
{k : W ⟶ CategoryTheory.Limits.pullback f g}
{l : W ⟶ CategoryTheory.Limits.pullback f g}
(h₀ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g))
(h₁ : CategoryTheory.CategoryStruct.comp k (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g))
:
k = l
Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal
def
CategoryTheory.Limits.pullbackIsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The pullback cone built from the pullback projections is a pullback.
theorem
CategoryTheory.Limits.pushout.hom_ext_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
{W : C}
{k : CategoryTheory.Limits.pushout f g ⟶ W}
{l : CategoryTheory.Limits.pushout f g ⟶ W}
:
k = l ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l ∧ CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l
theorem
CategoryTheory.Limits.pushout.hom_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
{W : C}
{k : CategoryTheory.Limits.pushout f g ⟶ W}
{l : CategoryTheory.Limits.pushout f g ⟶ W}
(h₀ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l)
(h₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) k = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l)
:
k = l
Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal
def
CategoryTheory.Limits.pushoutIsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The pushout cocone built from the pushout coprojections is a pushout.
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[CategoryTheory.Limits.HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂)
:
Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.
W ⟶ Y
↘ ↘
S ⟶ T
↗ ↗
X ⟶ Z
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.mapDesc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(i : S ⟶ T)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
:
The canonical map X ×ₛ Y ⟶ X ×ₜ Y given S ⟶ T.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.pullback.map_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
{X'' : C}
{Y'' : C}
{Z'' : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
{f'' : X'' ⟶ Z''}
{g'' : Y'' ⟶ Z''}
(i₁ : X ⟶ X')
(j₁ : X' ⟶ X'')
(i₂ : Y ⟶ Y')
(j₂ : Y' ⟶ Y'')
(i₃ : Z✝ ⟶ Z')
(j₃ : Z' ⟶ Z'')
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' g']
[CategoryTheory.Limits.HasPullback f'' g'']
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
(e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'')
(e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g'')
{Z : C}
(h : CategoryTheory.Limits.pullback f'' g'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁)
(CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯)
h
theorem
CategoryTheory.Limits.pullback.map_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
{X'' : C}
{Y'' : C}
{Z'' : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{f' : X' ⟶ Z'}
{g' : Y' ⟶ Z'}
{f'' : X'' ⟶ Z''}
{g'' : Y'' ⟶ Z''}
(i₁ : X ⟶ X')
(j₁ : X' ⟶ X'')
(i₂ : Y ⟶ Y')
(j₂ : Y' ⟶ Y'')
(i₃ : Z ⟶ Z')
(j₃ : Z' ⟶ Z'')
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback f' g']
[CategoryTheory.Limits.HasPullback f'' g'']
(e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g')
(e₃ : CategoryTheory.CategoryStruct.comp f' j₃ = CategoryTheory.CategoryStruct.comp j₁ f'')
(e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₂ g'')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)
(CategoryTheory.Limits.pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) = CategoryTheory.Limits.pullback.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₁ j₁)
(CategoryTheory.CategoryStruct.comp i₂ j₂) (CategoryTheory.CategoryStruct.comp i₃ j₃) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Limits.pullback.map_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[CategoryTheory.Limits.HasPullback f g]
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[CategoryTheory.Limits.HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[CategoryTheory.Limits.HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂)
:
Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.
W ⟶ Y
↗ ↗
S ⟶ T
↘ ↘
X ⟶ Z
Equations
- One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.mapLift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
:
The canonical map X ⨿ₛ Y ⟶ X ⨿ₜ Y given S ⟶ T.
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Limits.pushout.map_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
{X'' : C}
{Y'' : C}
{Z'' : C}
{f : X ⟶ Y}
{g : X ⟶ Z✝}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
{f'' : X'' ⟶ Y''}
{g'' : X'' ⟶ Z''}
(i₁ : X ⟶ X')
(j₁ : X' ⟶ X'')
(i₂ : Y ⟶ Y')
(j₂ : Y' ⟶ Y'')
(i₃ : Z✝ ⟶ Z')
(j₃ : Z' ⟶ Z'')
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout f' g']
[CategoryTheory.Limits.HasPushout f'' g'']
(e₁ : CategoryTheory.CategoryStruct.comp f i₂ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₁ g')
(e₃ : CategoryTheory.CategoryStruct.comp f' j₂ = CategoryTheory.CategoryStruct.comp j₁ f'')
(e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₁ g'')
{Z : C}
(h : CategoryTheory.Limits.pushout f'' g'' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pushout.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₂ j₂)
(CategoryTheory.CategoryStruct.comp i₃ j₃) (CategoryTheory.CategoryStruct.comp i₁ j₁) ⋯ ⋯)
h
theorem
CategoryTheory.Limits.pushout.map_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
{X'' : C}
{Y'' : C}
{Z'' : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
{f' : X' ⟶ Y'}
{g' : X' ⟶ Z'}
{f'' : X'' ⟶ Y''}
{g'' : X'' ⟶ Z''}
(i₁ : X ⟶ X')
(j₁ : X' ⟶ X'')
(i₂ : Y ⟶ Y')
(j₂ : Y' ⟶ Y'')
(i₃ : Z ⟶ Z')
(j₃ : Z' ⟶ Z'')
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout f' g']
[CategoryTheory.Limits.HasPushout f'' g'']
(e₁ : CategoryTheory.CategoryStruct.comp f i₂ = CategoryTheory.CategoryStruct.comp i₁ f')
(e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₁ g')
(e₃ : CategoryTheory.CategoryStruct.comp f' j₂ = CategoryTheory.CategoryStruct.comp j₁ f'')
(e₄ : CategoryTheory.CategoryStruct.comp g' j₃ = CategoryTheory.CategoryStruct.comp j₁ g'')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.map f g f' g' i₂ i₃ i₁ e₁ e₂)
(CategoryTheory.Limits.pushout.map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) = CategoryTheory.Limits.pushout.map f g f'' g'' (CategoryTheory.CategoryStruct.comp i₂ j₂)
(CategoryTheory.CategoryStruct.comp i₃ j₃) (CategoryTheory.CategoryStruct.comp i₁ j₁) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Limits.pushout.map_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[CategoryTheory.Limits.HasPushout f g]
:
instance
CategoryTheory.Limits.pullback.map_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[CategoryTheory.Limits.HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[CategoryTheory.Limits.HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂)
[CategoryTheory.IsIso i₁]
[CategoryTheory.IsIso i₂]
[CategoryTheory.IsIso i₃]
:
CategoryTheory.IsIso (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Limits.pullback.congrHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
(CategoryTheory.Limits.pullback.congrHom h₁ h₂).hom = CategoryTheory.Limits.pullback.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
def
CategoryTheory.Limits.pullback.congrHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pullback.congrHom_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Z}
{f₂ : X ⟶ Z}
{g₁ : Y ⟶ Z}
{g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPullback f₁ g₁]
[CategoryTheory.Limits.HasPullback f₂ g₂]
:
(CategoryTheory.Limits.pullback.congrHom h₁ h₂).inv = CategoryTheory.Limits.pullback.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯
instance
CategoryTheory.Limits.pushout.map_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{W : C}
{X : C}
{Y : C}
{Z : C}
{S : C}
{T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[CategoryTheory.Limits.HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[CategoryTheory.Limits.HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂)
[CategoryTheory.IsIso i₁]
[CategoryTheory.IsIso i₂]
[CategoryTheory.IsIso i₃]
:
CategoryTheory.IsIso (CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.pullback.mapDesc_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
{S' : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
(i' : S ⟶ S')
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i i'))
(CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp i i'))]
[CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) i')
(CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g i) i')]
:
CategoryTheory.Limits.pullback.mapDesc f g (CategoryTheory.CategoryStruct.comp i i') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.mapDesc f g i)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pullback.mapDesc (CategoryTheory.CategoryStruct.comp f i)
(CategoryTheory.CategoryStruct.comp g i) i')
(CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom)
@[simp]
theorem
CategoryTheory.Limits.pushout.congrHom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
(CategoryTheory.Limits.pushout.congrHom h₁ h₂).hom = CategoryTheory.Limits.pushout.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
def
CategoryTheory.Limits.pushout.congrHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
If f₁ = f₂ and g₁ = g₂, we may construct a canonical
isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pushout.congrHom_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{f₁ : X ⟶ Y}
{f₂ : X ⟶ Y}
{g₁ : X ⟶ Z}
{g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[CategoryTheory.Limits.HasPushout f₁ g₁]
[CategoryTheory.Limits.HasPushout f₂ g₂]
:
(CategoryTheory.Limits.pushout.congrHom h₁ h₂).inv = CategoryTheory.Limits.pushout.map f₂ g₂ f₁ g₁ (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
theorem
CategoryTheory.Limits.pushout.mapLift_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{S : C}
{T : C}
{S' : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
(i' : S' ⟶ S)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i f))
(CategoryTheory.CategoryStruct.comp i' (CategoryTheory.CategoryStruct.comp i g))]
[CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp i' i) g)]
:
CategoryTheory.Limits.pushout.mapLift f g (CategoryTheory.CategoryStruct.comp i' i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.congrHom ⋯ ⋯).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.pushout.mapLift (CategoryTheory.CategoryStruct.comp i f)
(CategoryTheory.CategoryStruct.comp i g) i')
(CategoryTheory.Limits.pushout.mapLift f g i))
def
CategoryTheory.Limits.pullbackComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
G.obj (CategoryTheory.Limits.pullback f g) ⟶ CategoryTheory.Limits.pullback (G.map f) (G.map g)
The comparison morphism for the pullback of f,g.
This is an isomorphism iff G preserves the pullback of f,g; see
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Equations
- CategoryTheory.Limits.pullbackComparison G f g = CategoryTheory.Limits.pullback.lift (G.map (CategoryTheory.Limits.pullback.fst f g)) (G.map (CategoryTheory.Limits.pullback.snd f g)) ⋯
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{Z : D}
(h : G.obj X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.fst f g)) h
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) = G.map (CategoryTheory.Limits.pullback.fst f g)
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{Z : D}
(h : G.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.snd f g)) h
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
(CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) = G.map (CategoryTheory.Limits.pullback.snd f g)
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp h✝ f = CategoryTheory.CategoryStruct.comp k g)
{Z : D}
(h : CategoryTheory.Limits.pullback (G.map f) (G.map g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h✝ k w))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (G.map h✝) (G.map k) ⋯) h
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.lift h k w))
(CategoryTheory.Limits.pullbackComparison G f g) = CategoryTheory.Limits.pullback.lift (G.map h) (G.map k) ⋯
def
CategoryTheory.Limits.pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.Limits.pushout (G.map f) (G.map g) ⟶ G.obj (CategoryTheory.Limits.pushout f g)
The comparison morphism for the pushout of f,g.
This is an isomorphism iff G preserves the pushout of f,g; see
Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
Equations
- CategoryTheory.Limits.pushoutComparison G f g = CategoryTheory.Limits.pushout.desc (G.map (CategoryTheory.Limits.pushout.inl f g)) (G.map (CategoryTheory.Limits.pushout.inr f g)) ⋯
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inl f g)) h
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (G.map f) (G.map g))
(CategoryTheory.Limits.pushoutComparison G f g) = G.map (CategoryTheory.Limits.pushout.inl f g)
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g)) h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
(CategoryTheory.Limits.pushoutComparison G f g) = G.map (CategoryTheory.Limits.pushout.inr f g)
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z✝ ⟶ W}
(w : CategoryTheory.CategoryStruct.comp f h✝ = CategoryTheory.CategoryStruct.comp g k)
{Z : D}
(h : G.obj W ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.desc h✝ k w)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.desc (G.map h✝) (G.map k) ⋯) h
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(G : CategoryTheory.Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g)
(G.map (CategoryTheory.Limits.pushout.desc h k w)) = CategoryTheory.Limits.pushout.desc (G.map h) (G.map k) ⋯
theorem
CategoryTheory.Limits.hasPullback_symmetry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pullbackSymmetry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
The isomorphism X ×[Z] Y ≅ Y ×[Z] X.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z✝)
(g : Y ⟶ Z✝)
[CategoryTheory.Limits.HasPullback f g]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
:
theorem
CategoryTheory.Limits.hasPushout_symmetry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pushoutSymmetry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
The isomorphism Y ⨿[X] Z ≅ Z ⨿[X] Y.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout g f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout g f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout f g ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z✝)
[CategoryTheory.Limits.HasPushout f g]
{Z : C}
(h : CategoryTheory.Limits.pushout f g ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[CategoryTheory.Limits.HasPushout f g]
:
@[reducible, inline]
HasPullbacks represents a choice of pullback for every pair of morphisms
@[reducible, inline]
HasPushouts represents a choice of pushout for every pair of morphisms
theorem
CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)]
:
If C has all limits of diagrams cospan f g, then it has all pullbacks
theorem
CategoryTheory.Limits.hasPushouts_of_hasColimit_span
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)]
:
If C has all colimits of diagrams span f g, then it has all pushouts
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map
{X₁ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair}
{X₂ : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair}
:
∀ (a : X₁ ⟶ X₂),
CategoryTheory.Limits.walkingSpanOpEquiv.inverse.map a = CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair X₁ X₂ a
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_functor_map :
∀ {X Y : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
CategoryTheory.Limits.walkingSpanOpEquiv.functor.map f = (CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X)
f.unop).unop
The duality equivalence WalkingSpanᵒᵖ ≌ WalkingCospan
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_functor_map :
∀ {X Y : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ} (f : X ⟶ Y),
CategoryTheory.Limits.walkingCospanOpEquiv.functor.map f = (CategoryTheory.Limits.widePullbackShapeOpMap CategoryTheory.Limits.WalkingPair (Opposite.unop Y) (Opposite.unop X)
f.unop).unop
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map
{X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair}
{Y : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair}
:
∀ (a : X ⟶ Y),
CategoryTheory.Limits.walkingCospanOpEquiv.inverse.map a = CategoryTheory.Limits.widePushoutShapeOpMap CategoryTheory.Limits.WalkingPair X Y a
The duality equivalence WalkingCospanᵒᵖ ≌ WalkingSpan
@[instance 100]
instance
CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks
(D : Type u)
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.Limits.HasWidePullbacks D]
:
Having wide pullback at any universe level implies having binary pullbacks.
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Limits.hasPushouts_of_hasWidePushouts
(D : Type u)
[CategoryTheory.Category.{v, u} D]
[CategoryTheory.Limits.HasWidePushouts D]
:
Having wide pushout at any universe level implies having binary pushouts.
Equations
- ⋯ = ⋯