Fixed vectors of a finite-dimensional representation of p-power order in characteristic p

Let k be a field of exponential characteristic p. The endomorphism algebra of a nonzero k-module has the same exponential characteristic, because k acts faithfully on it, so an operator satisfying f ^ p ^ n = 1 has f - 1 nilpotent (Module.End.isNilpotent_sub_one_of_pow_expChar_pow_eq_one). A representation in which every element acts with p-power order is therefore a representation by unipotent operators, and Kolchin's theorem (Representation.exists_common_fixed_vector_of_isUnipotent) fixes a nonzero vector of a finite-dimensional carrier. No finiteness is asked of the acting monoid, and the corollaries for a p-group hold for an infinite p-group.

This complements TauCeti/RepresentationTheory/PGroupInvariants.lean, which proves the same conclusion for a finite group over a commutative ring of characteristic p with no finiteness hypothesis on the module, by an orbit count rather than by Kolchin's theorem. Neither invariant-vector statement subsumes the other: the results here allow an infinite acting monoid, at the cost of asking the module to be finite-dimensional over a field, while there the module is arbitrary and the group must be finite. The irreducible corollaries here also cover a finite group, since an irreducible representation of a finite group is finite-dimensional (Mathlib's instance on ρ.asModule, read back on V along ρ.asModuleEquiv).

Main results

• Representation.exists_common_fixed_vector_of_forall_pow_expChar_pow_eq_one: a nonzero finite-dimensional representation of a monoid in which every element acts with p-power order, over a field of exponential characteristic p, fixes a nonzero vector, with Representation.exists_fixed_submodule_finrank_eq_one_of_forall_pow_expChar_pow_eq_one its fixed-line form.
• Representation.invariants_ne_bot_of_forall_pow_expChar_pow_eq_one: the submodule form of that fixed vector, for a group.
• Representation.IsIrreducible.eq_trivial_of_forall_pow_expChar_pow_eq_one and Representation.IsIrreducible.finrank_eq_one_of_forall_pow_expChar_pow_eq_one: such a representation is irreducible only if it is the trivial representation on a line.
• Representation.exists_common_fixed_vector_of_isPGroup, Representation.invariants_ne_bot_of_isPGroup, Representation.IsIrreducible.eq_trivial_of_isPGroup and Representation.IsIrreducible.finrank_eq_one_of_isPGroup: the specializations to a p-group, which need not be finite.

References

• A. Borel, Linear Algebraic Groups, §4.8, for Kolchin's theorem.
• J. L. Alperin, Local Representation Theory, Cambridge University Press (1986), for the characteristic-p statement that the trivial module is the only simple module of a p-group.

theorem Representation.forall_isNilpotent_sub_one_of_forall_pow_expChar_pow_eq_one {k : Type u} {H : Type v} {V : Type w} [Field k] [Monoid H] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] (ρ : Representation k H V) (hρ : ∀ (g : H), ∃ (n : ℕ), ρ g ^ p ^ n = 1) (g : H) : IsNilpotent (ρ g - 1)

In exponential characteristic p, a representation in which every element acts with p-power order is a representation by unipotent operators. This is Module.End.isNilpotent_sub_one_of_pow_expChar_pow_eq_one applied to each operator ρ g, and it is the hypothesis Kolchin's theorem consumes.

theorem Representation.exists_common_fixed_vector_of_forall_pow_expChar_pow_eq_one {k : Type u} {H : Type v} {V : Type w} [Field k] [Monoid H] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] [Nontrivial V] (ρ : Representation k H V) (hρ : ∀ (g : H), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ∃ (v : V), v ≠ 0 ∧ ∀ (g : H), (ρ g) v = v

A nonzero finite-dimensional representation in which every element acts with p-power order, over a field of exponential characteristic p, fixes a nonzero vector. It is a representation by unipotent operators, so this is a consequence of Kolchin's theorem (Representation.exists_common_fixed_vector_of_isUnipotent). The acting monoid is arbitrary, in particular it may be infinite, where the orbit-counting Representation.exists_ne_zero_apply_eq_self_of_forall_pow_eq_one asks for a finite group; the price is the finite dimensionality of the carrier, which that theorem does not need.

theorem Representation.exists_fixed_submodule_finrank_eq_one_of_forall_pow_expChar_pow_eq_one {k : Type u} {H : Type v} {V : Type w} [Field k] [Monoid H] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] [Nontrivial V] (ρ : Representation k H V) (hρ : ∀ (g : H), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ∃ (q : Submodule k V), Module.finrank k ↥q = 1 ∧ ∀ (g : H), ∀ y ∈ q, (ρ g) y = y

The fixed-line form of Representation.exists_common_fixed_vector_of_forall_pow_expChar_pow_eq_one: such a representation fixes a line pointwise, the first step of an invariant complete flag.

theorem Representation.invariants_ne_bot_of_forall_pow_expChar_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] [Nontrivial V] (ρ : Representation k G V) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ρ.invariants ≠ ⊥

The submodule form of Representation.exists_common_fixed_vector_of_forall_pow_expChar_pow_eq_one: the invariants of such a representation are nonzero. This is the infinite-group counterpart of Representation.invariants_ne_bot_of_forall_pow_eq_one, which drops the finite dimensionality of the module and asks instead that the group be finite.

theorem Representation.IsIrreducible.eq_trivial_of_forall_pow_expChar_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : ρ = trivial k G V

A finite-dimensional irreducible representation in which every element acts with p-power order, over a field of exponential characteristic p, is the trivial representation. It has a nonzero invariant vector, and a nontrivial irreducible representation has none. The acting group need not be finite; for a finite group the finite dimensionality is automatic (Mathlib's instance on ρ.asModule, read back on V along ρ.asModuleEquiv).

theorem Representation.IsIrreducible.finrank_eq_one_of_forall_pow_expChar_pow_eq_one {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hρ : ∀ (g : G), ∃ (n : ℕ), ρ g ^ p ^ n = 1) : Module.finrank k V = 1

Such an irreducible representation is a line, an irreducible representation of any other dimension having no nonzero invariant vector.

theorem Representation.exists_common_fixed_vector_of_isPGroup {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] [Nontrivial V] (hG : IsPGroup p G) (ρ : Representation k G V) : ∃ (v : V), v ≠ 0 ∧ ∀ (g : G), (ρ g) v = v

A nonzero finite-dimensional representation of a p-group over a field of exponential characteristic p fixes a nonzero vector. The group is not assumed finite.

theorem Representation.invariants_ne_bot_of_isPGroup {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] [Nontrivial V] (hG : IsPGroup p G) (ρ : Representation k G V) : ρ.invariants ≠ ⊥

The submodule form of Representation.exists_common_fixed_vector_of_isPGroup: the invariants of such a representation are nonzero.

theorem Representation.IsIrreducible.eq_trivial_of_isPGroup {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hG : IsPGroup p G) : ρ = trivial k G V

The specialization of Representation.IsIrreducible.eq_trivial_of_forall_pow_expChar_pow_eq_one to a p-group: a finite-dimensional irreducible representation of a p-group in exponential characteristic p is the trivial representation.

theorem Representation.IsIrreducible.finrank_eq_one_of_isPGroup {k : Type u} {G : Type v} {V : Type w} [Field k] [Group G] [AddCommGroup V] [Module k V] {p : ℕ} [ExpChar k p] [FiniteDimensional k V] {ρ : Representation k G V} (h : ρ.IsIrreducible) (hG : IsPGroup p G) : Module.finrank k V = 1

Such an irreducible representation of a p-group is a line.