ClassBranchLifting.lean

1 import PaperX.RepresentationClasses
2 import PaperX.RepresentationTopology
3 import PaperX.FiniteFiberBranches
4 
5 /-!
6 A prescribed compatible branch of actual change-of-basis classes lifts to
7 exactly compatible matrices over finite quotient rings.  Completeness then
8 reconstructs a representation with exactly those reduction classes.  No lift
9 of a prescribed change-of-basis matrix is assumed.
10 -/
11 set_option autoImplicit false
12 
13 namespace PaperX.ClassBranchLifting
14 open PaperX.Compactness PaperX.FiniteFiberBranches
15 open PaperX.RepresentationLimits PaperX.RepresentationClasses
16 open PaperX.RepresentationTopology
17 
18 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
19 variable (I : Ideal R)
20 
21 /-- The tower contains actual quotient representations. -/
22 def matrixTower : Tower where
23   Level k := MatrixRep (R ⧸ I ^ k) G ι
24   parent k := transition I (Nat.le_succ k)
25 
26 /-- The quotient tower contains their actual invertible-change-of-basis classes. -/
27 def classTower : Tower where
28   Level k := ClassRep (R ⧸ I ^ k) G ι
29   parent k := transitionClass I (Nat.le_succ k)
30 
31 /-- Coefficient reduction commutes with passing to a conjugacy class. -/
32 def classTowerMap : TowerMap (matrixTower (G := G) (ι := ι) I)
33     (classTower (G := G) (ι := ι) I) where
34   map _ := classOf
35   parent_commutes _ _ := rfl
36 
37 /-- Finiteness of each coefficient quotient suffices to lift a fixed branch.
38 Finiteness of the source group or of all representation classes is not required. -/
39 theorem lift_class_branch
40     (finiteR : ∀ k, Finite (R ⧸ I ^ k))
41     (b : Branch (classTower (G := G) (ι := ι) I)) :
42     ∃ a : Branch (matrixTower (G := G) (ι := ι) I),
43       ∀ k, classOf (a.value k) = b.value k := by
44   apply lift_branch (classTowerMap I) (fun _ => classOf_surjective)
45   intro k c
46   let : Finite (R ⧸ I ^ k) := finiteR k
47   exact finite_class_fiber c
48 
49 /-- Immediate compatibility of actual matrices implies compatibility between
50 every pair of precisions. -/
51 theorem matrix_branch_compatible
52     (a : Branch (matrixTower (G := G) (ι := ι) I))
53     {j k : ℕ} (h : j ≤ k) : transition I h (a.value k) = a.value j := by
54   ext g i l
55   apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
56     (fun _ _ h => Ideal.pow_le_pow_right h)
57     (fun m => DFunLike.coe (F := MatrixRep (R ⧸ I ^ m) G ι) (a.value m) g i l) ?_ h).symm
58   intro m
59   exact (congrArg (fun (ρ : MatrixRep (R ⧸ I ^ m) G ι) => ρ g i l)
60     (a.compatible m)).symm
61 
62 /-- A strictly compatible matrix branch gives the existing reconstruction input. -/
63 def matrixBranchFamily (a : Branch (matrixTower (G := G) (ι := ι) I)) :
64     Family R I G ι where
65   maps := a.value
66   compatible := matrix_branch_compatible I a
67 
68 /-- Every prescribed compatible class branch has a fully compatible matrix
69 family above it. This theorem needs no completeness assumption. -/
70 theorem family_of_class_branch
71     (finiteR : ∀ k, Finite (R ⧸ I ^ k))
72     (b : Branch (classTower (G := G) (ι := ι) I)) :
73     ∃ f : Family R I G ι, ∀ k, classOf (f.maps k) = b.value k := by
74   obtain ⟨a, ha⟩ := lift_class_branch I finiteR b
75   exact ⟨matrixBranchFamily I a, ha⟩
76 
77 /-- The reconstructed integral representation has each prescribed finite class.
78 The theorem does not assert uniqueness up to integral conjugacy. -/
79 theorem realization_of_class_branch [IsAdicComplete I R]
80     (finiteR : ∀ k, Finite (R ⧸ I ^ k))
81     (b : Branch (classTower (G := G) (ι := ι) I)) :
82     ∃ ρ : MatrixRep R G ι, ∀ k, classOf (reduce I ρ k) = b.value k := by
83   obtain ⟨f, hf⟩ := family_of_class_branch I finiteR b
84   refine ⟨reconstruct I f, ?_⟩
85   intro k
86   rw [reconstruct_reduces]
87   exact hf k
88 
89 /-- Actual continuous finite representatives give an actually adically continuous
90 integral representation. Continuity is explicitly required for the selected
91 classes and is not inferred from the finite coefficient rings alone. -/
92 theorem continuous_realization_of_class_branch [TopologicalSpace G]
93     [IsAdicComplete I R]
94     (finiteR : ∀ k, Finite (R ⧸ I ^ k))
95     (b : Branch (classTower (G := G) (ι := ι) I))
96     (continuous : ∀ k (ρ : MatrixRep (R ⧸ I ^ k) G ι),
97       classOf ρ = b.value k → FiniteRepContinuous ρ) :
98     ∃ ρ : MatrixRep R G ι,
99       (∀ k, classOf (reduce I ρ k) = b.value k) ∧ AdicRepContinuous I ρ := by
100   obtain ⟨f, hf⟩ := family_of_class_branch I finiteR b
101   refine ⟨reconstruct I f, ?_, reconstructed_continuous I f ?_⟩
102   · intro k
103     rw [reconstruct_reduces]
104     exact hf k
105   · intro k
106     exact continuous k (f.maps k) (hf k)
107 
108 end PaperX.ClassBranchLifting

Back to source controls