# Zulip Chat Archive

## Stream: maths

### Topic: Lie algebras

#### Johan Commelin (Jun 13 2018 at 08:43):

I am completely stuck on the sorried definition. Is this just to ambitious at the moment?

import algebra.module class has_bracket (α : Type*) := (bracket : α → α → α) local notation `[` a `,` b `]` := has_bracket.bracket a b class lie_algebra (R : out_param $ Type*) (𝔤 : Type*) [out_param $ comm_ring R] extends module R 𝔤, has_bracket 𝔤 := (left_linear := ∀ y : 𝔤, is_linear_map (λ x : 𝔤, [x,y])) (right_linear := ∀ x : 𝔤, is_linear_map (λ y : 𝔤, [x,y])) (alternating := ∀ x : 𝔤, [x,x] = 0) (Jacobi_identity := ∀ x y z : 𝔤, [x,[y,z]] + [z,[x,y]] + [y,[z,x]] = 0) (anti_comm := ∀ x y : 𝔤, [x,y] = -([y,x])) variables {R : Type*} [ri : comm_ring R] variables {𝔤 : Type*} [la : lie_algebra R 𝔤] include ri la section from_ring variables {S : Type*} [ring S] variables {f : R → S} [is_ring_hom f] instance commutator_bracket : has_bracket S := ⟨λ x y, x*y - y*x⟩ definition ring.to_lie_algebra : lie_algebra R S := sorry -- { sorry, -- ..ring.to_module } end from_ring

#### Kevin Buzzard (Jun 13 2018 at 08:47):

definition ring.to_lie_algebra : lie_algebra R S := begin constructor, -- fails end

#### Kevin Buzzard (Jun 13 2018 at 08:47):

I am a bit surprised about this.

#### Kevin Buzzard (Jun 13 2018 at 08:50):

`{}`

is more instructive

#### Kevin Buzzard (Jun 13 2018 at 08:50):

It says it can't prove `module R S`

#### Kevin Buzzard (Jun 13 2018 at 08:51):

which is fair enough because you never mentioned `f`

#### Kevin Buzzard (Jun 13 2018 at 08:53):

and `ring.to_module`

is only the statement that `R`

is an `R`

-module

#### Johan Commelin (Jun 13 2018 at 08:54):

Right. Thanks a lot!

#### Kevin Buzzard (Jun 13 2018 at 08:54):

I think when I was in your position a few months ago, wrestling with the type class inference system (but in a much less complex situation) Sebastian just pointed out that I could over-ride everything.

#### Kevin Buzzard (Jun 13 2018 at 08:55):

so I would just go and make my own explicit instances of everything

#### Kevin Buzzard (Jun 13 2018 at 08:55):

and this got me a bit further

#### Kevin Buzzard (Jun 13 2018 at 08:56):

I guess `constructor`

doesn't work because it didn't even get round to thinking about how to construct the extra fields, it just gets hung up with the fact that it can't even make the extension

#### Johan Commelin (Jun 13 2018 at 08:57):

Ok, so I've got a proof of `module R S`

. How do I feed it to the system?

#### Johan Commelin (Jun 13 2018 at 08:57):

Because `@lie_algebra`

is not interested in such a proof...

#### Johan Commelin (Jun 13 2018 at 08:58):

Is the `extends module R _`

giving me trouble? Does that `extends`

imply that it wants do deduce the module structure by type class inference?

#### Kevin Buzzard (Jun 13 2018 at 09:00):

I used to ask this sort of question all the time. If you search for type class woes you'll find my thread where I asked about 10 questions of this nature.

#### Kevin Buzzard (Jun 13 2018 at 09:02):

Unfortunately I can't keep all the answers in my head and I still have not found the time to go through that thread and write down all the tips in a proper doc

#### Johan Commelin (Jun 13 2018 at 09:12):

@Kevin Buzzard Misa stupid! In the definition of the class I shouldn't use `:=`

but `:`

for the axioms... it should be

class lie_algebra (R : out_param $ Type*) (𝔤 : Type*) [out_param $ comm_ring R] extends module R 𝔤, has_bracket 𝔤 := (left_linear : ∀ y : 𝔤, is_linear_map (λ x : 𝔤, [x,y])) (right_linear : ∀ x : 𝔤, is_linear_map (λ y : 𝔤, [x,y])) (alternating : ∀ x : 𝔤, [x,x] = 0) (Jacobi_identity : ∀ x y z : 𝔤, [x,[y,z]] + [z,[x,y]] + [y,[z,x]] = 0) (anti_comm : ∀ x y : 𝔤, [x,y] = -([y,x]))

