Lie-Rinehart algebras

Stream: mathlib4

[Leonid Ryvkin]

Hello,
I am currently getting started in Lean and thought to take as a learning project defining Lie Rinehart algebras and a few of their basic properties. I think I managed to define them as objects and to define their morphism,
but when I try creating an instance of morphism (the identity morphism) I am getting.

typeclass instance problem is stuck, it is often due to metavariables

I tried searching for solutions but was not very successful thus far. I am somehow running into this error message quite often. For instance, I wanted R to be implicit in the definition of Lie-Rinehart algebras, but it also caused such a problem. Is there some general nice fix for this type of issue? (Also I am very grateful for any feedback/ advice on how to better define things.) A shortened version of the relevant code below (The problem occurs on the last line).

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Ring.Defs
import Mathlib.Algebra.Algebra.Defs
import Mathlib.Algebra.Module.Defs
import Mathlib.Algebra.Lie.Basic
import Mathlib.RingTheory.Derivation.Basic
import Mathlib.RingTheory.Derivation.Lie
import Mathlib.Algebra.Module.LinearMap.Basic


/-- A Lie-Rinehart algebra over a commutative Ring `R` is a commutative `R`-algebra `A` together
with an `A`-module `L` equipped with a Lie bracket and a Lie algebra and module homomorphism
`ρ:L→ Der_R(A,A)` to the derivations of `A`, such that the Leibniz rule `⁅x,a•y⁆=a•⁅x,y⁆+ρ(x)(a)•y`
is satisfied.
-/
class LieRinehartAlgebra (R A L : Type*) [CommRing R] [CommRing A] [Algebra R A]
[AddCommMonoid L] [Module A L] [LieRing L] [LieAlgebra R L] (ρ : L →ₗ[A] Derivation R A A) where
islie : ∀ (x y : L), ρ ⁅x,y⁆ = ⁅ ρ x, ρ y ⁆
leibniz : ∀ (x y : L) (a : A), ⁅x,a • y⁆ = a• ⁅ x, y ⁆ + ((ρ (x)) (a))•y


