traceForm_eq_zero_of_mem_ker_of_mem_span_coroot

English

The trace form vanishes on any pair from kernel of α and span of coroot α.

Русский

Трассовая форма обращается в ноль на пары из ядра α и подпространства корота α.

LaTeX

$$traceForm K H L x y = 0$$

Lean4

theorem traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {α : Weight K H L} {x y : H} (hx : x ∈ α.ker)
    (hy : y ∈ K ∙ coroot α) : traceForm K H L x y = 0 :=
  by
  rw [← coe_corootSpace_eq_span_singleton, LieSubmodule.mem_toSubmodule, mem_corootSpace'] at hy
  induction hy using Submodule.span_induction with
  | mem z hz =>
    obtain ⟨u, hu, v, -, huv⟩ := hz
    change killingForm K L (x : L) (z : L) = 0
    replace hx : α x = 0 := by simpa using hx
    rw [← huv, ← traceForm_apply_lie_apply, ← LieSubalgebra.coe_bracket_of_module, lie_eq_smul_of_mem_rootSpace hu, hx,
      zero_smul, map_zero, LinearMap.zero_apply]
  | zero => simp
  | add _ _ _ _ hx hy => simp [hx, hy]
  | smul _ _ _ hz => simp [hz]

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