GaloisRealization.lean

1 import PaperXII.RepresentationData
2 import PaperXII.DenseFrobenius
3 
4 /-! Paper XII 9.4, conditional Galois identification with the arithmetic topology
5 made explicit. Frobenius density, semisimplification existence and algebraic
6 Brauer–Nesbitt remain supplied standard inputs. Dense extension and all actual
7 representation comparisons are derived. -/
8 set_option autoImplicit false
9 namespace PaperXII.GaloisRealization
10 
11 open Matrix RepresentationData DenseFrobenius
12 
13 variable {E Γ Ω ι : Type*} [Field E] [CharZero E] [Group Γ]
14     [TopologicalSpace E] [IsTopologicalRing E] [T2Space E]
15     [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
16 
17 /-- The semisimplification of a continuous representation is identified with a
18 semisimple attached representation using only the general standard input. -/
19 theorem pointwise_semisimple_identification (bn : BrauerNesbitt E Γ ι)
20     (ρ σ : Γ →ₜ* GL ι E) (s : Semisimplification ρ.toMonoidHom)
21     (hσ : Representation.IsSemisimpleRepresentation (representation σ.toMonoidHom))
22     (frob : Ω → Γ) (good : Ω → Prop)
23     (hdense : Dense (conjugacySaturation frob good))
24     (hpoly : ∀ v, good v → (ρ (frob v)).val.charpoly = (σ (frob v)).val.charpoly) :
25     Isomorphic s.rep σ.toMonoidHom := by
26   have hall := charpoly_eq_of_dense_frobenius ρ σ frob good hdense hpoly
27   exact bn s.rep σ.toMonoidHom s.semisimple hσ
28     (fun g ↦ (s.charpoly_eq g).trans (hall g))
29 
30 /-- The irreducible case gives an isomorphism of the original representations. -/
31 theorem pointwise_irreducible_identification (bn : BrauerNesbitt E Γ ι)
32     (ρ σ : Γ →ₜ* GL ι E)
33     (hρ : Representation.IsIrreducible (representation ρ.toMonoidHom))
34     (hσ : Representation.IsSemisimpleRepresentation (representation σ.toMonoidHom))
35     (frob : Ω → Γ) (good : Ω → Prop)
36     (hdense : Dense (conjugacySaturation frob good))
37     (hpoly : ∀ v, good v → (ρ (frob v)).val.charpoly = (σ (frob v)).val.charpoly) :
38     Isomorphic ρ.toMonoidHom σ.toMonoidHom :=
39   bn ρ.toMonoidHom σ.toMonoidHom (irreducible_semisimple _ hρ) hσ
40     (charpoly_eq_of_dense_frobenius ρ σ frob good hdense hpoly)
41 
42 /-- Both printed conclusions for an arbitrary mapped Hecke polynomial spine. -/
43 theorem common_spine_identification {B : Type*} [CommRing B]
44     (bn : BrauerNesbitt E Γ ι) (ρ σ : Γ →ₜ* GL ι E)
45     (s : Semisimplification ρ.toMonoidHom)
46     (hσ : Representation.IsSemisimpleRepresentation (representation σ.toMonoidHom))
47     (frob : Ω → Γ) (good : Ω → Prop)
48     (hdense : Dense (conjugacySaturation frob good)) (x : B →+* E)
49     (P : Ω → Polynomial B)
50     (hρP : ∀ v, good v → (ρ (frob v)).val.charpoly = (P v).map x)
51     (hσP : ∀ v, good v → (σ (frob v)).val.charpoly = (P v).map x) :
52     Isomorphic s.rep σ.toMonoidHom ∧
53       (Representation.IsIrreducible (representation ρ.toMonoidHom) →
54         Isomorphic ρ.toMonoidHom σ.toMonoidHom) := by
55   have heq : ∀ v, good v →
56       (ρ (frob v)).val.charpoly = (σ (frob v)).val.charpoly :=
57     fun v hv ↦ (hρP v hv).trans (hσP v hv).symm
58   exact ⟨pointwise_semisimple_identification bn ρ σ s hσ frob good hdense heq,
59     fun hρ ↦ pointwise_irreducible_identification bn ρ σ hρ hσ frob good hdense heq⟩
60 
61 variable {R : Type*} [CommRing R]
62 
63 /-- Actual coefficient specialization of the universal matrix representation. -/
64 def specialize (ρR : Γ →* GL ι R) (x : R →+* E) : Γ →* GL ι E :=
65   (GeneralLinearGroup.map x).comp ρR
66 
67 omit [CharZero E] [TopologicalSpace E] [IsTopologicalRing E] [T2Space E]
68     [TopologicalSpace Γ] in
69 /-- Specialization maps every coefficient of the universal characteristic polynomial. -/
70 theorem specialize_charpoly (ρR : Γ →* GL ι R) (x : R →+* E) (g : Γ) :
71     (specialize ρR x g).val.charpoly = ((ρR g).val.charpoly).map x :=
72   Matrix.charpoly_map _ _
73 
74 /-- Continuity of the specialization under consideration is explicit. -/
75 def continuousSpecialization (ρR : Γ →* GL ι R) (x : R →+* E)
76     (hx : Continuous (specialize ρR x)) : Γ →ₜ* GL ι E :=
77   { __ := specialize ρR x, continuous_toFun := hx }
78 
79 /-- Source-shaped pointwise realization: the compared representation is literally
80 x composed with the supplied universal representation. -/
81 theorem universal_pointwise_realization {T : Type*} [CommRing T]
82     (bn : BrauerNesbitt E Γ ι) (ρR : Γ →* GL ι R) (x : R →+* E)
83     (hx : Continuous (specialize ρR x))
84     (s : Semisimplification (specialize ρR x))
85     (σ : Γ →ₜ* GL ι E)
86     (hσ : Representation.IsSemisimpleRepresentation (representation σ.toMonoidHom))
87     (frob : Ω → Γ) (good : Ω → Prop)
88     (hdense : Dense (conjugacySaturation frob good))
89     (y : T →+* E) (P : Ω → Polynomial T)
90     (hρP : ∀ v, good v → (specialize ρR x (frob v)).val.charpoly = (P v).map y)
91     (hσP : ∀ v, good v → (σ (frob v)).val.charpoly = (P v).map y) :
92     Isomorphic s.rep σ.toMonoidHom ∧
93       (Representation.IsIrreducible (representation (specialize ρR x)) →
94         Isomorphic (specialize ρR x) σ.toMonoidHom) :=
95   common_spine_identification bn (continuousSpecialization ρR x hx) σ s hσ
96     frob good hdense y P hρP hσP
97 
98 end PaperXII.GaloisRealization

Back to source controls