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 for HasLimit (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 that C admits all pullbacks, it is implemented as an abbreviation for HasLimitsOfShape WalkingCospan C

• pullback f g: Given a HasPullback f g instance, this function returns the choice of a limit object corresponding to the pullback of f and g. It fits into the following diagram:

  pullback f g ---pullback.fst f g---> X
      |                                |
      |                                |
pullback.snd f g                       f
      |                                |
      v                                v
      Y --------------g--------------> Z

• HasPushout f g: this is an abbreviation for HasColimit (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 that C admits all pushouts, it is implemented as an abbreviation for HasColimitsOfShape WalkingSpan C
• pushout f g: Given a HasPushout f g instance, this function returns the choice of a colimit object corresponding to the pushout of f and g. It fits into the following diagram:

      X --------------f--------------> Y
      |                                |
      g                          pushout.inl f g
      |                                |
      v                                v
      Z ---pushout.inr 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.map is the induced map between pullbacks W ×ₛ X ⟶ Y ×ₜ Z given pointwise (compatible) maps W ⟶ Y, X ⟶ Z and S ⟶ T.

• pullbackComparison: Given a functor G, this is the natural morphism G.obj (pullback f g) ⟶ pullback (G.map f) (G.map g)

• pullbackSymmetry provides the natural isomorphism pullback f g ≅ pullback g f

(The dual results for pushouts are also available)

References

• Stacks: Fibre products
• Stacks: Pushouts

@[reducible, inline]

abbrev CategoryTheory.Limits.HasPullback {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : Prop

Two morphisms f : X ⟶ Z and g : Y ⟶ Z have a pullback if the diagram cospan f g has a limit.

Equations

• CategoryTheory.Limits.HasPullback f g = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasPushout {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : Prop

Two morphisms f : X ⟶ Y and g : X ⟶ Z have a pushout if the diagram span f g has a colimit.

Equations

• CategoryTheory.Limits.HasPushout f g = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)

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

• CategoryTheory.Limits.pullback f g = CategoryTheory.Limits.limit (CategoryTheory.Limits.cospan f g)

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

Equations

• CategoryTheory.Limits.pullback.cone f g = CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f 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

• CategoryTheory.Limits.pushout f g = CategoryTheory.Limits.colimit (CategoryTheory.Limits.span f g)

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

Equations

• CategoryTheory.Limits.pushout.cocone f g = CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f 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] : pullback f g ⟶ X

The first projection of the pullback of f and g.

Equations

• CategoryTheory.Limits.pullback.fst f g = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.left

@[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] : pullback f g ⟶ Y

The second projection of the pullback of f and g.

Equations

• CategoryTheory.Limits.pullback.snd f g = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.right

@[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] : Y ⟶ pushout f g

The first inclusion into the pushout of f and g.

Equations

• CategoryTheory.Limits.pushout.inl f g = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.left

@[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] : Z ⟶ pushout f g

The second inclusion into the pushout of f and g.

Equations

• CategoryTheory.Limits.pushout.inr f g = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.right

@[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 := by cat_disch) : W ⟶ pullback f 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.

Equations

• CategoryTheory.Limits.pullback.lift h k w = CategoryTheory.Limits.limit.lift (CategoryTheory.Limits.cospan f g) (CategoryTheory.Limits.PullbackCone.mk h k w)

@[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 := by cat_disch) : pushout f g ⟶ W

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.

Equations

• CategoryTheory.Limits.pushout.desc h k w = CategoryTheory.Limits.colimit.desc (CategoryTheory.Limits.span f g) (CategoryTheory.Limits.PushoutCocone.mk h k 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] : IsLimit (cone f g)

The cone associated to a pullback is a limit cone.

Equations

• CategoryTheory.Limits.pullback.isLimit f g = CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.cospan f g)

@[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] : IsColimit (cocone f g)

The cocone associated to a pushout is a colimit cone.

Equations

• CategoryTheory.Limits.pushout.isColimit f g = CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.span f g)

