# Zulip Chat Archive

## 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

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

(deleted)

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

Try changing `\ox`

to `\ox[R]`

?

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

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,
rw ← sum_add_distrib,
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,
rw add_tmul,
end
```

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

```
begin
intros,
simp only [pi.add_apply, add_tmul, sum_add_distrib],
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

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

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