English
Let C be a category. If X × Y exists and the equalizer of π1 ∘ f and π2 ∘ g exists, then the pullback of f and g exists. It is constructed by taking e to be the equalizer of π1 ∘ f and π2 ∘ g, and using e ∘ π1 and e ∘ π2 as the two projections; this pullback cone satisfies the universal property.
Русский
Пусть C — категория. Если существует произведение X × Y и равнозначитель для π1 ∘ f и π2 ∘ g, то существует пуллбэк для f и g. Его строят как равнозначитель e равнозначителя π1 ∘ f и π2 ∘ g, а проекции задаются как e ∘ π1 и e ∘ π2; полученный пуллбэк удовлетворяет универсальному свойству.
LaTeX
$$$$\exists P,\; \pi_1: P \to X,\; \pi_2: P \to Y,\; f \circ \pi_1 = g \circ \pi_2 \;\land\; \forall Q,\; \exists! u: Q \to P,\; \pi_1 \circ u = q_1,\; \pi_2 \circ u = q_2.$$$$
Lean4
/-- If the product `X ⨯ Y` and the equalizer of `π₁ ≫ f` and `π₂ ≫ g` exist, then the
pullback of `f` and `g` exists: It is given by composing the equalizer with the projections. -/
theorem hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [𝒞 : Category.{v} C] {X Y Z : C}
(f : X ⟶ Z) (g : Y ⟶ Z) [HasLimit (pair X Y)] [HasLimit (parallelPair (prod.fst ≫ f) (prod.snd ≫ g))] :
HasLimit (cospan f g) :=
let π₁ : X ⨯ Y ⟶ X := prod.fst
let π₂ : X ⨯ Y ⟶ Y := prod.snd
let e := equalizer.ι (π₁ ≫ f) (π₂ ≫ g)
HasLimit.mk
{ cone :=
PullbackCone.mk (e ≫ π₁) (e ≫ π₂) <|
by
rw [Category.assoc, equalizer.condition]
simp [e]
isLimit :=
PullbackCone.IsLimit.mk _
(fun s =>
equalizer.lift (prod.lift (s.π.app WalkingCospan.left) (s.π.app WalkingCospan.right)) <|
by
rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π]
exact PullbackCone.condition _)
(by simp [π₁, e]) (by simp [π₂, e]) fun s m h₁ h₂ =>
by
ext
· dsimp; simpa using h₁
· simpa using h₂ }
