Eigenspaces of complex structures

This file records the eigenspace decomposition of an endomorphism f whose square is negative one. When the scalars contain a square root i of -1 and 2 is invertible, the module is the direct sum of the i- and -i-eigenspaces of f. These are the two complementary pieces used in complex-structure and Hodge decompositions, where the scalars are ℂ and i = Complex.I. The projections onto the i- and -i-eigenspaces are explicitly (1 - i f) / 2 and (1 + i f) / 2, fixing the normalization used in complex tangent type decompositions.

Main declarations

• Module.End.isCompl_eigenspace_eigenspace_neg_of_comp_self_eq_neg_id: the i- and -i-eigenspaces of an endomorphism squaring to -1 are complementary.
• Module.End.projection_eigenspace_eigenspace_neg_apply and Module.End.projection_eigenspace_neg_eigenspace_apply: the explicit formulas for the native projections onto the two eigenspaces.

theorem Module.End.isCompl_eigenspace_eigenspace_neg_of_comp_self_eq_neg_id {K : Type u} {W : Type v} [CommRing K] [AddCommGroup W] [Module K W] {i : K} (h2 : IsUnit 2) (hi : i * i = -1) (f : End K W) (hf : f ∘ₗ f = -LinearMap.id) : IsCompl (f.eigenspace i) (f.eigenspace (-i))

If 2 is a unit and i is a square root of -1, the i- and -i-eigenspaces of an endomorphism squaring to -1 are complementary.

theorem Module.End.projection_eigenspace_eigenspace_neg_apply {K : Type u} {W : Type v} [CommRing K] [AddCommGroup W] [Module K W] {i : K} (h2 : IsUnit 2) (hi : i * i = -1) (f : End K W) (hf : f ∘ₗ f = -LinearMap.id) (x : W) : ((f.eigenspace i).projection (f.eigenspace (-i)) ⋯) x = ↑h2.unit⁻¹ • (x - i • f x)

The projection onto the i-eigenspace of a complex structure along its -i-eigenspace is the explicit operator (1 - i f) / 2, with 1 / 2 the inverse of the unit 2.

theorem Module.End.projection_eigenspace_neg_eigenspace_apply {K : Type u} {W : Type v} [CommRing K] [AddCommGroup W] [Module K W] {i : K} (h2 : IsUnit 2) (hi : i * i = -1) (f : End K W) (hf : f ∘ₗ f = -LinearMap.id) (x : W) : ((f.eigenspace (-i)).projection (f.eigenspace i) ⋯) x = ↑h2.unit⁻¹ • (x + i • f x)

The projection onto the -i-eigenspace of a complex structure along its i-eigenspace is the explicit operator (1 + i f) / 2, with 1 / 2 the inverse of the unit 2.