# Zulip Chat Archive

## 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, map_add := λ s₁ s₂, finsupp.sum_add_index h₁ h₂ } 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 := { add := (linear_extension.is_add_monoid_hom (λ x, is_add_group_hom.zero (f x)) (λ x, (h x).add)).map_add } 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 := { add := (linear_extension.is_add_group_hom (λ x, ⟨(h x).add⟩)).add, -- gives stupid error 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

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

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