Zulip Chat Archive

Stream: maths

Topic: tensor products of algebras


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Jalex Stark (Jun 19 2020 at 19:11):

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

view this post on Zulip Jalex Stark (Jun 19 2020 at 19:11):

(deleted)

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 19:14):

Try changing \ox to \ox[R]?

view this post on Zulip Jalex Stark (Jun 19 2020 at 19:14):

ooh thank

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 19:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jun 19 2020 at 23:26):

begin
  intros,
  simp only [pi.add_apply, add_tmul, sum_add_distrib],
end

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 23:51):

wait, maybe it didn't work

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 23:52):

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

view this post on Zulip Jalex Stark (Jun 19 2020 at 23:54):

thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Sebastien Gouezel (Jun 20 2020 at 09:54):

See Note [forgetful inheritance]

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 09:59):

It's the metric space nightmare all over again

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 20 2020 at 10:02):

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

view this post on Zulip 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. :-)

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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