Zulip Chat Archive

Stream: Is there code for X?

Topic: linear map to matrices, ring_equiv


view this post on Zulip 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,
  map_add' := linear_equiv.map_add' _}

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

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:44):

docs#matrix_algebra

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:45):

Do we also have docs#linear_map.algebra?

view this post on Zulip Adam Topaz (Mar 01 2021 at 15:46):

What do you want linear_map.algebra to do?

view this post on Zulip 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,
  map_add' := linear_equiv.map_add' _,
  commutes' := λ _, by {
    ext,
    simp only [matrix.algebra_map_eq_smul, module.algebra_map_End_apply,
               to_matrix'_apply, pi.smul_apply],
    congr } }

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 15:48):

Not sure how these should all be named.

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:54):

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

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:56):

Probably not

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:57):

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

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

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

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 18:53):

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

view this post on Zulip Adam Topaz (Mar 01 2021 at 18:56):

(deleted)

view this post on Zulip Adam Topaz (Mar 01 2021 at 18:57):

nevermind... forgot to assume comm_semiring.

view this post on Zulip Adam Topaz (Mar 01 2021 at 18:59):

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

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

view this post on Zulip Adam Topaz (Mar 01 2021 at 19:00):

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

view this post on Zulip 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_add' := finsupp.coe_add,
    map_smul' := finsupp.coe_smul,
    ..finsupp.equiv_fun_on_fintype }

view this post on Zulip Adam Topaz (Mar 01 2021 at 19:01):

That's a linear equiv, not an algebra equiv

view this post on Zulip Adam Topaz (Mar 01 2021 at 19:02):

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

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

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 19:02):

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

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

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

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 19:03):

And you already have docs#linear_map.to_matrix

view this post on Zulip 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,
  map_add' := linear_map.to_matrix'.map_add,
  commutes' := by simp [module.algebra_map_End_eq_smul_id] }

And you asked for the unprimed versions

view this post on Zulip Eric Wieser (Mar 01 2021 at 19:04):

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 19:04):

And possibly have to think about commutes' slightly

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

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 19:06):

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 19:10):

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

view this post on Zulip 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,
  map_add' := (linear_map.to_matrix hv hv).map_add,
  commutes' := sorry}

view this post on Zulip 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,
  map_add' := (linear_map.to_matrix hv hv).map_add,
  commutes' := by simp [module.algebra_map_End_eq_smul_id, linear_map.to_matrix_id] }

view this post on Zulip Yakov Pechersky (Mar 01 2021 at 19:32):

Thanks!

view this post on Zulip Eric Wieser (Mar 01 2021 at 19:33):

But to answer your question, the thing that's missing is:

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) }

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