Playing with GL(V)

Stream: new members

[Robert Spencer]

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_1 : add_comm_group V,
_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]

I agree that this is unfortunate.

[Johan Commelin]

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

[Robert Spencer]

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]

what? this isn't a scalar product at all

[Mario Carneiro]

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

[Mario Carneiro]

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

[Robert Spencer]

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

[Robert Spencer]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Robert Spencer]

Herpdederp, fair enough.

[Robert Spencer]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe there's just a missing coercion.

[Robert Spencer]

Explicit output of that case:

/home/.../basic.lean:18:0: error: failed to synthesize type class instance for
V : Type,
_inst_1 : add_comm_group V,
_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_1 : add_comm_group V,
_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]

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

[Robert Spencer]

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

[Kevin Buzzard]

There should be some coercion which is not kicking in.

[Kevin Buzzard]

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]

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

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

#check f.val -- works

[Kevin Buzzard]

Now you're back on track.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Robert Spencer]

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

[Kevin Buzzard]

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

[Mario Carneiro]

it can be added now

[Mario Carneiro]

this was because of module ring out_param