mul_action_hom.map_matrix

Stream: maths

[Filippo A. E. Nuccio]

I find in data/matrix/basic.lean the definition def add_monoid_hom.map_matrix showing that a map as additive monoids between coefficients induces an additive map between matrices. I am unable to find the equivalent for multiplicative structures, in particular the fact that if R,S are A-algebras, every A-algebra morphism f:R--->S induces a map of A-modules between the matrices. I am happy to PR all this, but I wonder if it is not already there.

[Eric Wieser]

Can you give the lean statement of what you're describing?

[Eric Wieser]

(docs#add_monoid_hom.map_matrix for reference)

[Filippo A. E. Nuccio]

Yes, one second

[Eric Wieser]

Do we have docs#matrix.map?

[Anne Baanen]

I know there is docs#ring_hom.map_matrix, I don't think there is something like docs#alg_hom.map_matrix?

[Filippo A. E. Nuccio]

variables {β M N: Type*} [comm_ring β] [add_comm_monoid M] [add_comm_monoid N]

def foo [module β M] [module β N] (f : M →[β] N) :
  matrix m n M →[β] matrix m n N :=

[Eric Wieser]

docs#mul_action_hom is extremely underdeveloped, so we almost certainly don't have that

[Filippo A. E. Nuccio]

There is a funny

-- TODO: there should be a way to avoid restating these for each `foo_hom`.

which seems to point in that direction...

[Anne Baanen]

"a map of A-modules" is docs#linear_map, not docs#mul_action_hom, right?

[Filippo A. E. Nuccio]

@Anne Baanen You're right, but I don't know if it is better the way I proposed it, or if it is better to simply assume that M, N have a multiplicative action of $\beta$

[Filippo A. E. Nuccio]

After all, we can create matrices of sets, if we don't require to add them

[Anne Baanen]

In either case I agree with @Eric Wieser that there does not seem to be anything in this direction.

[Anne Baanen]

Filippo A. E. Nuccio said:

Anne Baanen You're right, but I don't know if it is better the way I proposed it, or if it is better to simply assume that M, N have a multiplicative action of $\beta$

Why not add both? :grinning:

[Filippo A. E. Nuccio]

OK, I'll go for a PR!

[Anne Baanen]

Thank you!

[Eric Wieser]

I'd probably lean towards adding this for linear_map and alg_hom, but leaving mul_action_hom missing

[Filippo A. E. Nuccio]

Ok, and why so? I mean, I suspect that you have a stronger reason that saving me 3 lines of code: consistency with other files, useless circular things, etc...?

[Eric Wieser]

I think there's little point developing mul_action_hom as it's basically unused. Ideally we'd generalize as many lemmas as possible away from linear_map down the heirarchy, and then use automation to copy them back up

[Eric Wieser]

But if you actually do need it, then you should add it!

[Filippo A. E. Nuccio]

Here it is: #8061