structure ReductiveGroupData : Type 1

Combinatorial data abstracting a reductive group G acting on a representation V, together with a unipotent subgroup U, an indexing I of irreducible subrepresentations W i, and bookkeeping axioms: faithfulness of U, irreducibility of each W i, complete reducibility of V, the existence of unipotent fixed points in any nonzero subrepresentation, and the existence of the fixed-point subspace under U of any subrepresentation.

• G : Type
• U : Type
• V : Type
• g_one : self.G
• u_incl : self.U → self.G
• u_one : self.U
• u_incl_one : self.u_incl self.u_one = self.g_one
• act : self.G → self.V → self.V
• v_zero : self.V
• act_zero (g : self.G) : self.act g self.v_zero = self.v_zero
• act_id (v : self.V) : self.act self.g_one v = v
• u_faithful (u : self.U) : (∀ (v : self.V), self.act (self.u_incl u) v = v) → u = self.u_one
• Sub : Type
• mem_sub : self.Sub → self.V → Prop
• I : Type
• W : self.I → self.Sub
• W_nonempty (i : self.I) : ∃ (w : self.V), self.mem_sub (self.W i) w ∧ w ≠ self.v_zero
• irred (i : self.I) (W' : self.Sub) : (∀ (w : self.V), self.mem_sub W' w → self.mem_sub (self.W i) w) → (∃ (w : self.V), self.mem_sub W' w ∧ w ≠ self.v_zero) → ∀ (w : self.V), self.mem_sub (self.W i) w → self.mem_sub W' w
• completely_reducible (g : self.G) : (∀ (i : self.I) (w : self.V), self.mem_sub (self.W i) w → self.act g w = w) → ∀ (v : self.V), self.act g v = v
• unipotent_fixed_pt (W' : self.Sub) : (∃ (w : self.V), self.mem_sub W' w ∧ w ≠ self.v_zero) → ∃ (w : self.V), self.mem_sub W' w ∧ w ≠ self.v_zero ∧ ∀ (u : self.U), self.act (self.u_incl u) w = w
• fixed_pts_sub (W' : self.Sub) : ∃ (W_U : self.Sub), ∀ (w : self.V), self.mem_sub W_U w ↔ self.mem_sub W' w ∧ ∀ (u : self.U), self.act (self.u_incl u) w = w

theorem ReductiveGroupData.u_acts_trivially_on_summand (D : ReductiveGroupData) (i : D.I) (w : D.V) : D.mem_sub (D.W i) w → ∀ (u : D.U), D.act (D.u_incl u) w = w

The unipotent subgroup U acts trivially on each irreducible summand W i: combining irreducibility with the existence of a unipotent fixed point forces U to fix every element of W i.

theorem ReductiveGroupData.u_acts_trivially (D : ReductiveGroupData) (v : D.V) (u : D.U) : D.act (D.u_incl u) v = v

The unipotent subgroup U acts trivially on all of V, by complete reducibility together with triviality on each summand.

theorem ReductiveGroupData.u_is_trivial (D : ReductiveGroupData) (u : D.U) : u = D.u_one

The unipotent subgroup is trivial: every element of U equals the identity.

theorem ReductiveGroupData.lemma_1_30_2 (D : ReductiveGroupData) (u : D.U) : u = D.u_one

Lemma 1.30.2 (Etingof–Gelaki–Nikshych–Ostrik): A reductive group acting on a completely reducible faithful representation has trivial unipotent radical.