ExistingCompatibleSystems.lean

1 import PaperXII.DenseFrobenius
2 import PaperXII.RepresentationData
3 
4 set_option autoImplicit false
5 
6 /-! Paper XII, Theorems 10.7 and 12.5. Two already existing families of actual
7 continuous matrix representations carry the same coefficient-field polynomial
8 spine. Density of the good Frobenius conjugacy classes gives equality of their
9 characteristic polynomials everywhere. The universally quantified algebraic
10 Brauer--Nesbitt input then gives actual invertible linear intertwiners.
11 
12 The distinguished member and its ordinary or derived completion datum are
13 unnecessary after both families and the common spine have been supplied, as
14 the source statements explicitly assume. No missing companion is constructed,
15 and the derived completion theorem 12.4 is not asserted here. -/
16 namespace PaperXII.ExistingCompatibleSystems
17 
18 open Matrix
19 open PaperXII.RepresentationData
20 
21 variable {Λ Ω Γ ι L : Type*} [Group Γ] [TopologicalSpace Γ]
22     [Fintype ι] [DecidableEq ι] [Field L]
23     {E : Λ → Type*} [∀ l, Field (E l)] [∀ l, TopologicalSpace (E l)]
24     [∀ l, IsTopologicalRing (E l)] [∀ l, T2Space (E l)]
25 
26 /-- The common mapped spine determines all characteristic polynomials at every
27 declared coefficient place, even when the good set depends on that place. -/
28 theorem memberwise_charpoly_eq
29     (ρ σ : ∀ l, Γ →ₜ* GL ι (E l)) (frob : Ω → Γ) (good : Λ → Ω → Prop)
30     (hdense : ∀ l, Dense (PaperXII.DenseFrobenius.conjugacySaturation frob (good l)))
31     (emb : ∀ l, L →+* E l) (P : Ω → Polynomial L)
32     (hρ : ∀ l v, good l v → (ρ l (frob v)).val.charpoly = (P v).map (emb l))
33     (hσ : ∀ l v, good l v → (σ l (frob v)).val.charpoly = (P v).map (emb l)) :
34     ∀ l g, (ρ l g).val.charpoly = (σ l g).val.charpoly := by
35   intro l
36   exact PaperXII.DenseFrobenius.common_spine_charpoly_eq
37     (ρ l) (σ l) frob (good l) (hdense l) (emb l) P (hρ l) (hσ l)
38 
39 variable [∀ l, CharZero (E l)]
40 
41 /-- Theorem 10.7: a semisimple existing family is isomorphic member by member
42 to the semisimplification of the supplied attached family with the same spine.
43 The attached family itself need not be semisimple. -/
44 theorem one_member_propagation
45     (ρ σ : ∀ l, Γ →ₜ* GL ι (E l)) (frob : Ω → Γ) (good : Λ → Ω → Prop)
46     (hdense : ∀ l, Dense (PaperXII.DenseFrobenius.conjugacySaturation frob (good l)))
47     (emb : ∀ l, L →+* E l) (P : Ω → Polynomial L)
48     (hρ : ∀ l v, good l v → (ρ l (frob v)).val.charpoly = (P v).map (emb l))
49     (hσ : ∀ l v, good l v → (σ l (frob v)).val.charpoly = (P v).map (emb l))
50     (hsemisimple : ∀ l, Representation.IsSemisimpleRepresentation
51       (representation (ρ l).toMonoidHom))
52     (ss : ∀ l, Semisimplification (σ l).toMonoidHom)
53     (bn : ∀ l, BrauerNesbitt (E l) Γ ι) :
54     ∀ l, Isomorphic (ρ l).toMonoidHom (ss l).rep := by
55   intro l
56   apply bn l (ρ l).toMonoidHom (ss l).rep (hsemisimple l) (ss l).semisimple
57   intro g
58   exact (memberwise_charpoly_eq ρ σ frob good hdense emb P hρ hσ l g).trans
59     ((ss l).charpoly_eq g).symm
60 
61 /-- Theorem 12.5, with actual memberwise intertwining equivalences selected
62 simultaneously. Both representation families already exist in the hypotheses.
63 The earlier completion at one member supplies its arithmetic interpretation;
64 it does not replace the common-spine or existence hypotheses used here. -/
65 theorem system_completion
66     (ρ σ : ∀ l, Γ →ₜ* GL ι (E l)) (frob : Ω → Γ) (good : Λ → Ω → Prop)
67     (hdense : ∀ l, Dense (PaperXII.DenseFrobenius.conjugacySaturation frob (good l)))
68     (emb : ∀ l, L →+* E l) (P : Ω → Polynomial L)
69     (hρ : ∀ l v, good l v → (ρ l (frob v)).val.charpoly = (P v).map (emb l))
70     (hσ : ∀ l v, good l v → (σ l (frob v)).val.charpoly = (P v).map (emb l))
71     (hsemisimple : ∀ l, Representation.IsSemisimpleRepresentation
72       (representation (ρ l).toMonoidHom))
73     (ss : ∀ l, Semisimplification (σ l).toMonoidHom)
74     (bn : ∀ l, BrauerNesbitt (E l) Γ ι) :
75     Nonempty (∀ l, Representation.Equiv (representation (ρ l).toMonoidHom)
76       (representation (ss l).rep)) := by
77   classical
78   exact ⟨fun l => Classical.choice
79     (one_member_propagation ρ σ frob good hdense emb P hρ hσ hsemisimple ss bn l)⟩
80 
81 end PaperXII.ExistingCompatibleSystems

Back to source controls