CuspidalContraction105.lean

1 import Mathlib.RepresentationTheory.Basic
2 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
3 
4 /-! Finite cuspidality excludes a map on which an actual radical contracts to
5 identity. The averaging sum and its vanishing are derived, not supplied. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.CuspidalContraction105
9 open Representation
10 variable {k U V W : Type*} [Field k]
11   [Group U] [Fintype U] [AddCommGroup V] [Module k V]
12   [AddCommGroup W] [Module k W]
13 
14 def NoFixed (ρ : Representation k U V) : Prop :=
15   ∀ v : V, (∀ u : U, ρ u v = v) → v = 0
16 
17 theorem sum_fixed (ρ : Representation k U V) (v : V) (u : U) :
18     ρ u (∑ x : U, ρ x v) = ∑ x : U, ρ x v := by
19   simp only [map_sum, ← Module.End.mul_apply, ← map_mul]
20   exact Fintype.sum_equiv (Equiv.mulLeft u) (fun x => ρ (u * x) v)
21     (fun x => ρ x v) (fun _ => rfl)
22 
23 theorem sum_eq_zero (ρ : Representation k U V) (hρ : NoFixed ρ) (v : V) :
24     (∑ x : U, ρ x v) = 0 := hρ _ (sum_fixed ρ v)
25 
26 theorem map_eq_zero [CharZero k] (ρ : Representation k U V) (hρ : NoFixed ρ)
27     (T : V →ₗ[k] W) (hT : ∀ u v, T (ρ u v) = T v) : T = 0 := by
28   ext v
29   have hsum := congrArg T (sum_eq_zero ρ hρ v)
30   simp only [map_sum, hT, Finset.sum_const, Finset.card_univ, map_zero] at hsum
31   have hcard : (Fintype.card U : k) ≠ 0 :=
32     Nat.cast_ne_zero.mpr Fintype.card_ne_zero
33   have hmul : (Fintype.card U : k) • T v = 0 := by
34     simpa only [Nat.cast_smul_eq_nsmul] using hsum
35   exact (smul_eq_zero.mp hmul).resolve_left hcard
36 
37 end PaperXI.CuspidalContraction105

Back to source controls