Zulip Chat Archive

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

No, it's this one: https://github.com/leanprover-community/mathlib/blob/d60d1616958787ccb9842dc943534f90ea0bab64/src/ring_theory/algebra.lean#L192

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: Dec 20 2023 at 11:08 UTC