English
Given morphisms f: X → Z and g: Y → Z and a family of pullback cones pb indexed by i ∈ Function.Pullback f.f g.f, together with IsLimit(pb i), one constructs a pullback cone in FormalCoproduct by taking the pullback in C for each component and assembling them coherently.
Русский
Задавая morphisms f: X → Z и g: Y → Z и семейство конусов обратного предела pb, индексированное по i ∈ Function.Pullback f.f g.f, вместе с IsLimit(pb i), строим конус обратного предела в FormalCoproduct, взяв обратимый предел в C для каждого компонента и соединив их согласованно.
LaTeX
$$$\\text{pullbackCone}(f,g, pb) : \\mathrm{PullbackCone}\; f\\; g$$$
Lean4
/-- Given two morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`, given pullback in `C` over each component,
construct the pullback in `FormalCategory.{w} C`. -/
def pullbackCone : PullbackCone f g :=
.mk (W := ⟨Function.Pullback f.f g.f, fun i ↦ (pb i).pt⟩) ⟨fun i ↦ i.1.fst, fun i ↦ (pb i).fst⟩
⟨fun i ↦ i.1.snd, fun i ↦ (pb i).snd⟩ (hom_ext (funext fun i ↦ i.2) (fun i ↦ by simp [(pb i).condition]))
