English
From a linear equivalence f: A ⊗_R B ≃_l[S] C that preserves multiplication and unit on pure tensors, one constructs an algebra equivalence A ⊗_R B ≃_a[S] C.
Русский
Из линейного эквивалента f: A ⊗_R B ≃_l[S] C, сохраняющего умножение и единицу на чистых тензорах, строится алгебраическое эквивалентное соответствие A ⊗_R B ≃_a[S] C.
LaTeX
$$$\text{algEquivOfLinearEquivTensorProduct}\;f\;h_{mul}\;h_{one}: A\otimes_R B \simeq_S C$$$
Lean4
/-- To check a linear map preserves multiplication, it suffices to check it on pure tensors. See
`algHomOfLinearMapTensorProduct` for a bundled version. -/
theorem _root_.LinearMap.map_mul_of_map_mul_tmul {f : A ⊗[R] B →ₗ[S] C}
(hf : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) (x y : A ⊗[R] B) :
f (x * y) = f x * f y :=
f.map_mul_iff.2
(by
-- these instances are needed by the statement of `ext`, but not by the current definition.
letI : Algebra R C := RestrictScalars.algebra R S C
letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C
ext
dsimp
exact hf _ _ _ _)
x y
