Lie bracket vs commutator diamond

Stream: mathlib4

[Mario Carneiro]

This is an issue that @Kevin Buzzard and I ran into when trying to write down some definitions for FLT. There is a diamond on the ExtendScalar tensor product caused by the fact that it gets a lie bracket operation from the product structure, and also from being a ring (which yields a lie bracket ⁅x, y⁆ = x*y - y*x). This is a textbook example of a diamond, with the classic solution being to add a lie bracket operation to Ring. But neither of us was really feeling up to doing a big refactor like that...

[Eric Wieser]

Here's the test-case:

import Mathlib

variable (R A L M : Type*)
variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

example :
    LieAlgebra.ExtendScalars.instBracketTensorProduct R A B B = Ring.instBracket :=
  rfl -- fails

[Mario Carneiro]

this is what I came up with:

import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Algebra.Lie.BaseChange
import Mathlib.Analysis.Complex.Basic

open TensorProduct
example :
  (LieAlgebra.ExtendScalars.instLieRing .. : LieRing (ℝ ⊗[ℝ] ℝ)) =
  LieRing.ofAssociativeRing := rfl -- fail

[Eric Wieser]

What's the name of the bracket operator as a bilinear map?

[Mario Carneiro]

bracket?

[Mario Carneiro]

I'm not sure I understand the question

[Eric Wieser]

def bracketBilin {R L M} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
    [LieRingModule L M] [LieModule R L M] :
    L →ₗ[R] M →ₗ[R] M :=
  LinearMap.mk₂ _ (Bracket.bracket)
    add_lie smul_lie lie_add lie_smul

[Eric Wieser]

(I was trying to provide the non-rfl proof)

[Mario Carneiro]

ah, good, we just sorried it

[Kevin Buzzard]

One could remove the algebra to bracket instance I guess. I don't know how much trouble that would cause in the Lie algebra files though.

[Kevin Buzzard]

The mathematical reason this showed up was the following. Let $G$ be a real Lie group. The real Lie algebra $L$ of $G$ acts on the smooth complex-valued functions on $G$ (via first order differential operators), and when defining automorphic forms the book I read said that you immediately complexify, and get a $\mathbb{C}$-action of $L\otimes_{\R}{\mathbb{C}}$ on the smooth complex functions. Then you get an induced action of the universal enveloping algebra of this complex Lie algebra, and then of its center $A$, and these are the differential equations you want (the bi-invariant differential operators); part of the definition of an automorphic form is that it's annihilated by a finite (complex) codimension ideal of this commutative $\mathbb{C}$-algebra $A$ (which we know the structure of in the semisimple case, by Harish-Chandra).

When we found the diamond, my first instinct was "well OK we don't actually have to tensor up at that point, because we can do it later (after we've finished using the theory of Lie algebras)". Mario's post made me come back to this. My idea was that tensoring from $\mathbb{R}$ to $\mathbb{C}$ will no doubt commute with "take universal enveloping algebra" by some formal nonsense. But thinking about it more, it will no doubt also commute with taking the centre, and finally the predicate "I am annihiliated by an ideal of finite codimension under this action" also seems to be unaffected by tensoring up, and now I'm wondering if we can just skip the tensoring up completely.

[Eric Wieser]

Almost sorry-free:

import Mathlib


@[simps!]
def bracketBilin (R L M) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M]
    [LieRingModule L M] [LieModule R L M] :
    L →ₗ[R] M →ₗ[R] M :=
  LinearMap.mk₂ _ (Bracket.bracket)
    add_lie smul_lie lie_add lie_smul

attribute [ext] Bracket

open scoped TensorProduct

noncomputable instance instLieAlgebra'
  (S R A L : Type*) [CommRing S] [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L]
    [Module S A] [SMulCommClass R S A] :
  LieAlgebra S (A ⊗[R] L) where lie_smul _a _x _y := sorry -- whatever, probably true

variable (R A L M : Type*)
variable [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]

example :
    LieAlgebra.ExtendScalars.instBracketTensorProduct R A B B = Ring.instBracket := by
  ext x y
  conv_lhs => rw [← @bracketBilin_apply_apply R _ _ _ _]
  rw [← @bracketBilin_apply_apply R _ _ _ (_) (.ofAssociativeAlgebra) _ _ (_) (_) x y]
  rotate_left
  exact @lieAlgebraSelfModule _ _ _ (_) (_)
  refine LinearMap.congr_fun₂ ?_ x y
  ext xa xb ya yb
  change @Bracket.bracket _ _ (_) (xa ⊗ₜ[R] xb) (ya ⊗ₜ[R] yb) = _
  dsimp [Ring.lie_def]
  rw [TensorProduct.tmul_sub]

[Eric Wieser]

with the classic solution being to add a lie bracket operation to Ring

I think this is the only reasonable way to ensure the diamond commutes, assuming we keep using this pattern elsewhere

[Eric Wieser]

@Oliver Nash, do we have the bilinear map somewhere I build above?

[Mario Carneiro]

I've started working on this in branch#ring_bracket, but I expect to go several rounds with CI and anyone else is free to join in

[Eric Wieser]

I assume you mean NonUnitalNonAssocRing not Ring, right?

[Mario Carneiro]

that wasn't as clear of a branch name :)

[Eric Wieser]

Oh, that's not what you implemented...

[Kevin Buzzard]

