SpineCompletionBoundary.lean

1 import PaperX.InverseLimitLocalConditions
2 import PaperX.ClassBranchLifting
3 
4 /-!
5 The closure and occupancy premises do different work.  Allowing every finite
6 class does not force an arbitrary integral property, whereas an empty tower
7 satisfies every closure statement vacuously and has no realization.  These
8 boundary statements use actual representation classes and compatible families.
9 -/
10 set_option autoImplicit false
11 
12 namespace PaperX.SpineCompletionBoundary
13 open PaperX.RepresentationLimits PaperX.RepresentationClasses PaperX.ClassCompletion
14 open PaperX.InverseLimitLocalConditions PaperX.Compactness PaperX.ClassBranchLifting
15 
16 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
17 variable (I : Ideal R)
18 
19 /-- Every actual representation class is allowed. -/
20 def allClasses : ClassConditions (G := G) (ι := ι) I where
21   allowed _ _ := True
22   downward _ _ _ := True.intro
23 
24 /-- No actual representation class is allowed. -/
25 def emptyClasses : ClassConditions (G := G) (ι := ι) I where
26   allowed _ _ := False
27   downward _ _ h := h
28 
29 /-- The constant identity action is an actual integral representation. -/
30 def trivialRepresentation : MatrixRep R G ι where
31   toFun _ := 1
32   map_one' := rfl
33   map_mul' _ _ := (one_mul 1).symm
34 
35 /-- All precisions of the unrestricted class condition are occupied. -/
36 theorem allClasses_occupied (k : ℕ) :
37     ∃ c, (allClasses (G := G) (ι := ι) I).allowed k c :=
38   ⟨classOf (reduce I (trivialRepresentation (R := R) (G := G) (ι := ι)) k),
39     True.intro⟩
40 
41 /-- For a finite source group and finite quotient coefficients, unrestricted
42 levels also satisfy the finiteness premise. -/
43 theorem allClasses_finite (k : ℕ) [Finite G] [Finite (R ⧸ I^k)] :
44     Finite {c // (allClasses (G := G) (ι := ι) I).allowed k c} := by
45   let : Finite (MatrixRep (R ⧸ I^k) G ι) :=
46     Finite.of_injective DFunLike.coe DFunLike.coe_injective
47   let : Finite (ClassRep (R ⧸ I^k) G ι) :=
48     Finite.of_surjective classOf classOf_surjective
49   infer_instance
50 
51 /-- Even an actual compatible family in occupied levels need not satisfy an
52 arbitrarily prescribed local relation. -/
53 theorem compatible_family_fails_false [IsAdicComplete I R] :
54     ∃ f : Family R I G ι,
55       (∀ k, (allClasses I).allowed k (classOf (f.maps k))) ∧
56       ¬ (fun _ : MatrixRep R G ι => False) (reconstruct I f) :=
57   ⟨reduceFamily I trivialRepresentation, (fun _ => True.intro), not_false⟩
58 
59 /-- Inverse-limit closure cannot be omitted just because every class is allowed
60 and every precision is occupied. -/
61 theorem allClasses_not_closed_false [IsAdicComplete I R] :
62     ¬ InverseLimitClosed I (allClasses (G := G) (ι := ι) I) (fun _ => False) := by
63   intro h
64   obtain ⟨f, hf, hfalse⟩ := compatible_family_fails_false (G := G) (ι := ι) I
65   exact hfalse (h f hf)
66 
67 /-- No universally valid rule can infer all local relations from admissible
68 finite classes alone. -/
69 theorem not_all_local_relations_follow [IsAdicComplete I R] :
70     ¬ (∀ P : MatrixRep R G ι → Prop,
71       ∀ f : Family R I G ι,
72         (∀ k, (allClasses I).allowed k (classOf (f.maps k))) → P (reconstruct I f)) := by
73   intro h
74   exact allClasses_not_closed_false (G := G) (ι := ι) I (h (fun _ => False))
75 
76 /-- Every local relation is inverse-limit closed for the empty allowed tower,
77 because there is no compatible allowed family. -/
78 theorem emptyClasses_closed [IsAdicComplete I R] (P : MatrixRep R G ι → Prop) :
79     InverseLimitClosed I (emptyClasses I) P := by
80   intro f hf
81   exact False.elim (hf 1)
82 
83 /-- The empty allowed tower has no occupied level, at any precision. -/
84 theorem emptyClasses_unoccupied (k : ℕ) :
85     ¬ ∃ c, (emptyClasses (G := G) (ι := ι) I).allowed k c := by
86   rintro ⟨c, hc⟩
87   exact hc
88 
89 /-- In particular, the empty tower has no integral realization. -/
90 theorem emptyClasses_no_realization :
91     ¬ ∃ ρ : MatrixRep R G ι,
92       ∀ k, (emptyClasses I).allowed k (classOf (reduce I ρ k)) := by
93   rintro ⟨ρ, hρ⟩
94   exact hρ 1
95 
96 /-- Closure alone supplies no finite-level occupancy. -/
97 theorem closure_without_occupancy [IsAdicComplete I R] :
98     (∀ P : MatrixRep R G ι → Prop, InverseLimitClosed I (emptyClasses I) P) ∧
99       ¬ ∃ c, (emptyClasses (G := G) (ι := ι) I).allowed 1 c :=
100   ⟨emptyClasses_closed I, emptyClasses_unoccupied I 1⟩
101 
102 /-- An integral representation gives an actual compatible branch of conjugacy
103 classes; this construction requires no compactness or choice of frames. -/
104 def classBranchOfRepresentation (ρ : MatrixRep R G ι) :
105     Branch (classTower (G := G) (ι := ι) I) where
106   value k := classOf (reduce I ρ k)
107   compatible k := by
108     change transitionClass I (Nat.le_succ k) (classOf (reduce I ρ (k + 1))) = _
109     rw [transitionClass_classOf, transition_reduce]
110 
111 /-- Every pair of precisions in this branch has the required reduction, not
112 only consecutive levels. -/
113 theorem classBranchOfRepresentation_compatible (ρ : MatrixRep R G ι)
114     {j k : ℕ} (h : j ≤ k) :
115     transitionClass I h ((classBranchOfRepresentation I ρ).value k) =
116       (classBranchOfRepresentation I ρ).value j := by
117   change transitionClass I h (classOf (reduce I ρ k)) = classOf (reduce I ρ j)
118   rw [transitionClass_classOf, transition_reduce]
119 
120 /-- An integral realization therefore provides a compatible branch in precisely
121 the supplied admissible classes. -/
122 theorem classBranchOfRepresentation_allowed
123     (C : ClassConditions (G := G) (ι := ι) I) (ρ : MatrixRep R G ι)
124     (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k))) :
125     ∀ k, C.allowed k ((classBranchOfRepresentation I ρ).value k) := hρ
126 
127 end PaperX.SpineCompletionBoundary

Back to source controls