Zulip Chat Archive

Stream: general

Topic: new definition of linear_map

Kenny Lau (May 30 2020 at 13:21):

In #2866 I am categorifying mul_action (monoid acting on set) and distrib_mul_action (monoid acting on add_monoid) and mul_semiring_action (monoid acting on semiring)

Kenny Lau (May 30 2020 at 13:22):

and the homs are denoted X →[M] Y and A →+[M] B and R →+*[M] S respectively

Kenny Lau (May 30 2020 at 13:22):

and then I realized that A →+[M] B is exactly a linear_map

Kenny Lau (May 30 2020 at 13:23):

so in the future should we redefine linear_map to be distrib_mul_action_hom?

Kenny Lau (May 30 2020 at 13:24):

:thumbs_up: if you agree and :thumbs_down: if you disagree (you can vote both or neither)

Johan Commelin (May 30 2020 at 13:29):

Oof... that sounds like a major refactor...

Patrick Massot (May 30 2020 at 13:30):

I think that answering this question is impossible without seeing whether everything would become painful.

Kenny Lau (May 30 2020 at 13:31):

the API will be the same

Kenny Lau (May 30 2020 at 13:31):

like how module is to be an abbreviation of semimodule

Sebastien Gouezel (May 30 2020 at 13:38):

We should probably first merge #2848, which is a step in this direction as it already changes the definition of linear map from a linear map between modules on a ring to linear map between semimodules on a semiring. Then you can see how much breaks if you change the definition of linear maps to your definition (my guess would be: not too much, and at completely unexpected places).

Chris Hughes (May 30 2020 at 13:49):

I'm happy to just call a distrib_mul_action_hom a linear_map.

Kenny Lau (May 30 2020 at 13:52):

in the future PR?

Eric Wieser (Nov 03 2020 at 15:45):

Some of the pain here would be that every definition of linear_map now need to provide a map_zero, right? Or can auto_param be used somehow?

Yury G. Kudryashov (Nov 03 2020 at 19:20):

  1. Quite often map_zero' is a rfl or by simp.
  2. We can define linear_map.mk' or linear_map.of_core.
  3. Probably we can useauto_param but I don't know how to pass map_smul' to the tactic.

Yury G. Kudryashov (Nov 03 2020 at 19:21):

(Item 3 means that I know too little about Lean meta-programming, not that it's a hard thing to do)

Eric Wieser (Nov 03 2020 at 19:22):

I'm thinking an autoparam of by simp would likely be enough. The issue is that the field is inherited, so I don't know how to use auto_param on it

Yury G. Kudryashov (Nov 03 2020 at 19:24):

Should we use . tidy or . simp in more structures outside of category_theory?

Eric Wieser (Nov 03 2020 at 19:41):

Even if we should, how do we replace T with auto_param T in a base structure?

Last updated: May 02 2025 at 03:31 UTC