Documentation

Mathlib.Algebra.Lie.Basic

Lie algebras #

This file defines Lie rings and Lie algebras over a commutative ring together with their modules, morphisms and equivalences, as well as various lemmas to make these definitions usable.

Main definitions #

Notation #

Working over a fixed commutative ring R, we introduce the notations:

Implementation notes #

Lie algebras are defined as modules with a compatible Lie ring structure and thus, like modules, are partially unbundled.

References #

Tags #

lie bracket, jacobi identity, lie ring, lie algebra, lie module

class LieRing (L : Type v) extends AddCommGroup , Bracket :

A Lie ring is an additive group with compatible product, known as the bracket, satisfying the Jacobi identity.

Instances
    theorem LieRing.add_lie {L : Type v} [self : LieRing L] (x : L) (y : L) (z : L) :
    x + y, z = x, z + y, z

    A Lie ring bracket is additive in its first component.

    theorem LieRing.lie_add {L : Type v} [self : LieRing L] (x : L) (y : L) (z : L) :
    x, y + z = x, y + x, z

    A Lie ring bracket is additive in its second component.

    theorem LieRing.lie_self {L : Type v} [self : LieRing L] (x : L) :
    x, x = 0

    A Lie ring bracket vanishes on the diagonal in L × L.

    theorem LieRing.leibniz_lie {L : Type v} [self : LieRing L] (x : L) (y : L) (z : L) :

    A Lie ring bracket satisfies a Leibniz / Jacobi identity.

    class LieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] extends Module :
    Type (max u v)

    A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.

    • smul : RLL
    • one_smul : ∀ (b : L), 1 b = b
    • mul_smul : ∀ (x y : R) (b : L), (x * y) b = x y b
    • smul_zero : ∀ (a : R), a 0 = 0
    • smul_add : ∀ (a : R) (x y : L), a (x + y) = a x + a y
    • add_smul : ∀ (r s : R) (x : L), (r + s) x = r x + s x
    • zero_smul : ∀ (x : L), 0 x = 0
    • lie_smul : ∀ (t : R) (x y : L), x, t y = t x, y

      A Lie algebra bracket is compatible with scalar multiplication in its second argument.

      The compatibility in the first argument is not a class property, but follows since every Lie algebra has a natural Lie module action on itself, see LieModule.

    Instances
      theorem LieAlgebra.lie_smul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [self : LieAlgebra R L] (t : R) (x : L) (y : L) :
      x, t y = t x, y

      A Lie algebra bracket is compatible with scalar multiplication in its second argument.

      The compatibility in the first argument is not a class property, but follows since every Lie algebra has a natural Lie module action on itself, see LieModule.

      class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] extends Bracket :
      Type (max v w)

      A Lie ring module is an additive group, together with an additive action of a Lie ring on this group, such that the Lie bracket acts as the commutator of endomorphisms. (For representations of Lie algebras see LieModule.)

      Instances
        theorem LieRingModule.add_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [self : LieRingModule L M] (x : L) (y : L) (m : M) :
        x + y, m = x, m + y, m

        A Lie ring module bracket is additive in its first component.

        theorem LieRingModule.lie_add {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [self : LieRingModule L M] (x : L) (m : M) (n : M) :
        x, m + n = x, m + x, n

        A Lie ring module bracket is additive in its second component.

        theorem LieRingModule.leibniz_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [self : LieRingModule L M] (x : L) (y : L) (m : M) :

        A Lie ring module bracket satisfies a Leibniz / Jacobi identity.

        class LieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

        A Lie module is a module over a commutative ring, together with a linear action of a Lie algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms.

        • smul_lie : ∀ (t : R) (x : L) (m : M), t x, m = t x, m

          A Lie module bracket is compatible with scalar multiplication in its first argument.

        • lie_smul : ∀ (t : R) (x : L) (m : M), x, t m = t x, m

          A Lie module bracket is compatible with scalar multiplication in its second argument.

        Instances
          theorem LieModule.smul_lie {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [self : LieModule R L M] (t : R) (x : L) (m : M) :
          t x, m = t x, m

          A Lie module bracket is compatible with scalar multiplication in its first argument.

          theorem LieModule.lie_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [self : LieModule R L M] (t : R) (x : L) (m : M) :
          x, t m = t x, m

          A Lie module bracket is compatible with scalar multiplication in its second argument.

          @[simp]
          theorem add_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) :
          x + y, m = x, m + y, m
          @[simp]
          theorem lie_add {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : M) :
          x, m + n = x, m + x, n
          @[simp]
          theorem smul_lie {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] (t : R) (x : L) (m : M) :
          t x, m = t x, m
          @[simp]
          theorem lie_smul {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] (t : R) (x : L) (m : M) :
          x, t m = t x, m
          theorem leibniz_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) :
          @[simp]
          theorem lie_zero {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) :
          x, 0 = 0
          @[simp]
          theorem zero_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (m : M) :
          0, m = 0
          @[simp]
          theorem lie_self {L : Type v} [LieRing L] (x : L) :
          x, x = 0
          instance lieRingSelfModule {L : Type v} [LieRing L] :
          Equations
          @[simp]
          theorem lie_skew {L : Type v} [LieRing L] (x : L) (y : L) :
          instance lieAlgebraSelfModule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :
          LieModule R L L

          Every Lie algebra is a module over itself.

          Equations
          • =
          @[simp]
          theorem neg_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) :
          @[simp]
          theorem lie_neg {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) :
          @[simp]
          theorem sub_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) :
          x - y, m = x, m - y, m
          @[simp]
          theorem lie_sub {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : M) :
          x, m - n = x, m - x, n
          @[simp]
          theorem nsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ) :
          n x, m = n x, m
          @[simp]
          theorem lie_nsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (n : ) :
          x, n m = n x, m
          @[simp]
          theorem zsmul_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ) :
          a x, m = a x, m
          @[simp]
          theorem lie_zsmul {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (m : M) (a : ) :
          x, a m = a x, m
          @[simp]
          theorem lie_lie {L : Type v} {M : Type w} [LieRing L] [AddCommGroup M] [LieRingModule L M] (x : L) (y : L) (m : M) :
          theorem lie_jacobi {L : Type v} [LieRing L] (x : L) (y : L) (z : L) :
          Equations
          instance LinearMap.instLieRingModule {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] :
          Equations
          @[simp]
          theorem LieHom.lie_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] N) (x : L) (m : M) :
          x, f m = x, f m - f x, m
          instance LinearMap.instLieModule {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] :
          LieModule R L (M →ₗ[R] N)
          Equations
          • =
          instance Module.Dual.instLieRingModule {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] :

          We could avoid defining this by instead defining a LieRingModule L R instance with a zero bracket and relying on LinearMap.instLieRingModule. We do not do this because in the case that L = R we would have a non-defeq diamond via Ring.instBracket.

          Equations
          @[simp]
          theorem Module.Dual.lie_apply {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) (m : M) (f : M →ₗ[R] R) :
          x, f m = -f x, m
          instance Module.Dual.instLieModule {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 R L (M →ₗ[R] R)
          Equations
          • =
          structure LieHom (R : Type u_1) (L : Type u_2) (L' : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends LinearMap :
          Type (max u_2 u_3)

          A morphism of Lie algebras is a linear map respecting the bracket operations.

          • toFun : LL'
          • map_add' : ∀ (x y : L), (self).toFun (x + y) = (self).toFun x + (self).toFun y
          • map_smul' : ∀ (m : R) (x : L), (self).toFun (m x) = (RingHom.id R) m (self).toFun x
          • map_lie' : ∀ {x y : L}, (self).toFun x, y = (self).toFun x, (self).toFun y

            A morphism of Lie algebras is compatible with brackets.

          Instances For
            theorem LieHom.map_lie' {R : Type u_1} {L : Type u_2} {L' : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (self : L →ₗ⁅R L') {x : L} {y : L} :
            (self).toFun x, y = (self).toFun x, (self).toFun y

            A morphism of Lie algebras is compatible with brackets.

            A morphism of Lie algebras is a linear map respecting the bracket operations.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              instance LieHom.instCoeLinearMapId {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
              Coe (L₁ →ₗ⁅R L₂) (L₁ →ₗ[R] L₂)
              Equations
              • LieHom.instCoeLinearMapId = { coe := LieHom.toLinearMap }
              instance LieHom.instFunLike {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
              FunLike (L₁ →ₗ⁅R L₂) L₁ L₂
              Equations
              • LieHom.instFunLike = { coe := fun (f : L₁ →ₗ⁅R L₂) => (f).toFun, coe_injective' := }
              @[simp]
              theorem LieHom.coe_toLinearMap {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) :
              f = f
              @[simp]
              theorem LieHom.toFun_eq_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) :
              (f).toFun = f
              @[simp]
              theorem LieHom.map_smul {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (c : R) (x : L₁) :
              f (c x) = c f x
              @[simp]
              theorem LieHom.map_add {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (x : L₁) (y : L₁) :
              f (x + y) = f x + f y
              @[simp]
              theorem LieHom.map_sub {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (x : L₁) (y : L₁) :
              f (x - y) = f x - f y
              @[simp]
              theorem LieHom.map_neg {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (x : L₁) :
              f (-x) = -f x
              @[simp]
              theorem LieHom.map_lie {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (x : L₁) (y : L₁) :
              f x, y = f x, f y
              @[simp]
              theorem LieHom.map_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) :
              f 0 = 0
              def LieHom.id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
              L₁ →ₗ⁅R L₁

              The identity map is a morphism of Lie algebras.

              Equations
              • LieHom.id = let __src := LinearMap.id; { toLinearMap := __src, map_lie' := }
              Instances For
                @[simp]
                theorem LieHom.coe_id {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                LieHom.id = id
                theorem LieHom.id_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :
                LieHom.id x = x
                instance LieHom.instZero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
                Zero (L₁ →ₗ⁅R L₂)

                The constant 0 map is a Lie algebra morphism.

                Equations
                • LieHom.instZero = { zero := let __src := 0; { toLinearMap := __src, map_lie' := } }
                @[simp]
                theorem LieHom.coe_zero {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
                0 = 0
                theorem LieHom.zero_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (x : L₁) :
                0 x = 0
                instance LieHom.instOne {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                One (L₁ →ₗ⁅R L₁)

                The identity map is a Lie algebra morphism.

                Equations
                • LieHom.instOne = { one := LieHom.id }
                @[simp]
                theorem LieHom.coe_one {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                1 = id
                theorem LieHom.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :
                1 x = x
                instance LieHom.instInhabited {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
                Inhabited (L₁ →ₗ⁅R L₂)
                Equations
                • LieHom.instInhabited = { default := 0 }
                theorem LieHom.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] :
                Function.Injective DFunLike.coe
                theorem LieHom.ext {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} {g : L₁ →ₗ⁅R L₂} (h : ∀ (x : L₁), f x = g x) :
                f = g
                theorem LieHom.ext_iff {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} {g : L₁ →ₗ⁅R L₂} :
                f = g ∀ (x : L₁), f x = g x
                theorem LieHom.congr_fun {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] {f : L₁ →ₗ⁅R L₂} {g : L₁ →ₗ⁅R L₂} (h : f = g) (x : L₁) :
                f x = g x
                @[simp]
                theorem LieHom.mk_coe {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := h₁ }.toFun (m x) = (RingHom.id R) m { toFun := f, map_add' := h₁ }.toFun x) (h₃ : ∀ {x y : L₁}, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, y = { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun y) :
                { toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
                @[simp]
                theorem LieHom.coe_mk {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y) (h₂ : ∀ (m : R) (x : L₁), { toFun := f, map_add' := h₁ }.toFun (m x) = (RingHom.id R) m { toFun := f, map_add' := h₁ }.toFun x) (h₃ : ∀ {x y : L₁}, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, y = { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x, { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun y) :
                { toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
                def LieHom.comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
                L₁ →ₗ⁅R L₃

                The composition of morphisms is a morphism.

                Equations
                • f.comp g = let __src := f ∘ₗ g; { toLinearMap := __src, map_lie' := }
                Instances For
                  theorem LieHom.comp_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) (x : L₁) :
                  (f.comp g) x = f (g x)
                  @[simp]
                  theorem LieHom.coe_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
                  (f.comp g) = f g
                  @[simp]
                  theorem LieHom.coe_linearMap_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] (f : L₂ →ₗ⁅R L₃) (g : L₁ →ₗ⁅R L₂) :
                  (f.comp g) = f ∘ₗ g
                  @[simp]
                  theorem LieHom.comp_id {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) :
                  f.comp LieHom.id = f
                  @[simp]
                  theorem LieHom.id_comp {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) :
                  LieHom.id.comp f = f
                  def LieHom.inverse {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] (f : L₁ →ₗ⁅R L₂) (g : L₂L₁) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                  L₂ →ₗ⁅R L₁

                  The inverse of a bijective morphism is a morphism.

                  Equations
                  • f.inverse g h₁ h₂ = let __src := (f).inverse g h₁ h₂; { toLinearMap := __src, map_lie' := }
                  Instances For
                    def LieRingModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R L₂) :

                    A Lie ring module may be pulled back along a morphism of Lie algebras.

                    See note [reducible non-instances].

                    Equations
                    Instances For
                      theorem LieRingModule.compLieHom_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R L₂) (x : L₁) (m : M) :
                      x, m = f x, m
                      theorem LieModule.compLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M] [LieRingModule L₂ M] (f : L₁ →ₗ⁅R L₂) [Module R M] [LieModule R L₂ M] :
                      LieModule R L₁ M

                      A Lie module may be pulled back along a morphism of Lie algebras.

                      structure LieEquiv (R : Type u) (L : Type v) (L' : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] extends LieHom :
                      Type (max v w)

                      An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is more convenient to define via linear equivalence to get .toLinearEquiv for free.

                      • toFun : LL'
                      • 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
                      • invFun : L'L

                        The inverse function of an equivalence of Lie algebras

                      • left_inv : Function.LeftInverse self.invFun (self.toLieHom).toFun

                        The inverse function of an equivalence of Lie algebras is a left inverse of the underlying function.

                      • right_inv : Function.RightInverse self.invFun (self.toLieHom).toFun

                        The inverse function of an equivalence of Lie algebras is a right inverse of the underlying function.

                      Instances For
                        theorem LieEquiv.left_inv {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (self : L ≃ₗ⁅R L') :
                        Function.LeftInverse self.invFun (self.toLieHom).toFun

                        The inverse function of an equivalence of Lie algebras is a left inverse of the underlying function.

                        theorem LieEquiv.right_inv {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (self : L ≃ₗ⁅R L') :
                        Function.RightInverse self.invFun (self.toLieHom).toFun

                        The inverse function of an equivalence of Lie algebras is a right inverse of the underlying function.

                        An equivalence of Lie algebras is a morphism which is also a linear equivalence. We could instead define an equivalence to be a morphism which is also a (plain) equivalence. However it is more convenient to define via linear equivalence to get .toLinearEquiv for free.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def LieEquiv.toLinearEquiv {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₂) :
                          L₁ ≃ₗ[R] L₂

                          Consider an equivalence of Lie algebras as a linear equivalence.

                          Equations
                          • f.toLinearEquiv = let __src := f.toLieHom; { toLinearMap := __src, invFun := f.invFun, left_inv := , right_inv := }
                          Instances For
                            instance LieEquiv.hasCoeToLieHom {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                            Coe (L₁ ≃ₗ⁅R L₂) (L₁ →ₗ⁅R L₂)
                            Equations
                            • LieEquiv.hasCoeToLieHom = { coe := LieEquiv.toLieHom }
                            instance LieEquiv.hasCoeToLinearEquiv {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                            Coe (L₁ ≃ₗ⁅R L₂) (L₁ ≃ₗ[R] L₂)
                            Equations
                            • LieEquiv.hasCoeToLinearEquiv = { coe := LieEquiv.toLinearEquiv }
                            instance LieEquiv.instEquivLike {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                            EquivLike (L₁ ≃ₗ⁅R L₂) L₁ L₂
                            Equations
                            • LieEquiv.instEquivLike = { coe := fun (f : L₁ ≃ₗ⁅R L₂) => (f.toLieHom).toFun, inv := fun (f : L₁ ≃ₗ⁅R L₂) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                            theorem LieEquiv.coe_to_lieHom {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₂) :
                            e.toLieHom = e
                            @[simp]
                            theorem LieEquiv.coe_to_linearEquiv {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₂) :
                            e.toLinearEquiv = e
                            @[simp]
                            theorem LieEquiv.to_linearEquiv_mk {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₂) (g : L₂L₁) (h₁ : Function.LeftInverse g (f).toFun) (h₂ : Function.RightInverse g (f).toFun) :
                            { toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toLinearEquiv = { toLinearMap := f, invFun := g, left_inv := h₁, right_inv := h₂ }
                            theorem LieEquiv.coe_linearEquiv_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                            Function.Injective LieEquiv.toLinearEquiv
                            theorem LieEquiv.coe_injective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                            Function.Injective DFunLike.coe
                            theorem LieEquiv.ext {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₂} {g : L₁ ≃ₗ⁅R L₂} (h : ∀ (x : L₁), f x = g x) :
                            f = g
                            instance LieEquiv.instOne {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                            One (L₁ ≃ₗ⁅R L₁)
                            Equations
                            • LieEquiv.instOne = { one := let __src := 1; { toLinearMap := __src, map_lie' := , invFun := __src.invFun, left_inv := , right_inv := } }
                            @[simp]
                            theorem LieEquiv.one_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :
                            1 x = x
                            instance LieEquiv.instInhabited {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                            Inhabited (L₁ ≃ₗ⁅R L₁)
                            Equations
                            • LieEquiv.instInhabited = { default := 1 }
                            theorem LieEquiv.map_lie {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₂) (x : L₁) (y : L₁) :
                            e x, y = e x, e y
                            def LieEquiv.refl {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                            L₁ ≃ₗ⁅R L₁

                            Lie algebra equivalences are reflexive.

                            Equations
                            • LieEquiv.refl = 1
                            Instances For
                              @[simp]
                              theorem LieEquiv.refl_apply {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] (x : L₁) :
                              LieEquiv.refl x = x
                              def LieEquiv.symm {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₂) :
                              L₂ ≃ₗ⁅R L₁

                              Lie algebra equivalences are symmetric.

                              Equations
                              • e.symm = let __src := e.inverse e.invFun ; let __src_1 := e.toLinearEquiv.symm; { toLieHom := __src, invFun := __src_1.invFun, left_inv := , right_inv := }
                              Instances For
                                @[simp]
                                theorem LieEquiv.symm_symm {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₂) :
                                e.symm.symm = e
                                theorem LieEquiv.symm_bijective {R : Type u} {L₁ : Type v} {L₂ : Type w} [CommRing R] [LieRing L₁] [LieRing L₂] [LieAlgebra R L₁] [LieAlgebra R L₂] :
                                Function.Bijective LieEquiv.symm
                                @[simp]
                                theorem LieEquiv.apply_symm_apply {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₂) (x : L₂) :
                                e (e.symm x) = x
                                @[simp]
                                theorem LieEquiv.symm_apply_apply {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₂) (x : L₁) :
                                e.symm (e x) = x
                                @[simp]
                                theorem LieEquiv.refl_symm {R : Type u} {L₁ : Type v} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] :
                                LieEquiv.refl.symm = LieEquiv.refl
                                def LieEquiv.trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) :
                                L₁ ≃ₗ⁅R L₃

                                Lie algebra equivalences are transitive.

                                Equations
                                • e₁.trans e₂ = let __src := e₂.comp e₁.toLieHom; let __src_1 := e₁.toLinearEquiv.trans e₂.toLinearEquiv; { toLieHom := __src, invFun := __src_1.invFun, left_inv := , right_inv := }
                                Instances For
                                  @[simp]
                                  theorem LieEquiv.self_trans_symm {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₂) :
                                  e.trans e.symm = LieEquiv.refl
                                  @[simp]
                                  theorem LieEquiv.symm_trans_self {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₂) :
                                  e.symm.trans e = LieEquiv.refl
                                  @[simp]
                                  theorem LieEquiv.trans_apply {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) (x : L₁) :
                                  (e₁.trans e₂) x = e₂ (e₁ x)
                                  @[simp]
                                  theorem LieEquiv.symm_trans {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [CommRing R] [LieRing L₁] [LieRing L₂] [LieRing L₃] [LieAlgebra R L₁] [LieAlgebra R L₂] [LieAlgebra R L₃] (e₁ : L₁ ≃ₗ⁅R L₂) (e₂ : L₂ ≃ₗ⁅R L₃) :
                                  (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
                                  theorem LieEquiv.bijective {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₂) :
                                  Function.Bijective e.toLieHom
                                  theorem LieEquiv.injective {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₂) :
                                  Function.Injective e.toLieHom
                                  theorem LieEquiv.surjective {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₂) :
                                  Function.Surjective e.toLieHom
                                  @[simp]
                                  theorem LieEquiv.ofBijective_toFun {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.Bijective f) (a : L₁) :
                                  @[simp]
                                  theorem LieEquiv.ofBijective_invFun {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.Bijective f) :
                                  ∀ (a : L₂), (LieEquiv.ofBijective f h).invFun a = (LinearEquiv.ofBijective (f) h).symm a
                                  noncomputable def LieEquiv.ofBijective {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.Bijective f) :
                                  L₁ ≃ₗ⁅R L₂

                                  A bijective morphism of Lie algebras yields an equivalence of Lie algebras.

                                  Equations
                                  Instances For
                                    structure LieModuleHom (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends LinearMap :
                                    Type (max w w₁)

                                    A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.

                                    • toFun : MN
                                    • map_add' : ∀ (x y : M), (self).toFun (x + y) = (self).toFun x + (self).toFun y
                                    • map_smul' : ∀ (m : R) (x : M), (self).toFun (m x) = (RingHom.id R) m (self).toFun x
                                    • map_lie' : ∀ {x : L} {m : M}, (self).toFun x, m = x, (self).toFun m

                                      A module of Lie algebra modules is compatible with the action of the Lie algebra on the modules.

                                    Instances For
                                      theorem LieModuleHom.map_lie' {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (self : M →ₗ⁅R,L N) {x : L} {m : M} :
                                      (self).toFun x, m = x, (self).toFun m

                                      A module of Lie algebra modules is compatible with the action of the Lie algebra on the modules.

                                      A morphism of Lie algebra modules is a linear map which commutes with the action of the Lie algebra.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        instance LieModuleHom.instCoeOutLinearMapId {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                        Equations
                                        • LieModuleHom.instCoeOutLinearMapId = { coe := LieModuleHom.toLinearMap }
                                        instance LieModuleHom.instFunLike {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                        Equations
                                        • LieModuleHom.instFunLike = { coe := fun (f : M →ₗ⁅R,L N) => (f).toFun, coe_injective' := }
                                        @[simp]
                                        theorem LieModuleHom.coe_toLinearMap {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) :
                                        f = f
                                        @[simp]
                                        theorem LieModuleHom.map_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (c : R) (x : M) :
                                        f (c x) = c f x
                                        @[simp]
                                        theorem LieModuleHom.map_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (x : M) (y : M) :
                                        f (x + y) = f x + f y
                                        @[simp]
                                        theorem LieModuleHom.map_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (x : M) (y : M) :
                                        f (x - y) = f x - f y
                                        @[simp]
                                        theorem LieModuleHom.map_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (x : M) :
                                        f (-x) = -f x
                                        @[simp]
                                        theorem LieModuleHom.map_lie {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (x : L) (m : M) :
                                        f x, m = x, f m
                                        theorem LieModuleHom.map_lie₂ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] [LieModule R L N] [LieModule R L P] (f : M →ₗ⁅R,L N →ₗ[R] P) (x : L) (m : M) (n : N) :
                                        x, (f m) n = (f x, m) n + (f m) x, n
                                        @[simp]
                                        theorem LieModuleHom.map_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) :
                                        f 0 = 0
                                        def LieModuleHom.id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

                                        The identity map is a morphism of Lie modules.

                                        Equations
                                        • LieModuleHom.id = let __src := LinearMap.id; { toLinearMap := __src, map_lie' := }
                                        Instances For
                                          @[simp]
                                          theorem LieModuleHom.coe_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :
                                          LieModuleHom.id = id
                                          theorem LieModuleHom.id_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) :
                                          LieModuleHom.id x = x
                                          instance LieModuleHom.instZero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :

                                          The constant 0 map is a Lie module morphism.

                                          Equations
                                          • LieModuleHom.instZero = { zero := let __src := 0; { toLinearMap := __src, map_lie' := } }
                                          @[simp]
                                          theorem LieModuleHom.coe_zero {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                          0 = 0
                                          theorem LieModuleHom.zero_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (m : M) :
                                          0 m = 0
                                          instance LieModuleHom.instOne {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

                                          The identity map is a Lie module morphism.

                                          Equations
                                          • LieModuleHom.instOne = { one := LieModuleHom.id }
                                          instance LieModuleHom.instInhabited {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                          Equations
                                          • LieModuleHom.instInhabited = { default := 0 }
                                          theorem LieModuleHom.coe_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                          Function.Injective DFunLike.coe
                                          theorem LieModuleHom.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L N} {g : M →ₗ⁅R,L N} (h : ∀ (m : M), f m = g m) :
                                          f = g
                                          theorem LieModuleHom.ext_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L N} {g : M →ₗ⁅R,L N} :
                                          f = g ∀ (m : M), f m = g m
                                          theorem LieModuleHom.congr_fun {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {f : M →ₗ⁅R,L N} {g : M →ₗ⁅R,L N} (h : f = g) (x : M) :
                                          f x = g x
                                          @[simp]
                                          theorem LieModuleHom.mk_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (h : ∀ {x : L} {m : M}, (f).toFun x, m = x, (f).toFun m) :
                                          { toLinearMap := f, map_lie' := h } = f
                                          @[simp]
                                          theorem LieModuleHom.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, f.toFun x, m = x, f.toFun m) :
                                          { toLinearMap := f, map_lie' := h } = f
                                          theorem LieModuleHom.coe_linear_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ[R] N) (h : ∀ {x : L} {m : M}, f.toFun x, m = x, f.toFun m) :
                                          { toLinearMap := f, map_lie' := h } = f
                                          def LieModuleHom.comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :

                                          The composition of Lie module morphisms is a morphism.

                                          Equations
                                          • f.comp g = let __src := f ∘ₗ g; { toLinearMap := __src, map_lie' := }
                                          Instances For
                                            theorem LieModuleHom.comp_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) (m : M) :
                                            (f.comp g) m = f (g m)
                                            @[simp]
                                            theorem LieModuleHom.coe_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :
                                            (f.comp g) = f g
                                            @[simp]
                                            theorem LieModuleHom.coe_linearMap_comp {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (f : N →ₗ⁅R,L P) (g : M →ₗ⁅R,L N) :
                                            (f.comp g) = f ∘ₗ g
                                            def LieModuleHom.inverse {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : NM) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

                                            The inverse of a bijective morphism of Lie modules is a morphism of Lie modules.

                                            Equations
                                            • f.inverse g h₁ h₂ = let __src := (f).inverse g h₁ h₂; { toLinearMap := __src, map_lie' := }
                                            Instances For
                                              instance LieModuleHom.instAdd {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              • LieModuleHom.instAdd = { add := fun (f g : M →ₗ⁅R,L N) => let __src := f + g; { toLinearMap := __src, map_lie' := } }
                                              instance LieModuleHom.instSub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              • LieModuleHom.instSub = { sub := fun (f g : M →ₗ⁅R,L N) => let __src := f - g; { toLinearMap := __src, map_lie' := } }
                                              instance LieModuleHom.instNeg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              • LieModuleHom.instNeg = { neg := fun (f : M →ₗ⁅R,L N) => let __src := -f; { toLinearMap := __src, map_lie' := } }
                                              @[simp]
                                              theorem LieModuleHom.coe_add {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : M →ₗ⁅R,L N) :
                                              (f + g) = f + g
                                              theorem LieModuleHom.add_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : M →ₗ⁅R,L N) (m : M) :
                                              (f + g) m = f m + g m
                                              @[simp]
                                              theorem LieModuleHom.coe_sub {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : M →ₗ⁅R,L N) :
                                              (f - g) = f - g
                                              theorem LieModuleHom.sub_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : M →ₗ⁅R,L N) (m : M) :
                                              (f - g) m = f m - g m
                                              @[simp]
                                              theorem LieModuleHom.coe_neg {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) :
                                              (-f) = -f
                                              theorem LieModuleHom.neg_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (m : M) :
                                              (-f) m = -f m
                                              instance LieModuleHom.hasNSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              • LieModuleHom.hasNSMul = { smul := fun (n : ) (f : M →ₗ⁅R,L N) => let __src := n f; { toLinearMap := __src, map_lie' := } }
                                              @[simp]
                                              theorem LieModuleHom.coe_nsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ) (f : M →ₗ⁅R,L N) :
                                              (n f) = n f
                                              theorem LieModuleHom.nsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (n : ) (f : M →ₗ⁅R,L N) (m : M) :
                                              (n f) m = n f m
                                              instance LieModuleHom.hasZSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              • LieModuleHom.hasZSMul = { smul := fun (z : ) (f : M →ₗ⁅R,L N) => let __src := z f; { toLinearMap := __src, map_lie' := } }
                                              @[simp]
                                              theorem LieModuleHom.coe_zsmul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ) (f : M →ₗ⁅R,L N) :
                                              (z f) = z f
                                              theorem LieModuleHom.zsmul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (z : ) (f : M →ₗ⁅R,L N) (m : M) :
                                              (z f) m = z f m
                                              instance LieModuleHom.instAddCommGroup {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                              Equations
                                              instance LieModuleHom.instSMul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] :
                                              Equations
                                              • LieModuleHom.instSMul = { smul := fun (t : R) (f : M →ₗ⁅R,L N) => let __src := t f; { toLinearMap := __src, map_lie' := } }
                                              @[simp]
                                              theorem LieModuleHom.coe_smul {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L N) :
                                              (t f) = t f
                                              theorem LieModuleHom.smul_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] (t : R) (f : M →ₗ⁅R,L N) (m : M) :
                                              (t f) m = t f m
                                              instance LieModuleHom.instModule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] [LieModule R L N] :
                                              Equations
                                              structure LieModuleEquiv (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] extends LieModuleHom :
                                              Type (max w w₁)

                                              An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.

                                              • toFun : MN
                                              • map_add' : ∀ (x y : M), (self.toLieModuleHom).toFun (x + y) = (self.toLieModuleHom).toFun x + (self.toLieModuleHom).toFun y
                                              • map_smul' : ∀ (m : R) (x : M), (self.toLieModuleHom).toFun (m x) = (RingHom.id R) m (self.toLieModuleHom).toFun x
                                              • map_lie' : ∀ {x : L} {m : M}, (self.toLieModuleHom).toFun x, m = x, (self.toLieModuleHom).toFun m
                                              • invFun : NM

                                                The inverse function of an equivalence of Lie modules

                                              • left_inv : Function.LeftInverse self.invFun (self.toLieModuleHom).toFun

                                                The inverse function of an equivalence of Lie modules is a left inverse of the underlying function.

                                              • right_inv : Function.RightInverse self.invFun (self.toLieModuleHom).toFun

                                                The inverse function of an equivalence of Lie modules is a right inverse of the underlying function.

                                              Instances For
                                                theorem LieModuleEquiv.left_inv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (self : M ≃ₗ⁅R,L N) :
                                                Function.LeftInverse self.invFun (self.toLieModuleHom).toFun

                                                The inverse function of an equivalence of Lie modules is a left inverse of the underlying function.

                                                theorem LieModuleEquiv.right_inv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (self : M ≃ₗ⁅R,L N) :
                                                Function.RightInverse self.invFun (self.toLieModuleHom).toFun

                                                The inverse function of an equivalence of Lie modules is a right inverse of the underlying function.

                                                An equivalence of Lie algebra modules is a linear equivalence which is also a morphism of Lie algebra modules.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def LieModuleEquiv.toLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :

                                                  View an equivalence of Lie modules as a linear equivalence.

                                                  Equations
                                                  • e.toLinearEquiv = { toLinearMap := e.toLieModuleHom, invFun := e.invFun, left_inv := , right_inv := }
                                                  Instances For
                                                    def LieModuleEquiv.toEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                    M N

                                                    View an equivalence of Lie modules as a type level equivalence.

                                                    Equations
                                                    • e.toEquiv = { toFun := (e.toLieModuleHom).toFun, invFun := e.invFun, left_inv := , right_inv := }
                                                    Instances For
                                                      instance LieModuleEquiv.hasCoeToEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                      CoeOut (M ≃ₗ⁅R,L N) (M N)
                                                      Equations
                                                      • LieModuleEquiv.hasCoeToEquiv = { coe := LieModuleEquiv.toEquiv }
                                                      instance LieModuleEquiv.hasCoeToLieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                      Equations
                                                      • LieModuleEquiv.hasCoeToLieModuleHom = { coe := LieModuleEquiv.toLieModuleHom }
                                                      instance LieModuleEquiv.hasCoeToLinearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                      Equations
                                                      • LieModuleEquiv.hasCoeToLinearEquiv = { coe := LieModuleEquiv.toLinearEquiv }
                                                      instance LieModuleEquiv.instEquivLike {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                      Equations
                                                      • LieModuleEquiv.instEquivLike = { coe := fun (f : M ≃ₗ⁅R,L N) => (f.toLieModuleHom).toFun, inv := fun (f : M ≃ₗ⁅R,L N) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                                                      @[simp]
                                                      theorem LieModuleEquiv.coe_coe {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                      e.toLieModuleHom = e
                                                      theorem LieModuleEquiv.injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                      theorem LieModuleEquiv.surjective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                      @[simp]
                                                      theorem LieModuleEquiv.toEquiv_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (g : NM) (h₁ : Function.LeftInverse g (f).toFun) (h₂ : Function.RightInverse g (f).toFun) :
                                                      { toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toEquiv = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }
                                                      @[simp]
                                                      theorem LieModuleEquiv.coe_mk {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (f : M →ₗ⁅R,L N) (invFun : NM) (h₁ : Function.LeftInverse invFun (f).toFun) (h₂ : Function.RightInverse invFun (f).toFun) :
                                                      { toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ } = f
                                                      theorem LieModuleEquiv.coe_to_lieModuleHom {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                      e.toLieModuleHom = e
                                                      @[simp]
                                                      theorem LieModuleEquiv.coe_to_linearEquiv {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                      e.toLinearEquiv = e
                                                      theorem LieModuleEquiv.toEquiv_injective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                      Function.Injective LieModuleEquiv.toEquiv
                                                      theorem LieModuleEquiv.ext {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e₁ : M ≃ₗ⁅R,L N) (e₂ : M ≃ₗ⁅R,L N) (h : ∀ (m : M), e₁ m = e₂ m) :
                                                      e₁ = e₂
                                                      instance LieModuleEquiv.instOne {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :
                                                      Equations
                                                      • LieModuleEquiv.instOne = { one := let __src := 1; { toLinearMap := __src, map_lie' := , invFun := __src.invFun, left_inv := , right_inv := } }
                                                      @[simp]
                                                      theorem LieModuleEquiv.one_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) :
                                                      1 m = m
                                                      instance LieModuleEquiv.instInhabited {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :
                                                      Equations
                                                      • LieModuleEquiv.instInhabited = { default := 1 }
                                                      def LieModuleEquiv.refl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

                                                      Lie module equivalences are reflexive.

                                                      Equations
                                                      • LieModuleEquiv.refl = 1
                                                      Instances For
                                                        @[simp]
                                                        theorem LieModuleEquiv.refl_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) :
                                                        LieModuleEquiv.refl m = m
                                                        def LieModuleEquiv.symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :

                                                        Lie module equivalences are symmetric.

                                                        Equations
                                                        • e.symm = let __src := e.inverse e.invFun ; let __src_1 := e.toLinearEquiv.symm; { toLieModuleHom := __src, invFun := __src_1.invFun, left_inv := , right_inv := }
                                                        Instances For
                                                          @[simp]
                                                          theorem LieModuleEquiv.apply_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) (x : N) :
                                                          e (e.symm x) = x
                                                          @[simp]
                                                          theorem LieModuleEquiv.symm_apply_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) (x : M) :
                                                          e.symm (e x) = x
                                                          theorem LieModuleEquiv.apply_eq_iff_eq_symm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] {m : M} {n : N} (e : M ≃ₗ⁅R,L N) :
                                                          e m = n m = e.symm n
                                                          @[simp]
                                                          theorem LieModuleEquiv.symm_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                          e.symm.symm = e
                                                          theorem LieModuleEquiv.symm_bijective {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] :
                                                          Function.Bijective LieModuleEquiv.symm
                                                          def LieModuleEquiv.trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) :

                                                          Lie module equivalences are transitive.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem LieModuleEquiv.trans_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) (m : M) :
                                                            (e₁.trans e₂) m = e₂ (e₁ m)
                                                            @[simp]
                                                            theorem LieModuleEquiv.symm_trans {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] [LieRingModule L M] [LieRingModule L N] [LieRingModule L P] (e₁ : M ≃ₗ⁅R,L N) (e₂ : N ≃ₗ⁅R,L P) :
                                                            (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
                                                            @[simp]
                                                            theorem LieModuleEquiv.self_trans_symm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                            e.trans e.symm = LieModuleEquiv.refl
                                                            @[simp]
                                                            theorem LieModuleEquiv.symm_trans_self {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [LieRingModule L M] [LieRingModule L N] (e : M ≃ₗ⁅R,L N) :
                                                            e.symm.trans e = LieModuleEquiv.refl