Documentation

Mathlib.Algebra.Lie.Abelian

Trivial Lie modules and Abelian Lie algebras #

The action of a Lie algebra L on a module M is trivial if ⁅x, m⁆ = 0 for all x ∈ L and m ∈ M. In the special case that M = L with the adjoint action, triviality corresponds to the concept of an Abelian Lie algebra.

In this file we define these concepts and provide some related definitions and results.

Main definitions #

Tags #

lie algebra, abelian, commutative, center

class LieModule.IsTrivial (L : Type v) (M : Type w) [Bracket L M] [Zero M] :

A Lie (ring) module is trivial iff all brackets vanish.

  • trivial : ∀ (x : L) (m : M), x, m = 0
Instances
    theorem LieModule.IsTrivial.trivial {L : Type v} {M : Type w} [Bracket L M] [Zero M] [self : LieModule.IsTrivial L M] (x : L) (m : M) :
    x, m = 0
    @[simp]
    theorem trivial_lie_zero (L : Type v) (M : Type w) [Bracket L M] [Zero M] [LieModule.IsTrivial L M] (x : L) (m : M) :
    x, m = 0
    @[reducible, inline]
    abbrev IsLieAbelian (L : Type v) [Bracket L L] [Zero L] :

    A Lie algebra is Abelian iff it is trivial as a Lie module over itself.

    Equations
    Instances For
      instance LieIdeal.isLieAbelian_of_trivial (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [h : LieModule.IsTrivial L I] :
      IsLieAbelian I
      Equations
      • =
      theorem Function.Injective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : Function.Injective f) :
      theorem Function.Surjective.isLieAbelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} (h₁ : Function.Surjective f) (h₂ : IsLieAbelian L₁) :
      theorem lie_abelian_iff_equiv_lie_abelian {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] (e : L₁ ≃ₗ⁅R L₂) :
      theorem commutative_ring_iff_abelian_lie_ring {A : Type v} [Ring A] :
      (Std.Commutative fun (x x_1 : A) => x * x_1) IsLieAbelian A
      def LieModule.ker (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

      The kernel of the action of a Lie algebra L on a Lie module M as a Lie ideal in L.

      Equations
      Instances For
        @[simp]
        theorem LieModule.mem_ker (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) :
        x LieModule.ker R L M ∀ (m : M), x, m = 0
        def LieModule.maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :

        The largest submodule of a Lie module M on which the Lie algebra L acts trivially.

        Equations
        Instances For
          @[simp]
          theorem LieModule.mem_maxTrivSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (m : M) :
          m LieModule.maxTrivSubmodule R L M ∀ (x : L), x, m = 0
          def LieModule.maxTrivHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L N) :

          maxTrivSubmodule is functorial.

          Equations
          Instances For
            @[simp]
            theorem LieModule.coe_maxTrivHom_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L N) (m : (LieModule.maxTrivSubmodule R L M)) :
            ((LieModule.maxTrivHom f) m) = f m
            def LieModule.maxTrivEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L N) :

            The maximal trivial submodules of Lie-equivalent Lie modules are Lie-equivalent.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem LieModule.coe_maxTrivEquiv_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L N) (m : (LieModule.maxTrivSubmodule R L M)) :
              ((LieModule.maxTrivEquiv e) m) = e m
              @[simp]
              theorem LieModule.maxTrivEquiv_of_refl_eq_refl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
              LieModule.maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl
              @[simp]
              theorem LieModule.maxTrivEquiv_of_equiv_symm_eq_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (e : M ≃ₗ⁅R,L N) :
              def LieModule.maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] :

              A linear map between two Lie modules is a morphism of Lie modules iff the Lie algebra action on it is trivial.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : (LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :
                (LieModule.maxTrivLinearMapEquivLieModuleHom f) = f
                @[simp]
                theorem LieModule.coe_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L N) :
                (LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = f
                @[simp]
                theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : (LieModule.maxTrivSubmodule R L (M →ₗ[R] N))) :
                (LieModule.maxTrivLinearMapEquivLieModuleHom f) = f
                @[simp]
                theorem LieModule.coe_linearMap_maxTrivLinearMapEquivLieModuleHom_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] (f : M →ₗ⁅R,L N) :
                (LieModule.maxTrivLinearMapEquivLieModuleHom.symm f) = f
                @[reducible, inline]
                abbrev LieAlgebra.center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

                The center of a Lie algebra is the set of elements that commute with everything. It can be viewed as the maximal trivial submodule of the Lie algebra as a Lie module over itself via the adjoint representation.

                Equations
                Instances For
                  @[simp]
                  theorem LieAlgebra.abelian_of_le_center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (h : I LieAlgebra.center R L) :
                  IsLieAbelian I
                  theorem LieModule.commute_toEnd_of_mem_center_left {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x LieAlgebra.center R L) (y : L) :
                  Commute ((LieModule.toEnd R L M) x) ((LieModule.toEnd R L M) y)
                  theorem LieModule.commute_toEnd_of_mem_center_right {R : Type u} {L : Type v} (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {x : L} (hx : x LieAlgebra.center R L) (y : L) :
                  Commute ((LieModule.toEnd R L M) y) ((LieModule.toEnd R L M) x)
                  @[simp]
                  theorem LieSubmodule.trivial_lie_oper_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (I : LieIdeal R L) [LieModule.IsTrivial L M] :
                  theorem lie_eq_self_of_isAtom_of_ne_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {I : LieIdeal R L} (hN : IsAtom N) (h : I, N ) :
                  I, N = N
                  theorem lie_eq_self_of_isAtom_of_nonabelian {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (hI : IsAtom I) (h : ¬IsLieAbelian I) :
                  I, I = I