English
If x lies in the lower central series and y is central, then traceForm(x,y) = 0.
Русский
Если x лежит в нижнем центральном слое, а y — в центрe, то traceForm(x,y) = 0.
LaTeX
$$$$ \text{traceForm}(x,y) = 0 \quad\text{if } x\in \text{lowerCentralSeries}(R,L,L,1), \ y\in \text{center}(R,L). $$$$
Lean4
@[simp]
theorem traceForm_genWeightSpace_eq [Module.Free R M] [IsDomain R] [IsPrincipalIdealRing R] [LieRing.IsNilpotent L]
[IsNoetherian R M] [LinearWeights R L M] (χ : L → R) (x y : L) :
traceForm R L (genWeightSpace M χ) x y = finrank R (genWeightSpace M χ) • (χ x * χ y) :=
by
set d := finrank R (genWeightSpace M χ)
have h₁ : χ y • d • χ x - χ y • χ x • (d : R) = 0 := by simp [mul_comm (χ x)]
have h₂ : χ x • d • χ y = d • (χ x * χ y) := by simpa [nsmul_eq_mul, smul_eq_mul] using mul_left_comm (χ x) d (χ y)
have := traceForm_eq_zero_of_isNilpotent R L (shiftedGenWeightSpace R L M χ)
replace this := LinearMap.congr_fun (LinearMap.congr_fun this x) y
rwa [LinearMap.zero_apply, LinearMap.zero_apply, traceForm_apply_apply, shiftedGenWeightSpace.toEnd_eq,
shiftedGenWeightSpace.toEnd_eq, ← LinearEquiv.conj_comp, LinearMap.trace_conj', LinearMap.comp_sub,
LinearMap.sub_comp, LinearMap.sub_comp, map_sub, map_sub, map_sub, LinearMap.comp_smul, LinearMap.smul_comp,
LinearMap.comp_id, LinearMap.id_comp, LinearMap.map_smul, LinearMap.map_smul, trace_toEnd_genWeightSpace,
trace_toEnd_genWeightSpace, LinearMap.comp_smul, LinearMap.smul_comp, LinearMap.id_comp, map_smul, map_smul,
LinearMap.trace_id, ← traceForm_apply_apply, h₁, h₂, sub_zero, sub_eq_zero] at this
