English
Given a compatible family of maps ih_i: F_i → C, the precomposition map from the direct limit agrees with the canonical representative: for every i, map₀ f ih = ⟦⟨i, ih(i)⟩⟧.
Русский
Пусть есть совместимый набор отображений ih_i: F_i → C; тогда отображение map₀ через предел совпадает с каноническим представлением: для каждого i выполняется map₀ f ih = ⟦⟨i, ih(i)⟩⟧.
LaTeX
$$$\\forall i,\\; \\mathrm{map_0}(f,ih) = \\llbracket\\langle i, ih(i)\\rangle\\rrbracket$$
Lean4
theorem map₀_def (compat : ∀ i j h, f i j h (ih i) = ih j) (i) : map₀ f ih = ⟦⟨i, ih i⟩⟧ :=
have ⟨j, hcj, hij⟩ := exists_ge_ge (Classical.arbitrary ι) i
Quotient.sound ⟨j, hcj, hij, (compat ..).trans (compat ..).symm⟩
