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.snd f g---> Y
      |                                |
      |                                |
pullback.snd f g                       g
      |                                |
      v                                v
      X --------------f--------------> 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.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.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : Prop

HasPullback f g represents a particular choice of limiting cone for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.

Equations

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

@[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) : Prop

HasPushout f g represents a particular choice of colimiting cocone for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.

Equations

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

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

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

@[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] : CategoryTheory.Limits.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} [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

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

@[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] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] : Y ⟶ CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] : Z ⟶ CategoryTheory.Limits.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} [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) : W ⟶ CategoryTheory.Limits.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} [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) : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullback.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushout.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} [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)] : CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.fst 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)] : CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g)) = CategoryTheory.Limits.pullback.snd 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)] : CategoryTheory.Limits.PushoutCocone.inl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inl 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)] : CategoryTheory.Limits.PushoutCocone.inr (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) = CategoryTheory.Limits.pushout.inr 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift h✝ k w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp h✝ h

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

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

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

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

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

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

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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) (CategoryTheory.Limits.pushout.desc h k w) = 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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g h)

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] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) 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) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h)

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] : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inl f g) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.pushout.inr 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] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.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_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] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.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.

@[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₂) : CategoryTheory.Limits.pullback f₁ f₂ ⟶ CategoryTheory.Limits.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} [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)] : CategoryTheory.Limits.pullback f g ⟶ CategoryTheory.Limits.pullback (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] : CategoryTheory.Limits.pullback.map f g f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback 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₂) : CategoryTheory.Limits.pushout f₁ f₂ ⟶ CategoryTheory.Limits.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} [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)] : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g) ⟶ CategoryTheory.Limits.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_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] : CategoryTheory.Limits.pushout.map f g f g (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pushout 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₂] : CategoryTheory.Limits.pullback f₁ g₁ ≅ CategoryTheory.Limits.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_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₂] : CategoryTheory.Limits.pushout f₁ g₁ ≅ CategoryTheory.Limits.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_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] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.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_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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h

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

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

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

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

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

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] : CategoryTheory.Limits.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} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.Limits.pushout f g ≅ CategoryTheory.Limits.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_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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutSymmetry f g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g f) h

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

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

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

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

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

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

@[reducible, inline]

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

HasPullbacks represents a choice of pullback for every pair of morphisms

See https://stacks.math.columbia.edu/tag/001W

Equations

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

@[reducible, inline]

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

HasPushouts represents a choice of pushout for every pair of morphisms

Equations

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

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)] : CategoryTheory.Limits.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) [CategoryTheory.Category.{v, u} C] [∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)] : CategoryTheory.Limits.HasPushouts C

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_inverse_obj (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingSpanOpEquiv.inverse.obj X = Opposite.op X

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The duality equivalence WalkingSpanᵒᵖ ≌ WalkingCospan

Equations

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

@[simp]

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

@[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_obj (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair) : CategoryTheory.Limits.walkingCospanOpEquiv.inverse.obj X = Opposite.op X

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

The duality equivalence WalkingCospanᵒᵖ ≌ WalkingSpan

Equations

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

@[instance 100]

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

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

Equations

• ⋯ = ⋯