PrecisionCompletion.lean

1 import PaperX.PrecisionAveraging
2 import PaperX.AveragingCompletion
3 
4 /-! Completion with a finite-group type detected beyond the group-order loss.
5 
6 The allowed finite representations are first reconstructed as an actual
7 integral representation.  Precision averaging then proves that its integral
8 isomorphism type agrees with a supplied template.  The group order may be a
9 nonunit: it need only be nonzero and divide the specified power of the
10 principal-ideal generator.  Occupancy is still required at every precision.
11 -/
12 set_option autoImplicit false
13 
14 namespace PaperX.PrecisionCompletion
15 open PaperX.RepresentationLimits PaperX.RepresentationForests
16 open PaperX.RepresentationTopology PaperX.PrecisionAveraging
17 
18 variable {R Γ ι : Type} [CommRing R] [IsDomain R] [IsLocalRing R]
19   [Group Γ] [Fintype Γ] [Fintype ι] [DecidableEq ι]
20 variable (π : R)
21 variable (C : Conditions (G := Γ) (ι := ι) (Ideal.span ({π} : Set R)))
22 
23 /-- An actual isomorphism at the detecting precision, imposed on every allowed
24 representation at that precision.  No traces or chosen compatible witnesses
25 replace the invertible comparison matrix. -/
26 def FiniteType (e : ℕ) (τ : MatrixRep R Γ ι) : Prop :=
27   ∀ σ : MatrixRep (R ⧸ (Ideal.span ({π} : Set R))^(e+1)) Γ ι, C.allowed (e + 1) σ → ∃ B : (Matrix ι ι (R ⧸ (Ideal.span ({π} : Set R))^(e+1)))ˣ,
28     ∀ g, σ g * (B : Matrix ι ι (R ⧸ (Ideal.span ({π} : Set R))^(e+1))) =
29       (B : Matrix ι ι (R ⧸ (Ideal.span ({π} : Set R))^(e+1))) * (reduce (Ideal.span ({π} : Set R)) τ (e+1)) g
30 
31 /-- A completed integral representation has the template's integral type once
32 its detecting quotient has that type.  Completeness is not used in this
33 comparison step. -/
34 theorem integral_type_of_realization (e : ℕ) (τ : MatrixRep R Γ ι)
35     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
36     (hπ : ¬ IsUnit π) (htype : FiniteType π C e τ)
37     (ρ : MatrixRep R Γ ι) (hρ : Realizes (Ideal.span ({π} : Set R)) C ρ) :
38     ∃ P : (Matrix ι ι R)ˣ, ∀ g,
39       ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g := by
40   obtain ⟨B, hB⟩ := htype (reduce (Ideal.span ({π} : Set R)) ρ (e+1)) (hρ (e+1))
41   obtain ⟨P, _, hP⟩ := exists_isomorphism_lift π e 1 ρ τ hΓ hdiv hπ
42     (by decide) B hB
43   exact ⟨P, hP⟩
44 
45 /-- Every-level occupancy constructs an allowed representation of the required
46 integral type.  Neither invertibility of the group order nor coherent choices
47 of finite representations and isomorphisms are assumed. -/
48 theorem finite_group_completion [IsAdicComplete (Ideal.span ({π} : Set R)) R]
49     (e : ℕ) (τ : MatrixRep R Γ ι)
50     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
51     (hπ : ¬ IsUnit π) (htype : FiniteType π C e τ)
52     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k)) (occupied : ∀ k, ∃ σ, C.allowed k σ) :
53     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
54       Realizes (Ideal.span ({π} : Set R)) C ρ ∧
55       (∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ∧
56       Ideal.Quotient.mk ((Ideal.span ({π} : Set R))^1) (P : Matrix ι ι R).det ≠ 0 := by
57   obtain ⟨ρ, hρ⟩ := exists_realization (Ideal.span ({π} : Set R)) C
58     (PaperX.AveragingCompletion.finite_group_levels (Ideal.span ({π} : Set R)) C finiteR) occupied
59   obtain ⟨P, hP⟩ := integral_type_of_realization π C e τ hΓ hdiv hπ htype ρ hρ
60   refine ⟨ρ, P, hρ, hP, ?_⟩
61   let : Nontrivial (R ⧸ (Ideal.span ({π} : Set R))^1) := Ideal.Quotient.nontrivial_iff.mpr
62     (by simpa using (Ideal.span_singleton_ne_top hπ))
63   exact ((Matrix.isUnit_iff_isUnit_det _).mp P.isUnit).map
64     (Ideal.Quotient.mk ((Ideal.span ({π} : Set R))^1)) |>.ne_zero
65 
66 /-- The criterion is an equivalence for the actual allowed conditions.  A
67 single occupied detecting quotient alone does not imply existence of lifts. -/
68 theorem finite_group_completion_iff [IsAdicComplete (Ideal.span ({π} : Set R)) R]
69     (e : ℕ) (τ : MatrixRep R Γ ι)
70     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
71     (hπ : ¬ IsUnit π) (htype : FiniteType π C e τ)
72     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k)) :
73     (∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ), Realizes (Ideal.span ({π} : Set R)) C ρ ∧
74       ∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ↔
75       ∀ k, ∃ σ, C.allowed k σ := by
76   constructor
77   · rintro ⟨ρ, _, hρ, _⟩
78     exact levels_of_realization (Ideal.span ({π} : Set R)) C ρ hρ
79   · intro occupied
80     obtain ⟨ρ, P, hρ, hP, _⟩ := finite_group_completion π C e τ hΓ hdiv hπ
81       htype finiteR occupied
82     exact ⟨ρ, P, hρ, hP⟩
83 
84 /-- The constructed integral unit supplies real depth-one determinant
85 certificates, although identifying its integral type used depth `e+1`. -/
86 theorem depth_one_certificate_occupancy [IsAdicComplete (Ideal.span ({π} : Set R)) R]
87     (e : ℕ) (τ : MatrixRep R Γ ι)
88     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
89     (hπ : ¬ IsUnit π) (htype : FiniteType π C e τ)
90     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k)) (occupied : ∀ k, ∃ σ, C.allowed k σ) :
91     ∀ k, Nonempty (PaperX.ComparisonCertificates.Node (Ideal.span ({π} : Set R)) C
92       (fun _ : Unit => MonoidHom.id Γ) (fun _ : Unit => τ) (fun _ : Unit => 1) k) := by
93   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion π C e τ hΓ hdiv hπ
94     htype finiteR occupied
95   intro k
96   exact ⟨PaperX.ComparisonCertificates.node_of_integral (Ideal.span ({π} : Set R)) C
97     (fun _ : Unit => MonoidHom.id Γ) (fun _ : Unit => τ) (fun _ : Unit => 1)
98     ρ (fun _ => (P : Matrix ι ι R)) hρ (fun _ => hP) (fun _ => hdet) k⟩
99 
100 /-- On a finite discrete group the completed representation is continuous for
101 the principal-ideal adic topology on coefficients. -/
102 theorem continuous_finite_group_completion [IsAdicComplete (Ideal.span ({π} : Set R)) R]
103     [TopologicalSpace Γ] [DiscreteTopology Γ]
104     (e : ℕ) (τ : MatrixRep R Γ ι)
105     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
106     (hπ : ¬ IsUnit π) (htype : FiniteType π C e τ)
107     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k)) (occupied : ∀ k, ∃ σ, C.allowed k σ) :
108     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
109       Realizes (Ideal.span ({π} : Set R)) C ρ ∧ AdicRepContinuous (Ideal.span ({π} : Set R)) ρ ∧
110       (∀ g, ρ g * (P : Matrix ι ι R) = (P : Matrix ι ι R) * τ g) ∧
111       Ideal.Quotient.mk ((Ideal.span ({π} : Set R))^1) (P : Matrix ι ι R).det ≠ 0 := by
112   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion π C e τ hΓ hdiv hπ
113     htype finiteR occupied
114   refine ⟨ρ, P, hρ, ?_, hP, hdet⟩
115   let : TopologicalSpace R := (Ideal.span ({π} : Set R)).adicTopology
116   exact continuous_of_discreteTopology
117 
118 section Pullback
119 variable {G : Type} [Group G]
120 variable (q : G →* Γ) (D : Conditions (G := G) (ι := ι) (Ideal.span ({π} : Set R)))
121 
122 /-- The same finite map is used at every precision.  Conditions may depend on
123 the integral frame; they are imposed on the representation actually built. -/
124 theorem fixed_quotient_completion [IsAdicComplete (Ideal.span ({π} : Set R)) R]
125     (e : ℕ) (τ : MatrixRep R Γ ι)
126     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
127     (hπ : ¬ IsUnit π)
128     (htype : FiniteType π (PaperX.AveragingCompletion.pullbackConditions (Ideal.span ({π} : Set R)) q D) e τ)
129     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k))
130     (occupied : ∀ k, ∃ σ : MatrixRep (R ⧸ (Ideal.span ({π} : Set R))^k) Γ ι, D.allowed k (σ.comp q)) :
131     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
132       Realizes (Ideal.span ({π} : Set R)) D (ρ.comp q) ∧
133       (∀ g, (ρ.comp q) g * (P : Matrix ι ι R) =
134         (P : Matrix ι ι R) * (τ.comp q) g) ∧
135       Ideal.Quotient.mk ((Ideal.span ({π} : Set R))^1) (P : Matrix ι ι R).det ≠ 0 := by
136   obtain ⟨ρ, P, hρ, hP, hdet⟩ := finite_group_completion π
137     (PaperX.AveragingCompletion.pullbackConditions (Ideal.span ({π} : Set R)) q D) e τ hΓ hdiv hπ
138     htype finiteR occupied
139   exact ⟨ρ, P, hρ, fun g => hP (q g), hdet⟩
140 
141 /-- A continuous map to the fixed finite discrete group yields a continuous
142 pullback, including when the source is an infinite topological group. -/
143 theorem continuous_fixed_quotient_completion [IsAdicComplete (Ideal.span ({π} : Set R)) R]
144     [TopologicalSpace G] [TopologicalSpace Γ] [DiscreteTopology Γ]
145     (hq : Continuous q) (e : ℕ) (τ : MatrixRep R Γ ι)
146     (hΓ : (Fintype.card Γ : R) ≠ 0) (hdiv : (Fintype.card Γ : R) ∣ π^e)
147     (hπ : ¬ IsUnit π)
148     (htype : FiniteType π (PaperX.AveragingCompletion.pullbackConditions (Ideal.span ({π} : Set R)) q D) e τ)
149     (finiteR : ∀ k, Finite (R ⧸ (Ideal.span ({π} : Set R))^k))
150     (occupied : ∀ k, ∃ σ : MatrixRep (R ⧸ (Ideal.span ({π} : Set R))^k) Γ ι, D.allowed k (σ.comp q)) :
151     ∃ (ρ : MatrixRep R Γ ι) (P : (Matrix ι ι R)ˣ),
152       Realizes (Ideal.span ({π} : Set R)) D (ρ.comp q) ∧ AdicRepContinuous (Ideal.span ({π} : Set R)) (ρ.comp q) ∧
153       (∀ g, (ρ.comp q) g * (P : Matrix ι ι R) =
154         (P : Matrix ι ι R) * (τ.comp q) g) ∧
155       Ideal.Quotient.mk ((Ideal.span ({π} : Set R))^1) (P : Matrix ι ι R).det ≠ 0 := by
156   obtain ⟨ρ, P, hρ, hcont, hP, hdet⟩ := continuous_finite_group_completion π
157     (PaperX.AveragingCompletion.pullbackConditions (Ideal.span ({π} : Set R)) q D) e τ hΓ hdiv hπ
158     htype finiteR occupied
159   refine ⟨ρ, P, hρ, ?_, fun g => hP (q g), hdet⟩
160   let : TopologicalSpace R := (Ideal.span ({π} : Set R)).adicTopology
161   exact hcont.comp hq
162 
163 end Pullback
164 end PaperX.PrecisionCompletion

Back to source controls