Reflection Group In A Vector Space

Stream: new members

[Jeffrey Li]

Hi, I am new to Lean, and I am trying to implement a reflection group generated by root vectors in a vector space V. In my vector space V, I would like to create a basis, for example \alpha_1 -> \alpha_n, and for each vector in the basis define the reflection operators {s_1 -> s_n}

[Jeffrey Li]

In the docs it says that to create a basis All definitions are given for families of vectors, i.e. v : ι → M where M is the module or vector space and ι : Type* is an arbitrary indexing type.. How do I create the arbitrary indexing type? Thank you

[Kyle Miller]

It can be anything you want that has the right cardinality. For n things indexed 0, 1, ..., n-1, one option is fin n.

[Heather Macbeth]

@Jeffrey Li Have you seen the existing results on reflections? For example, docs#linear_isometry_equiv.reflections_generate stating that the orthogonal group is generated by reflections.

[Jeffrey Li]

Thank you, I hadn't looked at that yet. I wanted to work on simple roots of reflection groups so that topic is closely related. The proof for that result is a bit over my head currently so to begin with I'm just trying to implement a few basic results by myself.

[Jeffrey Li]

Hi, how come addition isn't defined in the following code? The inner product definitions are taken from docs#linear_isometry_equiv.reflections_generate

variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
local notation `absR` := has_abs.abs

def double (x : E) : E := (x + x)

[Jeffrey Li]

It says

failed to synthesize type class instance for
E : Type u_2,
x : E
⊢ has_add E

Thanks

[Kevin Buzzard]

Can you post a #mwe ? The code you posted doesn't compile. Include all imports etc.

[Kevin Buzzard]

The error you posted makes perfect sense -- the only thing Lean knows about E according to your local context is that it's a type, so sure you can't add two elements of it. On the other hand inner_product_space 𝕜 E wouldn't work if Lean only knew that E was a type, so you're not telling the truth in some sense. Edit: I take that back!

[Jeffrey Li]

Oh sorry, I missed a line

import tactic
import linear_algebra.finite_dimensional
import analysis.convex.basic
import analysis.inner_product_space.basic
import analysis.normed_space.is_R_or_C

open vector_space
open finite_dimensional
open finite_dimensional.basis

variables {𝕜 E F : Type*} [is_R_or_C 𝕜]
variables [inner_product_space 𝕜 E] [inner_product_space ℝ F]
local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
local notation `absR` := has_abs.abs
def double (x : E) : E := (x + x)

[Kevin Buzzard]

Oh I can guess what's going on -- Lean is not using inner_product_space 𝕜 E in your definition of double because you're not doing anything which indicates that E is supposed to be an inner product space in that lemma. You could put [inner_product_space 𝕜 E] as an assumption in double

[Jeffrey Li]

oh ok thank you i see, I assumed that already defining it as an inner product space would imply that addition was defined

[Jeffrey Li]

What does the line variables [inner_product_space 𝕜 E] [inner_product_space ℝ F] do then if it doesn't define E to be an inner product space over k? Thank you

[Kevin Buzzard]

So the way variables work is that Lean will only throw them in if it needs to. This works:

def double [inner_product_space 𝕜 E] (x : E) : E := (x + x)

The point is that even though [inner_product_space 𝕜 E] is a variable, Lean doesn't know to use it because you don't give it enough clues.

[Jeffrey Li]

Oh i see, thanks for the help!

[Kevin Buzzard]

It's actually a bit subtle. I think what's going on is that you never mentioned 𝕜. You're right that usually something like this should work

[Jeffrey Li]

What would I need to change for 2 * v to work as well?

[Kevin Buzzard]

def double (a : 𝕜) (x : E) : E := (x + x)

works. Lean somehow isn't smart enough to guess that it needs to use the variable.

[Frédéric Dupuis]

I'm pretty sure just adding include 𝕜 above double will do the trick.

[Kevin Buzzard]

That's probably a good way to get around this, yes.

[Jeffrey Li]

Is there a way to tell lean that 2 is in is_R_or_C so that I can multiply by a number? thanks

[Kevin Buzzard]

(2 : \bbk) is the 2 in \bbk

[Kevin Buzzard]

include 𝕜
variable (𝕜)
def double (x : E) : E := (x + x)

example (x : E) : double 𝕜 x = (2 : 𝕜) • x :=
begin
  sorry
end

I think you have to make \bbk explicit, or double won't be able to guess what to choose.

[Jeffrey Li]

Oh ok thanks so much this was kind of driving me nuts

[Kevin Buzzard]

