## Stream: Is there code for X?

### Topic: linear map to matrices, ring_equiv

#### Yakov Pechersky (Mar 01 2021 at 15:28):

Do we have this? Should we?

import linear_algebra.matrix
open matrix set linear_map
variables {R n : Type*} [comm_ring R] [fintype n] [decidable_eq n]

/-- Linear maps (n → R) →ₗ[R] (n → R) are ring-equivalent to matrix n n R. -/
def linear_map.to_matrix'' : ((n → R) →ₗ[R] (n → R)) ≃+* matrix n n R :=
{ to_fun := to_matrix',
inv_fun := to_lin',
left_inv := to_lin'_to_matrix',
right_inv := to_matrix'_to_lin',
map_mul' := to_matrix'_mul,


#### Eric Wieser (Mar 01 2021 at 15:31):

Do we have the R-algebra structure on square matrices sending r to r \smul I? (which would make that an alg_equiv)

#### Yakov Pechersky (Mar 01 2021 at 15:38):

We do have

instance matrix_algebra (n : Type u) (R : Type v)
[decidable_eq n] [fintype n] [comm_semiring R] : algebra R (matrix n n R) :=
{ commutes' := by { intros, simp [matrix.scalar], },
smul_def' := by { intros, simp [matrix.scalar], },
..(matrix.scalar n) }


#### Eric Wieser (Mar 01 2021 at 15:44):

docs#matrix_algebra

#### Eric Wieser (Mar 01 2021 at 15:45):

Do we also have docs#linear_map.algebra?

#### Adam Topaz (Mar 01 2021 at 15:46):

What do you want linear_map.algebra to do?

#### Yakov Pechersky (Mar 01 2021 at 15:47):

So this works:

@[simp] lemma matrix.algebra_map_eq_smul (r : R) : (algebra_map R (matrix n n R)) r = r • 1 := rfl

/-- Linear maps (n → R) →ₗ[R] (n → R) are ring-equivalent to matrix n n R. -/
def linear_map.to_matrix''a : ((n → R) →ₗ[R] (n → R)) ≃ₐ[R] matrix n n R :=
{ to_fun := to_matrix',
inv_fun := to_lin',
left_inv := to_lin'_to_matrix',
right_inv := to_matrix'_to_lin',
map_mul' := to_matrix'_mul,
commutes' := λ _, by {
ext,
simp only [matrix.algebra_map_eq_smul, module.algebra_map_End_apply,
to_matrix'_apply, pi.smul_apply],
congr } }


#### Yakov Pechersky (Mar 01 2021 at 15:48):

Not sure how these should all be named.

#### Eric Wieser (Mar 01 2021 at 15:54):

Ah, it's probably docs#module.endomorphism_algebra or something

#### Yakov Pechersky (Mar 01 2021 at 15:55):

Relatedly, do we have the to_monoid_hom versions of this?

@[simp]
lemma to_ring_hom_comp_symm_to_ring_hom (e : R ≃+* S) :
e.to_ring_hom.comp e.symm.to_ring_hom = ring_hom.id _ :=
by { ext, simp }


Probably not

#### Eric Wieser (Mar 01 2021 at 15:57):

But it might be written in terms of coercions instead of an explicit .to_...

#### Eric Wieser (Mar 01 2021 at 16:04):

If you're going to add that definition, it would be good to have an un-primed version that works for a more general M →ₗ[R] M given a basis

#### Eric Wieser (Mar 01 2021 at 16:09):

As for naming, the unprimed version could I guess be:

• linear_map.to_matrixₐ, matrix.to_linₐ
• linear_map.to_matrix_alg_equiv, matrix.to_lin_alg_equiv
• linear_map.to_square_matrix, matrix.square_to_lin

I think I prefer the long alg_equiv spelling over ₐ, as I don't know what if any precedent there is for the latter.

#### Yakov Pechersky (Mar 01 2021 at 18:52):

How would you do this for the is_basis version, given that there is no semiring (ι →₀ R)?

#### Eric Wieser (Mar 01 2021 at 18:53):

I don't follow, why do you need that semiring?

(deleted)

#### Adam Topaz (Mar 01 2021 at 18:57):

nevermind... forgot to assume comm_semiring.

#### Adam Topaz (Mar 01 2021 at 18:59):

Oh, and it looks like docs#is_basis requires a ring

#### Yakov Pechersky (Mar 01 2021 at 18:59):

I might be not understanding something about the right typeclass setup here, but:

variables [comm_ring R] [add_comm_group M] [semiring M] [algebra R M] [module R M] [fintype ι]
{v : ι → M} (h : is_basis R v)

/-- Canonical algebra equivalence between a module and the linear combinations of basis vectors. -/
def module_alg_equiv_finsupp : M ≃ₐ[R] ι →₀ R := sorry


gives that semiring (ι →₀ R) complaint

#### Adam Topaz (Mar 01 2021 at 19:00):

Oh you don't want M, but rather the endomorphism ring semiring of M.

#### Yakov Pechersky (Mar 01 2021 at 19:01):

I was trying to copy the definition for is_basis.equiv_fun:

/-- A module over R with a finite basis is linearly equivalent to functions from its basis to R.
-/
def is_basis.equiv_fun : M ≃ₗ[R] (ι → R) :=
linear_equiv.trans (module_equiv_finsupp h)
{ to_fun := coe_fn,
map_smul' := finsupp.coe_smul,
..finsupp.equiv_fun_on_fintype }


#### Adam Topaz (Mar 01 2021 at 19:01):

That's a linear equiv, not an algebra equiv

#### Adam Topaz (Mar 01 2021 at 19:02):

The issue is that is_basis needs to be generalized to semirings.

#### Yakov Pechersky (Mar 01 2021 at 19:02):

Yes, so to make it an alg equiv, I was going the lazy route of just substituting alg_equiv for linear_equiv where possible

#### Yakov Pechersky (Mar 01 2021 at 19:02):

Because that's what worked for the linear_map \to matrix alg_equivs

#### Adam Topaz (Mar 01 2021 at 19:02):

But in your code above,, over rings, this is not what you do:

def linear_map.to_matrix''a : ((n → R) →ₗ[R] (n → R)) ≃ₐ[R] matrix n n R :=


#### Eric Wieser (Mar 01 2021 at 19:03):

You're trying to construct this, right?

def linear_map.to_matrixa : (M →ₗ[R] M) ≃ₐ[R] matrix n n R :=


#### Adam Topaz (Mar 01 2021 at 19:03):

Mayube this will clarify things:

import linear_algebra.basis

variables {R M : Type*} [comm_semiring R] [add_comm_monoid M] [semimodule R M]

example : semiring (M →ₗ[R] M) := by apply_instance


#### Yakov Pechersky (Mar 01 2021 at 19:04):

/-- Linear maps (n → R) →ₗ[R] (n → R) are algebra equivalent to matrix n n R. -/
def linear_map.to_matrix_alg_equiv' : ((n → R) →ₗ[R] (n → R)) ≃ₐ[R] matrix n n R :=
{ to_fun := linear_map.to_matrix',
inv_fun := matrix.to_lin',
left_inv := matrix.to_lin'_to_matrix',
right_inv := linear_map.to_matrix'_to_lin',
map_mul' := linear_map.to_matrix'_mul,
commutes' := by simp [module.algebra_map_End_eq_smul_id] }


And you asked for the unprimed versions

#### Eric Wieser (Mar 01 2021 at 19:04):

Yes, I think you can just remove the ' from most of the lemmas you use

#### Eric Wieser (Mar 01 2021 at 19:04):

And possibly have to think about commutes' slightly

#### Yakov Pechersky (Mar 01 2021 at 19:05):

We have that

/-- Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases. -/
def linear_map.to_matrix : (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix m n R :=
linear_equiv.trans (linear_equiv.arrow_congr hv₁.equiv_fun hv₂.equiv_fun) linear_map.to_matrix'


but what fills in the underscore here?

/-- Given a basis of a module M₁ over a commutative ring R, we get an algebra
equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis. -/
def linear_map.to_matrix_alg_equiv : (M₁ →ₗ[R] M₁) ≃ₐ[R] matrix n n R :=
alg_equiv.trans _ linear_map.to_matrix_alg_equiv'


#### Yakov Pechersky (Mar 01 2021 at 19:06):

So going down this route, I wanted to write is_basis.alg_equiv_fun

#### Eric Wieser (Mar 01 2021 at 19:10):

I don't think you want to get there from here

#### Eric Wieser (Mar 01 2021 at 19:24):

The "just remove the primes" approach

def linear_map.to_matrix_alg_equiv {v₁ : n → M₁} (hv : is_basis R v₁) :
(M₁ →ₗ[R] M₁) ≃ₐ[R] matrix n n R :=
{ to_fun := linear_map.to_matrix hv hv,
inv_fun := matrix.to_lin hv hv,
left_inv := matrix.to_lin_to_matrix hv hv,
right_inv := linear_map.to_matrix_to_lin hv hv,
map_mul' := linear_map.to_matrix_mul hv,
commutes' := sorry}


#### Yakov Pechersky (Mar 01 2021 at 19:32):

/-- Given a basis of a module M₁ over a commutative ring R, we get an algebra
equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis. -/
def linear_map.to_matrix_alg_equiv {v₁ : n → M₁} (hv : is_basis R v₁) :
(M₁ →ₗ[R] M₁) ≃ₐ[R] matrix n n R :=
{ to_fun := linear_map.to_matrix hv hv,
inv_fun := matrix.to_lin hv hv,
left_inv := matrix.to_lin_to_matrix hv hv,
right_inv := linear_map.to_matrix_to_lin hv hv,
map_mul' := linear_map.to_matrix_mul hv,
commutes' := by simp [module.algebra_map_End_eq_smul_id, linear_map.to_matrix_id] }


Thanks!

#### Eric Wieser (Mar 01 2021 at 19:33):

variables { R : Type*} [comm_ring R]

variables {M₁ : Type*} [add_comm_group M₁] [semimodule R M₁]
variables {M₂ : Type*} [add_comm_group M₂] [semimodule R M₂]

def linear_equiv.arrow_congr₂ (e : M₁ ≃ₗ[R] M₂) : (M₁ →ₗ[R] M₁) ≃ₐ[R] (M₂ →ₗ[R] M₂) :=
{ map_mul' := λ x y, begin
ext,
simp,
end,
commutes' := λ r, begin
ext, simp
end,
..(linear_equiv.arrow_congr e e) }


#### Eric Wieser (Mar 01 2021 at 19:35):

Which probably belongs right after docs#module.endomorphism_algebra

Last updated: May 19 2021 at 03:22 UTC