tensor products of algebras

Stream: maths

[Jalex Stark]

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]

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]

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

[Jalex Stark]

(deleted)

[Kevin Buzzard]

Try changing \ox to \ox[R]?

[Jalex Stark]

ooh thank

[Kevin Buzzard]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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]

  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]

wait, maybe it didn't work

[Kevin Buzzard]

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

[Jalex Stark]

thanks!

[Scott Morrison]

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]

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]

See Note [forgetful inheritance]

[Kevin Buzzard]

It's the metric space nightmare all over again

[Kevin Buzzard]

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]

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

[Scott Morrison]

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]

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]

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]

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