That messed up everything. Now that I've fixed it, all of a sudden problems vanish!

#### Kevin Buzzard (Jun 13 2018 at 09:42):

Oh yeah. Sorry, I should have caught that.

#### Johan Commelin (Jun 13 2018 at 09:55):

Yoohoo!

section from_ring variables {S : Type*} [ring S] variables {f : R → S} [is_ring_hom f] variable {central : ∀ (r : R) (s : S), f(r) * s = s * f(r)} instance commutator_bracket : has_bracket S := ⟨λ x y, x*y - y*x⟩ include central definition ring.to_lie_algebra : lie_algebra R S := { left_linear := begin intro y, dsimp [commutator_bracket], constructor, { intros x₁ x₂, simp [left_distrib,right_distrib,mul_assoc] }, { intros r x, show f r * x * y + -(y * (f r * x)) = f r * (x * y + -(y * x)), simp [left_distrib,right_distrib,mul_assoc,central] } end, right_linear := begin intro x, dsimp [commutator_bracket], constructor, { intros x₁ x₂, simp [left_distrib,right_distrib,mul_assoc] }, { intros r y, show x * (f r * y) + -(f r * y * x) = f r * (x * y + -(y * x)), simp [left_distrib,right_distrib,mul_assoc,central] } end, alternating := begin intro x, dsimp [commutator_bracket], simp end, Jacobi_identity := begin intros x y z, dsimp [commutator_bracket], simp [left_distrib,right_distrib,mul_assoc], end, anti_comm := begin intros x y, dsimp [commutator_bracket], simp end, ..restriction_of_scalars.restriction_of_scalars f S } end from_ring

#### Johan Commelin (Jun 13 2018 at 09:55):

I like `simp`

!

#### Johan Commelin (Jun 13 2018 at 09:56):

It's a pity I can't use `ring`

because I'm not in a commutative setting...

#### Kevin Buzzard (Jun 13 2018 at 10:04):

It's a pity I can't use

`ring`

because I'm not in a commutative setting...

I can tell you how to write the non-commutative version :-)

#### Johan Commelin (Jun 13 2018 at 10:05):

Lol

#### Kevin Buzzard (Jun 13 2018 at 10:05):

actually there would be an issue

#### Johan Commelin (Jun 13 2018 at 10:05):

Yes, I wouldn't be surprised if commutativity is essential [also: lunch]

#### Kevin Buzzard (Jun 13 2018 at 10:06):

There's even an issue with my baby ring tactic -- one needs to be able to put every polynomial into a "canonical form", so that two polynomials (e.g. x^2+1 and 0*x^3+x^2+1) are equal if and only if their canonical forms are equal.

#### Chris Hughes (Jun 13 2018 at 10:07):

Make your polynomials a subtype, with a proof that the leading coeff is not zero

#### Chris Hughes (Jun 13 2018 at 10:07):

Like finsets.

#### Kevin Buzzard (Jun 13 2018 at 10:07):

In my baby ring tactic this isn't even present (yet). In the grown-up ring tactic Mario uses Gregoire-Mahboubi's strategy of writing everything in "horner form" because this is much more efficient for sparse polys

#### Kevin Buzzard (Jun 13 2018 at 10:07):

but in the non-comm case you would have to figure out a canonical form I guess, at least if you wanted to maximise the chance that the tactic worked.

#### Kevin Buzzard (Jun 13 2018 at 10:08):

Chris -- this doesn't work for zero

#### Kevin Buzzard (Jun 13 2018 at 10:08):

I was going to go for the following:

#### Kevin Buzzard (Jun 13 2018 at 10:08):

either an empty list, or a non-empty list with last element non-zero

#### Kevin Buzzard (Jun 13 2018 at 10:09):

One would have to check non-zero-ness in the ground ring (which might be Z/2Z)

#### Chris Hughes (Jun 13 2018 at 10:09):

What's the last element function?

#### Kevin Buzzard (Jun 13 2018 at 10:09):

I've seen one before

#### Kevin Buzzard (Jun 13 2018 at 10:09):

I've seen an n'th element function somewhere in list.lean

#### Chris Hughes (Jun 13 2018 at 10:09):

How does it habdle the empty list? If it's option you're okay.

#### Kevin Buzzard (Jun 13 2018 at 10:09):

unsurprisingly, there are all sorts of variants

#### Kevin Buzzard (Jun 13 2018 at 10:10):

e.g. one which asks for a proof that n < length before giving you a non-option n'th element

#### Chris Hughes (Jun 13 2018 at 10:11):

`list.head'`

looks like the best one, depending on the order of your lists.

Last updated: May 19 2021 at 02:10 UTC