Theorems · Theorem · nonassociative algebras

LieSubmodule.traceForm_eq_zero_of_isTrivial

∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M),
  ∀ I ≤ N.idealizer,
    ∀ (x : L) {y : L},
      y ∈ I →
        ∀ [LieModule.IsTrivial ↥I ↥N],
          (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) = 0

Note that this result is slightly stronger than it might look at first glance: we only assume that N is trivial over I rather than all of L. This means that it applies in the important case of an Abelian ideal (which has M = L and N = I).

Defined in

Mathlib.Algebra.Lie.TraceForm

Cited by

1 results in Mathlib

Foundations

Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleModule.FreeModule.FiniteIsDomainIsPrincipalIdealRingLieModule.IsTrivial