module.prod

Stream: Is there code for X?

[Alex Kontorovich]

I see submodule.prod but not module.prod...?

[Adam Topaz]

the type-theoretic product should get a module instance for free

[Yaël Dillies]

docs#prod.module

[Alex Kontorovich]

How do I get this to work? I just want to define a vector space W=V×V' and a map from an endomorphism of V to one on W (which does nothing on V'). Help please? Thanks!

universe v

variables {V V' : Type v} [add_comm_group V] [add_comm_group V'] [module ℂ V] [module ℂ V']
  [finite_dimensional ℂ V] [finite_dimensional ℂ V']

def W := prod V V'

def first_component_injection :
 (module.End ℂ V) → (module.End ℂ W) :=
begin
  sorry
end

[Alex Kontorovich]

It doesn't accept module.End ℂ W...

[Alex Kontorovich]

I was hoping to be able to write def W := V.prod V' but that doesn't work...

[Eric Wieser]

If you make W @[reducible] then it will work

[Eric Wieser]

By using def you're saying "make a new thing called W which by default lean knows nothing about"

[Eric Wieser]

Of course, what you'll find next is that when you write W, lean won't be able to guess what V and V' are

[Eric Wieser]

Forcing you to write @W V V' _ _ _ _ _ _ instead...

[Alex Kontorovich]

Sorry can you explain further? What's the recommended way to define W?

[Alex Kontorovich]

This still gives an error:

@[reducible] def W := prod V V'

def first_component_injection :
 (module.End ℂ V) → (module.End ℂ W) :=
begin
  sorry
end

[Eric Wieser]

If V and V' are really variables and not some specific type, then I don't think you want to define W at all (because at best you'd have to write it W V V', and that's harder to read than V × V')

[Eric Wieser]

So

def first_component_injection :
  module.End ℂ V → module.End ℂ (V × V') :=
begin
  sorry
end

[Alex Kontorovich]

Thanks!

[Eric Wieser]

Your other options is:

def first_component_injection :
  let W := V × V' in (module.End ℂ V → module.End ℂ W) :=
begin
  sorry
end

which reads much more like the mathematics, but probably ends up being annoying later (I think mathlib almost never does this).

[Yakov Pechersky]

notation `W` := V × V'

is a nice way to get shorthand

[Floris van Doorn]

I think you need local notation W := V × V' if you refer to local variables.