English
The algebra equivalence built from a linear equivalence acts by sending a pure tensor a ⊗ b to the image under f of that tensor.
Русский
Алгебраическое эквивалентность, построенная из линейного эквивалента, действует так, что на чистом тензоре a ⊗ b отображение даёт образ f(a ⊗ b).
LaTeX
$$$(\text{algEquivOfLinearEquivTensorProduct } f h_{mul} h_{one})(a\otimes b)=f(a\otimes b)$$$
Lean4
/-- Build an algebra equivalence from a linear equivalence 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 algEquivOfLinearEquivTensorProduct (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 :=
{ algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C) h_mul h_one, f with }
