linear map to matrices, ring_equiv

Stream: Is there code for X?

[Yakov Pechersky]

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' _}

[Eric Wieser]

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]

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]

docs#matrix_algebra

[Eric Wieser]

Do we also have docs#linear_map.algebra?

[Adam Topaz]

What do you want linear_map.algebra to do?

[Yakov Pechersky]

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

[Yakov Pechersky]

Not sure how these should all be named.

[Eric Wieser]

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

[Yakov Pechersky]

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 }

[Eric Wieser]

Probably not

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Adam Topaz]

(deleted)

[Adam Topaz]

nevermind... forgot to assume comm_semiring.

[Adam Topaz]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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 }

[Adam Topaz]

That's a linear equiv, not an algebra equiv

[Adam Topaz]

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

[Yakov Pechersky]

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]

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

[Adam Topaz]

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]

You're trying to construct this, right?

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

[Adam Topaz]

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

[Eric Wieser]

And you already have docs#linear_map.to_matrix

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

And possibly have to think about commutes' slightly

[Yakov Pechersky]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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}

[Yakov Pechersky]

/-- 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] }

[Yakov Pechersky]

Thanks!

[Eric Wieser]

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

[Eric Wieser]

Which probably belongs right after docs#module.endomorphism_algebra