English
Let f:A ≃ₐ[S] C and g:B ≃ₐ[R] D be algebra isomorphisms in their respective towers. Then there exists a natural S-algebra isomorphism A ⊗_R B ≅ C ⊗_R D determined by f and g, obtained by applying f and g to the two tensor factors.
Русский
Пусть f: A ≃ₐ[S] C и g: B ≃ₐ[R] D — алгебраические изоморфизмы в соответствующих тензорных тензорах. Тогда существует канонический S-алгебровый изоморфизм A ⊗_R B ≅ C ⊗_R D, определяемый f и g, получаемый путем применения к каждому тензорному фактору.
LaTeX
$$$A \otimes_R B \cong_S C \otimes_R D$$$
Lean4
/-- Construct an isomorphism between tensor products of an S-algebra with an R-algebra
from S- and R- isomorphisms between the tensor factors.
-/
def congr (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D) : A ⊗[R] B ≃ₐ[S] C ⊗[R] D :=
AlgEquiv.ofAlgHom (map f g) (map f.symm g.symm) (ext' fun b d => by simp) (ext' fun a c => by simp)
