## Stream: maths

### Topic: is_linear_map

#### Johan Commelin (Nov 22 2018 at 09:09):

Is there a reason why is_linear_map does not extend is_add_group_hom?

#### Johan Commelin (Nov 22 2018 at 09:14):

Here is what I'm trying to do:

import data.finset data.finsupp algebra.group
import algebra.group_power

universes u v w

namespace finsupp
noncomputable theory
local attribute [instance] classical.prop_decidable

variables {X Y : Type u} {M : Type v}

def linear_extension [add_comm_monoid M] (f : X → M → Y →₀ M) (s : X →₀ M) : Y →₀ M :=
s.sum $f namespace linear_extension instance [add_comm_monoid M] {f : X → M → Y →₀ M} (h₁ : ∀ (x : X), f x 0 = 0) (h₂ : ∀ (x : X) (m₁ m₂ : M), f x (m₁ + m₂) = f x m₁ + f x m₂) : is_add_monoid_hom$ linear_extension f :=
{ map_zero := rfl,

instance [add_comm_group M] {f : X → M → Y →₀ M} (h : ∀ (x : X), is_add_group_hom $f x) : is_add_group_hom$ linear_extension f :=

variables {R : Type w} [ring R] [add_comm_group M] [module R M]
include R

instance is_linear_map {f : X → M → Y →₀ M} (h : ∀ (x : X), @is_linear_map _ _ _ _ _ _ _ (finsupp.to_module _ _) $f x) : @is_linear_map _ _ _ _ _ _ (finsupp.to_module _ _) (finsupp.to_module _ _)$ linear_extension f :=
smul := _ }

end linear_extension

end finsupp


#### Johan Commelin (Nov 22 2018 at 09:15):

The error is:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
to_module Y M


#### Johan Commelin (Nov 22 2018 at 09:28):

@Mario Carneiro Somehow the @is_linear_map _ _ _ _ _ _ _ all over the place give me the feeling that I don't quite understand how to use modules.

#### Mario Carneiro (Nov 22 2018 at 09:29):

you shouldn't be using is_linear_map at all

#### Johan Commelin (Nov 22 2018 at 09:31):

So what should I use?

#### Mario Carneiro (Nov 22 2018 at 09:31):

linear_map

#### Johan Commelin (Nov 22 2018 at 09:32):

Ok, is there value in the other two instances? for add monoids/groups?

#### Mario Carneiro (Nov 22 2018 at 09:32):

but I understand that the reason you are getting these errors is because finsupp.to_module is not an instance

#### Mario Carneiro (Nov 22 2018 at 09:32):

you should try declaring it locally

Ok, that helps.

#### Johan Commelin (Nov 22 2018 at 09:36):

But I would like to use linear_extension in a context with and without modules.

#### Johan Commelin (Nov 22 2018 at 09:36):

Am I trying to be too flexible?

#### Mario Carneiro (Nov 22 2018 at 09:39):

no that's fine, you should just declare a wrapper for linear_extension making it into a linear map

#### Johan Commelin (Nov 22 2018 at 09:41):

But that is already there, right. You made is_linear_map.mk'. Or do you mean something else?

#### Mario Carneiro (Nov 22 2018 at 09:43):

I mean linear_extension : linear_map A B

#### Johan Commelin (Nov 22 2018 at 09:47):

But then it is no longer a function that can be a group hom if I'm not working with modules...

#### Mario Carneiro (Nov 22 2018 at 09:51):

you have another function for that; the function parts will be equal (even defeq)

#### Johan Commelin (Nov 22 2018 at 10:14):

@Mario Carneiro Ok, I finally completed the proof. So what is your suggestion? I should have two different names? One for the unbundled, and one for the bundled linear map? Are there naming conventions for this?

#### Kenny Lau (Nov 22 2018 at 15:37):

@Johan Commelin add l (that's a small L) in front of the name for the bundled version

#### Kenny Lau (Nov 22 2018 at 15:37):

so e.g. the map is mul and the linear_map is lmul

Last updated: May 12 2021 at 08:14 UTC