tensor product of two A-algebras

Stream: Is there code for X?

[Kevin Buzzard]

Do we know that the tensor product of two A-algebras is an A-algebra? All rings are commutative.

example (A : Type) [comm_ring A] (B C : Type) [comm_ring B] [comm_ring C] [algebra A B] [algebra A C] :
comm_ring (B ⊗[A] C) := infer_instance -- fails

[Riccardo Brasca]

Have you imported ring_theory.tensor_product? This should be docs#algebra.tensor_product.tensor_product.algebra

[Kevin Buzzard]

Yes, there it is! Somehow I am surprised that the statement compiles but not the proof: "I must have imported enough because the tensor product worked". Thanks!

[Kevin Buzzard]

Hmm. Now what I can't find is how to get an $A$-algebra map $B\otimes_AC\to D$ from $A$-algebra maps $B\to D$ and $C\to D$. The file you suggested above only seems to give an $A$-module map?

[Kevin Buzzard]

Oh, maybe I just use docs#algebra.tensor_product.alg_hom_of_linear_map_tensor_product ?

[Kevin Buzzard]

oh bingo, docs#algebra.tensor_product.product_map