English
For K with H ≤ K ≤ H.normalizer, there exists a LieIdeal I of K such that the LieSubalgebra I equals ofLe H ≤ K.
Русский
Для K с условием H ≤ K ≤ H.normalizer существуют I ∈ LieIdeal(K) такие, что I как подалгебра равен подпредсталению H внутри K.
LaTeX
$${K : LieSubalgebra R L} (h1 : H ≤ K) (h2 : K ≤ H.normalizer) : ∃ I : LieIdeal R K, (I : LieSubalgebra R K) = ofLe h1$$
Lean4
theorem lie_mem_sup_of_mem_normalizer {x y z : L} (hx : x ∈ H.normalizer) (hy : y ∈ (R ∙ x) ⊔ ↑H)
(hz : z ∈ (R ∙ x) ⊔ ↑H) : ⁅y, z⁆ ∈ (R ∙ x) ⊔ ↑H :=
by
rw [Submodule.mem_sup] at hy hz
obtain ⟨u₁, hu₁, v, hv : v ∈ H, rfl⟩ := hy
obtain ⟨u₂, hu₂, w, hw : w ∈ H, rfl⟩ := hz
obtain ⟨t, rfl⟩ := Submodule.mem_span_singleton.mp hu₁
obtain ⟨s, rfl⟩ := Submodule.mem_span_singleton.mp hu₂
apply Submodule.mem_sup_right
simp only [LieSubalgebra.mem_toSubmodule, smul_lie, add_lie, zero_add, lie_add, smul_zero, lie_smul, lie_self]
refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))
exacts [(H.mem_normalizer_iff' x).mp hx v hv, (H.mem_normalizer_iff x).mp hx w hw]
