Complete reducibility and linear reductivity

An affine group over a field is linearly reductive when every finite-dimensional rational representation is completely reducible. On coordinate rings, rational representations are comodules, and complete reducibility says that every subcomodule has a subcomodule complement.

This file introduces that intrinsic comodule formulation, proves that complete reducibility is invariant under corestriction along a coalgebra equivalence, and proves linear reductivity for every monoid-algebra coalgebra k[G]. The last proof makes an arbitrary linear projection onto a subcomodule equivariant: decompose a vector into its weights, apply the projection separately on each weight, and project the result back to that weight. The resulting idempotent comodule endomorphism has the original subcomodule as its range, so its kernel is an invariant complement.

Complete reducibility also turns a supply of fixed vectors into fixedness of the whole comodule: if every nonzero subcomodule of V contains a nonzero fixed vector, then a subcomodule complement of TauCeti.Comodule.fixedSubcomodule can contain no nonzero fixed vector, hence is zero, hence every vector of V is fixed. Kolchin's theorem supplies such vectors for a unipotent group, so this is the step that makes a linearly reductive unipotent group act trivially.

For an abelian group G, k[G] is the coordinate Hopf algebra of the diagonalizable group D(G). Thus every diagonalizable group, and in particular every split torus, is linearly reductive over an arbitrary field. This is the diagonalizable direction of the linear-reductivity milestone in Layer 6 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.Comodule.IsCompletelyReducible: every subcomodule has a subcomodule complement.
• TauCeti.Comodule.IsCompletelyReducible.of_exists_isCompl and TauCeti.Comodule.IsCompletelyReducible.exists_isCompl: construct and use complete reducibility through complementary subcomodules.
• TauCeti.Subcomodule.projection: the projection onto a subcomodule along a complementary subcomodule, as a comodule endomorphism.
• TauCeti.Comodule.isCompletelyReducible_iff_forall_exists_hom: complete reducibility means that every subcomodule is the image of a comodule endomorphism fixing it pointwise.
• TauCeti.Comodule.isCompletelyReducible_of_forall_eq_bot_or_eq_top: a comodule with no subcomodules other than ⊥ and ⊤ is completely reducible, whence TauCeti.Comodule.isCompletelyReducible_of_subsingleton and TauCeti.Comodule.isCompletelyReducible_of_isSimpleOrder: subsingleton and simple comodules are completely reducible.
• TauCeti.Comodule.fixedSubcomodule_eq_top_of_isCompletelyReducible_of_forall_exists_fixed and TauCeti.Comodule.coact_eq_tmul_one_of_isCompletelyReducible_of_forall_exists_fixed: a completely reducible comodule all of whose nonzero subcomodules contain nonzero fixed vectors is fixed.
• TauCeti.Comodule.isCompletelyReducible_of_orderIso: transfer complete reducibility across compatible order isomorphisms of subcomodules and underlying submodules.
• TauCeti.Comodule.isCompletelyReducible_transport_iff: complete reducibility is invariant under transport along a linear equivalence.
• TauCeti.Coalgebra.IsLinearlyReductive: every finite-dimensional comodule is completely reducible, with constructor TauCeti.Coalgebra.IsLinearlyReductive.of_forall_isCompletelyReducible.
• TauCeti.Coalgebra.IsLinearlyReductive.isCompletelyReducible_sameUniverse: use linear reductivity for a comodule in the carrier universe named by the hypothesis.
• TauCeti.Coalgebra.IsLinearlyReductive.isCompletelyReducible: testing finite-dimensional comodules in the base-field universe suffices for comodules in every universe.
• TauCeti.Comodule.isCompletelyReducible_corestrict_iff_of_coalgEquiv: complete reducibility is invariant under a coalgebra equivalence.
• TauCeti.Coalgebra.isLinearlyReductive_iff_of_coalgEquiv: linear reductivity is invariant under a coalgebra equivalence.
• TauCeti.Coalgebra.isLinearlyReductive_monoidAlgebra: monoid-algebra coalgebras are linearly reductive over a field.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Section 3.2.
• J. S. Milne, Algebraic Groups (2017), Theorem 12.12.

def TauCeti.Comodule.IsCompletelyReducible (k : Type u) (C : Type v) (V : Type w) [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] : Prop

A comodule is completely reducible when each subcomodule has a complementary subcomodule.

The complement is taken in the lattice of underlying submodules, so the statement says both that the two subcomodules intersect trivially and that together they span the whole comodule.

Equations

