## Stream: new members

### Topic: Playing with GL(V)

#### Robert Spencer (Mar 15 2019 at 08:54):

I am fiddling around with the following code.

import algebra.module
import data.complex.basic
import linear_algebra.basic

-- Throughout let  V be a vector space.
variables (V : Type) [add_comm_group V] [vector_space ℂ V]

notation GL( a ) := linear_map.general_linear_group ℂ a

#check GL(V)

variable f : GL(V)
variable v : V

#check f v


I would expect this to tell me that f v has type V. However, it complains that f is of type units (V →ₗ[ℂ] V) and not a function. Fair enough, I suppose. So I turn to the slightly more ugly f.val v. This too gives an error:

/home/.../basic.lean:17:8: error: failed to synthesize type class instance for
V : Type,
_inst_2 : vector_space ℂ V,
f : GL(V),
v : V
⊢ monoid (V →ₗ[ℂ] V)
/home/.../basic.lean:17:8: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
ring.to_monoid (V →ₗ[ℂ] V)


I will admit I am now a little stumped. What exactly is it asking me to prove here? Is it asking for a proof that (V →ₗ[ℂ] V) is a ring? Is it asking for a proof that rings are monoids?

And on an aesthetic note, is there any way to remove the .val? Saying "let f be a member of the general linear group. Then f.val of v is a vector" feels clumsy.

#### Johan Commelin (Mar 15 2019 at 08:58):

I agree that this is unfortunate.

#### Johan Commelin (Mar 15 2019 at 08:59):

However, would it make sense to introduce a scalar multiplication? f • v?

#### Robert Spencer (Mar 15 2019 at 09:05):

Ah, yes. That's better looking. Something along the lines of

infix •:50 := fun {c : Type} (a : GL(c)) (b : c), a.val b


(I know I'm probably butchering best practices/naming conventions, but humour me).

Ok, I am satisfied for the aesthetic. Still got the ring.to_monoid problem.

#### Mario Carneiro (Mar 15 2019 at 09:07):

what? this isn't a scalar product at all

#### Mario Carneiro (Mar 15 2019 at 09:08):

and vector spaces already have a notion of scalar product that conflicts with this

#### Mario Carneiro (Mar 15 2019 at 09:11):

eh, lean is on the fritz, can't test. Does #check (f.val : V-> V) x work?

#### Robert Spencer (Mar 15 2019 at 09:25):

Well since field elements inject into GL(V) it more extends rather than conflicts, doen't it?

#### Robert Spencer (Mar 15 2019 at 09:25):

Unfortunately (f.val : V -> V) v falls over in the same way

#### Mario Carneiro (Mar 15 2019 at 11:28):

I mean that's not how scalar products work: V is not a vector space over GL(V)

#### Kenny Lau (Mar 15 2019 at 11:28):

it isn't scalar product, it's group action

#### Robert Spencer (Mar 15 2019 at 11:58):

Herpdederp, fair enough.

#### Robert Spencer (Mar 15 2019 at 12:00):

Well at the moment is an error. Thinking about it, is it because Lean doesn't know which monoidal structure to use for the ring?

#### Kevin Buzzard (Mar 15 2019 at 12:01):

I think we have group actions in Lean. Make it a group action?

#### Kevin Buzzard (Mar 15 2019 at 12:01):

It's a G-module; a group acting on an abelian group.

#### Kevin Buzzard (Mar 15 2019 at 12:01):

I have a student working on this, they're doing group cohomology, and this is the first definition.

#### Kevin Buzzard (Mar 15 2019 at 12:02):

One way of setting it up is to make V a module for the group $\mathbb{Z}[G]$, because the group ring is already in Lean.

#### Kevin Buzzard (Mar 15 2019 at 12:02):

This might look daunting but it might also be the right way to do it.

#### Kevin Buzzard (Mar 15 2019 at 12:03):

Maybe Chris did groups acting on sets, but groups acting on abelian groups by abelian group automorphisms (which is what we have here) is a richer theory.

#### Robert Spencer (Mar 15 2019 at 12:04):

Wait. So the endomorphism ring of a v. space, which is defined in terms of maps from the space to itself needs to have its action on the space explicitly defined? It can't be deduced/inherited from the fact that the elements of the ring are exactly functions from the space to itself?

#### Kevin Buzzard (Mar 15 2019 at 12:05):

Hard to believe isn't it -- there should be a better way in this case.

#### Kevin Buzzard (Mar 15 2019 at 12:05):

Did you try Mario's g.val : V -> V thing? What's the error?

#### Kevin Buzzard (Mar 15 2019 at 12:05):

Maybe there's just a missing coercion.

#### Robert Spencer (Mar 15 2019 at 12:09):

Explicit output of that case:

/home/.../basic.lean:18:0: error: failed to synthesize type class instance for
V : Type,
_inst_2 : vector_space ℂ V,
f : GL(V),
v : V
⊢ monoid (V →ₗ[ℂ] V)
/home/.../basic.lean:18:0: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
ring.to_monoid (V →ₗ[ℂ] V)
/home/.../basic.lean:18:0: error: failed to synthesize type class instance for
V : Type,
_inst_2 : vector_space ℂ V,
f : GL(V),
v : V
⊢ monoid (V →ₗ[ℂ] V)
/home/.../basic.lean:18:0: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
ring.to_monoid (V →ₗ[ℂ] V)


#### Kevin Buzzard (Mar 15 2019 at 12:14):

@Kenny Lau what is going on here? Something is wrong.

#### Robert Spencer (Mar 15 2019 at 12:14):

Hell, #check f.val throws the same error.

#### Kevin Buzzard (Mar 15 2019 at 12:14):

There should be some coercion which is not kicking in.

#### Kevin Buzzard (Mar 15 2019 at 12:16):

Aah here we are:

-- declaring this an instance breaks real.lean with reaching max. instance resolution depth
def endomorphism_ring : ring (β →ₗ[α] β) :=


There's a missing instance which should be there but it broke something else so it wasn't added.

#### Kevin Buzzard (Mar 15 2019 at 12:18):

noncomputable instance : ring (V →ₗ[ℂ] V) := linear_map.endomorphism_ring _ _

noncomputable instance : monoid (V →ₗ[ℂ] V) := by apply_instance

#check f.val -- works


#### Kevin Buzzard (Mar 15 2019 at 12:18):

Now you're back on track.

#### Kevin Buzzard (Mar 15 2019 at 12:19):

https://github.com/leanprover-community/mathlib/blob/2bf44d312d5f5f358ce8d9e682c23238e2e86429/src/linear_algebra/basic.lean#L123

#### Kevin Buzzard (Mar 15 2019 at 12:19):

That's what you ran into. It should be an instance but it broke something so it wasn't made an instance.

#### Robert Spencer (Mar 15 2019 at 12:20):

Ahhh. Many thanks. Turns out lean will infer the monoid structure automatically, so its a one-line-fix.

#### Kevin Buzzard (Mar 15 2019 at 12:20):

So we need to add it explicitly. In the long term someone should figure out how to add the instance, I guess.