Linear maps of modules with coefficients in a principal ideal domain #
Since a submodule of a free module over a PID is free, certain constructions which are often developed only for vector spaces may be generalised to any module with coefficients in a PID.
This file is a location for such results and exists to avoid making large parts of the linear algebra import hierarchy have to depend on the theory of PIDs.
Main results: #
theorem
LinearMap.trace_restrict_eq_of_forall_mem
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
[Module.Free R M]
[IsDomain R]
[IsPrincipalIdealRing R]
(p : Submodule R M)
(f : M →ₗ[R] M)
(hf : ∀ (x : M), f x ∈ p)
(hf' : optParam (∀ x ∈ p, f x ∈ p) (_ : ∀ x ∈ p, f x ∈ p))
:
(LinearMap.trace R ↥p) (LinearMap.restrict f hf') = (LinearMap.trace R M) f
If a linear endomorphism of a (finite, free) module M takes values in a submodule p ⊆ M,
then the trace of its restriction to p is equal to its trace on M.