ContinuousClasses.lean

1 import PaperXII.AdicSpines
2 import PaperX.ClassInvariants
3 import Mathlib.Basic.Finite.Sigma
4 
5 /-! Bridge actual continuous GL representations to the checked change-of-basis
6 classes. Finite coefficient rings make each individual fiber finite, even for
7 an infinite source group. No choice of compatible frames is assumed. -/
8 set_option autoImplicit false
9 namespace PaperXII.ContinuousClasses
10 
11 open ContinuousMonoidHom Matrix
12 open PaperX.RepresentationLimits PaperX.RepresentationClasses
13 open PaperX.RepresentationTopology PaperX.ClassInvariants
14 
15 variable {Γ ι S : Type} [Group Γ] [TopologicalSpace Γ]
16     [Fintype ι] [DecidableEq ι] [CommRing S] [TopologicalSpace S]
17 
18 /-- Forget the topology and retain the actual matrix representation. -/
19 def matrixRep (ρ : Γ →ₜ* GL ι S) : MatrixRep S Γ ι where
20   toFun g := (ρ g).val
21   map_one' := congrArg Units.val ρ.map_one
22   map_mul' g h := congrArg Units.val (ρ.map_mul g h)
23 
24 /-- The underlying matrix representation determines the continuous GL map. -/
25 theorem matrixRep_injective : Function.Injective (matrixRep (Γ := Γ) (ι := ι) (S := S)) := by
26   intro ρ σ h
27   apply ContinuousMonoidHom.ext
28   intro g
29   apply Units.ext
30   exact DFunLike.congr_fun h g
31 
32 /-- The actual change-of-basis class of a continuous representation. -/
33 def classOfRep (ρ : Γ →ₜ* GL ι S) : ClassRep S Γ ι := classOf (matrixRep ρ)
34 
35 /-- Locally constant matrix entries produce an actual continuous GL representation. -/
36 noncomputable def fromMatrix (ρ : MatrixRep S Γ ι) (hρ : FiniteRepContinuous ρ) :
37     Γ →ₜ* GL ι S where
38   __ := ρ.toHomUnits
39   continuous_toFun := by
40     apply IsLocallyConstant.continuous
41     apply (IsLocallyConstant.iff_eventually_eq _).mpr
42     intro g
43     filter_upwards [finiteRepContinuous_matrix ρ hρ g] with h hh
44     exact Units.ext hh
45 
46 /-- Passing to GL and forgetting back to matrices is exact. -/
47 theorem matrixRep_fromMatrix (ρ : MatrixRep S Γ ι) (hρ : FiniteRepContinuous ρ) :
48     matrixRep (fromMatrix ρ hρ) = ρ := rfl
49 
50 /-- A continuous representation into discrete coefficients has locally constant entries. -/
51 theorem matrixRep_finiteContinuous [DiscreteTopology S] (ρ : Γ →ₜ* GL ι S) :
52     FiniteRepContinuous (matrixRep ρ) := by
53   intro i j
54   apply (IsLocallyConstant.iff_eventually_eq _).mp
55   apply (IsLocallyConstant.iff_continuous _).mpr
56   have hm : Continuous (fun g : Γ ↦ (ρ g).val) := Units.continuous_val.comp ρ.continuous
57   exact (continuous_apply j).comp ((continuous_apply i).comp hm)
58 
59 /-- Every class arising from a continuous finite representation is a continuous class. -/
60 theorem classOfRep_continuous [DiscreteTopology S] (ρ : Γ →ₜ* GL ι S) :
61     ClassContinuous (classOfRep ρ) := matrixRep_finiteContinuous ρ
62 
63 /-- A continuous class has an actual continuous representative. -/
64 theorem exists_continuous_representative (c : ClassRep S Γ ι) (hc : ClassContinuous c) :
65     ∃ ρ : Γ →ₜ* GL ι S, classOfRep ρ = c := by
66   obtain ⟨σ, rfl⟩ := classOf_surjective c
67   exact ⟨fromMatrix σ hc, rfl⟩
68 
69 /-- The class-level continuity condition is precisely existence of a continuous frame. -/
70 theorem continuous_class_iff [DiscreteTopology S] (c : ClassRep S Γ ι) :
71     ClassContinuous c ↔ ∃ ρ : Γ →ₜ* GL ι S, classOfRep ρ = c := by
72   refine ⟨exists_continuous_representative c, ?_⟩
73   rintro ⟨ρ, rfl⟩
74   exact classOfRep_continuous ρ
75 
76 /-- Individual continuous class fibers are finite over finite coefficients. -/
77 theorem finite_continuous_fiber [Finite S] (c : ClassRep S Γ ι) :
78     Finite {ρ : Γ →ₜ* GL ι S // classOfRep ρ = c} := by
79   let _ : Finite {ρ : MatrixRep S Γ ι // classOf ρ = c} := finite_class_fiber c
80   let f : {ρ : Γ →ₜ* GL ι S // classOfRep ρ = c} →
81       {ρ : MatrixRep S Γ ι // classOf ρ = c} := fun ρ ↦ ⟨matrixRep ρ.val, ρ.property⟩
82   apply Finite.of_injective f
83   intro ρ σ h
84   apply Subtype.ext
85   exact matrixRep_injective (congrArg Subtype.val h)
86 
87 /-- Finitely many admissible classes give finitely many actual continuous frames. -/
88 theorem finite_allowed_frames [Finite S] (C : ClassRep S Γ ι → Prop)
89     [Finite {c // C c}] : Finite {ρ : Γ →ₜ* GL ι S // C (classOfRep ρ)} := by
90   let _ : ∀ c : {c // C c}, Finite {ρ : Γ →ₜ* GL ι S // classOfRep ρ = c.val} :=
91     fun c ↦ finite_continuous_fiber c.val
92   let f : {ρ : Γ →ₜ* GL ι S // C (classOfRep ρ)} →
93       Σ c : {c // C c}, {ρ : Γ →ₜ* GL ι S // classOfRep ρ = c.val} :=
94     fun ρ ↦ ⟨⟨classOfRep ρ.val, ρ.property⟩, ⟨ρ.val, rfl⟩⟩
95   apply Finite.of_injective f
96   intro ρ σ h
97   exact Subtype.ext (congrArg (fun x ↦ x.2.val) h)
98 
99 /-- Class invariants refer to the full characteristic polynomial of the actual map. -/
100 theorem classCharpoly_classOfRep (ρ : Γ →ₜ* GL ι S) (g : Γ) :
101     classCharpoly (classOfRep ρ) g = (ρ g).val.charpoly := rfl
102 
103 /-- Class triviality is exactly triviality of the actual continuous representation. -/
104 theorem classTrivial_classOfRep (H : Subgroup Γ) (ρ : Γ →ₜ* GL ι S) :
105     ClassTrivial H (classOfRep ρ) ↔ ∀ g, g ∈ H → ρ g = 1 := by
106   constructor
107   · intro h g hg
108     exact Units.ext (h g hg)
109   · intro h g hg
110     exact congrArg Units.val (h g hg)
111 
112 end PaperXII.ContinuousClasses

Back to source controls