@[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)] : fst (limit.cone (cospan f g)) = pullback.fst 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)] : snd (limit.cone (cospan f g)) = pullback.snd 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)] : inl (colimit.cocone (span f g)) = pushout.inl 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)] : inr (colimit.cocone (span f g)) = pushout.inr 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) : CategoryStruct.comp (lift h k w) (fst f g) = h

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✝) : CategoryStruct.comp (lift h k w) (CategoryStruct.comp (fst f g) h✝) = CategoryStruct.comp h h✝

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) : CategoryStruct.comp (lift h k w) (snd f g) = k

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✝) : CategoryStruct.comp (lift h k w) (CategoryStruct.comp (snd f g) h✝) = CategoryStruct.comp k h✝

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) : CategoryStruct.comp (inl f g) (desc h k w) = h

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✝) : CategoryStruct.comp (inl f g) (CategoryStruct.comp (desc h k w) h✝) = CategoryStruct.comp h h✝

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) : CategoryStruct.comp (inr f g) (desc h k w) = 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✝) : CategoryStruct.comp (inr f g) (CategoryStruct.comp (desc h k w) h✝) = CategoryStruct.comp k h✝

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) : { l : W ⟶ pullback f g // CategoryStruct.comp l (fst f g) = h ∧ CategoryStruct.comp l (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} [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] : CategoryStruct.comp (fst f g) f = CategoryStruct.comp (snd f g) 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] : CategoryStruct.comp f (inl f g) = CategoryStruct.comp g (inr 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)) : k = l

Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal

theorem CategoryTheory.Limits.pullback.hom_ext_iff {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} : k = l ↔ CategoryStruct.comp k (fst f g) = CategoryStruct.comp l (fst f g) ∧ CategoryStruct.comp k (snd f g) = CategoryStruct.comp l (snd f g)

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.

Equations

• CategoryTheory.Limits.pullbackIsPullback f g = CategoryTheory.Limits.PullbackCone.mkSelfIsLimit (CategoryTheory.Limits.pullback.isLimit f g)

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) : k = l

Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal

theorem CategoryTheory.Limits.pushout.hom_ext_iff {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} : k = l ↔ CategoryStruct.comp (inl f g) k = CategoryStruct.comp (inl f g) l ∧ CategoryStruct.comp (inr f g) k = CategoryStruct.comp (inr f g) l

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] : lift (fst f g) (snd f g) ⋯ = CategoryStruct.id (pullback 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] : desc (inl f g) (inr f g) ⋯ = CategoryStruct.id (pushout 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₂) : pullback f₁ f₂ ⟶ pullback g₁ 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)] : pullback f g ⟶ pullback (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₂) : pushout f₁ f₂ ⟶ pushout g₁ 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)] : pushout (CategoryStruct.comp i f) (CategoryStruct.comp i g) ⟶ pushout f 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₃] : IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

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₂] : pullback f₁ g₁ ≅ pullback 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₃] : IsIso (map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)

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₂] : pushout f₁ g₁ ≅ pushout 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)] : G.obj (pullback f g) ⟶ 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 {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)] : pushout (G.map f) (G.map g) ⟶ G.obj (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 {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] : pullback f g ≅ pullback g f

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] : CategoryStruct.comp (pullbackSymmetry f g).hom (pullback.fst g f) = pullback.snd 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] : CategoryStruct.comp (pullbackSymmetry f g).hom (pullback.snd g f) = pullback.fst 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] : CategoryStruct.comp (pullbackSymmetry f g).inv (pullback.fst f g) = pullback.snd g f

@[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] : CategoryStruct.comp (pullbackSymmetry f g).inv (pullback.snd f g) = pullback.fst g f

@[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] : pushout f g ≅ pushout g f

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] : CategoryStruct.comp (pushout.inl f g) (pushoutSymmetry f g).hom = pushout.inr g f

@[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] : CategoryStruct.comp (pushout.inr f g) (pushoutSymmetry f g).hom = pushout.inl g f

@[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] : CategoryStruct.comp (pushout.inl g f) (pushoutSymmetry f g).inv = pushout.inr 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] : CategoryStruct.comp (pushout.inr g f) (pushoutSymmetry f g).inv = pushout.inl 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]

