Zulip Chat Archive

Stream: maths

Topic: Lie algebras


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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:47):

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:47):

I am a bit surprised about this.

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:50):

{} is more instructive

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:50):

It says it can't prove module R S

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:51):

which is fair enough because you never mentioned f

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:53):

and ring.to_module is only the statement that R is an R-module

view this post on Zulip Johan Commelin (Jun 13 2018 at 08:54):

Right. Thanks a lot!

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:55):

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 08:55):

and this got me a bit further

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

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

view this post on Zulip Johan Commelin (Jun 13 2018 at 08:57):

Because @lie_algebra is not interested in such a proof...

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

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

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

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 09:42):

Oh yeah. Sorry, I should have caught that.

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

view this post on Zulip Johan Commelin (Jun 13 2018 at 09:55):

I like simp!

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

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

view this post on Zulip Johan Commelin (Jun 13 2018 at 10:05):

Lol

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:05):

actually there would be an issue

view this post on Zulip Johan Commelin (Jun 13 2018 at 10:05):

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

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

view this post on Zulip Chris Hughes (Jun 13 2018 at 10:07):

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

view this post on Zulip Chris Hughes (Jun 13 2018 at 10:07):

Like finsets.

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

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:08):

Chris -- this doesn't work for zero

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:08):

I was going to go for the following:

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:08):

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

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

view this post on Zulip Chris Hughes (Jun 13 2018 at 10:09):

What's the last element function?

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:09):

I've seen one before

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:09):

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

view this post on Zulip Chris Hughes (Jun 13 2018 at 10:09):

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

view this post on Zulip Kevin Buzzard (Jun 13 2018 at 10:09):

unsurprisingly, there are all sorts of variants

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

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