English
Let R be a commutative semiring and A1, A2, A3, A1', A2', A3' be R-algebras. If e1 : A1 ≃ₐ[R] A1', e2 : A2 ≃ₐ[R] A2', e3 : A3 ≃ₐ[R] A3' are algebra isomorphisms and f : A1 →ₐ[R] A2, g : A2 →ₐ[R] A3 are algebra homomorphisms, then transporting f and g along e1, e2, e3 yields a displayed equality of algebra homomorphisms: arrowCongr e1 e3 (g ∘ f) = (arrowCongr e2 e3 g) ∘ (arrowCongr e1 e2 f).
Русский
Пусть R - коммутативная полупринодина; A1, A2, A3, A1', A2', A3' - R-алгебры. Пусть e1 : A1 ≅ₐ[R] A1', e2 : A2 ≅ₐ[R] A2', e3 : A3 ≅ₐ[R] A3' - алгебраические изоморфизмы, и f : A1 →ₐ[R] A2, g : A2 →ₐ[R] A3 - мороморфизмы. Тогда перенесение f и g вдоль эти изоморфизмов удовлетворяет: arrowCongr e1 e3 (g ∘ f) = (arrowCongr e2 e3 g) ∘ (arrowCongr e1 e2 f).
LaTeX
$$$\\forall {R} {A_1} {A_2} {A_3} {A_1'} {A_2'} {A_3'}[CommSemiring R][Semiring A_1][Semiring A_2][Semiring A_3][Semiring A_1'][Semiring A_2'][Semiring A_3'](e_1 : A_1 ≃_R A_1')(e_2 : A_2 ≃_R A_2')(e_3 : A_3 ≃_R A_3')(f : A_1 →_R A_2)(g : A_2 →_R A_3),\\arrowCongr e_1 e_3 (g \\circ f) = (arrowCongr e_2 e_3 g) \\circ (arrowCongr e_1 e_2 f)$$$
Lean4
theorem arrowCongr_comp (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂') (e₃ : A₃ ≃ₐ[R] A₃') (f : A₁ →ₐ[R] A₂)
(g : A₂ →ₐ[R] A₃) : arrowCongr e₁ e₃ (g.comp f) = (arrowCongr e₂ e₃ g).comp (arrowCongr e₁ e₂ f) :=
by
ext
simp
