Endomorphisms preserving a submodule family and their centralizer

For a family of submodules, the family-invariant endomorphisms are those preserving each member. An automorphism permuting the family preserves this space under conjugation. Over a field, if one member is disjoint from the sum of the others, every subspace of that member is the range of a family-invariant projection. Consequently an automorphism commuting with the scalar extensions of all family-invariant endomorphisms preserves the scalar extension of every such subspace.

The scalar-extension statement allows arbitrary coefficient algebras, including nonreduced ones. It supplies the linear-algebra step in the normal-subgroup kernel argument: subgroup points act by scalars on character spaces, and centralizing their family-invariant endomorphisms forces preservation of a Chevalley line inside one character space.

The construction uses Mathlib's Submodule.compatibleMaps, Submodule.projection, and LinearMap.IsIdempotentElem.commute_iff_of_isUnit.

References

• J. E. Humphreys, Linear Algebraic Groups, §11.5.
• A. Borel, Linear Algebraic Groups, §5.5.

def Submodule.familyInvariant {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] (S : ι → Submodule R V) : Submodule R (Module.End R V)

The endomorphisms preserving every submodule in a family. For a direct-sum decomposition, these are exactly the block-diagonal endomorphisms.

Equations

• Submodule.familyInvariant S = ⨅ (i : ι), (S i).compatibleMaps (S i)

@[simp]

theorem Submodule.mem_familyInvariant {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] {S : ι → Submodule R V} {f : Module.End R V} : f ∈ familyInvariant S ↔ ∀ (i : ι), ∀ v ∈ S i, f v ∈ S i

A family-invariant endomorphism preserves each member.

theorem Submodule.mul_mem_familyInvariant {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] {S : ι → Submodule R V} {f g : Module.End R V} (hf : f ∈ familyInvariant S) (hg : g ∈ familyInvariant S) : f * g ∈ familyInvariant S

Family-invariant endomorphisms are closed under composition.

theorem Submodule.conj_mem_familyInvariant {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] (S : ι → Submodule R V) (e : V ≃ₗ[R] V) (σ : Equiv.Perm ι) (he : ∀ (i : ι), map (↑e) (S i) = S (σ i)) {f : Module.End R V} (hf : f ∈ familyInvariant S) : (LinearEquiv.conjAlgEquiv R e) f ∈ familyInvariant S

Conjugation by an automorphism permuting the family preserves family-invariant endomorphisms. No independence or spanning assumption is needed.

theorem Submodule.map_conj_familyInvariant {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] (S : ι → Submodule R V) (e : V ≃ₗ[R] V) (σ : Equiv.Perm ι) (he : ∀ (i : ι), map (↑e) (S i) = S (σ i)) : map (LinearEquiv.conjAlgEquiv R e).toLinearMap (familyInvariant S) = familyInvariant S

An automorphism permuting the family maps the space of family-invariant endomorphisms onto itself under conjugation.

theorem Submodule.commute_baseChange_of_forall_tmul_eq_smul {R : Type u_1} {V : Type u_2} {ι : Type u_3} [CommSemiring R] [AddCommMonoid V] [Module R V] {A : Type u_4} [Semiring A] [Algebra R A] (S : ι → Submodule R V) (hS : ⨆ (i : ι), S i = ⊤) (T : Module.End A (TensorProduct R A V)) (c : ι → A) (hT : ∀ (i : ι), ∀ v ∈ S i, T (1 ⊗ₜ[R] v) = c i • 1 ⊗ₜ[R] v) {f : Module.End R V} (hf : f ∈ familyInvariant S) : Commute T (LinearMap.baseChange A f)

If an operator acts by a scalar on each member of a spanning family, it commutes with every scalar-extended family-invariant endomorphism. The scalars may belong to the coefficient algebra; no independence or finiteness of the family is needed.

theorem Submodule.exists_projection_mem_familyInvariant {k : Type u_1} {V : Type u_2} {ι : Type u_3} [Field k] [AddCommGroup V] [Module k V] (S : ι → Submodule k V) (i : ι) (hS : Disjoint (S i) (⨆ (j : ι), ⨆ (_ : j ≠ i), S j)) (L : Submodule k V) (hL : L ≤ S i) : ∃ p ∈ familyInvariant S, IsIdempotentElem p ∧ LinearMap.range p = L

Every subspace of a family member disjoint from the sum of the other members is the range of a family-invariant idempotent, even when the family does not span the ambient space.

theorem Submodule.map_baseChange_eq_of_forall_commute_familyInvariant {k : Type u_1} {V : Type u_2} {ι : Type u_3} [Field k] [AddCommGroup V] [Module k V] {A : Type u_4} [Ring A] [Algebra k A] (S : ι → Submodule k V) (i : ι) (hS : Disjoint (S i) (⨆ (j : ι), ⨆ (_ : j ≠ i), S j)) (L : Submodule k V) (hL : L ≤ S i) (e : TensorProduct k A V ≃ₗ[A] TensorProduct k A V) (he : ∀ p ∈ familyInvariant S, Commute (↑e) (LinearMap.baseChange A p)) : map (↑e) (baseChange A L) = baseChange A L

An automorphism commuting with every scalar-extended family-invariant endomorphism preserves any scalar-extended subspace of a family member disjoint from the sum of the other members. This tests arbitrary algebra-valued automorphisms rather than just rational points.