endomorphism algebra

Stream: new members

[Oliver Nash]

Be gentle, this is my first ever question!

For a module M over a commutative ring R, we have the endomorphism algebra. Looking in Mathlib, I can see the ring structure defined here: https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/basic.lean#L176 and I can see a scalar action defined here: https://github.com/leanprover-community/mathlib/blob/master/src/linear_algebra/basic.lean#L257 but I cannot find anywhere putting it all together and actually asserting the algebra structure. After hacking around a bit, the following seems to give me what I want:

  variables (M : Type v) [add_comm_group M]
  variables (R : Type u) [comm_ring R] [module R M]

  instance endomorphism_algebra : algebra R (M →ₗ[R] M) :=
  begin
    refine algebra.mk _ _ _,
    { exact λ r, r • linear_map.id, },
    { refine is_ring_hom.mk _ _ _; intros; ext; simp [mul_smul, add_smul], },
    repeat { intros, ext, simp, },
  end

Am I missing something or is this truly a small gap that deserves filling?

[Chris Hughes]

Probably it is a small gap that needs filling. There are many more.

[Scott Morrison]

Yes, please, let's have it! Would probably be clearer to directly write a structure rather than begin refine ... end. Then a reader can see which proof goes with which proof obligation.

[Johan Commelin]

It might also make sense to define a wrapper type abbreviation module.End (R) (M) := (M →ₗ[R] M). I guess we will want that at some point. @Scott Morrison Can you estimate whether this should be abbreviation or def?

[Johan Commelin]

@Oliver Nash Welcome by the way! It's always nice to see new contributors in the algebra direction (-;

[Oliver Nash]

Thank you all very much for the helpful replies and for the warm welcome @Johan Commelin ! I'll see if I can put together a PR this afternoon.

[Oliver Nash]

FWIW, I find the Mathlib project hugely exciting, and the energy of the community here amazing.

[Oliver Nash]

Finally found time for this. I just created https://github.com/leanprover-community/mathlib/pull/1618 I am grateful to @Scott Morrison for the tips on style (which I hope I have followed). I also tried to introduce the module.End abbreviation (which I like) suggested by @Johan Commelin but I ran into trouble so I left it out. For reasons I don't yet understand, the instance definition seemed not to be able to find the [comm_ring R] data when I used the abbreviation. (Most likely PEBKAC.)