English
If there is a family of equivalences e_i between G_i and G'_i compatible with f, then mapping via e yields a well-defined map between the direct limits that commutes with the injections.
Русский
Если существует семейство эквивалентностей между G_i и G'_i, совместимо с f, тогда получаем корректное отображение между прямыми пределами, сохраняющее инъекции.
LaTeX
$$$\text{congr}(e,he)$ defines a map $\varinjlim G f \to \varinjlim G' f'$ compatible with injections.$$
Lean4
theorem congr_symm_apply_of (e : (i : ι) → G i ≃+ G' i)
(he : ∀ i j h, (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i)) {i : ι} (g : G' i) :
(congr e he).symm (of G' f' i g) = of G f i ((e i).symm g) := by
simp only [congr, AddMonoidHom.toAddEquiv_symm_apply, map_apply_of, AddMonoidHom.coe_coe]