• TauCeti.Comodule.IsCompletelyReducible k C V = ∀ (W : TauCeti.Subcomodule k C V), ∃ (Q : TauCeti.Subcomodule k C V), IsCompl W.toSubmodule Q.toSubmodule

theorem TauCeti.Comodule.IsCompletelyReducible.of_exists_isCompl {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] (h : ∀ (W : Subcomodule k C V), ∃ (Q : Subcomodule k C V), IsCompl W.toSubmodule Q.toSubmodule) : IsCompletelyReducible k C V

Construct complete reducibility by supplying a complementary subcomodule for every subcomodule.

theorem TauCeti.Comodule.IsCompletelyReducible.exists_isCompl {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] (h : IsCompletelyReducible k C V) (W : Subcomodule k C V) : ∃ (Q : Subcomodule k C V), IsCompl W.toSubmodule Q.toSubmodule

The subcomodule complement supplied by complete reducibility.

TauCeti.Comodule.IsCompletelyReducible is a definition, so its body is not available outside this file; this is the accessor that unfolds it.

theorem TauCeti.Comodule.isCompletelyReducible_of_forall_eq_bot_or_eq_top {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] (h : ∀ (W : Subcomodule k C V), W = ⊥ ∨ W = ⊤) : IsCompletelyReducible k C V

A comodule with no subcomodules except ⊥ and ⊤ is completely reducible: each of the two is complemented by the other.

This is the common content of the two criteria below. Note that it is weaker than IsSimpleOrder (Subcomodule k C V), which additionally requires ⊥ ≠ ⊤, and so covers the subsingleton case as well.

theorem TauCeti.Comodule.isCompletelyReducible_of_subsingleton {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] [Subsingleton V] : IsCompletelyReducible k C V

A comodule on a subsingleton module is completely reducible.

theorem TauCeti.Comodule.isCompletelyReducible_of_isSimpleOrder {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] [IsSimpleOrder (Subcomodule k C V)] : IsCompletelyReducible k C V

A comodule whose subcomodule lattice is simple is completely reducible.

theorem TauCeti.Comodule.fixedSubcomodule_eq_top_of_isCompletelyReducible_of_forall_exists_fixed {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] [One C] (hcr : IsCompletelyReducible k C V) (hfix : ∀ (N : Subcomodule k C V), N ≠ ⊥ → ∃ v ∈ N, v ≠ 0 ∧ coact v = v ⊗ₜ[k] 1) : fixedSubcomodule k C V = ⊤

If V is completely reducible and every nonzero subcomodule of V contains a nonzero fixed vector, then the fixed subcomodule is everything.

A subcomodule complement of the fixed subcomodule meets it trivially, so it contains no nonzero fixed vector and is therefore zero.

theorem TauCeti.Comodule.coact_eq_tmul_one_of_isCompletelyReducible_of_forall_exists_fixed {k : Type u} {C : Type v} {V : Type w} [CommSemiring k] [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid V] [Module k V] [Comodule k C V] [One C] (hcr : IsCompletelyReducible k C V) (hfix : ∀ (N : Subcomodule k C V), N ≠ ⊥ → ∃ v ∈ N, v ≠ 0 ∧ coact v = v ⊗ₜ[k] 1) (v : V) : coact v = v ⊗ₜ[k] 1

The vectorwise form of TauCeti.Comodule.fixedSubcomodule_eq_top_of_isCompletelyReducible_of_forall_exists_fixed.

theorem TauCeti.Comodule.isCompletelyReducible_iff_forall_exists_hom {R : Type u} {C : Type v} {V : Type w} [CommRing R] [AddCommMonoid C] [Module R C] [Coalgebra R C] [AddCommGroup V] [Module R V] [Comodule R C V] [Module.Flat R C] : IsCompletelyReducible R C V ↔ ∀ (W : Subcomodule R C V), ∃ (P : Hom R C V V), (∀ (v : V), P v ∈ W) ∧ ∀ w ∈ W, P w = w

Complete reducibility via equivariant retractions. A comodule is completely reducible exactly when every subcomodule is the image of a comodule endomorphism that fixes it pointwise.

def TauCeti.Coalgebra.IsLinearlyReductive (k : Type u) (C : Type v) [Field k] [AddCommMonoid C] [Module k C] [Coalgebra k C] : Prop

