RepresentationData.lean

1 import Mathlib.RepresentationTheory.Semisimple
2 import Mathlib.RepresentationTheory.Irreducible
3 import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
4 import Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
5 
6 /-! Actual matrix actions and explicit standard finite-dimensional algebra inputs.
7 Semisimplification is specified by a semisimple representative with the same
8 characteristic polynomials. Its existence and the general Brauer–Nesbitt theorem
9 are external inputs; no particular comparison is supplied as an assumption. -/
10 set_option autoImplicit false
11 namespace PaperXII.RepresentationData
12 
13 open Matrix
14 
15 variable {E Γ ι : Type*} [Field E] [Group Γ] [Fintype ι] [DecidableEq ι]
16 
17 /-- The actual linear action associated with an invertible matrix representation. -/
18 def representation (ρ : Γ →* GL ι E) : Representation E Γ (ι → E) :=
19   (Units.coeHom (Module.End E (ι → E))).comp
20     (GeneralLinearGroup.toLin.toMonoidHom.comp ρ)
21 
22 /-- This action applies the original matrix to the original coordinate vector. -/
23 theorem representation_apply (ρ : Γ →* GL ι E) (g : Γ) (v : ι → E) :
24     representation ρ g v = (ρ g).val.mulVec v := rfl
25 
26 /-- Isomorphism means an actual invertible linear intertwiner. -/
27 abbrev Isomorphic (ρ σ : Γ →* GL ι E) :=
28   Nonempty (Representation.Equiv (representation ρ) (representation σ))
29 
30 /-- A supplied semisimplification representative, characterized in characteristic zero
31 by actual semisimplicity and preservation of all characteristic polynomials.
32 No chosen automorphic representation or comparison is part of this datum. -/
33 structure Semisimplification (ρ : Γ →* GL ι E) where
34   rep : Γ →* GL ι E
35   semisimple : Representation.IsSemisimpleRepresentation (representation rep)
36   charpoly_eq : ∀ g, (rep g).val.charpoly = (ρ g).val.charpoly
37 
38 /-- The general algebraic Brauer–Nesbitt input from Fact 9.2. This universally
39 quantifies over representations, independently of points or automorphic data. -/
40 def BrauerNesbitt (E Γ ι : Type*) [Field E] [CharZero E] [Group Γ]
41     [Fintype ι] [DecidableEq ι] : Prop :=
42   ∀ (ρ σ : Γ →* GL ι E),
43     Representation.IsSemisimpleRepresentation (representation ρ) →
44     Representation.IsSemisimpleRepresentation (representation σ) →
45     (∀ g, (ρ g).val.charpoly = (σ g).val.charpoly) → Isomorphic ρ σ
46 
47 /-- An irreducible representation is semisimple in the actual subrepresentation lattice. -/
48 theorem irreducible_semisimple (ρ : Γ →* GL ι E)
49     (hρ : Representation.IsIrreducible (representation ρ)) :
50     Representation.IsSemisimpleRepresentation (representation ρ) := by
51   let := hρ
52   infer_instance
53 
54 /-- A semisimple representation is itself a valid semisimplification representative. -/
55 def selfSemisimplification (ρ : Γ →* GL ι E)
56     (hρ : Representation.IsSemisimpleRepresentation (representation ρ)) :
57     Semisimplification ρ := ⟨ρ, hρ, fun _ ↦ rfl⟩
58 
59 variable [CharZero E]
60 
61 /-- Any two supplied semisimplifications are isomorphic; choice of representative is harmless. -/
62 theorem semisimplification_unique (bn : BrauerNesbitt E Γ ι) (ρ : Γ →* GL ι E)
63     (s t : Semisimplification ρ) : Isomorphic s.rep t.rep := by
64   exact bn s.rep t.rep s.semisimple t.semisimple
65     (fun g ↦ (s.charpoly_eq g).trans (t.charpoly_eq g).symm)
66 
67 /-- Semisimplification fixes any semisimple representation up to an actual intertwiner. -/
68 theorem semisimplification_of_semisimple (bn : BrauerNesbitt E Γ ι)
69     (ρ : Γ →* GL ι E) (s : Semisimplification ρ)
70     (hρ : Representation.IsSemisimpleRepresentation (representation ρ)) :
71     Isomorphic ρ s.rep :=
72   bn ρ s.rep hρ s.semisimple (fun g ↦ (s.charpoly_eq g).symm)
73 
74 /-- The irreducible conclusion is derived, rather than included in the supplied choice. -/
75 theorem semisimplification_of_irreducible (bn : BrauerNesbitt E Γ ι)
76     (ρ : Γ →* GL ι E) (s : Semisimplification ρ)
77     (hρ : Representation.IsIrreducible (representation ρ)) : Isomorphic ρ s.rep :=
78   semisimplification_of_semisimple bn ρ s (irreducible_semisimple ρ hρ)
79 
80 /-- Applying semisimplification twice does not change its isomorphism class. -/
81 theorem semisimplification_idempotent (bn : BrauerNesbitt E Γ ι)
82     (ρ : Γ →* GL ι E) (s : Semisimplification ρ) (t : Semisimplification s.rep) :
83     Isomorphic s.rep t.rep :=
84   semisimplification_of_semisimple bn s.rep t s.semisimple
85 
86 end PaperXII.RepresentationData

Back to source controls