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 abbrevation 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 abbrevation 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)

NOTE: golfed some proofs also

References #

source

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

Instances For

source

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

Instances For

source

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

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)

Instances For

source

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

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)

Instances For

source

@[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 = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.left

Instances For

source

@[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 = CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.right

Instances For

source

@[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 = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.left

Instances For

source

@[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 = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.span f g) CategoryTheory.Limits.WalkingSpan.right

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

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 h) = CategoryTheory.CategoryStruct.comp h✝ h

source

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 = h

source

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 h) = CategoryTheory.CategoryStruct.comp k h

source

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 = k

source

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

source

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 (CategoryTheory.Limits.pushout.desc h k w) = h

source

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

source

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 (CategoryTheory.Limits.pushout.desc h k w) = k

source

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 = h ∧ CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd = 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, ⋯⟩

Instances For

source

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 l = h ∧ CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr 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, ⋯⟩

Instances For

source

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

source

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 = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g

source

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 h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)

source

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 = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.pushout.inr

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

k = l

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

source

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 CategoryTheory.Limits.pullback.snd ⋯)

The pullback cone built from the pullback projections is a pullback.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

k = l

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

source

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 CategoryTheory.Limits.pushout.inr ⋯)

The pushout cocone built from the pushout coprojections is a pushout.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

⋯ = ⋯

source

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

source

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.

Instances For

source

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

source

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

⋯ = ⋯

source

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)

source

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

source

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.

Instances For

source

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

source

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))

source

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) (G.map CategoryTheory.Limits.pullback.snd) ⋯

Instances For

source

@[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 h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) h

source

@[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 CategoryTheory.Limits.pullback.fst

source

@[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 h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) h

source

@[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 CategoryTheory.Limits.pullback.snd

source

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

source

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

source

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) (G.map CategoryTheory.Limits.pushout.inr) ⋯

Instances For

source

@[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 (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inl) h

source

@[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 (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inl

source

@[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 (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutComparison G f g) h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pushout.inr) h

source

@[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 (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inr

source

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

source

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

source

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.

source

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.

Instances For

source

@[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 h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h

source

@[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 = CategoryTheory.Limits.pullback.snd

source

@[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 h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h

source

@[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 = CategoryTheory.Limits.pullback.fst

source

@[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 h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h

source

@[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 = CategoryTheory.Limits.pullback.snd

source

@[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 h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h

source

@[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 = CategoryTheory.Limits.pullback.fst

source

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.

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

source

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

source

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

source

@[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 Y.unop X.unop f.unop).unop

source

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

source

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_functor_obj (X : (CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) :

CategoryTheory.Limits.walkingSpanOpEquiv.functor.obj X = X.unop

source

@[simp]

theorem CategoryTheory.Limits.walkingSpanOpEquiv_inverse_obj (X : CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair) :

CategoryTheory.Limits.walkingSpanOpEquiv.inverse.obj X = { unop := X }

source

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

source

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

source

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

Instances For

source

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

source

@[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 Y.unop X.unop f.unop).unop

source

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

source

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

source

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_functor_obj (X : (CategoryTheory.Limits.WidePullbackShape CategoryTheory.Limits.WalkingPair)ᵒᵖ) :

CategoryTheory.Limits.walkingCospanOpEquiv.functor.obj X = X.unop

source

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

source

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

source

@[simp]

theorem CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair) :

CategoryTheory.Limits.walkingCospanOpEquiv.inverse.obj X = { unop := X }

source

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

Instances For

source

@[instance 100]

instance CategoryTheory.Limits.hasPullbacks_of_hasWidePullbacks (D : Type u) [h : CategoryTheory.Category.{v, u} D] [h' : CategoryTheory.Limits.HasWidePullbacks D] :

CategoryTheory.Limits.HasPullbacks D

Having wide pullback at any universe level implies having binary pullbacks.

Equations

⋯ = ⋯

source

@[instance 100]

instance CategoryTheory.Limits.hasPushouts_of_hasWidePushouts (D : Type u) [h : CategoryTheory.Category.{v, u} D] [h' : CategoryTheory.Limits.HasWidePushouts D] :

CategoryTheory.Limits.HasPushouts D

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

Equations

⋯ = ⋯

Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

HasPullback #

Main definitions #

Main results & API #

References #