def LieAlgebra.nilradical (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieIdeal R L

注意: これは {name}maxNilpotentIdeal とは異なります。{name}maxNilpotentIdeal は最大の {name}L-冪零イデアル ですが、 {given -show}𝔫{lean}nilradical R L = 𝔫 は最大の {name}𝔫-冪零イデアルです。

Equations

• LieAlgebra.nilradical R L = sSup {N : LieIdeal R L | LieRing.IsNilpotent ↥N}

instance LieRing.instIsNilpotentSubtypeMemLieIdealNilradicalOfIsNoetherian {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : IsNilpotent ↥(LieAlgebra.nilradical R L)

@[simp]

theorem LieAlgebra.nilradical_eq_top_of_isNilpotent {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] : nilradical R L = ⊤

@[simp]

theorem LieAlgebra.map_equiv_nilradical {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieIdeal.map e.toLieHom (nilradical R L) = nilradical R L₂

@[simp]

theorem LieAlgebra.comap_equiv_nilradical {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieIdeal.comap e.toLieHom (nilradical R L₂) = nilradical R L

theorem LieAlgebra.center_le_nilradical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : center R L ≤ nilradical R L

theorem LieAlgebra.nilradical_le_radical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : nilradical R L ≤ radical R L

theorem LieIdeal.isNilpotent_iff_le_nilradical {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] (I : LieIdeal R L) : LieRing.IsNilpotent ↥I ↔ I ≤ LieAlgebra.nilradical R L