Weak pullbacks

These are weak limits for diagrams of shape WalkingCospan.

If a category has binary products and weak equalizers, then it has weak pullbacks (see hasWeakPullbacks_of_hasBinaryProducts_of_hasWeakEqualizers).

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeakPullback {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : Prop

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

Equations

• CategoryTheory.Limits.HasWeakPullback f g = CategoryTheory.Limits.HasWeakLimit (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : C

weakPullback f g computes the weak pullback of a pair of morphisms with the same target.

Equations

• CategoryTheory.Limits.weakPullback f g = CategoryTheory.Limits.weakLimit (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.cone {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : PullbackCone f g

The cone associated to the weak pullback of f and g

Equations

• CategoryTheory.Limits.weakPullback.cone f g = CategoryTheory.Limits.weakLimit.cone (CategoryTheory.Limits.cospan f g)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.fst {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : weakPullback f g ⟶ X

The first projection of the weak pullback of f and g.

Equations

• CategoryTheory.Limits.weakPullback.fst f g = CategoryTheory.Limits.weakLimit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.left

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.snd {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : weakPullback f g ⟶ Y

The second projection of the weak pullback of f and g.

Equations

• CategoryTheory.Limits.weakPullback.snd f g = CategoryTheory.Limits.weakLimit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.right

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.lift {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g := by cat_disch) : W ⟶ weakPullback f g

A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism weakPullback.lift : W ⟶ weakPullback f g.

Equations

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

theorem CategoryTheory.Limits.weakPullback.exists_lift {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g := by cat_disch) : ∃ (l : W ⟶ weakPullback f g), CategoryStruct.comp l (fst f g) = h ∧ CategoryStruct.comp l (snd f g) = k

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.isWeakLimit {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : IsWeakLimit (cone f g)

The cone associated to a weak pullback is a weak limit cone.

Equations

• CategoryTheory.Limits.weakPullback.isWeakLimit f g = CategoryTheory.Limits.weakLimit.isWeakLimit (CategoryTheory.Limits.cospan f g)

@[simp]

theorem CategoryTheory.Limits.weakLimit.pullbackConeFst_cone_cospan {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakLimit (cospan f g)] : PullbackCone.fst (cone (cospan f g)) = weakPullback.fst f g

@[simp]

theorem CategoryTheory.Limits.weakLimit.pullbackConeSnd_cone_cospan {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakLimit (cospan f g)] : PullbackCone.snd (cone (cospan f g)) = weakPullback.snd f g

theorem CategoryTheory.Limits.weakPullback.lift_fst {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift h k w) (fst f g) = h

theorem CategoryTheory.Limits.weakPullback.lift_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryStruct.comp (lift h k w) (CategoryStruct.comp (fst f g) h✝) = CategoryStruct.comp h h✝

theorem CategoryTheory.Limits.weakPullback.lift_snd {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift h k w) (snd f g) = k

theorem CategoryTheory.Limits.weakPullback.lift_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryStruct.comp (lift h k w) (CategoryStruct.comp (snd f g) h✝) = CategoryStruct.comp k h✝

noncomputable def CategoryTheory.Limits.weakPullback.lift' {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : { l : W ⟶ weakPullback f g // CategoryStruct.comp l (fst f g) = h ∧ CategoryStruct.comp l (snd f g) = k }

A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism l : W ⟶ weakPullback f g such that l ≫ weakPullback.fst = h and l ≫ weakPullback.snd = k.

Equations

• CategoryTheory.Limits.weakPullback.lift' h k w = ⟨CategoryTheory.Limits.weakPullback.lift h k w, ⋯⟩

theorem CategoryTheory.Limits.weakPullback.condition {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] : CategoryStruct.comp (fst f g) f = CategoryStruct.comp (snd f g) g

theorem CategoryTheory.Limits.weakPullback.condition_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasWeakPullback f g] {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (fst f g) (CategoryStruct.comp f h) = CategoryStruct.comp (snd f g) (CategoryStruct.comp g h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.map {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [HasWeakPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [HasWeakPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁) (eq₂ : CategoryStruct.comp f₂ i₃ = CategoryStruct.comp i₂ g₂) : weakPullback f₁ f₂ ⟶ weakPullback g₁ g₂

Given such a diagram, then there is a natural morphism from the weak pullback of W ⟶ S and X ⟶ S to the weak pullback of Y ⟶ T and Z ⟶ T.

W ⟶ Y
  ↘   ↘
  S ⟶ T
  ↗   ↗
X ⟶ Z

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.weakPullback.mapDesc {C : Type u_1} [Category.{v_1, u_1} C] {X Y S T : C} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [HasWeakPullback f g] [HasWeakPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] : weakPullback f g ⟶ weakPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)

A morphism from the weak pullback of W ⟶ S and X ⟶ S to the weak pullback of Y ⟶ T and Z ⟶ T given S ⟶ T.

Equations

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

def CategoryTheory.Limits.PullbackCone.isWeakLimitAux {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) (lift : (s : PullbackCone f g) → s.pt ⟶ t.pt) (fac_left : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) t.fst = s.fst) (fac_right : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) t.snd = s.snd) : IsWeakLimit t

This is a slightly more convenient method to verify that a pullback cone is a weak limit cone. It only asks for a proof of facts that carry any mathematical content

Equations

• t.isWeakLimitAux lift fac_left fac_right = { lift := lift, fac := ⋯ }

def CategoryTheory.Limits.PullbackCone.isWeakLimitAux' {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (t : PullbackCone f g) (create : (s : PullbackCone f g) → { l : s.pt ⟶ t.pt // CategoryStruct.comp l t.fst = s.fst ∧ CategoryStruct.comp l t.snd = s.snd }) : IsWeakLimit t

This is another convenient method to verify that a pullback cone is a weak limit cone. It only asks for a proof of facts that carry any mathematical content, and allows access to the same s for all parts.

Equations

• t.isWeakLimitAux' create = t.isWeakLimitAux (fun (s : CategoryTheory.Limits.PullbackCone f g) => ↑(create s)) ⋯ ⋯

def CategoryTheory.Limits.PullbackCone.IsWeakLimit.mk {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} {fst : W ⟶ X} {snd : W ⟶ Y} (eq : CategoryStruct.comp fst f = CategoryStruct.comp snd g) (lift : (s : PullbackCone f g) → s.pt ⟶ W) (fac_left : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : PullbackCone f g), CategoryStruct.comp (lift s) snd = s.snd) : IsWeakLimit (PullbackCone.mk fst snd eq)

This is a more convenient formulation to show that a PullbackCone constructed using PullbackCone.mk is a weak limit cone.

Equations

• CategoryTheory.Limits.PullbackCone.IsWeakLimit.mk eq lift fac_left fac_right = (CategoryTheory.Limits.PullbackCone.mk fst snd eq).isWeakLimitAux lift fac_left fac_right

def CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : W ⟶ t.pt

If t is a weak limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that h ≫ f = k ≫ g, then we get l : W ⟶ t.pt, which satisfies l ≫ fst t = h and l ≫ snd t = k, see IsWeakLimit.lift_fst and IsWeakLimit.lift_snd.

Equations

• CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w = ht.lift (CategoryTheory.Limits.PullbackCone.mk h k w)

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_fst {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift ht h k w) t.fst = h

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryStruct.comp (lift ht h k w) (CategoryStruct.comp t.fst h✝) = CategoryStruct.comp h h✝

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_snd {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : CategoryStruct.comp (lift ht h k w) t.snd = k

@[simp]

theorem CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryStruct.comp (lift ht h k w) (CategoryStruct.comp t.snd h✝) = CategoryStruct.comp k h✝

def CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift' {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) : { l : W ⟶ t.pt // CategoryStruct.comp l t.fst = h ∧ CategoryStruct.comp l t.snd = k }

If t is a weak limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that h ≫ f = k ≫ g, then we have l : W ⟶ t.pt satisfying l ≫ fst t = h and l ≫ snd t = k.

Equations

• CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift' ht h k w = ⟨CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w, ⋯⟩

def CategoryTheory.Limits.PullbackCone.mkSelfIsWeakLimit {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {t : PullbackCone f g} (ht : IsWeakLimit t) : IsWeakLimit (mk t.fst t.snd ⋯)

The pullback cone reconstructed using PullbackCone.mk from a pullback cone that is a weak limit, is also a weak limit.

Equations

• CategoryTheory.Limits.PullbackCone.mkSelfIsWeakLimit ht = ht.ofIsoWeakLimit t.eta

noncomputable def CategoryTheory.Limits.weakPullbackIsWeakPullback {C : Type u_1} [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasWeakPullback f g] : IsWeakLimit (PullbackCone.mk (weakPullback.fst f g) (weakPullback.snd f g) ⋯)

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

Equations

• CategoryTheory.Limits.weakPullbackIsWeakPullback f g = CategoryTheory.Limits.PullbackCone.mkSelfIsWeakLimit (CategoryTheory.Limits.weakPullback.isWeakLimit f g)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasWeakPullbacks (C : Type u_1) [Category.{v_1, u_1} C] : Prop

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

Equations

• CategoryTheory.Limits.HasWeakPullbacks C = CategoryTheory.Limits.HasWeakLimitsOfShape CategoryTheory.Limits.WalkingCospan C

@[instance 100]

instance CategoryTheory.Limits.HasWeakPullbacksOfHasPullbacks (C : Type u_1) [Category.{v_1, u_1} C] [HasPullbacks C] : HasWeakPullbacks C

theorem CategoryTheory.Limits.hasWeakLimit_cospan_of_hasLimit_pair_of_hasWeakLimit_parallelPair (C : Type u_1) [Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (pair X Y)] [HasWeakLimit (parallelPair (CategoryStruct.comp prod.fst f) (CategoryStruct.comp prod.snd g))] : HasWeakLimit (cospan f g)

If the product X ⨯ Y and the weak equalizer of π₁ ≫ f and π₂ ≫ g exist, then the weak pullback of f and g exists: it is given by composing the equalizer with the projections.

theorem CategoryTheory.Limits.hasWeakPullbacks_of_hasBinaryProducts_of_hasWeakEqualizers (C : Type u_1) [Category.{v_1, u_1} C] [HasBinaryProducts C] [HasWeakEqualizers C] : HasWeakPullbacks C

If a category has all binary products and all weak equalizers, then it also has all weak pullbacks. As usual, this is not an instance, since there may be a more direct way to construct weak pullbacks.