English
The symmetric version of congr_apply_of holds: applying the inverse equivalence gives back the original representative.
Русский
Симметричная версия congr_apply_of сохраняет обратимость: применение обратной эквивалентности возвращает исходного представителя.
LaTeX
$$$\\text{congr\_symm\_apply\_of}(e,h,i,g) = \\text{of}(i, e_i^{-1} g)$$$
Lean4
theorem map_comp (g₁ : (i : ι) → G i →ₗ[R] G' i) (g₂ : (i : ι) → G' i →ₗ[R] G'' i)
(hg₁ : ∀ i j h, g₁ j ∘ₗ f i j h = f' i j h ∘ₗ g₁ i) (hg₂ : ∀ i j h, g₂ j ∘ₗ f' i j h = f'' i j h ∘ₗ g₂ i) :
(map g₂ hg₂ ∘ₗ map g₁ hg₁ : DirectLimit G f →ₗ[R] DirectLimit G'' f'') =
(map (fun i ↦ g₂ i ∘ₗ g₁ i) fun i j h ↦ by
rw [LinearMap.comp_assoc, hg₁ i, ← LinearMap.comp_assoc, hg₂ i, LinearMap.comp_assoc] :
DirectLimit G f →ₗ[R] DirectLimit G'' f'') :=
by ext; simp
