English
From a linear equivalence f: A ⊗_R B ≃_l[S] C that preserves multiplication on pure tensors, construct 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
/-- Build an algebra equivalence from a linear equivalence out of a triple tensor product,
and evidence of multiplicativity on pure tensors.
-/
def algEquivOfLinearEquivTripleTensorProduct (f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D)
(h_mul :
∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
f ((a₁ * a₂) ⊗ₜ (b₁ * b₂) ⊗ₜ (c₁ * c₂)) = f (a₁ ⊗ₜ b₁ ⊗ₜ c₁) * f (a₂ ⊗ₜ b₂ ⊗ₜ c₂))
(h_one : f (((1 : A) ⊗ₜ[R] (1 : B)) ⊗ₜ[R] (1 : C)) = 1) : A ⊗[R] B ⊗[R] C ≃ₐ[R] D :=
AlgEquiv.ofLinearEquiv f h_one <|
f.map_mul_iff.2 <| by
ext
dsimp
exact h_mul _ _ _ _ _ _
