English
Composition of maps equals the map of the composite maps.
Русский
Сложение отображений эквивалентно отображению, индуцированному композицией.
LaTeX
$$$\\mathrm{map}(g_2) \\circ \\mathrm{map}(g_1) = \\mathrm{map}(g_2 \\circ g_1).$$$
Lean4
theorem map_comp (g₁ : (i : ι) → G i →+* G' i) (g₂ : (i : ι) → G' i →+* G'' i)
(hg₁ : ∀ i j h, (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
(hg₂ : ∀ i j h, (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)) :
((map g₂ hg₂).comp (map g₁ hg₁) : DirectLimit G (fun _ _ h ↦ f _ _ h) →+* DirectLimit G'' fun _ _ h ↦ f'' _ _ h) =
(map (fun i ↦ (g₂ i).comp (g₁ i)) fun i j h ↦ by
rw [RingHom.comp_assoc, hg₁ i, ← RingHom.comp_assoc, hg₂ i, RingHom.comp_assoc] :
DirectLimit G (fun _ _ h ↦ f _ _ h) →+* DirectLimit G'' fun _ _ h ↦ f'' _ _ h) :=
by ext; simp
