class LieModule.HasNondegenerateTraceForm (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] : Prop

{name}IsKilling の Lie 加群バージョン

• nondegenerate_traceForm : (traceForm R L M).Nondegenerate

theorem LieModule.hasNondegenerateTraceForm_def (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] : HasNondegenerateTraceForm R L M ↔ (traceForm R L M).Nondegenerate

noncomputable def LieIdeal.traceCompl (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) : LieIdeal R L

{name}killingCompl の Lie 加群バージョン

Equations

• LieIdeal.traceCompl R L M I = LieAlgebra.InvariantForm.orthogonal (LieModule.traceForm R L M) ⋯ I

@[simp]

theorem LieIdeal.mem_traceCompl {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} {x : L} : x ∈ traceCompl R L M I ↔ ∀ y ∈ I, ((LieModule.traceForm R L M) y) x = 0

@[simp]

theorem LieIdeal.traceCompl_eq_killingCompl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : traceCompl R L L I = killingCompl R L I

theorem LieModule.hasNondegenerateTraceForm_iff_traceCompl_top_eq_bot {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] : HasNondegenerateTraceForm R L M ↔ LieIdeal.traceCompl R L M ⊤ = ⊥

@[simp]

theorem LieModule.hasNondegenerateTraceForm_iff_isKilling {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : HasNondegenerateTraceForm R L L ↔ LieAlgebra.IsKilling R L

instance LieModule.instHasNondegenerateTraceFormOfIsKilling {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsKilling R L] : HasNondegenerateTraceForm R L L

instance LieModule.instHasNondegenerateTraceFormOfCharZeroOfIsDomainOfIsNoetherianOfFreeOfHasTrivialRadicalOfIsFaithful {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] [CharZero R] [IsDomain R] [IsNoetherian R M] [Module.Free R M] [LieAlgebra.HasTrivialRadical R L] [IsFaithful R L M] : HasNondegenerateTraceForm R L M

instance LieAlgebra.instIsKillingOfHasNondegenerateTraceForm {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieModule.HasNondegenerateTraceForm R L L] : IsKilling R L