Zulip Chat Archive

Stream: maths

Topic: is_linear_map


view this post on Zulip Johan Commelin (Nov 22 2018 at 09:09):

Is there a reason why is_linear_map does not extend is_add_group_hom?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 22 2018 at 09:29):

you shouldn't be using is_linear_map at all

view this post on Zulip Johan Commelin (Nov 22 2018 at 09:31):

So what should I use?

view this post on Zulip Mario Carneiro (Nov 22 2018 at 09:31):

linear_map

view this post on Zulip Johan Commelin (Nov 22 2018 at 09:32):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 22 2018 at 09:32):

you should try declaring it locally

view this post on Zulip Johan Commelin (Nov 22 2018 at 09:36):

Ok, that helps.

view this post on Zulip Johan Commelin (Nov 22 2018 at 09:36):

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

view this post on Zulip Johan Commelin (Nov 22 2018 at 09:36):

Am I trying to be too flexible?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 22 2018 at 09:43):

I mean linear_extension : linear_map A B

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Nov 22 2018 at 09:51):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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