## Stream: maths

### Topic: module refactor

#### Sebastien Gouezel (Mar 21 2019 at 18:10):

@Mario Carneiro I have two questions about the module refactor.

• line 111 of module.lean, there is a declaration class is_linear_map. Isn't the rule now that unbundled stuff should not be a class?
• line 364 of normed_space/basic.lean, there is the definition
class normed_space (α : out_param $Type*) (β : Type*) [out_param$ normed_field α]
extends normed_group β, vector_space α β :=


Should the out_param be removed now?

#### Kevin Buzzard (Mar 21 2019 at 18:33):

@Kenny Lau do you have any opinions on this?

#### Kenny Lau (Mar 22 2019 at 00:35):

It happened quite a while ago, I don't remember the reason for the choices I made.

#### Kevin Buzzard (Mar 22 2019 at 01:05):

Should the outparam be removed?

#### Mario Carneiro (Mar 22 2019 at 03:48):

the out_param should be removed

#### Mario Carneiro (Mar 22 2019 at 03:49):

do we have a rule that is_linear_map et al should not be classes? Is this the case for is_group_hom?

#### Kevin Buzzard (Mar 22 2019 at 03:55):

@Kenny Lau what is your opinion?

#### Sebastien Gouezel (Mar 22 2019 at 08:07):

I remember someone (Mario or Kenny?) saying that unbundled stuff should not be classes, but I am probably wrong as is_group_hom is a class currently.

#### Mario Carneiro (Mar 22 2019 at 08:09):

the fact that is_group_hom is a class currently entails some things like having to write simp [is_group_hom.map_add f] in order to work with the rewrite rules, but my recommended solution is actually to just forget about is_group_hom entirely rather than make it not a class

#### Johan Commelin (Mar 22 2019 at 08:10):

How am I supposed to do mathematics and forget about is_group_hom? :grimacing:

#### Mario Carneiro (Mar 22 2019 at 08:11):

use group_hom instead

#### Johan Commelin (Mar 22 2019 at 08:16):

Does that exist in mathlib?

#### Johan Commelin (Mar 22 2019 at 08:16):

Chris raised some issues that weren't resolved as far as I know

#### Sebastien Gouezel (Mar 22 2019 at 08:18):

In the same way, should we avoid is_linear_map and use linear_map instead?

#### Johan Commelin (Mar 22 2019 at 08:20):

That is what I've been doing so far.

#### Johan Commelin (Mar 22 2019 at 08:20):

But when you use f : alg_hom you get a lot of ugly f.to_linear_maps in your code

#### Mario Carneiro (Mar 22 2019 at 08:20):

for linear_map, yes that's the recommendation. For group_hom, it doesn't exist yet but I think chris was working on it

#### Johan Commelin (Mar 22 2019 at 08:20):

I think @Chris Hughes hoped to solve that with unification hints. But so far, no luck

#### Mario Carneiro (Mar 22 2019 at 08:21):

I'm not up to date on the issues with coercions between different augmented-function types

#### Mario Carneiro (Mar 22 2019 at 08:22):

but I would hope that coe would suffice in most cases

#### Mario Carneiro (Mar 22 2019 at 08:23):

I don't think there is a need for unification hints in this area

#### Sebastien Gouezel (Mar 22 2019 at 10:59):

I am currently removing the outparams in normed_space. It breaks some things, especially since bounded_linear_maps did not have the field explicit. Clearly, it should be, so I am adding it everywhere. But then it also shows up in the definition of the derivative -- and here again it seems like a good idea to make the field explicit : for instance, on a complex vector space, we want to be able to talk about the complex differential and the real differential, and discuss their relationships. @Jeremy Avigad , is it all right for you?

#### Kevin Buzzard (Mar 22 2019 at 11:02):

class is_linear_map (α : Type u) {β : Type v} {γ : Type w}
[ring α] [add_comm_group β] [add_comm_group γ] [module α β] [module α γ]
(f : β → γ) : Prop :=
(add  : ∀x y, f (x + y) = f x + f y)
(smul : ∀(c : α) x, f (c • x) = c • f x)

structure linear_map (α : Type u) (β : Type v) (γ : Type w)
[ring α] [add_comm_group β] [add_comm_group γ] [module α β] [module α γ] :=
(to_fun : β → γ)
(add  : ∀x y, to_fun (x + y) = to_fun x + to_fun y)
(smul : ∀(c : α) x, to_fun (c • x) = c • to_fun x)


Johan -- is this the question? You're asking whether you should use a class or a structure?

#### Kevin Buzzard (Mar 22 2019 at 11:04):

The structure has a coercion, so you should just be able to hide all those f.to_funs

#### Kevin Buzzard (Mar 22 2019 at 11:05):

Oh I see, f moves too. You're asking whether you should be bundled or unbundled.

#### Johan Commelin (Mar 22 2019 at 11:07):

I think @Mario Carneiro is saying that we should make that a coercion.

#### Sebastien Gouezel (Mar 22 2019 at 11:23):

the out_param should be removed

Done in #844

#### Jeremy Avigad (Mar 22 2019 at 22:36):

@Sebastien Gouezel I trust your judgment here. Thanks for doing it.

Last updated: May 06 2021 at 18:20 UTC