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}
[Category.{v, u} C]
{X Y 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}
[Category.{v, u} C]
{X Y 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}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[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}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
PullbackCone f g
The cone associated to the pullback of f and g
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[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}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
PushoutCocone f g
The cocone associated to the pullback of f and g
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.fst
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
The first projection of the pullback of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.snd
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
The second projection of the pullback of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.inl
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
The first inclusion into the pushout of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.inr
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
The second inclusion into the pushout of f and g.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.lift
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = 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}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = 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}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
The cone associated to a pullback is a limit cone.
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.isColimit
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
The cocone associated to a pushout is a colimit cone.
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.fst_limit_cone
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasLimit (cospan f g)]
:
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.snd_limit_cone
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasLimit (cospan f g)]
:
theorem
CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[HasColimit (span f g)]
:
theorem
CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : Z ⟶ X)
(g : Z ⟶ Y)
[HasColimit (span f g)]
:
theorem
CategoryTheory.Limits.pullback.lift_fst
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.pullback.lift_fst_assoc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
{Z✝ : C}
(h✝ : X ⟶ Z✝)
:
theorem
CategoryTheory.Limits.pullback.lift_snd
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
theorem
CategoryTheory.Limits.pullback.lift_snd_assoc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
{Z✝ : C}
(h✝ : Y ⟶ Z✝)
:
theorem
CategoryTheory.Limits.pushout.inl_desc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
theorem
CategoryTheory.Limits.pushout.inl_desc_assoc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Z✝ : C}
(h✝ : W ⟶ Z✝)
:
theorem
CategoryTheory.Limits.pushout.inr_desc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
theorem
CategoryTheory.Limits.pushout.inr_desc_assoc
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Z✝ : C}
(h✝ : W ⟶ Z✝)
:
def
CategoryTheory.Limits.pullback.lift'
{C : Type u}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
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}
[Category.{v, u} C]
{W X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
(h : Y ⟶ W)
(k : Z ⟶ W)
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
{ l : pushout f g ⟶ W // CategoryStruct.comp (pushout.inl f g) l = h ∧ CategoryStruct.comp (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
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
:
theorem
CategoryTheory.Limits.pullback.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
{Z✝ : C}
(h : Z ⟶ Z✝)
:
CategoryStruct.comp (fst f g) (CategoryStruct.comp f h) = CategoryStruct.comp (snd f g) (CategoryStruct.comp g h)
theorem
CategoryTheory.Limits.pushout.condition
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
:
theorem
CategoryTheory.Limits.pushout.condition_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
{Z✝ : C}
(h : pushout f g ⟶ Z✝)
:
CategoryStruct.comp f (CategoryStruct.comp (inl f g) h) = CategoryStruct.comp g (CategoryStruct.comp (inr f g) h)
theorem
CategoryTheory.Limits.pullback.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
{W : C}
{k l : W ⟶ pullback f g}
(h₀ : CategoryStruct.comp k (fst f g) = CategoryStruct.comp l (fst f g))
(h₁ : CategoryStruct.comp k (snd f g) = CategoryStruct.comp l (snd f g))
:
Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal
def
CategoryTheory.Limits.pullbackIsPullback
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
IsLimit (PullbackCone.mk (pullback.fst f g) (pullback.snd f g) ⋯)
The pullback cone built from the pullback projections is a pullback.
theorem
CategoryTheory.Limits.pushout.hom_ext
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
{W : C}
{k l : pushout f g ⟶ W}
(h₀ : CategoryStruct.comp (inl f g) k = CategoryStruct.comp (inl f g) l)
(h₁ : CategoryStruct.comp (inr f g) k = CategoryStruct.comp (inr f g) 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}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
IsColimit (PushoutCocone.mk (pushout.inl f g) (pushout.inr 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.
@[simp]
theorem
CategoryTheory.Limits.pullback.lift_fst_snd
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pushout.desc_inl_inr
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
@[reducible, inline]
abbrev
CategoryTheory.Limits.pullback.map
{C : Type u}
[Category.{v, u} C]
{W X Y Z S T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryStruct.comp f₂ i₃ = 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}
[Category.{v, u} C]
{X Y S T : C}
(f : X ⟶ S)
(g : Y ⟶ S)
(i : S ⟶ T)
[HasPullback f g]
[HasPullback (CategoryStruct.comp f i) (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
{C : Type u}
[Category.{v, u} C]
{X Y Z X' Y' Z' X'' Y'' 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'')
[HasPullback f g]
[HasPullback f' g']
[HasPullback f'' g'']
(e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f')
(e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g')
(e₃ : CategoryStruct.comp f' j₃ = CategoryStruct.comp j₁ f'')
(e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₂ g'')
:
CategoryStruct.comp (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) = map f g f'' g'' (CategoryStruct.comp i₁ j₁) (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) ⋯ ⋯
theorem
CategoryTheory.Limits.pullback.map_comp_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z X' Y' Z' X'' Y'' 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'')
[HasPullback f g]
[HasPullback f' g']
[HasPullback f'' g'']
(e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f')
(e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g')
(e₃ : CategoryStruct.comp f' j₃ = CategoryStruct.comp j₁ f'')
(e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₂ g'')
{Z✝ : C}
(h : pullback f'' g'' ⟶ Z✝)
:
CategoryStruct.comp (map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryStruct.comp (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄) h) = CategoryStruct.comp
(map f g f'' g'' (CategoryStruct.comp i₁ j₁) (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) ⋯ ⋯) h
@[simp]
theorem
CategoryTheory.Limits.pullback.map_id
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
[HasPullback f g]
:
map f g f g (CategoryStruct.id X) (CategoryStruct.id Y) (CategoryStruct.id Z) ⋯ ⋯ = CategoryStruct.id (pullback f g)
@[reducible, inline]
abbrev
CategoryTheory.Limits.pushout.map
{C : Type u}
[Category.{v, u} C]
{W X Y Z S T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryStruct.comp f₁ i₁ = CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryStruct.comp f₂ i₂ = 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}
[Category.{v, u} C]
{X Y S T : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
[HasPushout f g]
[HasPushout (CategoryStruct.comp i f) (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
{C : Type u}
[Category.{v, u} C]
{X Y Z X' Y' Z' X'' Y'' 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'')
[HasPushout f g]
[HasPushout f' g']
[HasPushout f'' g'']
(e₁ : CategoryStruct.comp f i₂ = CategoryStruct.comp i₁ f')
(e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₁ g')
(e₃ : CategoryStruct.comp f' j₂ = CategoryStruct.comp j₁ f'')
(e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₁ g'')
:
CategoryStruct.comp (map f g f' g' i₂ i₃ i₁ e₁ e₂) (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) = map f g f'' g'' (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) (CategoryStruct.comp i₁ j₁) ⋯ ⋯
theorem
CategoryTheory.Limits.pushout.map_comp_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z X' Y' Z' X'' Y'' 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'')
[HasPushout f g]
[HasPushout f' g']
[HasPushout f'' g'']
(e₁ : CategoryStruct.comp f i₂ = CategoryStruct.comp i₁ f')
(e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₁ g')
(e₃ : CategoryStruct.comp f' j₂ = CategoryStruct.comp j₁ f'')
(e₄ : CategoryStruct.comp g' j₃ = CategoryStruct.comp j₁ g'')
{Z✝ : C}
(h : pushout f'' g'' ⟶ Z✝)
:
CategoryStruct.comp (map f g f' g' i₂ i₃ i₁ e₁ e₂) (CategoryStruct.comp (map f' g' f'' g'' j₂ j₃ j₁ e₃ e₄) h) = CategoryStruct.comp
(map f g f'' g'' (CategoryStruct.comp i₂ j₂) (CategoryStruct.comp i₃ j₃) (CategoryStruct.comp i₁ j₁) ⋯ ⋯) h
@[simp]
theorem
CategoryTheory.Limits.pushout.map_id
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
[HasPushout f g]
:
map f g f g (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯ = CategoryStruct.id (pushout f g)
instance
CategoryTheory.Limits.pullback.map_isIso
{C : Type u}
[Category.{v, u} C]
{W X Y Z S T : C}
(f₁ : W ⟶ S)
(f₂ : X ⟶ S)
[HasPullback f₁ f₂]
(g₁ : Y ⟶ T)
(g₂ : Z ⟶ T)
[HasPullback g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁)
(eq₂ : CategoryStruct.comp f₂ i₃ = CategoryStruct.comp i₂ g₂)
[IsIso i₁]
[IsIso i₂]
[IsIso i₃]
:
def
CategoryTheory.Limits.pullback.congrHom
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPullback f₁ g₁]
[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_hom
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPullback f₁ g₁]
[HasPullback f₂ g₂]
:
(congrHom h₁ h₂).hom = map f₁ g₁ f₂ g₂ (CategoryStruct.id X) (CategoryStruct.id Y) (CategoryStruct.id Z) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Limits.pullback.congrHom_inv
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Z}
{g₁ g₂ : Y ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPullback f₁ g₁]
[HasPullback f₂ g₂]
:
(congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (CategoryStruct.id X) (CategoryStruct.id Y) (CategoryStruct.id Z) ⋯ ⋯
instance
CategoryTheory.Limits.pushout.map_isIso
{C : Type u}
[Category.{v, u} C]
{W X Y Z S T : C}
(f₁ : S ⟶ W)
(f₂ : S ⟶ X)
[HasPushout f₁ f₂]
(g₁ : T ⟶ Y)
(g₂ : T ⟶ Z)
[HasPushout g₁ g₂]
(i₁ : W ⟶ Y)
(i₂ : X ⟶ Z)
(i₃ : S ⟶ T)
(eq₁ : CategoryStruct.comp f₁ i₁ = CategoryStruct.comp i₃ g₁)
(eq₂ : CategoryStruct.comp f₂ i₂ = CategoryStruct.comp i₃ g₂)
[IsIso i₁]
[IsIso i₂]
[IsIso i₃]
:
theorem
CategoryTheory.Limits.pullback.mapDesc_comp
{C : Type u}
[Category.{v, u} C]
{X Y S T S' : C}
(f : X ⟶ T)
(g : Y ⟶ T)
(i : T ⟶ S)
(i' : S ⟶ S')
[HasPullback f g]
[HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)]
[HasPullback (CategoryStruct.comp f (CategoryStruct.comp i i')) (CategoryStruct.comp g (CategoryStruct.comp i i'))]
[HasPullback (CategoryStruct.comp (CategoryStruct.comp f i) i') (CategoryStruct.comp (CategoryStruct.comp g i) i')]
:
mapDesc f g (CategoryStruct.comp i i') = CategoryStruct.comp (mapDesc f g i)
(CategoryStruct.comp (mapDesc (CategoryStruct.comp f i) (CategoryStruct.comp g i) i') (congrHom ⋯ ⋯).hom)
def
CategoryTheory.Limits.pushout.congrHom
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPushout f₁ g₁]
[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_hom
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPushout f₁ g₁]
[HasPushout f₂ g₂]
:
(congrHom h₁ h₂).hom = map f₁ g₁ f₂ g₂ (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯
@[simp]
theorem
CategoryTheory.Limits.pushout.congrHom_inv
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{f₁ f₂ : X ⟶ Y}
{g₁ g₂ : X ⟶ Z}
(h₁ : f₁ = f₂)
(h₂ : g₁ = g₂)
[HasPushout f₁ g₁]
[HasPushout f₂ g₂]
:
(congrHom h₁ h₂).inv = map f₂ g₂ f₁ g₁ (CategoryStruct.id Y) (CategoryStruct.id Z) (CategoryStruct.id X) ⋯ ⋯
theorem
CategoryTheory.Limits.pushout.mapLift_comp
{C : Type u}
[Category.{v, u} C]
{X Y S T S' : C}
(f : T ⟶ X)
(g : T ⟶ Y)
(i : S ⟶ T)
(i' : S' ⟶ S)
[HasPushout f g]
[HasPushout (CategoryStruct.comp i f) (CategoryStruct.comp i g)]
[HasPushout (CategoryStruct.comp i' (CategoryStruct.comp i f)) (CategoryStruct.comp i' (CategoryStruct.comp i g))]
[HasPushout (CategoryStruct.comp (CategoryStruct.comp i' i) f) (CategoryStruct.comp (CategoryStruct.comp i' i) g)]
:
mapLift f g (CategoryStruct.comp i' i) = CategoryStruct.comp (congrHom ⋯ ⋯).hom
(CategoryStruct.comp (mapLift (CategoryStruct.comp i f) (CategoryStruct.comp i g) i') (mapLift f g i))
def
CategoryTheory.Limits.pullbackComparison
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (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
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
:
CategoryStruct.comp (pullbackComparison G f g) (pullback.fst (G.map f) (G.map g)) = G.map (pullback.fst f g)
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_fst_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
{Z✝ : D}
(h : G.obj X ⟶ Z✝)
:
CategoryStruct.comp (pullbackComparison G f g) (CategoryStruct.comp (pullback.fst (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (pullback.fst f g)) h
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
:
CategoryStruct.comp (pullbackComparison G f g) (pullback.snd (G.map f) (G.map g)) = G.map (pullback.snd f g)
@[simp]
theorem
CategoryTheory.Limits.pullbackComparison_comp_snd_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
{Z✝ : D}
(h : G.obj Y ⟶ Z✝)
:
CategoryStruct.comp (pullbackComparison G f g) (CategoryStruct.comp (pullback.snd (G.map f) (G.map g)) h) = CategoryStruct.comp (G.map (pullback.snd f g)) h
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
:
CategoryStruct.comp (G.map (pullback.lift h k w)) (pullbackComparison G f g) = pullback.lift (G.map h) (G.map k) ⋯
@[simp]
theorem
CategoryTheory.Limits.map_lift_pullbackComparison_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPullback (G.map f) (G.map g)]
{W : C}
{h : W ⟶ X}
{k : W ⟶ Y}
(w : CategoryStruct.comp h f = CategoryStruct.comp k g)
{Z✝ : D}
(h✝ : pullback (G.map f) (G.map g) ⟶ Z✝)
:
CategoryStruct.comp (G.map (pullback.lift h k w)) (CategoryStruct.comp (pullbackComparison G f g) h✝) = CategoryStruct.comp (pullback.lift (G.map h) (G.map k) ⋯) h✝
def
CategoryTheory.Limits.pushoutComparison
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map 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
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
:
CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) (pushoutComparison G f g) = G.map (pushout.inl f g)
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutComparison_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
{Z✝ : D}
(h : G.obj (pushout f g) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inl (G.map f) (G.map g)) (CategoryStruct.comp (pushoutComparison G f g) h) = CategoryStruct.comp (G.map (pushout.inl f g)) h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
:
CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) (pushoutComparison G f g) = G.map (pushout.inr f g)
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutComparison_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
{Z✝ : D}
(h : G.obj (pushout f g) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inr (G.map f) (G.map g)) (CategoryStruct.comp (pushoutComparison G f g) h) = CategoryStruct.comp (G.map (pushout.inr f g)) h
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
:
CategoryStruct.comp (pushoutComparison G f g) (G.map (pushout.desc h k w)) = pushout.desc (G.map h) (G.map k) ⋯
@[simp]
theorem
CategoryTheory.Limits.pushoutComparison_map_desc_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
{D : Type u₂}
[Category.{v₂, u₂} D]
(G : Functor C D)
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
[HasPushout (G.map f) (G.map g)]
{W : C}
{h : Y ⟶ W}
{k : Z ⟶ W}
(w : CategoryStruct.comp f h = CategoryStruct.comp g k)
{Z✝ : D}
(h✝ : G.obj W ⟶ Z✝)
:
CategoryStruct.comp (pushoutComparison G f g) (CategoryStruct.comp (G.map (pushout.desc h k w)) h✝) = CategoryStruct.comp (pushout.desc (G.map h) (G.map k) ⋯) h✝
theorem
CategoryTheory.Limits.hasPullback_symmetry
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
HasPullback g f
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pullbackSymmetry
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[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
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
{Z✝ : C}
(h : Y ⟶ Z✝)
:
CategoryStruct.comp (pullbackSymmetry f g).hom (CategoryStruct.comp (pullback.fst g f) h) = CategoryStruct.comp (pullback.snd f g) h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
{Z✝ : C}
(h : X ⟶ Z✝)
:
CategoryStruct.comp (pullbackSymmetry f g).hom (CategoryStruct.comp (pullback.snd g f) h) = CategoryStruct.comp (pullback.fst f g) h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
{Z✝ : C}
(h : X ⟶ Z✝)
:
CategoryStruct.comp (pullbackSymmetry f g).inv (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pullback.snd g f) h
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
:
@[simp]
theorem
CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
{Z✝ : C}
(h : Y ⟶ Z✝)
:
CategoryStruct.comp (pullbackSymmetry f g).inv (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pullback.fst g f) h
theorem
CategoryTheory.Limits.hasPushout_symmetry
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
HasPushout g f
Making this a global instance would make the typeclass search go in an infinite loop.
def
CategoryTheory.Limits.pushoutSymmetry
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[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
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
{Z✝ : C}
(h : pushout g f ⟶ Z✝)
:
CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushoutSymmetry f g).hom h) = CategoryStruct.comp (pushout.inr g f) h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
{Z✝ : C}
(h : pushout g f ⟶ Z✝)
:
CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushoutSymmetry f g).hom h) = CategoryStruct.comp (pushout.inl g f) h
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
{Z✝ : C}
(h : pushout f g ⟶ Z✝)
:
CategoryStruct.comp (pushout.inl g f) (CategoryStruct.comp (pushoutSymmetry f g).inv h) = CategoryStruct.comp (pushout.inr f g) h
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
:
@[simp]
theorem
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv_assoc
{C : Type u}
[Category.{v, u} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
[HasPushout f g]
{Z✝ : C}
(h : pushout f g ⟶ Z✝)
:
CategoryStruct.comp (pushout.inr g f) (CategoryStruct.comp (pushoutSymmetry f g).inv h) = CategoryStruct.comp (pushout.inl f g) h
@[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)
[Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, HasLimit (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)
[Category.{v, u} C]
[∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, HasColimit (span f g)]
:
If C has all colimits of diagrams span f g, then it has all pushouts
The duality equivalence WalkingSpanᵒᵖ ≌ WalkingCospan
@[simp]
@[simp]
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_functor_map
{X✝ Y✝ : (WidePushoutShape WalkingPair)ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
walkingSpanOpEquiv.functor.map f = (widePushoutShapeOpMap WalkingPair (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
@[simp]
theorem
CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map
{X₁ X₂ : WidePullbackShape WalkingPair}
(a✝ : X₁ ⟶ X₂)
:
@[simp]
@[simp]
The duality equivalence WalkingCospanᵒᵖ ≌ WalkingSpan
@[simp]
@[simp]
@[simp]
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map
{X Y : WidePushoutShape WalkingPair}
(a✝ : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.Limits.walkingCospanOpEquiv_functor_map
{X✝ Y✝ : (WidePullbackShape WalkingPair)ᵒᵖ}
(f : X✝ ⟶ Y✝)
:
walkingCospanOpEquiv.functor.map f = (widePullbackShapeOpMap WalkingPair (Opposite.unop Y✝) (Opposite.unop X✝) f.unop).unop
@[simp]
@[instance 100]
instance
CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks
(D : Type u)
[Category.{v, u} D]
[HasWidePullbacks D]
:
Having wide pullback at any universe level implies having binary pullbacks.
@[instance 100]
instance
CategoryTheory.Limits.hasPushouts_of_hasWidePushouts
(D : Type u)
[Category.{v, u} D]
[HasWidePushouts D]
:
Having wide pushout at any universe level implies having binary pushouts.