English
There is a binary lift from two direct limits given compatible ih, which maps ⟦⟨i,x⟩⟧ and ⟦⟨i,y⟧ to the pair ⟨ih i x, ih i y⟩.
Русский
Существует двоечное подъёмное отображение между пределами, переводя пары элементов в пары их ih-образов.
LaTeX
$$$\\mathrm{DirectLimit.lift\\_2}\\; f_1\\; f_2\\; ih\\; compat : \\mathrm{DirectLimit}(F_1,f_1) \\to \\mathrm{DirectLimit}(F_2,f_2)$ with $\\mathrm{lift\\_2}(z,w) = \\mathrm{lift\\_2Aux}(f_1,f_2,ih,compat,z,w)$$$
Lean4
/-- To define a binary function from the direct limit, it suffices to provide one binary function
from each component subject to a compatibility condition. -/
protected noncomputable def lift₂ (z : DirectLimit F₁ f₁) (w : DirectLimit F₂ f₂) : C :=
z.hrecOn₂ w (φ := fun _ _ ↦ C) (lift₂Aux f₁ f₂ ih compat · ·) fun _ _ _ _ ⟨j, hx, hyj, jeq⟩ ⟨k, hyk, hz, keq⟩ ↦
heq_of_eq <| by
have ⟨i, hji, hki⟩ := exists_ge_ge j k
simp_rw [(lift₂Aux ..).2 _ (hx.trans hji) (hyk.trans hki), (lift₂Aux ..).2 _ (hyj.trans hji) (hz.trans hki), ←
map_map' _ hx hji, jeq, ← map_map' _ hz hki, ← keq, map_map']