/-- A homomorphism of Lie-Rinehart algebras `(A,L)`, `(A',L')` consists of an algebra map `σ:A→ A'`
and an `A`-linear map `F: L→L'` which is also a Lie algebra homomorphism.
-/
structure LRHom {R A A' : Type*} [CommRing R] [CommRing A] [Algebra R A] [CommRing A']
[Algebra R A'] (σ : A →+* A') (L L' : Type*) [AddCommMonoid L] [Module A L] [LieRing L]
[LieAlgebra R L] [AddCommMonoid L'] [Module A' L'] [LieRing L'] [LieAlgebra R L']
{ρ : L →ₗ[A] Derivation R A A} {ρ' : L' →ₗ[A'] Derivation R A' A'}
[LieRinehartAlgebra R A L ρ] [LieRinehartAlgebra R A' L' ρ'] extends LinearMap σ L L' where
isLie : ∀ (x y : L), toFun ⁅x,y⁆ = ⁅ toFun x, toFun y ⁆
anchorcomp: ∀ (a : A) (l : L), σ ((ρ l) a)  =  ((ρ' (toFun l)) (σ a))


variable {R : Type} [CommRing R]
variable {A : Type} [CommRing A] [Algebra R A]
variable {L : Type} [AddCommMonoid L] [Module A L] [LieRing L] [LieAlgebra R L]
variable (ρ : L →ₗ[A] Derivation R A A) [LieRinehartAlgebra R A L ρ]


instance : LRHom (RingHom.id A) L L where

[Johan Commelin]

@Leonid Ryvkin This can indeed be confusing.

1. The instance keyword is meant for examples of classes. Since your def of morphisms is (correctly) a structure, you should use def instead. In the case of classes, there should be at most 1 instance for each class, otherwise Lean gets confused. But of course you want to have more than 1 morphism between to LR algebras, so structure + def is indeed the way to go.
2. For your specific example (identity morphism) Lean does not know how to figure out which R you precisely mean. For example, I suppose that every LR algebra over R is also an LR algebra over $\Z$. This fact has not been explained to Lean yet in your code, but imagine that it were. In that case, Lean wouldn't know what value to pick for the identity map: do you want R or $\Z$?. For this reason Lean and Mathlib are conservative, and ask you to make the base ring explicit almost always. (The linear algebra library specifies the base ring of scalars in many places, because groups can be vector spaces over multiple fields/rings at the same time, e.g. over $\mathbb{C}$ and $\R$ at the same time.)

[Leonid Ryvkin]

@Johan Commelin Thank you very much, that is extremely helpful!

[Leonid Ryvkin]

I now changed to def and made the Ring R explicit, however the typeclass instance problem is stuck again, this time because it can not find the 'anchor' \rho. Would it be a reasonable solution to have \rho as one of the field in the class definition, to access it more easily, as below:

class LieRinehartAlgebra (R A L : Type*) [CommRing R] [CommRing A] [Algebra R A]
[AddCommMonoid L] [Module A L] [LieRing L] [LieAlgebra R L] where
ρ : L →ₗ[A] Derivation R A A
islie : ∀ (x y : L), ρ ⁅x,y⁆ = ⁅ ρ x, ρ y ⁆
leibniz : ∀ (x y : L) (a : A), ⁅x,a • y⁆ = a• ⁅ x, y ⁆ + ((ρ (x)) (a))•y

Or is it better to just pass R A L \rho explicitly to every construction?

[Johan Commelin]

@Leonid Ryvkin Do you think that $L$ could be an LR-algebra over the same $R$ and $A$ with respect to multiple anchors $\rho$?
I don't know the maths well enough to guess the answer.

[Johan Commelin]

If you claim that this never happens in the entire theory, then you could make $\rho$ an output parameter of the typeclass. Which means that Lean will start synthesizing instances before it knows $\rho$, and will then infer $\rho$ from the instance it found.

[Johan Commelin]

If you claim that multiple $\rho$'s do show up for given $(R,A,L)$ triples, then it will be better in practice to supply $\rho$ explicitly where needed.

[Leonid Ryvkin]

@Johan Commelin Thanks a lot!
Then I will pass it explicitly, In principle multiple $\rho$ would be possible, and I think there are even interesting examples where different ones appear....

[Johan Commelin]

Sounds good. This pattern pops up in different places. We are still researching ways to locally say: "In this file, there is always only one $\rho$, just use it without me specifying it."

Or "In this file $p$ is a prime number, stop bugging me."

Etc... We have partial solutions, but there are definitely rough edges in the user experience here.

(Aside: on Zulip you can write maths with double $$. So $$\sqrt{a+b}$$ gives $\sqrt{a+b}$.)

[Oliver Nash]

I've never worked with Lie-Rinehart algebras but assuming I've understood the above, here's a possible way to set things up:

import Mathlib.RingTheory.Derivation.Lie

class LRAlgebra (R A L : Type*) [CommRing R]
  [LieRing L] [LieAlgebra R L]
  [CommRing A] [Algebra R A] [Module A L] extends IsScalarTower R A L where
  toDer (R) : L →ₗ[A] Derivation R A A
  toDer_lie : ∀ x y : L, toDer ⁅x, y⁆ = ⁅toDer x, toDer y⁆
  protected lie_smul : ∀ (x y : L) (a : A), ⁅x, a • y⁆ = a • ⁅x, y⁆ + toDer x a • y

variable (R : Type*) [CommRing R]
  (L : Type*) [LieRing L] [LieAlgebra R L]
  (A : Type*) [CommRing A] [Algebra R A] [Module A L]
  (L' : Type*) [LieRing L'] [LieAlgebra R L']
  (A' : Type*) [CommRing A'] [Algebra R A'] [Module A' L']
  [LRAlgebra R A L] [LRAlgebra R A' L']

open LRAlgebra

structure LRHom where
  toLieHom : L →ₗ⁅R⁆ L'
  toRingHom : A →+* A'
  toRingHom_toDer (x : L) (a : A) : toRingHom (toDer R x a) = toDer R (toLieHom x) (toRingHom a)

/-- The identity map as a morphism of Lie-Rinehart pairs. -/
def LRHom.id : LRHom R L A L A where
  toLieHom := LieHom.id
  toRingHom := RingHom.id A
  toRingHom_toDer x A := by simp

[Oliver Nash]

Connecting with Johan's point, this design is optimised for the situation where a given pair $(L, A)$ have a canonical structure as an LR-algebra. The design would be different if you want to vary this structure.

Also, we could even have formalism to support both designs, similar to how if we have two commutative rings, $R$ and $A$ we have both R →+* A and [Algebra R A], and both are useful.

[Oliver Nash]

Comparing with your code above, I've really just made two small fixes, but I think they are worth highlighting:

1. I have dropped [AddCommMonoid L] since this endows L with an addition but so does [LieRing L] and thus if we include both typeclasses we're endowing L with two additions. (We should really have a linter to warn about things like this.)
2. I have added the class IsScalarTower R A L to make the actions of R and A on L compatible.

[Oliver Nash]

The design space is actually quite large here.

For example, it might be useful to define everything first in the absence of the coefficients R. One advantage of this would be that LRAlgebra.toDer would no longer redundantly demand to know R.

For the sake of highlighting another design, if one wanted to emphasise the fact that a morphism of LR algebras was a morphism of Lie algebras one could replace the definition I've proposed above with:

structure LRHom extends L →ₗ⁅R⁆ L' where
  toRingHom : A →+* A'
  toRingHom_toDer (x : L) (a : A) : toRingHom (toDer R x a) = toDer R (toFun x) (toRingHom a)

I can also see quite a few other design choices.

[Leonid Ryvkin]

@Oliver Nash Thanks a lot for the suggestions and corrections!
I am very hesitant on the canonicity of the anchor: I think in principle I could construct esoteric examples where there are multiple distinct anchors, but upon reexamination they don't seem to turn up in practice very often...

My current tendency is to leave everything except the anchor implicit, since it (via domain and codomain) seems to determine everything. Here is my current version.

I will play around with a few versions and see which one seems to work best....

[Leonid Ryvkin]

I managed to get the basic definitions working somehow, I am now stuck at a different place.
I don't fully understand how I can tell lean which module structure to use, when multiple ones could be around.
E.g.

import Mathlib.RingTheory.Derivation.Lie

variable {R : Type} [CommRing R]
variable {A : Type} [CommRing A] [Algebra R A]
variable {A' : Type} [CommRing A'] [Algebra R A']
variable (σ : A →ₐ[R] A')

#check σ.toAlgebra.toModule -- Module A A'
#check Derivation R A A' -- failed to synthesize Module A A'

I did not manage to create an instance to solve it, all attempts have lead to errors that I can not fully interpret.
and I also could not find a way to pass the module structure explicitly to 'Derivation'. I guess it is a general thing in Lean I would have to learn, but I did not manage to find the right piece of documentation/explanation.
Is there a nice reference for such things?

[Aaron Liu]

since σ is not mentioned anywhere in your typeclass goal, typeclass has no way of knowing about it

[Aaron Liu]

and docs#RingHom.toAlgebra is not an instance

[Aaron Liu]

I think the right thing to do here is to add [Algebra A A'] [IsScalarTower R A A'] to your hypotheses

[Leonid Ryvkin]

@Aaron Liu Thanks a lot!
Unfortunately in the context I am working in, there could be multiple different $\sigma$,
Those will give different module structures on $A'$ and different derivation modules, (which I might need in parallel).

[Aaron Liu]

uh oh

[Leonid Ryvkin]

I think I have something like a solution, it feels a little artificial but it works:
It is similar to how Mathlib/Analysis/Normed/Lp/WithLp.lean works, ...

import Mathlib.Algebra.LieRinehart.Defs
import Mathlib.LinearAlgebra.TensorProduct.Basic

variable {R : Type} [CommRing R]

variable {A : Type} [CommRing A] [Algebra R A]
variable {A' : Type} [CommRing A'] [Algebra R A']
variable (σ : A →ₐ[R] A')
variable {L : Type} [LieRing L] [LieAlgebra R L] [Module A L] [IsScalarTower R A L]

def inducedMod (_ : A →ₐ[R] A') : Type := A'

instance (σ : A →ₐ[R] A') : AddCommMonoid (inducedMod σ) :=
by simpa [inducedMod] using (inferInstance : AddCommMonoid A')

instance (σ : A →ₐ[R] A') : Semiring (inducedMod σ) :=
by simpa [inducedMod] using (inferInstance : Semiring A')

instance (σ : A →ₐ[R] A') : Module R (inducedMod σ) :=
by simpa [inducedMod] using (inferInstance : Module R A')

instance (σ : A →ₐ[R] A') : Module A (inducedMod σ) :=
by simpa [inducedMod] using σ.toAlgebra.toModule

#check Derivation R A (inducedMod σ)

[Kevin Buzzard]

An instance like

instance (σ : A →ₐ[R] A') : AddCommMonoid (inducedMod σ)

will never fire, because typeclass inference will never find σ : A →ₐ[R] A' (algebra maps aren't classes, so sigma is not and cannot be in square brackets, so it's not visible to the typeclass system).

[Kenny Lau]

@Kevin Buzzard σ is in the type

[Kevin Buzzard]

Indeed -- what I said is nonsense. Thanks! sigma is visible to the typeclass system because as Kenny says the system can see the type.

[Kenny Lau]

I think nowadays Lean automatically complains when there is a bad instance, it gives the error "failed to find typeclass synthesisation order"

[Kenny Lau]

import Mathlib

class Foo (α : Type)

instance (_n : Nat) : Foo Nat := ⟨⟩

hmm I don't know why it didn't complain here tho

[Leonid Ryvkin]

@Kenny Lau , @Kevin Buzzard Thanks a lot for having a look at it!

[Leonid Ryvkin]

In the meantime I have advanced a little and arrived at a moment where I needed to 'improve' a certain result in mathlib:
Given a commutative ring $R$ an $R$-algebra $A$ and an $A$-module homomorphism $f:M\to N$, there is an $A$-linear pushforward from the derivations $Der_R(A,M)$ to $Der_R(A,N)$.
In the pushforward section of derivations this morphism is only declared to be $R$-linear.
I have changed that and created the pull request 31464.

1. It's my first PR, so I am grateful for any feedback!

2. Is there a way to test if the change creates a problem without creating the PR? (I tried to run lake test but it takes very long and I am not sure it is the right thing)

3. There were 2 other files which I needed to change, where the R-linearity of the map was asked for, so the (stronger) A-linearity was causing an issue. I resolved it by explictly reducing the A-linearity to R-linearity , but probably I could have just changed R-linearity to A-linearity in the other files, too (which might require more downstream changes...) What version of resolving it is preferred?

Thanks a lot and best wishes,
Leo

[Kenny Lau]

@Leonid Ryvkin Congrats for first PR!

2. You should create the PR to get the cache, that's the correct way to do it.
3. That would depend on the situation, but let's try not changing R-linear to A-linear in other files for now and see what happens.

[Leonid Ryvkin]

@Kenny Lau Thanks a lot, (and also for reviewing!)

[Leonid Ryvkin]

Dear all,
Happy new year!

@Sven Holtrop and I have just started a PR (currently still in draft mode), for the basics on Lie-Rinehart algebras. Here is the PR #33690.

Feedback is very welcome!

Thanks a lot and best wishes,
Leo

[Kim Morrison]

You can use #33690 to link to PRs. It won't appear on the #queue unless you mark it as ready for review (currently it is in draft mode).

[Leonid Ryvkin]

@Kim Morrison Thanks a lot, I fixed the link.
About the draft mode: I thought to to attend some feedback before marking it as ready to review, or do you think it would be better to mark it right away (once the CI does not complain anymore)?

[Kim Morrison]

It depends: many people use the #queue or the #queueboard to decide what to work on when they have time for reviewing, and PRs in draft mode won't show up there, so you may get less attention.

[Johan Commelin]

@Leonid Ryvkin Personally, as a reviewer I interpret draft mode as "author is still working on this, and doesn't want a review yet".

Note that if your PR doesn't pass CI, then it also will not show up on the #queue.

[Leonid Ryvkin]

@Kim Morrison Thanks a lot for the very detailed reviews and @Johan Commelin for the answer.
We'll try to work the current reviews in, and then undraft it :-)

[Leonid Ryvkin]

I have worked in @Kim Morrison s reviews and 'undrafted' it.
Do I have to do something specific to remove the 'awaiting-author' flag?

[Vlad Tsyrklevich]

I believe you can write -awaiting-author as a comment on the PR or do what I do and just click the gear icon next to "Labels" on the PR page and uncheck awaiting-author.

[Kevin Buzzard]

I suspect that most users don't have the rights to change labels in mathlib -- I believe the -awaiting-author comment is the way to do this.

[Michael Rothgang]

Kevin is right.

[Leonid Ryvkin]

Thanks a lot for the reviews and the explanation!
I think I have implemented them, and the -awaiting-author works.

[Leonid Ryvkin]

Hi all,
I am slowly continuing with the Lie-Rinehart material.
For this I noticed that I need the construction of semidirect products of Li algebras (which does not seem to be in mathlib yet), and for that I need the notion of the derivations of a Lie algebra (which does not seem to be in mathlib yet either... Please correct me if I missed it)

So I started implementing it and noticed that to create the Derivations of a Lie algebra I would need to copy word for word almost all of the Mathlib.RingTheory.Derivation files. Somehow I don't see a quick way to get all the instances I need if I define the derivations as a structure.... However, things are much easier if I do it as a submodule of linear maps.

import Mathlib.Algebra.Lie.Basic
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.RingTheory.Derivation.Lie


-- this is unfortunately unused for now, because creating all the instances takes eternity
structure DerivationOfLie (R : Type*) (L : Type*) (M : Type*) [CommRing R] [LieRing L]
    [AddCommGroup M] [LieAlgebra R L] [Module R M] [LieRingModule L M] [LieModule R L M]
    extends L →ₗ[R] M where
  leibniz' (a b : L) : toLinearMap (⁅a , b⁆) = ⁅ a, toLinearMap b ⁆ - ⁅ b, toLinearMap a⁆


section

variable {R : Type*} [CommRing R]
variable {L : Type*} [LieRing L] [LieAlgebra R L]
variable {M : Type*} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]

variable (R L M) in
def SubDerivationOfLie : Submodule R (L →ₗ[R] M) where
  carrier := {d | ∀ x y , d ⁅ x, y ⁆ = ⁅ x, d y ⁆ - ⁅ y, d x⁆ }
  add_mem'  {d e} hd he x y:= by simp; grind
  zero_mem' := by simp
  smul_mem' t {d} hd x y:= by
    simp only [LinearMap.smul_apply, lie_smul]
    rw [hd]
    simp [smul_sub]

end

• Is there an important reason to go with the structure definition?
• If yes, is there some shortcut for the instances / some way to reuse the word done for derivations of commutative algebras without copying all of it?

Thanks a lot and best wishes,
Leo

[Michael Rothgang]

Let me ask @Oliver Nash as the resident expert on Lie algebras - are we indeed missing semidirect products of Lie algebras?

[Oliver Nash]

I’m currently traveling (without laptop) so I must be very brief but I’ll point out that we do actually have derivations for Lie algebras, that you might be interested in docs#LieAlgebra.IsExtension, and that @Scott Carnahan may be more available to help than me for now.

[Leonid Ryvkin]

Thanks a lot,
You are absolutely right - Derivations do exist!
Sorry - I managed to miss the Mathlib.Algebra.Lie.Derivation.Basic file.

[Leonid Ryvkin]

I have now written a small module where the semi-direct sum is constructed and added a PR: #35300.
@Oliver Nash Thanks a lot also for the remark about IsExtension, I added the corresponding instance to the file.