Tensor maps

Stream: Is there code for X?

[Leo Mayer]

If I have an R-algebra A, is there an easy way to access the multiplication as a map (A ⊗[R] A) →ₐ[R] A? (I'm trying to implement Hopf algebras)?

[Heather Macbeth]

@Leo Mayer I think this is docs#algebra.lmul'

[Leo Mayer]

I think I need it as an R-algebra map, not just as an R-linear map.
Maybe I should build an R-algebra map out of that? If this isn't in mathlib, should it be?

[Heather Macbeth]

I see. Do we even have the notion of the tensor product of algebras?

[Adam Topaz]

It should obtain an algebra instance automatically

[Leo Mayer]

Here's the tensor product of algebras

[Adam Topaz]

import ring_theory.tensor_product

variables (A R : Type*) [comm_ring A] [comm_ring R] [algebra A R]

open_locale tensor_product

example : algebra A (R ⊗[A] R) := infer_instance

example : (R ⊗[A] R) →ₐ[A] R := algebra.tensor_product.lmul' A

[Adam Topaz]

Found using library search

[Adam Topaz]

BTW it looks like @Vasily Ilin might also be working on Hopf algebras.

[Leo Mayer]

Thanks Adam!
Vas and I are working together on it!

[Adam Topaz]

Great! Looking forward to seeing this in mathlib!

[Vasily Ilin]

We are workign on it together

[Leo Mayer]

Is there a way for lean to apply natural isomorphisms automatically as coersions? For example, all of the diagrams defining hopf algebras make use of associativity of tensor product or the fact that the base ring is a tensor identity, and it's quickly making the code cumbersome.

import ring_theory.tensor_product

open_locale tensor_product
open algebra.tensor_product

structure hopf_algebra (K : Type) [field K] (V : Type) [comm_ring V] [algebra K V] :=
(comul : V →ₐ[K] (V ⊗[K] V))
(counit : V →ₐ[K] K)
(coassoc : (tensor_product.assoc K V V V) ∘ (map comul (alg_hom.id K V)) ∘ comul = map (alg_hom.id K V) comul ∘ comul)
(counit_left : (tensor_product.lid K V) ∘ (map counit (alg_hom.id K V)) ∘ comul = (alg_hom.id K V))
(counit_right : (tensor_product.rid K V) ∘ (map (alg_hom.id K V) counit) ∘ comul = (alg_hom.id K V))
(coinv : V →ₐ[K] V)
(coinv_right : (lmul' K) ∘ (map (alg_hom.id K V) coinv) ∘ comul = (algebra.of_id K V) ∘ counit)
(coinv_left : (lmul' K) ∘ (map coinv (alg_hom.id K V)) ∘ comul = (algebra.of_id K V) ∘ counit)

[Scott Morrison]

Sorry. :-) Cleverly chosen simp normal forms, and writing domain specific tactics?

[Scott Morrison]

I'd try to tempt you into defining a hopf algebra internal to any monoidal category. Some things get harder, but you can also use the nice new coherence tactic for assistance dealing with associators.