Zulip Chat Archive

Stream: new members

Topic: Playing with GL(V)


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

view this post on Zulip Johan Commelin (Mar 15 2019 at 08:58):

I agree that this is unfortunate.

view this post on Zulip Johan Commelin (Mar 15 2019 at 08:59):

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

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

view this post on Zulip Mario Carneiro (Mar 15 2019 at 09:07):

what? this isn't a scalar product at all

view this post on Zulip Mario Carneiro (Mar 15 2019 at 09:08):

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

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

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

view this post on Zulip Robert Spencer (Mar 15 2019 at 09:25):

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

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

view this post on Zulip Kenny Lau (Mar 15 2019 at 11:28):

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

view this post on Zulip Robert Spencer (Mar 15 2019 at 11:58):

Herpdederp, fair enough.

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:01):

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:01):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:02):

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

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

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:05):

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:05):

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:05):

Maybe there's just a missing coercion.

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:14):

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

view this post on Zulip Robert Spencer (Mar 15 2019 at 12:14):

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:14):

There should be some coercion which is not kicking in.

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

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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:18):

Now you're back on track.

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 12:19):

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

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

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

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

view this post on Zulip Mario Carneiro (Mar 15 2019 at 12:29):

it can be added now

view this post on Zulip Mario Carneiro (Mar 15 2019 at 12:29):

this was because of module ring out_param


Last updated: May 14 2021 at 21:11 UTC