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