abbrev CategoryTheory.Limits.HasPullbacksAlong {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

HasPullbacksAlong f states that pullbacks of all morphisms into Y along f : X ⟶ Y exist.

Equations

• CategoryTheory.Limits.HasPullbacksAlong f = ∀ {W : C} (h : W ⟶ Y), CategoryTheory.Limits.HasPullback h f

@[reducible, inline]

abbrev CategoryTheory.Limits.HasPushoutsAlong {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) : Prop

HasPushoutsAlong f states that pushouts of all morphisms out of X along f : X ⟶ Y exist.

Equations

• CategoryTheory.Limits.HasPushoutsAlong f = ∀ {W : C} (h : X ⟶ W), CategoryTheory.Limits.HasPushout h f

@[reducible, inline]

abbrev CategoryTheory.Limits.HasPullbacks (C : Type u) [Category.{v, u} C] : Prop

A category HasPullbacks if it has all limits of shape WalkingCospan, i.e. if it has a pullback for every pair of morphisms with the same codomain.

Equations

• CategoryTheory.Limits.HasPullbacks C = CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingCospan C

@[reducible, inline]

abbrev CategoryTheory.Limits.HasPushouts (C : Type u) [Category.{v, u} C] : Prop

A category HasPushouts if it has all colimits of shape WalkingSpan, i.e. if it has a pushout for every pair of morphisms with the same domain.

Equations

• CategoryTheory.Limits.HasPushouts C = CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C

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)] : HasPullbacks C

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)] : HasPushouts C

If C has all colimits of diagrams span f g, then it has all pushouts

def CategoryTheory.Limits.walkingSpanOpEquiv : WalkingSpanᵒᵖ ≌ WalkingCospan

The duality equivalence WalkingSpanᵒᵖ ≌ WalkingCospan

Equations

• CategoryTheory.Limits.walkingSpanOpEquiv = CategoryTheory.Limits.widePushoutShapeOpEquiv CategoryTheory.Limits.WalkingPair

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_hom_app (X : WidePullbackShape WalkingPair) : walkingSpanOpEquiv.counitIso.hom.app X = CategoryStruct.id X

@[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_unitIso_hom_app (X : (WidePushoutShape WalkingPair)ᵒᵖ) : walkingSpanOpEquiv.unitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj (X : WidePullbackShape WalkingPair) : walkingSpanOpEquiv.inverse.obj X = Opposite.op X

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_counitIso_inv_app (X : WidePullbackShape WalkingPair) : walkingSpanOpEquiv.counitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_inverse_map {X₁ X₂ : WidePullbackShape WalkingPair} (a✝ : X₁ ⟶ X₂) : walkingSpanOpEquiv.inverse.map a✝ = widePullbackShapeOpMap WalkingPair X₁ X₂ a✝

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj (X : (WidePushoutShape WalkingPair)ᵒᵖ) : walkingSpanOpEquiv.functor.obj X = Opposite.unop X

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_unitIso_inv_app (X : (WidePushoutShape WalkingPair)ᵒᵖ) : walkingSpanOpEquiv.unitIso.inv.app X = CategoryStruct.id X

def CategoryTheory.Limits.walkingCospanOpEquiv : WalkingCospanᵒᵖ ≌ WalkingSpan

The duality equivalence WalkingCospanᵒᵖ ≌ WalkingSpan

Equations

• CategoryTheory.Limits.walkingCospanOpEquiv = CategoryTheory.Limits.widePullbackShapeOpEquiv CategoryTheory.Limits.WalkingPair

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj (X : WidePushoutShape WalkingPair) : walkingCospanOpEquiv.inverse.obj X = Opposite.op X

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_inv_app (X : (WidePullbackShape WalkingPair)ᵒᵖ) : walkingCospanOpEquiv.unitIso.inv.app X = CategoryStruct.id X

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

theorem CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_hom_app (X : WidePushoutShape WalkingPair) : walkingCospanOpEquiv.counitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_counitIso_inv_app (X : WidePushoutShape WalkingPair) : walkingCospanOpEquiv.counitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_unitIso_hom_app (X : (WidePullbackShape WalkingPair)ᵒᵖ) : walkingCospanOpEquiv.unitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj (X : (WidePullbackShape WalkingPair)ᵒᵖ) : walkingCospanOpEquiv.functor.obj X = Opposite.unop X

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_inverse_map {X Y : WidePushoutShape WalkingPair} (a✝ : X ⟶ Y) : walkingCospanOpEquiv.inverse.map a✝ = widePushoutShapeOpMap WalkingPair X Y a✝

@[instance 100]

instance CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks (D : Type u) [Category.{v, u} D] [HasWidePullbacks D] : HasPullbacks 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] : HasPushouts D

Having wide pushout at any universe level implies having binary pushouts.