English
There is a canonical map between two direct limits, built from ih: F_i → F'_i and a compatibility condition; it sends ⟦⟨i,x⟩⟧ to ⟦⟨i, ih i x⟩⟧.
Русский
Существует каноническое отображение между двумя пределами, построенное из ih_i и совместимости; оно отправляет ⟦⟨i,x⟩⟧ в ⟦⟨i, ih_i(x)⟩⟧.
LaTeX
$$$\\mathrm{DirectLimit.map}\\; f_1\\; f_2\\; ih\\; compat : \\mathrm{DirectLimit}(F_1,f_1) \\to \\mathrm{DirectLimit}(F_2,f_2)$$$
Lean4
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition. -/
def map (z : DirectLimit F₁ f₁) : DirectLimit F₂ f₂ :=
z.lift _ (fun i x ↦ ⟦⟨i, ih i x⟩⟧) fun j k h x ↦
Quotient.sound <|
have ⟨i, hji, hki⟩ := exists_ge_ge j k
⟨i, hji, hki, by simp_rw [compat, map_map']⟩
