Basic type question when trying to do complex reps

Stream: new members

[Ryan Smith]

I'm trying to prove some basic results about finite dimensional complex representations of finite groups, hopefully with an eye to contributing this stuff to mathlib eventually since we need a bunch of facts which are not there to do more interesting things. FDRep k G is a type which depends on a field k and a group G. Because these results are specific to complex representations I'm taking k to be \C.

import Mathlib

open Group ComplexConjugate

universe u

variable {G : Type u} [Group G] [Finite G]

theorem comp_char_inv_conj (V : FDRep ℂ G) (g : G) : V.character g⁻¹ = conj V.character g := by
  sorry

This has a type error objection at G

Application type mismatch: In the application
  @FDRep ℂ G
the argument
  G
has type
  Type u : Type (u + 1)
but is expected to have type
  Type : Type 1Lean 4
G : Type u

I suspect this is something fairly basic about how lean handles types that's showing a misunderstanding on my part. Why is not not legitimate and / or how would I modify what I wrote to make sense?

[Aaron Liu]

The issue is that docs#FDRep is universe monomorphic

[Ryan Smith]

What does that mean? That the group and ring must be of the same level? Can we bump the level of one of them to match?

[Aaron Liu]

You can use ULift

[Aaron Liu]

but the correct thing to do here would be to fix FDRep

[Kenny Lau]

correct is a strong word, i think bundled things should be monomorphic and unbundled things should be polymorphic

[Aaron Liu]

Lots of bundled things are already polymorphic

[Aaron Liu]

Like docs#ModuleCat

[Aaron Liu]

and docs#Action

[Ryan Smith]

Is this a question of how things are organized in packages? This is over my head :). I don't mind if people want to refactor later, I'm just trying to figure out how to appease the type system to create complex representations

[Matt Diamond]

if you change it to {G : Type} it works

[Matt Diamond]

it's because it has to match the same type universe as ℂ, which is Type

[Aaron Liu]

I guess since it's finite you can always shrink it

[Matt Diamond]

why would that be necessary? this seems like a very simple problem with a very simple solution: use {G : Type} instead of {G : Type u}

[Aaron Liu]

I meant if you want to use this for a Type u

[Matt Diamond]

I suspect @Ryan Smith just wants his code to work and wrote Type u because that's often good practice... but yes, if he needs universe polymorphism then he'll have to do some extra work

[Aaron Liu]

Kenny Lau said:

correct is a strong word, i think bundled things should be monomorphic and unbundled things should be polymorphic

Can I ask why?

[Kenny Lau]

Aaron Liu said:

Can I ask why?

I think sometimes Lean has trouble with solving max u v stuff

[Aaron Liu]

but all your universes are coming from the types

[Aaron Liu]

you don't need to solve any max u v stuff

[Aaron Liu]

docs#MvPolynomial is polymorphic without causing any problems

[Aaron Liu]

so is docs#ModuleCat

[Ryan Smith]

This is enough to start fighting with lean over theorem specific issues :)

How do you check for existing results in a library? Surely we must have a result for the trace of the power of a matrix but I'm just finding it for matrices over finite fields and Z/pZ. As an inexperienced user a find 70% of the time is just hunting for stuff already buried somewhere in mathlib that I can't find. So far I just use moogle.ai and guess at keywords?

[Aaron Liu]

Ryan Smith said:

Surely we must have a result for the trace of the power of a matrix but I'm just finding it for matrices over finite fields and Z/pZ.

Which result are you looking for?

[Ryan Smith]

Something which when I thought it over was not true in the general case and needed extra hypotheses :)

[Kenny Lau]

Ryan Smith said:

How do you check for existing results in a library?

if you're starting out, leanexplore and leansearch allow you to search using natural language (i.e. english),

and if you have more experience, you would want to gradually shift to loogle, which requires you to know about the names of the moving parts, or parts of the name of the theorem

[Kenny Lau]

Ryan Smith said:

the trace of the power of a matrix

so for example here i see "trace" and "power", and in lean they are Matrix.trace (I guessed this one with experience, Lean names are by design very predictable) and _ ^ _, so I typed those to Loogle: Matrix.trace, _ ^ _

[Kenny Lau]

and indeed we only have the charp result

[Ryan Smith]

Ok, a concrete example of trying to find stuff in mathlib: tr A = sum eigenvalues A for complex matrix A. Lots of searches involving "eigenvalue", "trace", "algebraically closed" etc. I suppose in an ideal world it would be the trace of a linear map rather than picking a basis but this has to be somewhere right?