I'm stuck here with Eric's sorry:

S : Type u_1
R : Type u_2
A : Type u_3
L : Type u_4
inst✝⁷ : CommRing S
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : Module S A
inst✝ : SMulCommClass R S A
a : S
x✝¹ : A
y✝¹ : L
x✝ : A
y✝ : L
⊢ a • x✝ * x✝¹ = a • (x✝¹ * x✝)

Did I take a wrong turn?

[Eric Wieser]

You're done, right?

[Eric Wieser]

rw [mul_comm, smul_mul_assoc] or something

[Mario Carneiro]

I assume there is no mul_comm?

[Eric Wieser]

A is commutative

[Mario Carneiro]

otherwise we wouldn't be talking about commutators

[Eric Wieser]

Sure, I guess I set up my problem incorrectly

[Eric Wieser]

But in Kevin's goal state it's there

[Oliver Nash]

It’s very late here so I can only write a brief remark for now. I think the right solution is to demote the bracket instance on an associative ring to a def. (In fact it was not I who promoted it, and I’ve been wanting to undo this for years.)

Aside from the diamond issue, if we don’t demote, I don’t see how we can ever talk about Poisson algebras.

[Oliver Nash]

I’ll write more over the weekend.

[Oliver Nash]

:sleeping:

[Mario Carneiro]

do you think we should move it into the ring structure?

[Oliver Nash]

I think not.

[Kevin Buzzard]

failed to synthesize
  IsScalarTower S A A

on smul_mul_assoc

[Eric Wieser]

Give yourself Algebra S A as a treat

[Eric Wieser]

(or add that assumption, more realistically)

[Eric Wieser]

Most of these compatibility classes you just add as you need them, then look back and check you did something sane

[Mario Carneiro]

Oliver Nash said:

I think the right solution is to demote the bracket instance on an associative ring to a def.

That sounds reasonable. In that case, we'll have to rethink docs#UniversalEnvelopingAlgebra.lift, which is the original theorem whose application failed due to this diamond (it contains this ofAssociativeRing instance in its type)

[Mario Carneiro]

the initial modified statement I came up with is

variable (R : Type*) (L : Type*)
variable [CommRing R] [LieRing L] [LieAlgebra R L]
variable {A : Type*} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A)
variable {A' : Type*} [LieRing A'] [LieAlgebra R A']

def lift' (e : A' ≃ₗ[R] A) (h : ∀ x y, e ⁅x, y⁆ = e x * e y - e y * e x) :
    (L →ₗ⁅R⁆ A) ≃ (UniversalEnvelopingAlgebra R L →ₐ[R] A) := by

but maybe there is a better one that is less annoying to use

[Kevin Buzzard]

noncomputable instance instLieAlgebra'
  (S R A L : Type*) [CommRing S] [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L]
    [Algebra S A] [SMulCommClass R S A] :
    LieAlgebra S (A ⊗[R] L) where
  lie_smul a x y := by
    induction x using TensorProduct.induction_on generalizing y
    · simp
    · induction y using TensorProduct.induction_on
      · simp
      · simp [TensorProduct.smul_tmul']
      · simp_all
    · simp_all [add_lie]

[Eric Wieser]

Ideally we can get that with fewer characters by generalizing the existing proof of the non-heterogeneous instance

[Johan Commelin]

I agree that the commutator bracket should probably not be a global instance but a scoped one.

[Oliver Nash]

Eric Wieser said:

Oliver Nash, do we have the bilinear map somewhere I build above?

Yes, it is docs#LieModule.toEnd As you will note it is more than just bilinear: it is a morphism of Lie algebras (provided we give the endomorphism ring the instance which I claim we should demote).

[Oliver Nash]

Mario Carneiro said:

the initial modified statement I came up with is [...] but maybe there is a better one that is less annoying to use

Mathematically this is of course perfect but I think we could probably do this nicely if we demoted docs#Ring.instBracket and added a new typeclass:

class IsCommutatorBracket (A : Type*) [Mul A] [Sub A] [Bracket A A] : Prop :=
  lie_eq_mul_sub_mul : ∀ a b : A, ⁅a, b⁆ = a * b - b * a

For statements like this so that they do not depend on the data that is docs#Ring.instBracket and instead just the Prop that would be IsCommutatorBracket.

[Oliver Nash]

Just to repeat my point about Poisson algebras above, here is how we would like to define them:

class PoissonRing (A : Type _) extends LieRing A, Ring A where
  lie_mul : ∀ (x y z : A), ⁅x, y * z⁆ = ⁅x, y⁆ * z + y * ⁅x, z⁆

except docs#Ring.instBracket makes this nonsense (two brackets on A).

[Oliver Nash]

Unfortunately my life these days is a series of errands and appointments so I must now run! I hope to have some non-trivial time to say more this evening.

[Bernhard Reinke]

I was looking to see whether Poisson algebras are already in mathlib and found this thread. Has there been any progress on resolving this diamond?

[Oliver Nash]

Nope. The required refactor is not very hard but would require some perseverance. The knowledge that someone has definite plans for Poisson algebras might provide sufficient motivation for someone (maybe me) to do it.

[Oliver Nash]

Incidentally I did think briefly about implementing Poisson algebras a year or so ago and I think I convinced myself that we might encounter some interesting challenges associated with Poisson modules and right actions but I'd have to dig out some old notes to remind myself of the details.