## 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: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 :-)

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

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