[Chase Norman]

Using leansearch I got Matrix.trace_eq_sum_roots_charpoly, but I’m not sure if that’s what you want

[Ryan Smith]

Searching for module endomorphism eigenvalues produces a wealth of useful stuff, thanks for the other search links.

One tangible question though, it seems that Module.End.Eigenvalues is a type and not something concrete like a list of eigenvalues. If I need to prove something about all eigenvalues of a particular endomorphism what is the hypothesis which says "let z \in \C be an eigenvalue of ___" ?

[Kenny Lau]

Ryan Smith said:

tr A = sum eigenvalues A for complex matrix

Please PR!

[Kenny Lau]

Ryan Smith said:

what is the hypothesis which says

it's best to answer this question by looking at real life theorems using it

[Kenny Lau]

which, I would agree, is not a lot

[Ryan Smith]

Wasn't trying to be vague, just trying to avoid clutter.

To be specific, I have V : FDRep ℂ G and from that we're accessing the representation V.ρ : G →* ↑V.V →ₗ[ℂ] ↑V.V (not sure why there is a type coercion since I don't think it needs one?). G is a finite group, and I need to prove multiple lemmas about each of the eigenvalues of V.ρ g in order to prove results about the character of V. For a warm up we are showing an arbitrary eigenvector has norm 1. Easy math, but have to explain what we mean to lean. The plan is to say z is an eigenvalue, get the existence of a vector, then use an existing theorem in mathlib about the eigenvalues of a kth power.

Where I'm failing is to write our hypothesis h here:

lemma tmp (V : FDRep ℂ G) (g : G) (z : ℂ) (h : (V.ρ g).HasEigenvalue z) : ‖z‖ = 1 := by sorry

This doesn't work because

Invalid field `HasEigenvalue`: The environment does not contain `LinearMap.HasEigenvalue`
  V.ρ g
has type
  ↑V.V →ₗ[ℂ] ↑V.V

I'm surprised this fails because something like this from math in lean works:

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ φ.eigenspace a ≠ ⊥ :=
  Iff.rfl

And End K V is just an abbreviation for K linear maps V -> V

[Matt Diamond]

here's one approach:

lemma tmp (V : FDRep ℂ G) (g : G) (z : ℂ) (h : (show Module.End _ _ from V.ρ g).HasEigenvalue z) : ‖z‖ = 1 := by sorry

this uses the show _ from _ pattern to cast the LinearMap to a Module.End

[Ryan Smith]

You can do that in a declaration? Interesting

[Aaron Liu]

It gives you an ugly have this := V.ρ g; this

[Ryan Smith]

No doubt its ugly, is there a better way? Working with that hypothesis is going to be a bit challenging . Normal programming languages seem like that would be ok with (V.ρ g).HasEigenvalue but I guess thats invalid syntax here

[Matt Diamond]

it's invalid because V.ρ g has the wrong type... HasEigenvalue requires a value of type Module.End

[Matt Diamond]

(also I wouldn't be surprised if there's a better way... I was just throwing out one possible solution)

[Aaron Liu]

You could write out Module.End.HasEigenvalue (V.ρ g) z

[Matt Diamond]

oh yeah that's a much better idea lol

[Matt Diamond]

sorry I led you astray, @Ryan Smith ... looks like the issue was just that using dot notation requires a strict type match

[Ryan Smith]

So does an abbreviation create a new type?

abbrev Module.End (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] :=
  M →ₗ[R] M

Thank you both for help with this

[Matt Diamond]

there's some good information on what abbrev does in this part of the manual:

https://lean-lang.org/doc/reference/latest/Definitions/Definitions/

[Matt Diamond]

you're defining a new type (in the sense that it's a new constant), though it's definitionally equal to the old one

[Matt Diamond]

also here's the section on generalized field notation:

http://lean-lang.org/doc/reference/latest/Terms/Function-Application/#generalized-field-notation

[Matt Diamond]

you can see that it looks up the function based on the name of the type... it can unfold the type if it doesn't find anything, but the problem here is that LinearMap doesn't unfold to Module.End, but rather the reverse, so unfolding can't help here

[Ryan Smith]

Kenny Lau: PR ?

[Matt Diamond]

FYI you can tag Kenny Lau using the @ symbol (or you can tag without notifying with @_, which I just did)

[Kenny Lau]

Ryan Smith said:

Kenny Lau: PR ?

it's the process of getting stuff into mathlib, see https://leanprover-community.github.io/contribute/index.html for more details