The index of a linear map

In this file we define the index of a linear map and provide some basic API.

Main definitions / results:

• LinearMap.index: the index of a linear map, with sign convention index = dim ker - dim coker.
• LinearMap.index_comp: the index is additive under composition.

noncomputable def LinearMap.index {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] (f : M →ₗ[R] N) : ℤ

The index of a linear map with sign convention index = dim ker - dim coker.

In the case that either the kernel or cokernel has infinite rank, the value is junk.

Equations

• f.index = ↑(Module.finrank R ↥f.ker) - ↑(Module.finrank R (N ⧸ f.range))

theorem LinearMap.index_eq_finrank_sub {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] {f : M →ₗ[R] N} : f.index = ↑(Module.finrank R ↥f.ker) - ↑(Module.finrank R (N ⧸ f.range))

theorem LinearMap.index_of_subsingleton {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] {f : M →ₗ[R] N} [Subsingleton R] : f.index = 0

@[simp]

theorem LinearMap.index_zero {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] : index 0 = ↑(Module.finrank R M) - ↑(Module.finrank R N)

theorem LinearMap.index_of_injective {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] {f : M →ₗ[R] N} [Nontrivial R] (hf : Function.Injective ⇑f) : f.index = -↑(Module.finrank R (N ⧸ f.range))

@[simp]

theorem LinearMap.index_subtype {M : Type u_1} [AddCommGroup M] {R : Type u_3} [Ring R] [Module R M] [Nontrivial R] {S : Submodule R M} : S.subtype.index = -↑(Module.finrank R (M ⧸ S))

theorem LinearMap.index_of_surjective {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] {f : M →ₗ[R] N} [StrongRankCondition R] (hf : Function.Surjective ⇑f) : f.index = ↑(Module.finrank R ↥f.ker)

@[simp]

theorem LinearMap.index_mkQ {M : Type u_1} [AddCommGroup M] {R : Type u_3} [Ring R] [Module R M] [StrongRankCondition R] {S : Submodule R M} : S.mkQ.index = ↑(Module.finrank R ↥S)

@[simp]

theorem LinearMap.index_projectionOnto {M : Type u_1} [AddCommGroup M] {R : Type u_3} [Ring R] [Module R M] [StrongRankCondition R] {S T : Submodule R M} (hST : IsCompl S T) : (S.projectionOnto T hST).index = ↑(Module.finrank R ↥T)

theorem LinearMap.index_of_bijective {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] {f : M →ₗ[R] N} [StrongRankCondition R] (hf : Function.Bijective ⇑f) : f.index = 0

@[simp]

theorem LinearMap.index_id {M : Type u_1} [AddCommGroup M] {R : Type u_3} [Ring R] [Module R M] [StrongRankCondition R] : id.index = 0

@[simp]

theorem LinearEquiv.index_eq_zero {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {R : Type u_3} [Ring R] [Module R M] [Module R N] [StrongRankCondition R] {e : M ≃ₗ[R] N} : (↑e).index = 0

@[simp]

theorem LinearMap.index_neg {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {k : Type u_3} [DivisionRing k] [Module k M] [Module k N] {f : M →ₗ[k] N} : (-f).index = f.index

theorem LinearMap.index_eq_of_finiteDimensional {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {k : Type u_3} [DivisionRing k] [Module k M] [Module k N] {f : M →ₗ[k] N} [FiniteDimensional k M] [FiniteDimensional k N] : f.index = ↑(Module.finrank k M) - ↑(Module.finrank k N)

@[simp]

theorem LinearMap.index_comp {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {k : Type u_3} [DivisionRing k] [Module k M] [Module k N] {P : Type u_4} [AddCommGroup P] [Module k P] (g : N →ₗ[k] P) (f : M →ₗ[k] N) [FiniteDimensional k ↥f.ker] [FiniteDimensional k ↥g.ker] [FiniteDimensional k (N ⧸ f.range)] [FiniteDimensional k (P ⧸ g.range)] : (g ∘ₗ f).index = g.index + f.index

theorem LinearMap.index_smul {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] {k : Type u_3} [Field k] [Module k M] [Module k N] {f : M →ₗ[k] N} (t : k) (ht : t ≠ 0) : (t • f).index = f.index