AveragingCompletion.lean

1 import PaperX.FiniteGroupAveraging
2 import PaperX.ComparisonCertificates
3 import Mathlib.RingTheory.LocalRing.Quotient
4 
5 /-! Completion with a prescribed tame finite-group representation type.
6 
7 Finite coefficient quotients and a finite source make the actual allowed
8 representation sets finite.  Residual conjugacy to the supplied template is
9 lifted by averaging after reconstruction.  Consequently no separate comparison
10 certificate occupancy or determinant-depth hypothesis is needed in this class.
11 The arbitrary allowed conditions may depend on the chosen integral frame.
12 -/
13 set_option autoImplicit false
14 
15 namespace PaperX.AveragingCompletion
16 open PaperX.RepresentationLimits PaperX.RepresentationForests
17 open PaperX.RepresentationTopology PaperX.FiniteGroupAveraging
18 
19 variable {R Γ ι : Type} [CommRing R] [Group Γ] [Fintype Γ]
20   [Fintype ι] [DecidableEq ι]
21 variable (I : Ideal R) (C : Conditions (G := Γ) (ι := ι) I)
22 
23 /-- For a finite source group, finite coefficients do imply finite actual
24 allowed representation sets.  No finite-generation proxy is used. -/
25 theorem finite_group_levels (finiteR : ∀ k, Finite (R ⧸ I^k)) :
26     ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) Γ ι // C.allowed k ρ} := by
27   intro k
28   let : Finite (R ⧸ I^k) := finiteR k
29   exact Finite.of_injective (fun ρ => (ρ.val : Γ → Matrix ι ι (R ⧸ I^k)))
30     (fun _ _ h => Subtype.ext (MonoidHom.ext (congrFun h)))
31 
32 /-- The first positive quotient remains nontrivial and its quotient map reflects
33 units.  In the maximal-ideal specialization this is the residue field map. -/
34 theorem first_quotient_local [IsLocalRing R] (hI : I ≠ ⊤) :
35     IsLocalHom (Ideal.Quotient.mk (I^1)) := by
36   let : Nontrivial (R ⧸ I^1) := Ideal.Quotient.nontrivial_iff.mpr (by simpa using hI)
37   exact IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective
38 
39 /-- Exact residual equivalence is imposed only at the first positive precision.
40 The witness is an actual invertible matrix, not equality of traces. -/
41 def ResidualType (τ : MatrixRep R Γ ι) : Prop :=
42   ∀ σ, C.allowed 1 σ → ∃ B : (Matrix ι ι (R ⧸ I^1))ˣ,
43     ∀ g, σ g * (B : Matrix ι ι (R ⧸ I^1)) =
44       (B : Matrix ι ι (R ⧸ I^1)) * (reduce I τ 1) g
45 
46 /-- Averaging proves preservation of the specified finite-group type.  This is
47 the missing local implication proved from residual type and a unit group order,
48 rather than supplied as an arbitrary limit-stability hypothesis. -/
49 theorem integral_type_of_realization [IsLocalRing R] (hI : I ≠ ⊤)
50     (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
51     (hres : ResidualType I C τ) (ρ : MatrixRep R Γ ι) (hρ : Realizes I C ρ) :
52     ∃ P : (Matrix ι ι R)ˣ, ∀ g,
53       ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g := by
54   let : IsLocalHom (Ideal.Quotient.mk (I^1)) := first_quotient_local I hI
55   obtain ⟨B, hB⟩ := hres (reduce I ρ 1) (hρ 1)
56   obtain ⟨P, _, hP⟩ := exists_isomorphism_lift (Ideal.Quotient.mk (I^1))
57     Ideal.Quotient.mk_surjective ρ τ hΓ B hB
58   exact ⟨P, hP⟩
59 
60 /-- Every-precision occupancy constructs a representation of the required
61 integral isomorphism type.  The detecting depth is a conclusion, not an input. -/
62 theorem finite_group_completion [IsLocalRing R] [IsAdicComplete I R]
63     (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
64     (hres : ResidualType I C τ) (finiteR : ∀ k, Finite (R ⧸ I^k))
65     (occupied : ∀ k, ∃ σ, C.allowed k σ) :
66     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
67       Realizes I C ρ ∧
68       (∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ∧
69       Ideal.Quotient.mk (I^1) (P : Matrix ι ι R).det ≠ 0 := by
70   obtain ⟨ρ, hρ⟩ := exists_realization I C (finite_group_levels I C finiteR) occupied
71   obtain ⟨P, hP⟩ := integral_type_of_realization I C hI τ hΓ hres ρ hρ
72   refine ⟨ρ, P, hρ, hP, ?_⟩
73   let : Nontrivial (R ⧸ I^1) := Ideal.Quotient.nontrivial_iff.mpr (by simpa using hI)
74   exact ((Matrix.isUnit_iff_isUnit_det _).mp P.isUnit).map
75     (Ideal.Quotient.mk (I^1)) |>.ne_zero
76 
77 /-- The finite criterion is an equivalence, with no surjectivity assumption on
78 the reductions between allowed levels. -/
79 theorem finite_group_completion_iff [IsLocalRing R] [IsAdicComplete I R]
80     (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
81     (hres : ResidualType I C τ) (finiteR : ∀ k, Finite (R ⧸ I^k)) :
82     (∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ), Realizes I C ρ ∧
83       ∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ↔
84       ∀ k, ∃ σ, C.allowed k σ := by
85   constructor
86   · rintro ⟨ρ, _, hρ, _⟩
87     exact levels_of_realization I C ρ hρ
88   · intro occupied
89     obtain ⟨ρ, P, hρ, hP, _⟩ := finite_group_completion I C hI τ hΓ hres finiteR occupied
90     exact ⟨ρ, P, hρ, hP⟩
91 
92 /-- This class supplies the actual depth-one certificates used in Block 15.
93 The matrices in the nodes are reductions of the constructed integral unit. -/
94 theorem depth_one_certificate_occupancy [IsLocalRing R] [IsAdicComplete I R]
95     (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
96     (hres : ResidualType I C τ) (finiteR : ∀ k, Finite (R ⧸ I^k))
97     (occupied : ∀ k, ∃ σ, C.allowed k σ) :
98     ∀ k, Nonempty (PaperX.ComparisonCertificates.Node I C
99       (fun _ : Unit => MonoidHom.id Γ) (fun _ : Unit => τ) (fun _ : Unit => 1) k) := by
100   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion I C hI τ hΓ hres finiteR occupied
101   intro k
102   exact ⟨PaperX.ComparisonCertificates.node_of_integral I C
103     (fun _ : Unit => MonoidHom.id Γ) (fun _ : Unit => τ) (fun _ : Unit => 1)
104     ρ (fun _ => (P : Matrix ι ι R)) hρ (fun _ => hP) (fun _ => hdet) k⟩
105 
106 /-- A finite group with its discrete topology gives an actual continuous
107 completion; continuity is not inferred for an arbitrary source topology. -/
108 theorem continuous_finite_group_completion [IsLocalRing R] [IsAdicComplete I R]
109     [TopologicalSpace Γ] [DiscreteTopology Γ]
110     (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
111     (hres : ResidualType I C τ) (finiteR : ∀ k, Finite (R ⧸ I^k))
112     (occupied : ∀ k, ∃ σ, C.allowed k σ) :
113     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
114       Realizes I C ρ ∧ AdicRepContinuous I ρ ∧
115       (∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ∧
116       Ideal.Quotient.mk (I^1) (P : Matrix ι ι R).det ≠ 0 := by
117   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion I C hI τ hΓ hres finiteR occupied
118   refine ⟨ρ, P, hρ, ?_, hP, hdet⟩
119   let : TopologicalSpace R := I.adicTopology
120   exact continuous_of_discreteTopology
121 
122 section Pullback
123 variable {G : Type} [Group G]
124 variable (q : G →* Γ) (D : Conditions (G := G) (ι := ι) I)
125 
126 /-- Conditions on an arbitrary group are tested on representations pulled back
127 from one fixed finite group map.  The map does not vary with precision. -/
128 def pullbackConditions : Conditions (G := Γ) (ι := ι) I where
129   allowed k σ := D.allowed k (σ.comp q)
130   downward h σ hσ := D.downward h (σ.comp q) hσ
131 
132 /-- Fixed finite-image completion for an arbitrary source group.  Independently
133 occupied finite levels need only admit factorizations through the fixed map;
134 compatible choices of those factors are not assumed. -/
135 theorem fixed_quotient_completion [IsLocalRing R] [IsAdicComplete I R]
136     (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι) (hΓ : IsUnit (Fintype.card Γ : R))
137     (hres : ResidualType I (pullbackConditions I q D) τ)
138     (finiteR : ∀ k, Finite (R ⧸ I^k))
139     (occupied : ∀ k, ∃ σ : MatrixRep (R ⧸ I^k) Γ ι, D.allowed k (σ.comp q)) :
140     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
141       Realizes I D (ρ.comp q) ∧
142       (∀ g, (ρ.comp q) g * (P : Matrix ι ι R) =
143         (P : Matrix ι ι R) * (τ.comp q) g) ∧
144       Ideal.Quotient.mk (I^1) (P : Matrix ι ι R).det ≠ 0 := by
145   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion I (pullbackConditions I q D)
146     hI τ hΓ hres finiteR occupied
147   exact ⟨ρ, P, hρ, fun g => hP (q g), hdet⟩
148 
149 /-- The reconstructed pullback is continuous for a continuous map to the finite
150 discrete group, including infinite profinite or absolute Galois sources when
151 that map is actually supplied. -/
152 theorem continuous_fixed_quotient_completion [IsLocalRing R] [IsAdicComplete I R]
153     [TopologicalSpace G] [TopologicalSpace Γ] [DiscreteTopology Γ]
154     (hq : Continuous q) (hI : I ≠ ⊤) (τ : MatrixRep R Γ ι)
155     (hΓ : IsUnit (Fintype.card Γ : R))
156     (hres : ResidualType I (pullbackConditions I q D) τ)
157     (finiteR : ∀ k, Finite (R ⧸ I^k))
158     (occupied : ∀ k, ∃ σ : MatrixRep (R ⧸ I^k) Γ ι, D.allowed k (σ.comp q)) :
159     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
160       Realizes I D (ρ.comp q) ∧ AdicRepContinuous I (ρ.comp q) ∧
161       (∀ g, (ρ.comp q) g * (P : Matrix ι ι R) =
162         (P : Matrix ι ι R) * (τ.comp q) g) ∧
163       Ideal.Quotient.mk (I^1) (P : Matrix ι ι R).det ≠ 0 := by
164   obtain ⟨ρ, P, hρ, hcont, hP, hdet⟩ := continuous_finite_group_completion I
165     (pullbackConditions I q D) hI τ hΓ hres finiteR occupied
166   refine ⟨ρ, P, hρ, ?_, fun g => hP (q g), hdet⟩
167   let : TopologicalSpace R := I.adicTopology
168   exact hcont.comp hq
169 
170 end Pullback
171 
172 end PaperX.AveragingCompletion

Back to source controls