Zulip Chat Archive

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_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 (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 Z[G]\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_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 (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.

Mario Carneiro (Mar 15 2019 at 12:29):

it can be added now

Mario Carneiro (Mar 15 2019 at 12:29):

this was because of module ring out_param


Last updated: Dec 20 2023 at 11:08 UTC