English
If a Lie algebra L is Killing and L' is Lie algebra isomorphic to L, then L' is Killing as well.
Русский
Если Ли‑алгебра L является Killing, и L' изоморфна L как Ли‑алгебра, то L' тоже является Killing.
LaTeX
$$IsKilling(R, L')$$
Lean4
/-- Given a Killing Lie algebra `L`, if `L'` is isomorphic to `L`, then `L'` is Killing too. -/
theorem isKilling_of_equiv [IsKilling R L] (e : L ≃ₗ⁅R⁆ L') : IsKilling R L' :=
by
constructor
ext x'
simp_rw [LieIdeal.mem_killingCompl, LieModule.traceForm_comm]
refine ⟨fun hx' ↦ ?_, fun hx y _ ↦ hx ▸ LinearMap.map_zero₂ (killingForm R L') y⟩
suffices e.symm x' ∈ LinearMap.ker (killingForm R L)
by
rw [IsKilling.ker_killingForm_eq_bot] at this
simpa [map_zero] using (e : L ≃ₗ[R] L').congr_arg this
ext y
replace hx' : ∀ y', killingForm R L' x' y' = 0 := by simpa using hx'
specialize hx' (e y)
rwa [← e.apply_symm_apply x', killingForm_of_equiv_apply] at hx'
