Theorems · Theorem · linear algebra

LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup

∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [∀ (i : ι), Module.Finite R ↥(N i)] [∀ (i : ι), Module.Free R ↥(N i)] (s : Finset ι),
  (iSupIndep fun i => N ↑i) →
    ∀ {f : Module.End R M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)) (p : Submodule R M) (hp : p = ⨆ i ∈ s, N i)
      (hp' : optParam (Set.MapsTo ⇑f ↑p ↑p) ⋯),
      (LinearMap.trace R ↥p) (LinearMap.restrict f hp') = ∑ i ∈ s, (LinearMap.trace R ↥(N i)) (LinearMap.restrict f ⋯)

The trace of an endomorphism of a direct sum is the sum of the traces on each component. Note that it is important the statement gives the user definitional control over p since the _type_ of the term trace R p (f.restrict hp') depends on p.

Defined in

Mathlib.Algebra.DirectSum.LinearMap

Cited by

1 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleModule.FiniteModule.Free