English
Given a linear map f: A ⊗_R B → C that is multiplicative on pure tensors and sends 1 ⊗ 1 to 1, one gets an algebra homomorphism f̂: A ⊗_R B →_S C extending f.
Русский
Пусть имеется линейное отображение f: A ⊗_R B → C, сохраняющее умножение на чистые тензоры и переводящее 1 ⊗ 1 в 1; тогда получается алгебра-гомоморфизм f̂: A ⊗_R B →_S C, являющийся продолжением f.
LaTeX
$$$\exists\;\hat f: A\otimes_R B \to_S C \text{ } \hat f\text{ линейно и алгебро-мормоморфен и}\; \hat f = f\text{ на чистых тензорах}$$$
Lean4
instance instCommSemiring : CommSemiring (A ⊗[R] B)
where
toSemiring := inferInstance
mul_comm x
y := by
refine TensorProduct.induction_on x ?_ ?_ ?_
· simp
· intro a₁ b₁
refine TensorProduct.induction_on y ?_ ?_ ?_
· simp
· intro a₂ b₂
simp [mul_comm]
· intro a₂ b₂ ha hb
simp [mul_add, add_mul, ha, hb]
· intro x₁ x₂ h₁ h₂
simp [mul_add, add_mul, h₁, h₂]
