Documentation

TauCeti.Algebra.Lie.Derivation.Cocycle

Lie derivations as 1-cocycles #

A Lie derivation D : L → M into an L-module M is a 1-cocycle of L with values in M, and it shears the action of L on M × R to ⁅x, (m, t)⁆ = (⁅x, m⁆ + t • D x, 0), an extension of the trivial module R by M. This file supplies:

These let structure theorems about Lie modules, such as Weyl's theorem, be applied to the sheared module, for instance to show that a Lie derivation is inner.

Implementation notes #

LieDerivation.ShearedModule D is a type synonym for M × R, so that the action sheared by D is a global instance on its own carrier rather than a local structure on M × R. As with Mathlib's LieAlgebra.ofProd, all access goes through the linear equivalence LieDerivation.ShearedModule.ofProd, which is the identity, and LieDerivation.ShearedModule.ofProd_symm_lie restates the bracket field of the instance, so it is proved by rfl.

source
@[simp]
theorem LieDerivation.d₁₂_eq_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
(LieModule.Cohomology.d₁₂ R L M) ↑D = 0

A Lie derivation is a 1-cocycle.

source
def LieDerivation.ofD₁₂EqZero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : LieModule.Cohomology.oneCochain R L M) (hf : (LieModule.Cohomology.d₁₂ R L M) f = 0) :
LieDerivation R L M

A 1-cochain f with d₁₂ f = 0 satisfies the Leibniz rule, so it is a Lie derivation.

Instances For
    source
    @[simp]
    theorem LieDerivation.coe_ofD₁₂EqZero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (f : LieModule.Cohomology.oneCochain R L M) (hf : (LieModule.Cohomology.d₁₂ R L M) f = 0) :
    ⇑(ofD₁₂EqZero f hf) = ⇑f
    source
    def LieDerivation.ShearedModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (_D : LieDerivation R L M) :
    Type (max u_1 u_3)

    The module M × R with the action of L sheared by a Lie derivation D: ⁅x, (m, t)⁆ = (⁅x, m⁆ + t • D x, 0). Use LieDerivation.ShearedModule.ofProd to pass between it and M × R.

    Instances For
      source
      @[instance_reducible]
      instance LieDerivation.ShearedModule.instAddCommGroup {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
      AddCommGroup D.ShearedModule
      source
      @[instance_reducible]
      instance LieDerivation.ShearedModule.instModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
      Module R D.ShearedModule
      source
      def LieDerivation.ShearedModule.ofProd {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
      (M × R) ≃ₗ[R] D.ShearedModule

      The identification of M × R with the module sheared by D, as a linear equivalence.

      Instances For
        source
        instance LieDerivation.ShearedModule.instFinite {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) [Module.Finite R M] :
        Module.Finite R D.ShearedModule
        source
        @[instance_reducible]
        instance LieDerivation.ShearedModule.instLieRingModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
        LieRingModule L D.ShearedModule
        source
        @[simp]
        theorem LieDerivation.ShearedModule.ofProd_symm_lie {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) (x : L) (v : D.ShearedModule) :
        (ofProd D).symm ⁅x, v⁆ = (⁅x, ((ofProd D).symm v).1⁆ + ((ofProd D).symm v).2 • D x, 0)
        source
        instance LieDerivation.ShearedModule.instLieModule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (D : LieDerivation R L M) :
        LieModule R L D.ShearedModule