Lie-Rinehart algebras

This file defines Lie-Rinehart algebras and their morphisms. It also shows that the derivations of a commutative algebra over a commutative Ring form such a Lie-Rinehart algebra. Lie-Rinehart algebras appear in differential geometry as section spaces of Lie algebroids and singular foliations. The typical Cartan calculus of differential geometry can be restated fully in terms of the Chevalley-Eilenberg algebra of a Lie-Rinehart algebra.

References

• [Rinehart, G. S., Differential forms on general commutative algebras. Zbl 0113.26204 Trans. Am. Math. Soc. 108, 195-222 (1963).][rinehart_1963]

class LieRinehartRing (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] [LieRingModule L A] : Prop

A Lie-Reinhart ring is a pair consisting of a commutative ring A and a Lie ring L such that A and L are each a module over the other, satisfying compatibility conditions.

• lie_smul_eq_mul (a b : A) (x : L) : ⁅a • x, b⁆ = a * ⁅x, b⁆
• leibniz_mul_right (x : L) (a b : A) : ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b
• leibniz_smul_right (x y : L) (a : A) : ⁅x, a • y⁆ = a • ⁅x, y⁆ + ⁅x, a⁆ • y

class LieRinehartAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing A] [LieRing L] [Module A L] [LieRingModule L A] [LieRinehartRing A L] [CommRing R] [Algebra R A] [LieAlgebra R L] extends IsScalarTower R A L, LieModule R L A : Prop

A Lie-Reinhart algebra with coefficients in a commutative ring R, is a pair consisting of a commutative R-algebra A and a Lie algebra L with coefficients in R, such that A and L are each a module over the other, satisfying compatibility conditions.

As shown below, this data determines a linear map L → Derivation R A A satisfying a Leibniz-like compatibility condition. This could even be taken as a definition, however the definition here has the advantage of being Prop-valued, thus mitigating potential diamonds.

• smul_assoc (x : R) (y : A) (z : L) : (x • y) • z = x • y • z
• smul_lie (t : R) (x : L) (m : A) : ⁅t • x, m⁆ = t • ⁅x, m⁆
• lie_smul (t : R) (x : L) (m : A) : ⁅x, t • m⁆ = t • ⁅x, m⁆

instance LieRinehartAlgebra.instLieRinehartRingDerivation {R : Type u_1} {A₁ : Type u_2} [CommRing R] [CommRing A₁] [Algebra R A₁] : LieRinehartRing A₁ (Derivation R A₁ A₁)

instance LieRinehartAlgebra.instDerivation {R : Type u_1} {A₁ : Type u_2} [CommRing R] [CommRing A₁] [Algebra R A₁] : LieRinehartAlgebra R A₁ (Derivation R A₁ A₁)

The derivations of a commutative Algebra themselves form a LieRinehart-Algebra.

