English
From a linear equivalence f: A ⊗_R B ⊗_R C ≃_l[S] D that preserves multiplication on pure tensors, build an algebra equivalence A ⊗_R B ⊗_R C ≃_a[S] D.
Русский
Из линейного эквивалента f: A ⊗_R B ⊗_R C ≃_l[S] D сохраняющего умножение на чистые тензоры, строится алгебраическое эквивалентность A ⊗_R B ⊗_R C ≃_a[S] D.
LaTeX
$$$\text{algEquivOfLinearEquivTripleTensorProduct}\;f\;h_{mul}\;h_{one}: A\otimes_R B\otimes_R C \simeq_R D$$$
Lean4
/-- Build an algebra morphism from a linear map out of a tensor product, and evidence that on pure
tensors, it preserves multiplication and the identity.
Note that we state `h_one` using `1 ⊗ₜ[R] 1` instead of `1` so that lemmas about `f` applied to pure
tensors can be directly applied by the caller (without needing `TensorProduct.one_def`).
-/
def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C)
(h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂))
(h_one : f (1 ⊗ₜ[R] 1) = 1) : A ⊗[R] B →ₐ[S] C :=
AlgHom.ofLinearMap f h_one (f.map_mul_of_map_mul_tmul h_mul)
