Eigenspaces of anticommuting endomorphisms

Let f and g be endomorphisms of a module with f * g + g * f = 0. Then (f + μ) g = -g (f - μ), so g carries the generalized μ-eigenspace of f into its generalized -μ-eigenspace, for every exponent. When g = e is invertible, its inverse also anticommutes with f, and e identifies the two generalized eigenspaces, which therefore have equal finrank. In particular, for a finite-dimensional vector space over a field, the eigenvalues of f come in pairs ±μ with equal geometric and algebraic multiplicities, and e preserves every generalized eigenspace of f at 0.

The basic example is a shape operator S of a complex submanifold, which anticommutes with the complex structure J: its principal curvatures come in pairs ±κ.

Main declarations

• Module.End.genEigenspace_neg: the generalized eigenspaces of -f are those of f at the negated eigenvalue.
• Module.End.genEigenspace_smul: over a field, the generalized eigenspaces of t • f for t ≠ 0 are those of f at the rescaled eigenvalue.
• Module.End.mapsTo_genEigenspace_neg_of_anticommute: an endomorphism anticommuting with f maps the generalized μ-eigenspace of f into its generalized -μ-eigenspace.
• Module.End.map_genEigenspace_of_anticommute: for an invertible such endomorphism this is an equality of submodules.
• Module.End.genEigenspaceEquivOfAnticommute: the induced linear equivalence between the generalized μ- and -μ-eigenspaces.
• Module.End.finrank_genEigenspace_neg_of_anticommute: the two generalized eigenspaces have the same dimension.
• Module.End.hasUnifEigenvalue_neg_iff_of_anticommute: -μ is a (generalized) eigenvalue exactly when μ is.

References

• J. Milnor, Morse Theory, Princeton University Press, 1963, Section 7.

@[simp]

theorem Module.End.genEigenspace_neg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : End R M) (μ : R) (k : ℕ∞) : ((-f).genEigenspace μ) k = (f.genEigenspace (-μ)) k

The generalized eigenspaces of -f are the generalized eigenspaces of f at the negated eigenvalue.

theorem Module.End.genEigenspace_smul {K : Type u_3} {V : Type u_4} [Field K] [AddCommGroup V] [Module K V] (f : End K V) {t : K} (ht : t ≠ 0) (μ : K) (k : ℕ∞) : ((t • f).genEigenspace μ) k = (f.genEigenspace (t⁻¹ * μ)) k

Over a field, the generalized eigenspaces of a nonzero multiple t • f are the generalized eigenspaces of f at the eigenvalue divided by t.

theorem Module.End.mapsTo_genEigenspace_neg_of_anticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f g : End R M} (h : f * g + g * f = 0) (μ : R) (k : ℕ∞) : Set.MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace (-μ)) k)

An endomorphism g anticommuting with f maps the generalized μ-eigenspace of f into its generalized -μ-eigenspace.

theorem Module.End.mul_symm_add_symm_mul_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} {e : M ≃ₗ[R] M} (h : f * ↑e + ↑e * f = 0) : f * ↑e.symm + ↑e.symm * f = 0

The inverse of an invertible endomorphism anticommuting with f also anticommutes with f.

theorem Module.End.map_genEigenspace_of_anticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) (μ : R) (k : ℕ∞) : Submodule.map (↑e) ((f.genEigenspace μ) k) = (f.genEigenspace (-μ)) k

An invertible endomorphism e anticommuting with f maps the generalized μ-eigenspace of f onto its generalized -μ-eigenspace.

def Module.End.genEigenspaceEquivOfAnticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) (μ : R) (k : ℕ∞) : ↥((f.genEigenspace μ) k) ≃ₗ[R] ↥((f.genEigenspace (-μ)) k)

An invertible endomorphism e anticommuting with f restricts to a linear equivalence between the generalized μ- and -μ-eigenspaces of f.

@[simp]

theorem Module.End.coe_genEigenspaceEquivOfAnticommute_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) (μ : R) (k : ℕ∞) (x : ↥((f.genEigenspace μ) k)) : ↑((genEigenspaceEquivOfAnticommute e h μ k) x) = e ↑x

@[simp]

theorem Module.End.coe_genEigenspaceEquivOfAnticommute_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) (μ : R) (k : ℕ∞) (x : ↥((f.genEigenspace (-μ)) k)) : ↑((genEigenspaceEquivOfAnticommute e h μ k).symm x) = e.symm ↑x

theorem Module.End.finrank_genEigenspace_neg_of_anticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) (μ : R) (k : ℕ∞) : finrank R ↥((f.genEigenspace (-μ)) k) = finrank R ↥((f.genEigenspace μ) k)

If an invertible endomorphism anticommutes with f, the generalized μ- and -μ-eigenspaces of f have the same finrank. For a finite-dimensional vector space over a field, these are the geometric multiplicities of μ and -μ when k = 1, and their algebraic multiplicities when k = ⊤.

theorem Module.End.hasUnifEigenvalue_neg_iff_of_anticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) {μ : R} {k : ℕ∞} : f.HasUnifEigenvalue (-μ) k ↔ f.HasUnifEigenvalue μ k

If an invertible endomorphism anticommutes with f, then -μ is a generalized eigenvalue of f exactly when μ is.

theorem Module.End.hasEigenvalue_neg_iff_of_anticommute {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : End R M} (e : M ≃ₗ[R] M) (h : f * ↑e + ↑e * f = 0) {μ : R} : f.HasEigenvalue (-μ) ↔ f.HasEigenvalue μ

If an invertible endomorphism anticommutes with f, then -μ is an eigenvalue of f exactly when μ is.