Linear maps between direct sums #
This file contains results about linear maps which respect direct sum decompositions of their domain and codomain.
theorem
LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal'
{ι : Type u_1}
[DecidableEq ι]
{R : Type u_4}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R]
[AddCommMonoid M₁]
[Module R M₁]
{N₁ : ι → Submodule R M₁}
(h₁ : DirectSum.IsInternal N₁)
[AddCommMonoid M₂]
[Module R M₂]
{N₂ : ι → Submodule R M₂}
(h₂ : DirectSum.IsInternal N₂)
{κ₁ : ι → Type u_7}
{κ₂ : ι → Type u_8}
[(i : ι) → Fintype (κ₁ i)]
[(i : ι) → Fintype (κ₂ i)]
[(i : ι) → DecidableEq (κ₁ i)]
[Fintype ι]
(b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i))
(b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i))
{f : M₁ →ₗ[R] M₂}
(hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N₁ i) ↑(N₂ i))
:
(LinearMap.toMatrix (DirectSum.IsInternal.collectedBasis h₁ b₁) (DirectSum.IsInternal.collectedBasis h₂ b₂)) f = Matrix.blockDiagonal' fun (i : ι) =>
(LinearMap.toMatrix (b₁ i) (b₂ i)) (LinearMap.restrict f (_ : Set.MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)))
If a linear map f : M₁ → M₂ respects direct sum decompositions of M₁ and M₂, then it has a
block diagonal matrix with respect to bases compatible with the direct sum decompositions.
theorem
LinearMap.trace_eq_sum_trace_restrict
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
{N : ι → Submodule R M}
[DecidableEq ι]
(h : DirectSum.IsInternal N)
[∀ (i : ι), Module.Finite R ↥(N i)]
[∀ (i : ι), Module.Free R ↥(N i)]
[Fintype ι]
{f : M →ₗ[R] M}
(hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i))
:
(LinearMap.trace R M) f = Finset.sum Finset.univ fun (i : ι) =>
(LinearMap.trace R ↥(N i)) (LinearMap.restrict f (_ : Set.MapsTo ⇑f ↑(N i) ↑(N i)))
theorem
LinearMap.trace_eq_sum_trace_restrict'
{ι : Type u_1}
{R : Type u_2}
{M : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
{N : ι → Submodule R M}
[DecidableEq ι]
(h : DirectSum.IsInternal N)
[∀ (i : ι), Module.Finite R ↥(N i)]
[∀ (i : ι), Module.Free R ↥(N i)]
(hN : Set.Finite {i : ι | N i ≠ ⊥})
{f : M →ₗ[R] M}
(hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i))
:
(LinearMap.trace R M) f = Finset.sum (Set.Finite.toFinset hN) fun (i : ι) =>
(LinearMap.trace R ↥(N i)) (LinearMap.restrict f (_ : Set.MapsTo ⇑f ↑(N i) ↑(N i)))
theorem
LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero
{R : Type u_2}
{M : Type u_3}
[CommRing R]
[AddCommGroup M]
[Module R M]
[IsDomain R]
[IsPrincipalIdealRing R]
[Module.Free R M]
[Module.Finite R M]
{f : Module.End R M}
{g : Module.End R M}
(h_comm : Commute f g)
(hf : ⨆ (μ : R), ⨆ (k : ℕ), (Module.End.generalizedEigenspace f μ) k = ⊤)
(hg : ∀ (μ : R),
(LinearMap.trace R ↥(⨆ (k : ℕ), (Module.End.generalizedEigenspace f μ) k))
(LinearMap.restrict g
(_ :
Set.MapsTo ⇑g ↑(⨆ (k : ℕ), (Module.End.generalizedEigenspace f μ) k)
↑(⨆ (k : ℕ), (Module.End.generalizedEigenspace f μ) k))) = 0)
:
(LinearMap.trace R M) (g ∘ₗ f) = 0
If f and g are commuting endomorphisms of a finite, free R-module M, such that f
is triangularizable, then to prove that the trace of g ∘ f vanishes, it is sufficient to prove
that the trace of g vanishes on each generalized eigenspace of f.