traceForm_eq_of_le_idealizer — Mathlib

English

Let N be a LieSubmodule of M and I a LieIdeal of L with h: I ≤ N.idealizer. Then the trace form on I,N equals the restriction of the trace form on L,M to I.

Русский

Пусть N — подмодуль Ли в M, I — Ли-идеал L и h: I ≤ N.idealizer. Тогда форма следа на паре I,N совпадает с ограничением формы следа на L,M к I.

LaTeX

$$$ traceForm\ R\ I\ N = (traceForm\ R\ L\ M).restrict I$$

Lean4

theorem traceForm_eq_of_le_idealizer : traceForm R I N = (traceForm R L M).restrict I :=
  by
  ext ⟨x, hx⟩ ⟨y, hy⟩
  change _ = trace R M (φ x ∘ₗ φ y)
  rw [N.trace_eq_trace_restrict_of_le_idealizer I h x hy]
  rfl

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