## Stream: maths

### Topic: tensor products of algebras

#### Jalex Stark (Jun 19 2020 at 19:10):

I'm playing with #3050 (which is now released) in hopes of getting a slick proof of cayley-hamilton.

import data.matrix.basic
import ring_theory.tensor_product

noncomputable theory
open_locale classical
open_locale tensor_product big_operators
open tensor_product finset

variables {R : Type*} [comm_ring R] {n : Type*} [fintype n] [inhabited n]
variables {A : Type*} [ring A] [algebra R A]

def elem_matrix (i j : n) : matrix n n R :=
λ i' j', if (i = i' ∧ j = j') then 1 else 0

instance : algebra R (matrix n n A) :=
begin
refine algebra.of_semimodule _ _;
{ intros,
ext, dsimp, unfold matrix.mul matrix.dot_product,
simp [smul_sum]},
end

instance : algebra R (A ⊗ matrix n n R) :=
begin
exact algebra.tensor_product.algebra,
end

example : matrix n n A →ₐ[R] A ⊗ matrix n n R :=
begin
refine {to_fun := λ x, ∑ i j : n, (x i j) ⊗ₜ[R] (elem_matrix i j),
map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _},
end


#### Jalex Stark (Jun 19 2020 at 19:10):

my problem right now is that in the last example above, typeclass inference wants to know algebra R (A ⊗ matrix n n R)

#### Jalex Stark (Jun 19 2020 at 19:11):

i think that I told it so pretty explicitly in the previous decl

(deleted)

#### Kevin Buzzard (Jun 19 2020 at 19:14):

Try changing \ox to \ox[R]?

ooh thank

#### Kevin Buzzard (Jun 19 2020 at 19:14):

Lean perhaps can't guess what you're tensoring over.

#### Jalex Stark (Jun 19 2020 at 19:15):

yeah, I expected that I would see metavariables in the goal if that were the case, but I was wrong

#### Jalex Stark (Jun 19 2020 at 19:33):

Dealing with double sums is tricky. I feel like i should be able to do this without conv mode.

import data.matrix.basic
import ring_theory.tensor_product

noncomputable theory
open_locale classical
open_locale tensor_product big_operators
open tensor_product finset

variables {R : Type*} [comm_ring R] {n : Type*} [fintype n] [inhabited n]
variables {A : Type*} [ring A] [algebra R A]

example (f : matrix n n R) :
∀ (x y : matrix n n A),
(∑ (i j : n), (x + y) i j ⊗ₜ[R] f i j) =
(∑ (i j : n), x i j ⊗ₜ[R] f i j) +
∑ (i j : n), y i j ⊗ₜ[R] f i j :=
begin
intros,
conv_rhs { congr, skip, funext, rw ← sum_add_distrib,},
apply sum_congr, {refl}, intro i, norm_num,
apply sum_congr, {refl}, intro j, norm_num,
end


#### Yury G. Kudryashov (Jun 19 2020 at 23:26):

begin
intros,
end


#### Jalex Stark (Jun 19 2020 at 23:48):

my latest problem is that I can't get this algebra_equiv construction to fire

import data.matrix.basic
import ring_theory.tensor_product

noncomputable theory
open_locale classical
open_locale tensor_product big_operators

open tensor_product finset
open algebra.tensor_product
#check algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product

variables {R : Type*} [comm_ring R] {n : Type*} [fintype n] [inhabited n]
variables {A : Type*} [ring A] [algebra R A]
variables {B : Type*} [ring B] [algebra R B]

instance : algebra R (matrix n n A) :=
begin
refine algebra.of_semimodule _ _;
{ intros, ext, dsimp, unfold matrix.mul matrix.dot_product,
simp [smul_sum] }
end

example : A ⊗[R] matrix n n R ≃ₐ[R] matrix n n A :=
begin
apply alg_equiv_of_linear_equiv_tensor_product,
end


#### Jalex Stark (Jun 19 2020 at 23:49):

In the last example, we get

invalid apply tactic, failed to unify
A ⊗ matrix n n R ≃ₐ[R] matrix n n A
with
?m_3 ⊗ ?m_4 ≃ₐ[?m_1] ?m_9


which I think means it can't infer some typeclass relating the arguments

#### Jalex Stark (Jun 19 2020 at 23:50):

I tried using @ and filling in holes but haven't yet figured out what instance is missing (or if the problem has some different nature)

#### Kevin Buzzard (Jun 19 2020 at 23:51):

  refine alg_equiv_of_linear_equiv_tensor_product _ _ _,


works. This might be the apply bug? All I know is that there's a bug in apply, I don't know what it is exactly.

#### Kevin Buzzard (Jun 19 2020 at 23:51):

wait, maybe it didn't work

#### Kevin Buzzard (Jun 19 2020 at 23:52):

hah no it did work, a very small a changed to a very small l

thanks!

#### Scott Morrison (Jun 20 2020 at 09:36):

Cool. I'm glad to see you're working on this @Jalex Stark! I had a go at this route, but I got stuck on the annoying fact that matrix n n A had two non-definitionally equal semimodule structures, from matrix.semimodule and from algebra.to_semimodule. It would be good to work out a clean fix for this.

#### Sebastien Gouezel (Jun 20 2020 at 09:53):

The standard way would be to have inside of algebra a semimodule field, and a Prop saying that the semimodule structure coincides with the one coming from algebra. Together with a constructor that builds the semimodule from the algebra structure if one doesn't care about another semimodule structure.

#### Sebastien Gouezel (Jun 20 2020 at 09:54):

See Note [forgetful inheritance]

#### Kevin Buzzard (Jun 20 2020 at 09:59):

It's the metric space nightmare all over again

#### Kevin Buzzard (Jun 20 2020 at 09:59):

We do a very good job of covering this up, but the moment someone looks at the definition of a metric space in mathlib they're like o_O

#### Kevin Buzzard (Jun 20 2020 at 10:02):

On the other hand it's well explained in the docs

#### Scott Morrison (Jun 20 2020 at 10:04):

Okay. I can have a go at this, unless/until someone (@Yury G. Kudryashov?) chimes in to point out an algebra-specific obstacle. (Or that they're already doing it. :-)

#### Sebastien Gouezel (Jun 20 2020 at 10:33):

Though I feel they should be defeq, there is nothing different in both definitions. Indeed,

example (R : Type v) (n : Type u) [fintype n]
[comm_ring R] [decidable_eq n] :
@matrix.semimodule n n _ _ R R _ _ _ = @algebra.to_semimodule R (matrix n n R) _ _ _ :=
begin
delta matrix.semimodule,
delta algebra.to_semimodule,
delta pi.semimodule,
refl,
end


Is the problem just because we are missing eta (or whatever it's called, I mean, two structures with equal fields are equal)?

#### Kevin Buzzard (Jun 20 2020 at 10:33):

I have had some frustrations working with algebras but I think they're unrelated. Algebras are a pretty weird way of bundling morphisms, because they're a class -- a "canonical map". In category theory you'd just make R-algebras and it would be embedded in the system in a different way.

#### Kevin Buzzard (Jun 20 2020 at 10:38):

Patrick thought very hard about topology as part of the perfectoid project and ended up making substantial changes. Algebras are something which hasn't really been pushed in that way but I hope to start on this over the summer

Last updated: May 09 2021 at 10:11 UTC