基靈型（Killing form）
/ KILL-ing (after Wilhelm Killing) /
李代數本身沒有長度或角度的概念；單靠括號給不出內積。基靈型由括號本身典範地製造出一個：它詢問代數如何作用於自身。它是附於任何李代數的自然對稱雙線性型，而讀出它的符號差與退化程度，便能診斷最深層的結構事實——代數是否半單、是否緊型、是否有中心。
精確地說，在有限維李代數 g 上定義 B(X, Y) = trace(ad(X) ad(Y))，其中 ad(X) = [X, -] 是 g 的伴隨自同態，跡取自合成線性映射 ad(X) ad(Y): g -> g。此 B 對稱且雙線性，並且是不變的（結合的）：B([X, Y], Z) = B(X, [Y, Z])，以及 Ad-不變，B(Ad(g)X, Ad(g)Y) = B(X, Y)。兩條定理使它成為診斷工具。卡坦半單判準：g 半單，當且僅當 B 非退化（其矩陣行列式非零）。卡坦緊型判準：實半單 g 是某緊群的李代數，當且僅當 B 負定。所以你計算一個跡型，就能得知代數是否剛性（半單），以及它是否積分為緊群。
基靈型是根系、單李代數分類，以及在緊群上構造雙不變度量的主力（取 B 的相反數得到正定不變內積，從而得到雙不變黎曼度量）。誠實提醒：基靈型可能退化（在任何阿貝爾李代數上恆為零，在任何非半單代數上退化），故它並非總是度量。而且它只是「一個」不變型；半單代數可攜帶其他不變雙線性型，不過在「單」代數上，每個不變對稱型都是 B 的純量倍。
對 su(2)，以類包立生成元參數化，使 [e_1, e_2] = e_3（並循環）。則 ad(e_1) 是把 e_2 |-> e_3、e_3 |-> -e_2、e_1 |-> 0 的矩陣，計算得 B(e_i, e_i) = trace(ad(e_i)^2) = -2（對每個 i），且 i != j 時 B(e_i, e_j) = 0。故 B 負定——診斷 su(2) 為半單且緊型，與 SU(2) 緊緻相符。
su(2) 的基靈型負定，證實其為緊型、半單。
基靈型在任何阿貝爾李代數上退化（實為零），故它並非總是內積。B 的非退化恰是半單性的判準級別檢驗（卡坦判準）。