It knows that E is a k-module but it is open to the possibility that E can also be a module over lots of other fields. In commutative algebra we always have to say which rings we're modules over.

[Kevin Buzzard]

Yeah I posted it because I tried to do what you were doing and noticed that there were several subleties! The \smul is another one, * won't work because * always takes two elements of the same type.

[Kevin Buzzard]

Sorry for accusing you of not telling the full story earlier -- the variable line wasn't working for a more subtle reason than I had realised.

[Kevin Buzzard]

example (x : E) : double 𝕜 x = (2 : 𝕜) • x :=
begin
  rw two_smul,
  refl,
end

[Kevin Buzzard]

Fortunately someone else got there first with two_smul

[Jeffrey Li]

Yeah no problem, I think I forgot to paste the full code anyhow. Thanks for your help!

[Jeffrey Li]

Hi, why doesn't the following code work

variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
local notation `absR` := has_abs.abs

variables (v : E) (w : E)

def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

example: s v w = s w v := sorry

[Jeffrey Li]

It says

don't know how to synthesize placeholder
context:
E : Type u_2,
v w : E
⊢ Type ?

[Yaël Dillies]

#MWE :smile:

[Eric Wieser]

How is lean supposed to work out the 𝕜?

[Jeffrey Li]

import tactic
import linear_algebra.finite_dimensional
import analysis.convex.basic
import analysis.inner_product_space.basic
import analysis.normed_space.is_R_or_C

open vector_space
open finite_dimensional
open finite_dimensional.basis


variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
local notation `absR` := has_abs.abs

variables (v : E) (w : E)

def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

example: s v w = s w v := sorry

[Kevin Buzzard]

Lean can't guess \bbk unless you make it explicit (my variable (\bbk) line in earlier code did this)

[Eric Wieser]

variables (𝕜)
def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

example: s 𝕜 v w = s 𝕜 w v := sorry

[Jeffrey Li]

Eric Wieser said:

How is lean supposed to work out the 𝕜?

Sorry I'm not sure what you mean. How would I tell it about \bbk? I tried doing include \bbk but it didn't work

[Jeffrey Li]

oh ok thank you. What does variables (\bbk) do? Didn't I already declare it at the top? Thanks

[Kevin Buzzard]

It changes the bracket

[Yaël Dillies]

It updates the brackets.

[Kevin Buzzard]

E is a \bbk-module but it's also an \int-module and for all Lean knows it could be a module for 37 other rings. Lean can't guess the ring from E.

[Jeffrey Li]

Eric Wieser said:

variables (𝕜)
def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

example: s 𝕜 v w = s 𝕜 w v := sorry

sorry now I have this new error

type mismatch at application
  s 𝕜 w
term
  w
has type
  E : Type u_2
but is expected to have type
  Type u_1 : Type (u_1+1)
Additional information:
c:\Data\COQ_Test\reflection_groups\src\reflection_groups\test.lean:22:19: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

[Jeffrey Li]

Am I passing \bbk as an argument to the function s?

[Kevin Buzzard]

We're saying that this is what you will need to do, yes.

[Kevin Buzzard]

Lean can figure out E from v but it can't figure out k from anything, unless you put it somewhere.

[Eric Wieser]

It seems that variables (𝕜) doesn't work properly here for some reason!

[Jeffrey Li]

Eric Wieser said:

It seems that variables (𝕜) doesn't work properly here for some reason!

Yes that's the error I'm getting, am I doing something wrong or?

[Eric Wieser]

Specifically, it seems that because 𝕜 appears only in the notation and not in the other parameters, it's new brackets don't get picked up by lean

[Eric Wieser]

This works:

variables (𝕜)
include 𝕜
def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

[Eric Wieser]

As does this, with the notation after the binders change:

variables (𝕜)
local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
def s := fun v : E, fun w : E, w - (2*⟪v, w⟫/⟪v,v⟫)•v

[Eric Wieser]

I'm afraid you've hit a weird corner-case

[Jeffrey Li]

Thank you, could you explain what the difference is between {\bbk} and (\bbk) is in the type declaration?

[Jeffrey Li]

How come when we initially declare \bbk we use {\bbk : Type* } instead of (\bbk : Type*)?

[Kevin Buzzard]

{} brackets mean "let Lean work out this input to the function" (or more precisely "let Lean's type unifier work out the input"), () brackets mean "let the user supply the input". variable (X : Type) means "whenever X is mentioned in a function, use round brackets for it", and then later on variable {X} means "I've changed my mind -- from now on use {} brackets"