A coalgebra is linearly reductive in carrier universe w when every finite-dimensional comodule over it whose carrier lies in Type w is completely reducible. For a commutative Hopf algebra representing an affine group, this is the usual complete-reducibility definition of a linearly reductive group at that universe.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Comodule.isCompletelyReducible_of_orderIso (k : Type u) [CommSemiring k] {C : Type v} {D : Type u_1} {V : Type w} {W : Type u_2} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] [AddCommMonoid V] [Module k V] [Comodule k C V] [AddCommMonoid W] [Module k W] [Comodule k D W] (Φ : Subcomodule k C V ≃o Subcomodule k D W) (E : Submodule k V ≃o Submodule k W) (hΦ : ∀ (A : Subcomodule k C V), (Φ A).toSubmodule = E A.toSubmodule) (h : IsCompletelyReducible k C V) : IsCompletelyReducible k D W

Complete reducibility transfers across compatible order isomorphisms of subcomodules and their underlying submodules.

theorem TauCeti.Comodule.isCompletelyReducible_transport_iff (k : Type u) [CommSemiring k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] {V : Type w} {W : Type u_1} [AddCommMonoid V] [Module k V] [Comodule k C V] [AddCommMonoid W] [Module k W] (e : V ≃ₗ[k] W) : IsCompletelyReducible k C W ↔ IsCompletelyReducible k C V

Complete reducibility is invariant under transporting a comodule structure along a linear equivalence.

theorem TauCeti.Comodule.isCompletelyReducible_corestrict_iff_of_coalgEquiv (k : Type u) [CommSemiring k] {C : Type v} {D : Type u_1} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] (e : C ≃ₗc[k] D) {V : Type w} [AddCommMonoid V] [Module k V] [Comodule k D V] : IsCompletelyReducible k C V ↔ IsCompletelyReducible k D V

Complete reducibility is unchanged by corestricting a comodule along a coalgebra equivalence.

theorem TauCeti.Coalgebra.IsLinearlyReductive.of_forall_isCompletelyReducible (k : Type u) [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] (h : ∀ (V : Type w) [inst : AddCommMonoid V] [inst_1 : Module k V] [inst_2 : Comodule k C V] [Module.Finite k V], Comodule.IsCompletelyReducible k C V) : IsLinearlyReductive k C

Construct linear reductivity by proving complete reducibility of every finite-dimensional comodule with carrier in the given universe.

theorem TauCeti.Coalgebra.IsLinearlyReductive.isCompletelyReducible_sameUniverse (k : Type u) [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] (h : IsLinearlyReductive k C) (V : Type w) [AddCommMonoid V] [Module k V] [Comodule k C V] [Module.Finite k V] : Comodule.IsCompletelyReducible k C V

Apply linear reductivity to a finite-dimensional comodule in the same carrier universe.

Every finite-dimensional comodule whose carrier lies in the universe quantified by the hypothesis is completely reducible.

theorem TauCeti.Coalgebra.IsLinearlyReductive.isCompletelyReducible (k : Type u) [Field k] {C : Type v} [AddCommMonoid C] [Module k C] [Coalgebra k C] (h : IsLinearlyReductive k C) {V : Type w} [AddCommMonoid V] [Module k V] [Comodule k C V] [Module.Finite k V] : Comodule.IsCompletelyReducible k C V

If every finite-dimensional comodule whose carrier is in the base-field universe is completely reducible, then every finite-dimensional comodule is completely reducible, regardless of its carrier universe.

theorem TauCeti.Coalgebra.isLinearlyReductive_iff_of_coalgEquiv (k : Type u) [Field k] {C : Type v} {D : Type u_1} [AddCommMonoid C] [Module k C] [Coalgebra k C] [AddCommMonoid D] [Module k D] [Coalgebra k D] (e : C ≃ₗc[k] D) : IsLinearlyReductive k C ↔ IsLinearlyReductive k D

Linear reductivity is invariant under equivalence of coalgebras.

theorem TauCeti.Comodule.isCompletelyReducible_monoidAlgebra (k : Type u) (G : Type v) (V : Type w) [Field k] [AddCommMonoid V] [Module k V] [Comodule k (MonoidAlgebra k G) V] : IsCompletelyReducible k (MonoidAlgebra k G) V

Every comodule over a monoid-algebra coalgebra over a field is completely reducible.

theorem TauCeti.Coalgebra.isLinearlyReductive_monoidAlgebra (k : Type u') (G : Type v') [Field k] : IsLinearlyReductive k (MonoidAlgebra k G)

A monoid-algebra coalgebra over a field is linearly reductive. For a commutative group G, this is the coordinate algebra statement that the diagonalizable group D(G) is linearly reductive.