Similarity invariants of linear maps

TheoremCharacteristic polynomial of a rank-two endomorphism#✓fully proved

The characteristic polynomial of an endomorphism of a free rank-two module is X² - tr f · X + det f, the familiar quadratic formula.

theorem LinearMap.charpoly_of_finrank_eq_two {R : Type*} {M : Type*} [CommRing R]
    [Nontrivial R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
    (h : Module.finrank R M = 2) (f : M →ₗ[R] M) :
    f.charpoly = Polynomial.X ^ 2 - Polynomial.C (LinearMap.trace R M f)
      * Polynomial.X + Polynomial.C (LinearMap.det f)

TheoremTrace and determinant are invariant under semiconjugacy#✓fully proved

Trace and determinant are preserved under semiconjugacy: if e intertwines f and g, then g is the conjugate of f by e, so both invariants agree.

theorem LinearMap.trace_eq_and_det_eq_of_semiconj {R : Type*} {M : Type*} {N : Type*}
    [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    (e : M ≃ₗ[R] N) (f : Module.End R M) (g : Module.End R N)
    (h : ∀ x : M, e (f x) = g (e x)) :
    LinearMap.trace R M f = LinearMap.trace R N g ∧ LinearMap.det f = LinearMap.det g

TheoremKernel of the dual map has the same dimension as the kernel#✓fully proved

The kernel of the dual map has the same finite dimension as the kernel: both are complementary to the range, by rank-nullity and the dual-annihilator dimension formula.

theorem LinearMap.finrank_ker_dualMap_eq_finrank_ker {K V : Type*} [Field K]
    [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : V →ₗ[K] V) :
    Module.finrank K (LinearMap.ker f.dualMap) = Module.finrank K (LinearMap.ker f)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.