English
In a concrete category, the pullback object of f1: X1 → S and f2: X2 → S is canonically identified with the set of compatible pairs in X1 × X2: a pair (x1,x2) is compatible if f1(x1) = f2(x2).
Русский
Для конкретной категории предельный объект pullback f1,f2 идентифицируется с множством совместимых пар в X1 × X2, где совместимость означает f1(x1) = f2(x2).
LaTeX
$$$pullbackEquiv\\; f_1\\; f_2 : ToType( pullback f_1 f_2 ) \\simeq \\{ p : ToType X_1 \\times ToType X_2 \\mid f_1(p_1)=f_2(p_2) \\}$$$
Lean4
/-- In a concrete category `C`, given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`,
the elements in `pullback f₁ f₁` can be identified to compatible tuples of
elements in `X₁` and `X₂`. -/
noncomputable def pullbackEquiv : ToType (pullback f₁ f₂) ≃ { p : ToType X₁ × ToType X₂ // f₁ p.1 = f₂ p.2 } :=
(PreservesPullback.iso (forget C) f₁ f₂ ≪≫
Types.pullbackIsoPullback ⇑(ConcreteCategory.hom f₁) ⇑(ConcreteCategory.hom f₂)).toEquiv