structure LieRinehartAlgebra.Hom {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_4} [CommRing R] [CommRing A₁] [CommRing A₂] [Algebra R A₁] [Algebra R A₂] (σ : A₁ →ₐ[R] A₂) (L₁ : Type u_8) (L₂ : Type u_9) [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [LieAlgebra R L₁] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [LieAlgebra R L₂] extends L₁ →ₗ⁅R⁆ L₂ : Type (max u_8 u_9)

A morphism of Lie-Rinehart algebras, from (A₁, L₁) to (A₂, L₂), consists of a pair of maps (σ, F) where σ : A₁ → A₂ is a morphism of algebras and F is a morphism of Lie algebras, which respect the module structures.

Here we define the type of such morphisms with fixed σ (which can be regarded as functions L₁ → L₂). In the future it may be useful to define the type of such morphisms with fixed F (which can be regarded as functions A₁ → A₂) and the type of all such morphisms (which can be regarded as functions A₁ × L₁ → A₂ × L₂).

• toFun : L₁ → L₂
• map_add' (x y : L₁) : (↑self.toLieHom).toFun (x + y) = (↑self.toLieHom).toFun x + (↑self.toLieHom).toFun y
• map_smul' (m : R) (x : L₁) : (↑self.toLieHom).toFun (m • x) = (RingHom.id R) m • (↑self.toLieHom).toFun x
• map_lie' {x y : L₁} : (↑self.toLieHom).toFun ⁅x, y⁆ = ⁅(↑self.toLieHom).toFun x, (↑self.toLieHom).toFun y⁆
• map_smul_apply' (a : A₁) (x : L₁) : self.toLieHom (a • x) = σ a • self.toLieHom x
• apply_lie' (a : A₁) (x : L₁) : σ ⁅x, a⁆ = ⁅self.toLieHom x, σ a⁆

def LieRinehartAlgebra.Hom.«term_→ₗ⁅_⁆_» : Lean.TrailingParserDescr

A morphism of Lie-Rinehart algebras, from (A₁, L₁) to (A₂, L₂), consists of a pair of maps (σ, F) where σ : A₁ → A₂ is a morphism of algebras and F is a morphism of Lie algebras, which respect the module structures.

Here we define the type of such morphisms with fixed σ (which can be regarded as functions L₁ → L₂). In the future it may be useful to define the type of such morphisms with fixed F (which can be regarded as functions A₁ → A₂) and the type of all such morphisms (which can be regarded as functions A₁ × L₁ → A₂ × L₂).

Equations

• One or more equations did not get rendered due to their size.

instance LieRinehartAlgebra.Hom.instCoeFunForall {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] {σ₁₂ : A₁ →ₐ[R] A₂} : CoeFun (Hom σ₁₂ L₁ L₂) fun (x : Hom σ₁₂ L₁ L₂) => L₁ → L₂

Equations

• LieRinehartAlgebra.Hom.instCoeFunForall = { coe := fun (f : LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) => ⇑f.toLieHom }

theorem LieRinehartAlgebra.Hom.map_smul_apply {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] {σ₁₂ : A₁ →ₐ[R] A₂} (f : Hom σ₁₂ L₁ L₂) (a : A₁) (x : L₁) : f.toLieHom (a • x) = σ₁₂ a • f.toLieHom x

This is LieRinehartAlgebra.Hom.map_smul_apply' restated using the coercion to function rather than LieRinehartAlgebra.Hom.toLieHom.

theorem LieRinehartAlgebra.Hom.apply_lie {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] {σ₁₂ : A₁ →ₐ[R] A₂} (f : Hom σ₁₂ L₁ L₂) (a : A₁) (x : L₁) : σ₁₂ ⁅x, a⁆ = ⁅f.toLieHom x, σ₁₂ a⁆

This is LieRinehartAlgebra.Hom.apply_lie' restated using the coercion to function rather than LieRinehartAlgebra.Hom.toLieHom.

def LieRinehartAlgebra.Hom.toLinearMap' {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] {σ₁₂ : A₁ →ₐ[R] A₂} (f : Hom σ₁₂ L₁ L₂) : L₁ →ₛₗ[σ₁₂.toRingHom] L₂

A morphism of Lie-Rinehart algebras as a semilinear map.

Equations

• f.toLinearMap' = { toFun := ⇑f.toLieHom, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LieRinehartAlgebra.Hom.toLinearMap'_apply {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] {σ₁₂ : A₁ →ₐ[R] A₂} (f : Hom σ₁₂ L₁ L₂) (x : L₁) : f.toLinearMap' x = f.toLieHom x

def LieRinehartAlgebra.Hom.comp {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} {A₂ : Type u_4} {L₂ : Type u_5} {A₃ : Type u_6} {L₃ : Type u_7} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [CommRing A₂] [LieRing L₂] [Module A₂ L₂] [LieRingModule L₂ A₂] [CommRing A₃] [LieRing L₃] [Module A₃ L₃] [LieRingModule L₃ A₃] [Algebra R A₁] [LieAlgebra R L₁] [Algebra R A₂] [LieAlgebra R L₂] [Algebra R A₃] [LieAlgebra R L₃] {σ₁₂ : A₁ →ₐ[R] A₂} {σ₂₃ : A₂ →ₐ[R] A₃} (f : Hom σ₁₂ L₁ L₂) (g : Hom σ₂₃ L₂ L₃) : Hom (σ₂₃.comp σ₁₂) L₁ L₃

The composition of Lie-Rinehart algebra morphisms is again a morphism.

Equations

• f.comp g = { toLieHom := g.comp f.toLieHom, map_smul_apply' := ⋯, apply_lie' := ⋯ }

def LieRinehartAlgebra.Hom.id {R : Type u_1} {A₁ : Type u_2} {L₁ : Type u_3} [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [Algebra R A₁] [LieAlgebra R L₁] : Hom (AlgHom.id R A₁) L₁ L₁

The identity morphism of a Lie-Rinehart algebra over the identity algebra homomorphism of the underlying algebra.

Equations

• LieRinehartAlgebra.Hom.id = { toLieHom := LieHom.id, map_smul_apply' := ⋯, apply_lie' := ⋯ }

def LieRinehartAlgebra.Hom.anchor (R : Type u_1) (A₁ : Type u_2) (L₁ : Type u_3) [CommRing R] [CommRing A₁] [LieRing L₁] [Module A₁ L₁] [LieRingModule L₁ A₁] [Algebra R A₁] [LieAlgebra R L₁] [LieRinehartRing A₁ L₁] [LieRinehartAlgebra R A₁ L₁] : Hom (AlgHom.id R A₁) L₁ (Derivation R A₁ A₁)

The anchor of a given Lie-Rinehart algebra L over A interpreted as a Lie-Rinehart morphism to the module of derivations of A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieRinehartAlgebra.Hom.anchor_derivation {R : Type u_1} {A₁ : Type u_2} [CommRing R] [CommRing A₁] [Algebra R A₁] : anchor R A₁ (Derivation R A₁ A₁) = Hom.id