English
Given algebra homomorphisms f: A →_S C and g: B →_R C that commute, there exists a canonical S-algebra homomorphism lift f g hfg: A ⊗_R B →_S C which extends f and g such that lift(a ⊗ b) = f(a) g(b).
Русский
Пусть существуют алгебраические гомоморфизмы f: A →_S C и g: B →_R C, которые коммутируют, тогда существует канонический S-алгебра-гомоморфизм lift f g hfg: A ⊗_R B →_S C, который на простом тензоре удовлетворяет lift(a ⊗ b) = f(a) g(b).
LaTeX
$$$\\exists! \\; \\phi: A \\otimes_R B \\to_S C \\,|\\; \\phi(a \\otimes b) = f(a)g(b) \\text{ for all } a\\in A, b\\in B.$$$
Lean4
/-- The forward direction of the universal property of tensor products of algebras; any algebra
morphism from the tensor product can be factored as the product of two algebra morphisms that
commute.
See `Algebra.TensorProduct.liftEquiv` for the fact that every morphism factors this way. -/
def lift (f : A →ₐ[S] C) (g : B →ₐ[R] C) (hfg : ∀ x y, Commute (f x) (g y)) : (A ⊗[R] B) →ₐ[S] C :=
algHomOfLinearMapTensorProduct
(AlgebraTensorModule.lift <|
letI restr : (C →ₗ[S] C) →ₗ[S] _ :=
{ toFun := (·.restrictScalars R)
map_add' := fun _ _ => LinearMap.ext fun _ => rfl
map_smul' := fun _ _ => LinearMap.ext fun _ => rfl }
LinearMap.flip <| (restr ∘ₗ LinearMap.mul S C ∘ₗ f.toLinearMap).flip ∘ₗ g)
(fun a₁ a₂ b₁ b₂ =>
show f (a₁ * a₂) * g (b₁ * b₂) = f a₁ * g b₁ * (f a₂ * g b₂) by
rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm])
(show f 1 * g 1 = 1 by rw [map_one, map_one, one_mul])
