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!)