English
Under the pushout, the canonical isomorphism sends a ⊗ b to the product of their images in the pushout base S'.
Русский
При отображении через свод pushout тензорного произведения, элемент a ⊗ b переходит в произведение его образов в S'.
LaTeX
$$equiv R S R' S' (a ⊗ₜ b) = algebraMap _ _ a * algebraMap _ _ b$$
Lean4
/-- The isomorphism `S' ≃ S ⊗[R] R` given `Algebra.IsPushout R S R' S'`. -/
noncomputable def equiv [h : Algebra.IsPushout R S R' S'] : S ⊗[R] R' ≃ₐ[S] S'
where
__ := h.out.equiv
map_mul' x
y := by
dsimp
induction x with
| zero => simp
| add x y _ _ => simp [*, add_mul]
| tmul a b =>
induction y with
| zero => simp
| add x y _ _ => simp [*, mul_add]
| tmul x y => simp [IsBaseChange.equiv_tmul, Algebra.smul_def, mul_mul_mul_comm]
commutes' := by simp [IsBaseChange.equiv_tmul, Algebra.smul_def]
