@[instance_reducible]

def Function.Injective.lieRingModule (L : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [LieRing L] [Bracket L M₁] [AddCommGroup M₁] [AddCommGroup M₂] [LieRingModule L M₂] (f : M₁ →+ M₂) (hf : Injective ⇑f) (bracket : ∀ (x : L) (m : M₁), f ⁅x, m⁆ = ⁅x, f m⁆) : LieRingModule L M₁

Equations

• Function.Injective.lieRingModule L f hf bracket = { toBracket := inst✝³, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

theorem Function.Injective.lieModule (R : Type u_1) (L : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₁] [LieRingModule L M₂] [LieModule R L M₂] (f : M₁ →ₗ[R] M₂) (hf : Injective ⇑f) (bracket : ∀ (x : L) (m : M₁), f ⁅x, m⁆ = ⁅x, f m⁆) : LieModule R L M₁

@[instance_reducible]

def AddEquiv.lieRingModule (L : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [LieRing L] [AddCommGroup M₁] [AddCommGroup M₂] [LieRingModule L M₂] (e : M₁ ≃+ M₂) : LieRingModule L M₁

Equations

• AddEquiv.lieRingModule L e = Function.Injective.lieRingModule L e.toAddMonoidHom ⋯ ⋯

theorem LinearEquiv.lieModule (R : Type u_1) (L : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (e : M₁ ≃ₗ[R] M₂) : LieModule R L M₁

def LinearEquiv.lieModuleEquiv (R : Type u_1) (L : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (e : M₁ ≃ₗ[R] M₂) : M₁ ≃ₗ⁅R,L⁆ M₂

Equations

• LinearEquiv.lieModuleEquiv R L e = { toLinearMap := ↑e, map_lie' := ⋯, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }

theorem Function.Injective.isFaithful {R : Type u_1} {L : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₁] [LieRingModule L M₂] [LieModule R L M₁] [LieModule R L M₂] [LieModule.IsFaithful R L M₁] (f : M₁ →ₗ⁅R,L⁆ M₂) (hf : Injective ⇑f) : LieModule.IsFaithful R L M₂

instance instIsFaithfulSubtypeMemLieIdeal_ado {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₁] (I : LieIdeal R L) [LieModule.IsFaithful R L M₁] : LieModule.IsFaithful R (↥I) M₁

theorem LieModuleEquiv.isFaithful_iff {R : Type u_1} {L : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₁] [LieRingModule L M₂] [LieModule R L M₁] [LieModule R L M₂] (e : M₁ ≃ₗ⁅R,L⁆ M₂) : LieModule.IsFaithful R L M₁ ↔ LieModule.IsFaithful R L M₂

@[simp]

theorem LieModuleEquiv.map_lie {R : Type u_1} {L : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₁] [LieRingModule L M₂] (e : M₁ ≃ₗ⁅R,L⁆ M₂) (x : L) (m : M₁) : e ⁅x, m⁆ = ⁅x, e m⁆

theorem LieModuleEquiv.isNilpotent_iff {R : Type u_1} {L : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [LieRingModule L M₁] [LieRingModule L M₂] [LieModule R L M₁] [LieModule R L M₂] (e : M₁ ≃ₗ⁅R,L⁆ M₂) : LieModule.IsNilpotent L M₁ ↔ LieModule.IsNilpotent L M₂