Trace on invariant subspaces

TheoremTrace is additive over an invariant subspace#✓fully proved

Let \(V\) be a finite-dimensional vector space over a field \(K\), let \(e\) be a linear endomorphism of \(V\), and let \(W\) be a subspace of \(V\) with \(e(W) \subseteq W\). Then the trace of \(e\) equals the trace of the restriction \(e|_W\) of \(e\) to \(W\) plus the trace of the endomorphism \(\bar e\) of the quotient \(V/W\) induced by \(e\): \(\operatorname{tr}(e) = \operatorname{tr}(e|_W) + \operatorname{tr}(\bar e)\).

theorem LinearMap.trace_eq_trace_restrict_add_trace_mapQ
    (W : Submodule K V) (e : V →ₗ[K] V) (he : W ≤ W.comap e) :
    LinearMap.trace K V e =
      LinearMap.trace K W (e.restrict he) +
        LinearMap.trace K (V ⧸ W) (W.mapQ W e he)

Used by 1

Used byTrace splits along a surjective intertwining map

TheoremTrace splits along a surjective intertwining map#✓fully proved

Let \(V\) be a finite-dimensional vector space over a field \(K\), let \(W\) be a vector space over \(K\), and let \(q : V \to W\) be a surjective linear map. If \(f\) is a linear endomorphism of \(V\) and \(g\) a linear endomorphism of \(W\) with \(q \circ f = g \circ q\), then \(f\) maps \(\ker q\) into itself, and the trace of \(f\) equals the trace of the restriction \(f|_{\ker q}\) of \(f\) to \(\ker q\) plus the trace of \(g\).

theorem LinearMap.trace_eq_trace_restrict_ker_add_of_surjective
    (q : V →ₗ[K] W) (f : V →ₗ[K] V) (g : W →ₗ[K] W)
    (hq : Function.Surjective q) (h : q.comp f = g.comp q) :
    LinearMap.trace K V f =
      LinearMap.trace K (LinearMap.ker q)
        (f.restrict (by
          change LinearMap.ker q ≤ (LinearMap.ker q).comap f
          rw [← LinearMap.ker_comp f q, h]
          exact LinearMap.ker_le_ker_comp q g)) +
      LinearMap.trace K W g

Uses 1 · Used by 1

Proof usesTrace is additive over an invariant subspace

Used byOne-step trace recurrence for the maximal-ideal-power quotients

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.