ClassCompletion.lean

1 import PaperX.RepresentationClasses
2 import PaperX.FiniteFiberBranches
3 import PaperX.CompletionAssembly
4 import Mathlib.RingTheory.Ideal.Quotient.Index
5 
6 /-! Complete finite-level representation conditions stated on actual conjugacy
7 classes. Finiteness of coefficients controls all frames in each class. -/
8 set_option autoImplicit false
9 namespace PaperX.ClassCompletion
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
11 open PaperX.RepresentationClasses PaperX.CompletionAssembly
12 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
13 variable (I : Ideal R)
14 
15 structure ClassConditions where
16   allowed : (k : ℕ) → ClassRep (R ⧸ I^k) G ι → Prop
17   downward : ∀ {j k} (h : j ≤ k) c, allowed k c → allowed j (transitionClass I h c)
18 
19 def framed (C : ClassConditions (G := G) (ι := ι) I) : Conditions (G := G) (ι := ι) I where
20   allowed k ρ := C.allowed k (classOf ρ)
21   downward h ρ hρ := C.downward h (classOf ρ) hρ
22 
23 theorem framed_nonempty_iff (C : ClassConditions (G := G) (ι := ι) I) (k : ℕ) :
24     (∃ ρ, (framed I C).allowed k ρ) ↔ ∃ c, C.allowed k c := by
25   constructor
26   · rintro ⟨ρ, hρ⟩
27     exact ⟨classOf ρ, hρ⟩
28   · rintro ⟨c, hc⟩
29     obtain ⟨ρ, rfl⟩ := classOf_surjective c
30     exact ⟨ρ, hc⟩
31 
32 theorem framed_finite (C : ClassConditions (G := G) (ι := ι) I) (k : ℕ)
33     [Finite (R ⧸ I^k)] [Finite {c // C.allowed k c}] :
34     Finite {ρ // (framed I C).allowed k ρ} := by
35   let f : {ρ // (framed I C).allowed k ρ} → {c // C.allowed k c} :=
36     fun ρ => ⟨classOf ρ.val, ρ.property⟩
37   have hf (c : {c // C.allowed k c}) : Finite {ρ // f ρ = c} := by
38     let : Finite {ρ : MatrixRep (R ⧸ I^k) G ι // classOf ρ = c.val} := finite_class_fiber c.val
39     let j : {ρ // f ρ = c} → {ρ : MatrixRep (R ⧸ I^k) G ι // classOf ρ = c.val} :=
40       fun ρ => ⟨ρ.val.val, congrArg Subtype.val ρ.property⟩
41     apply Finite.of_injective j
42     intro x y h
43     apply Subtype.ext
44     apply Subtype.ext
45     exact congrArg (fun z : {ρ : MatrixRep (R ⧸ I^k) G ι // classOf ρ = c.val} => z.val) h
46   exact PaperX.FiniteFiberBranches.finite_of_fibers f hf
47 
48 /-- Positive finite class levels suffice for actual integral representations. -/
49 theorem class_realization_iff [IsAdicComplete I R]
50     (C : ClassConditions (G := G) (ι := ι) I)
51     (finiteR : ∀ k, Finite (R ⧸ I^k))
52     (finiteC : ∀ k, 0 < k → Finite {c // C.allowed k c}) :
53     (∃ ρ : MatrixRep R G ι, ∀ k, C.allowed k (classOf (reduce I ρ k))) ↔
54       ∀ k, 0 < k → ∃ c, C.allowed k c := by
55   have hf : ∀ k, Finite {ρ // (framed I C).allowed k ρ} := by
56     apply positive_finite_levels
57     intro k hk
58     let : Finite (R ⧸ I^k) := finiteR k
59     let : Finite {c // C.allowed k c} := finiteC k hk
60     exact framed_finite I C k
61   change (∃ ρ, Realizes I (framed I C) ρ) ↔ _
62   rw [realization_iff I (framed I C) hf, ← positive_levels_iff_all]
63   exact forall_congr' fun k => forall_congr' fun _ => framed_nonempty_iff I C k
64 
65 /-- Finitely generated I and finite residue ring derive finiteness at every precision. -/
66 theorem finite_coefficients (hI : I.FG) [Finite (R ⧸ I)] (k : ℕ) :
67     Finite (R ⧸ I^k) := Ideal.finite_quotient_pow hI k
68 
69 end PaperX.ClassCompletion

Back to source controls