InverseLimitLocalConditions.lean

1 import PaperX.ClassCommonSpine
2 
3 /-!
4 Inverse-limit closure stated on actual compatible matrix families.  This is an
5 explicit hypothesis on a supplied property, not a definition of any arithmetic
6 invariant.  The equivalent realization formulation is the input used by the
7 common-spine completion theorem.  Arbitrarily many labelled conditions can be
8 assembled, and coefficient pullback is justified by actual commuting quotient
9 maps and preservation of the allowed classes.
10 -/
11 set_option autoImplicit false
12 
13 namespace PaperX.InverseLimitLocalConditions
14 open PaperX.RepresentationLimits PaperX.RepresentationClasses PaperX.ClassCompletion
15 
16 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
17 variable (I : Ideal R) [IsAdicComplete I R]
18 
19 /-- Every compatible family with allowed reduction classes reconstructs to an
20 integral representation satisfying the supplied property. -/
21 def InverseLimitClosed (C : ClassConditions (G := G) (ι := ι) I)
22     (P : MatrixRep R G ι → Prop) : Prop :=
23   ∀ f : Family R I G ι, (∀ k, C.allowed k (classOf (f.maps k))) → P (reconstruct I f)
24 
25 /-- For complete coefficients, closure on compatible families is precisely the
26 property needed for every integral realization of the allowed classes. -/
27 theorem inverseLimitClosed_iff_realizations
28     (C : ClassConditions (G := G) (ι := ι) I) (P : MatrixRep R G ι → Prop) :
29     InverseLimitClosed I C P ↔
30       ∀ ρ : MatrixRep R G ι, (∀ k, C.allowed k (classOf (reduce I ρ k))) → P ρ := by
31   constructor
32   · intro h ρ hρ
33     simpa only [reconstruct_reduce] using h (reduceFamily I ρ) hρ
34   · intro h f hf
35     apply h (reconstruct I f)
36     intro k
37     simpa only [reconstruct_reduces] using hf k
38 
39 /-- The family formulation supplies the closure premise of existing completion
40 theorems without assuming an integral realization in advance. -/
41 theorem of_realization (C : ClassConditions (G := G) (ι := ι) I)
42     (P : MatrixRep R G ι → Prop) (closed : InverseLimitClosed I C P)
43     (ρ : MatrixRep R G ι) (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k))) : P ρ :=
44   (inverseLimitClosed_iff_realizations I C P).mp closed ρ hρ
45 
46 /-- Restricting the allowed finite classes preserves a closure statement. -/
47 theorem restrict_allowed (C D : ClassConditions (G := G) (ι := ι) I)
48     (P : MatrixRep R G ι → Prop)
49     (included : ∀ k c, C.allowed k c → D.allowed k c)
50     (closed : InverseLimitClosed I D P) : InverseLimitClosed I C P := by
51   intro f hf
52   exact closed f (fun k => included k _ (hf k))
53 
54 /-- Closure transfers through a pointwise implication of integral conditions. -/
55 theorem implication (C : ClassConditions (G := G) (ι := ι) I)
56     (P Q : MatrixRep R G ι → Prop) (h : ∀ ρ, P ρ → Q ρ)
57     (closed : InverseLimitClosed I C P) : InverseLimitClosed I C Q := by
58   intro f hf
59   exact h _ (closed f hf)
60 
61 /-- Arbitrary intersections preserve closure; no finiteness of the label set is
62 required. -/
63 theorem forall_iff (C : ClassConditions (G := G) (ι := ι) I)
64     {S : Sort*} (P : S → MatrixRep R G ι → Prop) :
65     InverseLimitClosed I C (fun ρ => ∀ s, P s ρ) ↔
66       ∀ s, InverseLimitClosed I C (P s) := by
67   constructor
68   · intro h s f hf
69     exact h f hf s
70   · intro h f hf s
71     exact h s f hf
72 
73 /-- Binary intersections are a special case with an explicit conjunction. -/
74 theorem and_iff (C : ClassConditions (G := G) (ι := ι) I)
75     (P Q : MatrixRep R G ι → Prop) :
76     InverseLimitClosed I C (fun ρ => P ρ ∧ Q ρ) ↔
77       InverseLimitClosed I C P ∧ InverseLimitClosed I C Q := by
78   constructor
79   · intro h
80     exact ⟨fun f hf => (h f hf).1, fun f hf => (h f hf).2⟩
81   · rintro ⟨hP, hQ⟩ f hf
82     exact ⟨hP f hf, hQ f hf⟩
83 
84 /-- Prescribed labels enter through a supplied relation to the actual integral
85 representation.  Proving closure for each label proves their simultaneous form. -/
86 theorem labelled_relations (C : ClassConditions (G := G) (ι := ι) I)
87     {S : Type*} (Label : S → Type*) (label : ∀ s, Label s)
88     (relation : ∀ s, Label s → MatrixRep R G ι → Prop)
89     (closed : ∀ s, InverseLimitClosed I C (relation s (label s))) :
90     InverseLimitClosed I C (fun ρ => ∀ s, relation s (label s) ρ) :=
91   (forall_iff I C (fun s => relation s (label s))).mpr closed
92 
93 /-- Selected labels, including coefficient-dependent good-place conditions,
94 can be imposed simultaneously without requiring closure at unselected labels. -/
95 theorem selected_labelled_relations (C : ClassConditions (G := G) (ι := ι) I)
96     {S : Type*} (selected : S → Prop) (Label : S → Type*) (label : ∀ s, Label s)
97     (relation : ∀ s, Label s → MatrixRep R G ι → Prop)
98     (closed : ∀ s, selected s → InverseLimitClosed I C (relation s (label s))) :
99     InverseLimitClosed I C (fun ρ => ∀ s, selected s → relation s (label s) ρ) := by
100   intro f hf s hs
101   exact closed s hs f hf
102 
103 variable {S : Type} [CommRing S]
104 
105 /-- A coefficient condition is pulled back to actual integral representations;
106 the equivalence does not identify that condition with an arithmetic invariant. -/
107 theorem coefficient_condition_iff_realizations
108     (C : ClassConditions (G := G) (ι := ι) I) (inc : R →+* S)
109     (P : MatrixRep S G ι → Prop) :
110     InverseLimitClosed I C (fun ρ => P (changeCoefficients inc ρ)) ↔
111       ∀ ρ : MatrixRep R G ι, (∀ k, C.allowed k (classOf (reduce I ρ k))) →
112         P (changeCoefficients inc ρ) :=
113   inverseLimitClosed_iff_realizations I C (fun ρ => P (changeCoefficients inc ρ))
114 
115 omit [IsAdicComplete I R] in
116 /-- Commuting coefficient quotient maps give the corresponding equality of
117 actual reduced representations. -/
118 theorem changeCoefficients_reduce (J : Ideal S) (inc : R →+* S)
119     (q : ∀ k, R ⧸ I^k →+* S ⧸ J^k)
120     (commutes : ∀ k x, q k (Ideal.Quotient.mk (I^k) x) =
121       Ideal.Quotient.mk (J^k) (inc x))
122     (ρ : MatrixRep R G ι) (k : ℕ) :
123     changeCoefficients (q k) (reduce I ρ k) =
124       reduce J (changeCoefficients inc ρ) k := by
125   ext g i j
126   exact commutes k (ρ g i j)
127 
128 /-- A closed condition over the target coefficients pulls back when the
129 commuting finite quotient maps preserve every allowed class. -/
130 theorem changeCoefficients_pullback (J : Ideal S) [IsAdicComplete J S]
131     (C : ClassConditions (G := G) (ι := ι) I)
132     (D : ClassConditions (G := G) (ι := ι) J)
133     (inc : R →+* S) (q : ∀ k, R ⧸ I^k →+* S ⧸ J^k)
134     (commutes : ∀ k x, q k (Ideal.Quotient.mk (I^k) x) =
135       Ideal.Quotient.mk (J^k) (inc x))
136     (allowed : ∀ k c, C.allowed k c → D.allowed k (changeClassCoefficients (q k) c))
137     (P : MatrixRep S G ι → Prop) (closed : InverseLimitClosed J D P) :
138     InverseLimitClosed I C (fun ρ => P (changeCoefficients inc ρ)) := by
139   apply (coefficient_condition_iff_realizations I C inc P).mpr
140   intro ρ hρ
141   apply of_realization J D P closed (changeCoefficients inc ρ)
142   intro k
143   have h := allowed k (classOf (reduce I ρ k)) (hρ k)
144   simpa only [changeClassCoefficients_classOf,
145     changeCoefficients_reduce I J inc q commutes] using h
146 
147 end PaperX.InverseLimitLocalConditions

Back to source controls