exists_nested_lieIdeal_ofLe_normalizer

English

The idealizer of a Lie submodule N is the LieIdeal of L defined by {x ∈ L | ∀ m ∈ M, [x,m] ∈ N}.

Русский

Идеалайзер подмодуля Ли N — это Ли-идеал L, задаваемый как {x ∈ L | ∀ m ∈ M, [x,m] ∈ N}.

LaTeX

$$$ \\mathrm{idealizer}(N) = \\{ x \\in L \\mid \\forall m \\in M, [x,m] \\in N \\}$$$

Lean4

/-- A Lie subalgebra `H` is an ideal of any Lie subalgebra `K` containing `H` and contained in the
normalizer of `H`. -/
theorem exists_nested_lieIdeal_ofLe_normalizer {K : LieSubalgebra R L} (h₁ : H ≤ K) (h₂ : K ≤ H.normalizer) :
    ∃ I : LieIdeal R K, (I : LieSubalgebra R K) = ofLe h₁ :=
  by
  rw [exists_nested_lieIdeal_coe_eq_iff]
  exact fun x y hx hy => ideal_in_normalizer (h₂ hx) hy

Похожие утверждения