English
If ih is a compatible family from F_i to F₂ i.e. to the second system, then map₁₂ on ⟦⟨i,x⟩⟧ equals ⟦⟨i, ih i x⟩⟧.
Русский
Если ih совместима и отображает элементы F_i в F₂ i, тогда map₂def ⟦⟨i,x⟩⟧ = ⟦⟨i, ih i x⟩⟧.
LaTeX
$$$\\mathrm{map\\_def}\\;f_1\\;f_2\\;ih\\;compat\\; ⟦⟨i,x⟩⟧ = ⟦⟨i, ih i x⟩⟧$$$
Lean4
/-- To define a function from the direct limit, it suffices to provide one function from each
component subject to a compatibility condition. -/
noncomputable def map₂ : DirectLimit F₁ f₁ → DirectLimit F₂ f₂ → DirectLimit F f :=
DirectLimit.lift₂ f₁ f₂ (fun i x y ↦ ⟦⟨i, ih i x y⟩⟧) fun j k h x y ↦
Quotient.sound <|
have ⟨i, hji, hki⟩ := exists_ge_ge j k
⟨i, hji, hki, by simp_rw [compat, map_map']⟩
