RepresentationForests.lean

1 import PaperX.RepresentationTopology
2 import PaperX.Compactness
3 import Mathlib.Data.Fintype.EquivFin
4 
5 /-! Finite nonempty forests of actual finite-level representations have actual
6 integral realizations, once the coefficient ring is adically complete. Finite
7 level occupancy and continuity are hypotheses, not consequences of compactness. -/
8 set_option autoImplicit false
9 namespace PaperX.RepresentationForests
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology
11 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
12 variable (I : Ideal R)
13 
14 /-- The finite conditions live on actual quotient representations. -/
15 structure Conditions where
16   allowed : (k : ℕ) → MatrixRep (R ⧸ I^k) G ι → Prop
17   downward : ∀ {j k} (h : j ≤ k) ρ, allowed k ρ → allowed j (transition I h ρ)
18 
19 /-- Every chosen finite representation has a total reduction to the previous
20 allowed level. Surjectivity of these reduction maps is not assumed. -/
21 def tower (C : Conditions (G := G) (ι := ι) I) : PaperX.Compactness.Tower where
22   Level k := {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}
23   parent k ρ := ⟨transition I (Nat.le_succ k) ρ.val, C.downward _ _ ρ.property⟩
24 
25 theorem all_compatible (C : Conditions (G := G) (ι := ι) I)
26     (b : PaperX.Compactness.Branch (tower I C)) {j k : ℕ} (h : j ≤ k) :
27     transition I h (b.value k).val = (b.value j).val := by
28   ext g a c
29   apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
30     (fun _ _ h => Ideal.pow_le_pow_right h)
31     (fun m => (b.value m).val g a c) ?_ h).symm
32   intro m
33   exact (congrArg (fun x => x.val g a c) (b.compatible m)).symm
34 
35 def family (C : Conditions (G := G) (ι := ι) I)
36     (b : PaperX.Compactness.Branch (tower I C)) : Family R I G ι where
37   maps k := (b.value k).val
38   compatible := all_compatible I C b
39 
40 /-- Compactness is established for the actual subtype, not for the coefficient
41 ring alone. A finite coefficient ring does not imply finitely many group maps. -/
42 theorem finite_levels (C : Conditions (G := G) (ι := ι) I)
43     (h : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}) :
44     PaperX.Compactness.FiniteLevels (tower I C) := by
45   intro k
46   let : Finite ((tower I C).Level k) := h k
47   let : Fintype ((tower I C).Level k) := Fintype.ofFinite _
48   classical
49   exact ⟨Finset.univ.toList, by simp⟩
50 
51 /-- An actual realization satisfies the allowed constraints at every precision. -/
52 def Realizes (C : Conditions (G := G) (ι := ι) I) (ρ : MatrixRep R G ι) : Prop :=
53   ∀ k, C.allowed k (reduce I ρ k)
54 
55 theorem exists_realization [IsAdicComplete I R]
56     (C : Conditions (G := G) (ι := ι) I)
57     (finite : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
58     (occupied : ∀ k, ∃ ρ, C.allowed k ρ) :
59     ∃ ρ : MatrixRep R G ι, Realizes I C ρ := by
60   obtain ⟨b⟩ := PaperX.Compactness.finite_branch_compactness (tower I C)
61     (finite_levels I C finite) (fun k => let ⟨ρ,h⟩ := occupied k; ⟨ρ,h⟩)
62   refine ⟨reconstruct I (family I C b), ?_⟩
63   intro k
64   rw [reconstruct_reduces]
65   exact (b.value k).property
66 
67 /-- This converse does not need completeness, finiteness, or surjective reductions. -/
68 theorem levels_of_realization (C : Conditions (G := G) (ι := ι) I)
69     (ρ : MatrixRep R G ι) (h : Realizes I C ρ) :
70     ∀ k, ∃ τ, C.allowed k τ := fun k => ⟨reduce I ρ k, h k⟩
71 
72 /-- The completed congruence problem is nonempty iff all its finite levels are,
73 under the explicit complete-ring and finite-allowed-level assumptions. -/
74 theorem realization_iff [IsAdicComplete I R]
75     (C : Conditions (G := G) (ι := ι) I)
76     (finite : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}) :
77     (∃ ρ, Realizes I C ρ) ↔ ∀ k, ∃ τ, C.allowed k τ :=
78   ⟨fun ⟨ρ,h⟩ => levels_of_realization I C ρ h, exists_realization I C finite⟩
79 
80 /-- Failure at any precision obstructs a realization. -/
81 theorem empty_level_obstructs (C : Conditions (G := G) (ι := ι) I)
82     (k : ℕ) (h : ¬ ∃ τ, C.allowed k τ) : ¬ ∃ ρ, Realizes I C ρ := by
83   rintro ⟨ρ,hρ⟩
84   exact h ⟨reduce I ρ k, hρ k⟩
85 
86 variable [TopologicalSpace G]
87 
88 /-- Actual continuity is retained; no abstract realization map is assumed. -/
89 theorem exists_continuous_realization [IsAdicComplete I R]
90     (C : Conditions (G := G) (ι := ι) I)
91     (finite : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
92     (occupied : ∀ k, ∃ ρ, C.allowed k ρ)
93     (continuous : ∀ k ρ, C.allowed k ρ → FiniteRepContinuous ρ) :
94     ∃ ρ : MatrixRep R G ι, Realizes I C ρ ∧ AdicRepContinuous I ρ := by
95   obtain ⟨b⟩ := PaperX.Compactness.finite_branch_compactness (tower I C)
96     (finite_levels I C finite) (fun k => let ⟨ρ,h⟩ := occupied k; ⟨ρ,h⟩)
97   refine ⟨reconstruct I (family I C b), ?_, ?_⟩
98   · intro k
99     rw [reconstruct_reduces]
100     exact (b.value k).property
101   · apply reconstructed_continuous
102     intro k
103     exact continuous k (b.value k).val (b.value k).property
104 
105 /-- A separate local-property implication is explicit. This theorem does not
106 assert closedness or construct a Hodge--Tate/Weil--Deligne local condition. -/
107 theorem completion_with_local_condition [IsAdicComplete I R]
108     (C : Conditions (G := G) (ι := ι) I)
109     (finite : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
110     (occupied : ∀ k, ∃ ρ, C.allowed k ρ)
111     (continuous : ∀ k ρ, C.allowed k ρ → FiniteRepContinuous ρ)
112     (Local : MatrixRep R G ι → Prop)
113     (stable : ∀ ρ, Realizes I C ρ → Local ρ) :
114     ∃ ρ, Realizes I C ρ ∧ AdicRepContinuous I ρ ∧ Local ρ := by
115   obtain ⟨ρ,hρ,hc⟩ := exists_continuous_realization I C finite occupied continuous
116   exact ⟨ρ,hρ,hc,stable ρ hρ⟩
117 
118 end PaperX.RepresentationForests

Back to source controls