Dimensions of common fixed submodules

This file computes the dimension of the common fixed submodule of a finite family of commuting idempotent endomorphisms when each new fixed-point condition has an explicitly equivalent complementary eigenspace. The only input on the scalars is rank-nullity, so the results hold over any ring with HasRankNullity, such as a division ring or a commutative domain.

Main results

• IsIdempotentElem.two_mul_finrank_fixedSubmodule: an idempotent whose fixed submodule is linearly equivalent to its kernel has a fixed submodule of half the dimension.
• LinearMap.finrank_fixedSubmodule_restrict: the fixed submodule of the restriction of f to an invariant submodule p has the dimension of p ⊓ f.fixedSubmodule.
• TauCeti.two_mul_finrank_iInf_fixedSubmodule_insert: adjoining one such idempotent halves the common fixed-space dimension.
• TauCeti.pow_card_mul_finrank_iInf_fixedSubmodule: iterating the construction multiplies the common fixed-space dimension by a power of two.

theorem IsIdempotentElem.two_mul_finrank_fixedSubmodule {K : Type u_1} {W : Type u} [Ring K] [HasRankNullity.{u, u_1} K] [AddCommGroup W] [Module K W] {q : Module.End K W} (hq : IsIdempotentElem q) (e : ↥(LinearMap.fixedSubmodule q) ≃ₗ[K] ↥(LinearMap.ker q)) : 2 * Module.finrank K ↥(LinearMap.fixedSubmodule q) = Module.finrank K W

If the fixed submodule of an idempotent endomorphism q is linearly equivalent to the kernel of q, then it has half the dimension of the space. In infinite dimension both sides are 0.

theorem LinearMap.finrank_fixedSubmodule_restrict {K : Type u_1} {V : Type u_2} [Semiring K] [AddCommMonoid V] [Module K V] {f : V →ₗ[K] V} {p : Submodule K V} (hf : ∀ x ∈ p, f x ∈ p) : Module.finrank K ↥(f.restrict hf).fixedSubmodule = Module.finrank K ↥(p ⊓ f.fixedSubmodule)

If f maps a submodule p into itself, then the fixed submodule of the restriction of f to p has the same dimension as p ⊓ f.fixedSubmodule.

theorem TauCeti.two_mul_finrank_iInf_fixedSubmodule_insert {K : Type u_1} {ι : Type u_2} {V : Type u} [Ring K] [HasRankNullity.{u, u_1} K] [AddCommGroup V] [Module K V] [DecidableEq ι] (p : ι → Module.End K V) (s : Finset ι) (a : ι) (hpa : IsIdempotentElem (p a)) (hcomm : ∀ i ∈ s, Commute (p i) (p a)) (u v : Module.End K V) (huS : ∀ i ∈ s, Commute (p i) u) (hvS : ∀ i ∈ s, Commute (p i) v) (hu0 : ∀ (x : V), (p a) x = x → (p a) (u x) = 0) (hv1 : ∀ (x : V), (p a) x = 0 → (p a) (v x) = v x) (hvu : ∀ (x : V), (p a) x = x → v (u x) = x) (huv : ∀ (x : V), (p a) x = 0 → u (v x) = x) : 2 * Module.finrank K ↥(⨅ i ∈ insert a s, LinearMap.fixedSubmodule (p i)) = Module.finrank K ↥(⨅ i ∈ s, LinearMap.fixedSubmodule (p i))

If two endomorphisms exchange the fixed and zero eigenspaces of an idempotent inside the common fixed space of a commuting family, adjoining that idempotent halves the dimension.

The maps u and v are stated on the ambient module so callers can supply natural operators; the commuting hypotheses ensure that their restrictions preserve the previous common fixed space.

theorem TauCeti.pow_card_mul_finrank_iInf_fixedSubmodule {K : Type u_1} {ι : Type u_2} {V : Type u} [Ring K] [HasRankNullity.{u, u_1} K] [AddCommGroup V] [Module K V] (p : ι → Module.End K V) (t : Finset ι) (hp : ∀ a ∈ t, IsIdempotentElem (p a)) (hcomm : (↑t).Pairwise fun (a b : ι) => Commute (p a) (p b)) (u v : ι → Module.End K V) (huS : ∀ a ∈ t, ∀ i ∈ t, i ≠ a → Commute (p i) (u a)) (hvS : ∀ a ∈ t, ∀ i ∈ t, i ≠ a → Commute (p i) (v a)) (hu0 : ∀ a ∈ t, ∀ (x : V), (p a) x = x → (p a) ((u a) x) = 0) (hv1 : ∀ a ∈ t, ∀ (x : V), (p a) x = 0 → (p a) ((v a) x) = (v a) x) (hvu : ∀ a ∈ t, ∀ (x : V), (p a) x = x → (v a) ((u a) x) = x) (huv : ∀ a ∈ t, ∀ (x : V), (p a) x = 0 → (u a) ((v a) x) = x) : 2 ^ t.card * Module.finrank K ↥(⨅ i ∈ t, LinearMap.fixedSubmodule (p i)) = Module.finrank K V

A finite family of commuting idempotent endomorphisms has common fixed-space dimension 2 ^ (-|t|) times the ambient dimension when each idempotent's fixed and zero pieces are exchanged by inverse endomorphisms that commute with the other idempotents.