CertificateExamples.lean

1 import PaperX.CertificateBoundary
2 import PaperX.ComparisonCertificates
3 import PaperX.CertificateIsomorphisms
4 
5 /-! A fixed nonunit comparison over the actual ring of 3-adic integers.
6 The representations become isomorphic over Q_3, although their integral
7 representations are not conjugate. -/
8 set_option autoImplicit false
9 namespace PaperX.CertificateExamples
10 open scoped Matrix
11 open PaperX.CompletionBoundary PaperX.CertificateBoundary
12 open PaperX.RepresentationLimits PaperX.RepresentationClasses
13 open PaperX.RepresentationForests PaperX.RepresentationTopology
14 
15 noncomputable abbrev threeIdeal : Ideal ℤ_[3] := IsLocalRing.maximalIdeal ℤ_[3]
16 
17 noncomputable def rho : MatrixRep ℤ_[3] (Multiplicative ℤ) (Fin 2) := unipotent 3
18 noncomputable def tau : MatrixRep ℤ_[3] (Multiplicative ℤ) (Fin 2) := unipotent 1
19 noncomputable def positiveComparison : Matrix (Fin 2) (Fin 2) ℤ_[3] := comparison 3
20 
21 theorem positive_intertwining (g : Multiplicative ℤ) :
22     rho g * positiveComparison = positiveComparison * tau g :=
23   comparison_intertwines_representation 3 g
24 
25 theorem positive_det : positiveComparison.det = 3 := comparison_det 3
26 
27 /-- The comparison is detected at precision two: 3 is nonzero modulo 9. -/
28 theorem positive_det_mod_nine :
29     PadicInt.toZModPow 2 positiveComparison.det ≠ 0 := by
30   rw [positive_det]
31   rw [map_ofNat]
32   decide +kernel
33 
34 theorem positive_det_detected :
35     Ideal.Quotient.mk (threeIdeal^2) positiveComparison.det ≠ 0 := by
36   intro hz
37   have hm := Ideal.Quotient.eq_zero_iff_mem.mp hz
38   rw [show threeIdeal = Ideal.span {(3 : ℤ_[3])} from
39     PadicInt.maximalIdeal_eq_span_p, Ideal.span_singleton_pow] at hm
40   apply positive_det_mod_nine
41   change positiveComparison.det ∈ RingHom.ker (PadicInt.toZModPow 2)
42   rw [PadicInt.ker_toZModPow]
43   exact hm
44 
45 /-- The determinant certificate does not require an integral unit matrix. -/
46 theorem positive_comparison_not_unit : ¬ IsUnit positiveComparison := by
47   intro hu
48   have hd := (Matrix.isUnit_iff_isUnit_det positiveComparison).mp hu
49   rw [positive_det] at hd
50   have hf := hd.map (PadicInt.toZMod : ℤ_[3] →+* ZMod 3)
51   simp only [map_ofNat] at hf
52   rw [show (3 : ZMod 3) = 0 by decide +kernel] at hf
53   exact not_isUnit_zero hf
54 
55 theorem positive_field_conjugacy :
56     Conjugate (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) tau)
57       (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) rho) := by
58   simp only [rho, tau, changeCoefficients_unipotent, map_one, map_ofNat]
59   exact field_conjugate 3 (by norm_num)
60 
61 /-- No alternative integral invertible comparison exists either. -/
62 theorem positive_not_integrally_conjugate : ¬ Conjugate tau rho := by
63   rintro ⟨u, hu⟩
64   have hi : ∀ g, unipotent (3 : ℤ_[3]) g * (u : Matrix (Fin 2) (Fin 2) ℤ_[3]) =
65       (u : Matrix (Fin 2) (Fin 2) ℤ_[3]) * unipotent 1 g := by
66     intro g
67     have H := congrArg (fun σ : MatrixRep ℤ_[3] (Multiplicative ℤ) (Fin 2) => σ g) hu
68     change (u : Matrix (Fin 2) (Fin 2) ℤ_[3]) * unipotent 1 g *
69       (↑(u⁻¹) : Matrix (Fin 2) (Fin 2) ℤ_[3]) = unipotent 3 g at H
70     rw [← H, mul_assoc]
71     simp
72   have hd := representation_intertwiner_det 3 (u : Matrix (Fin 2) (Fin 2) ℤ_[3]) hi
73   have hf := (Matrix.isUnits_det_units u).map (PadicInt.toZMod : ℤ_[3] →+* ZMod 3)
74   rw [hd] at hf
75   simp only [map_mul, map_pow, map_ofNat] at hf
76   rw [show (3 : ZMod 3) = 0 by decide +kernel, zero_mul] at hf
77   exact not_isUnit_zero hf
78 
79 /-- There is no fixed determinant-detection depth for all the degenerating
80 3-adic representations, even when any integral comparison may be chosen. -/
81 theorem actual_three_adic_no_uniform_depth :
82     ¬ ∃ b : ℕ, ∀ n : ℕ, ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[3],
83       (∀ g, unipotent (3^n) g * P = P * unipotent 1 g) ∧
84       Ideal.Quotient.mk (threeIdeal^(b+1)) P.det ≠ 0 := by
85   apply no_uniform_detecting_depth threeIdeal 3
86   change (3 : ℤ_[3]) ∈ IsLocalRing.maximalIdeal ℤ_[3]
87   rw [PadicInt.maximalIdeal_eq_span_p]
88   exact Ideal.subset_span (by simp)
89 
90 theorem actual_three_adic_every_power_field_conjugate (n : ℕ) :
91     Conjugate (unipotent (1 : ℚ_[3])) (unipotent ((3 : ℚ_[3])^n)) :=
92   every_nonzero_power_field_conjugate 3 (by norm_num) n
93 
94 /-- The same integral representation family converges pointwise to the trivial
95 representation in the maximal-ideal-adic topology. -/
96 theorem actual_three_adic_degenerates (g : Multiplicative ℤ) :
97     letI : TopologicalSpace ℤ_[3] := threeIdeal.adicTopology
98     Filter.Tendsto (fun n : ℕ => unipotent ((3 : ℤ_[3])^n) g) Filter.atTop
99       (nhds (1 : Matrix (Fin 2) (Fin 2) ℤ_[3])) := by
100   apply unipotent_tendsto threeIdeal 3 _ g
101   change (3 : ℤ_[3]) ∈ IsLocalRing.maximalIdeal ℤ_[3]
102   rw [PadicInt.maximalIdeal_eq_span_p]
103   exact Ideal.subset_span (by simp)
104 
105 /-- A concrete finite condition set for the completion theorem. The infinite
106 source group does not make this allowed singleton infinite. -/
107 noncomputable def fixedRhoConditions :
108     Conditions (G := Multiplicative ℤ) (ι := Fin 2) threeIdeal where
109   allowed k σ := σ = reduce threeIdeal rho k
110   downward := by
111     intro j k hjk σ hσ
112     rw [hσ]
113     exact transition_reduce threeIdeal rho hjk
114 
115 theorem fixedRhoConditions_finite (k : ℕ) :
116     Finite {σ : MatrixRep (ℤ_[3] ⧸ threeIdeal^k) (Multiplicative ℤ) (Fin 2) //
117       fixedRhoConditions.allowed k σ} := by
118   let : Subsingleton {σ : MatrixRep (ℤ_[3] ⧸ threeIdeal^k) (Multiplicative ℤ) (Fin 2) //
119       fixedRhoConditions.allowed k σ} :=
120     ⟨fun x y => Subtype.ext (x.property.trans y.property.symm)⟩
121   infer_instance
122 
123 /-- Every augmented level is populated by reducing the actual nonunit comparison. -/
124 theorem positive_certificate_levels (k : ℕ) :
125     Nonempty (PaperX.ComparisonCertificates.Node threeIdeal fixedRhoConditions
126       (fun _ : Unit => MonoidHom.id (Multiplicative ℤ)) (fun _ => tau) (fun _ => 2) k) := by
127   exact ⟨PaperX.ComparisonCertificates.node_of_integral threeIdeal fixedRhoConditions
128     (fun _ : Unit => MonoidHom.id (Multiplicative ℤ)) (fun _ => tau) (fun _ => 2)
129     rho (fun _ => positiveComparison) (fun _ => rfl)
130     (fun _ g => positive_intertwining g) (fun _ => positive_det_detected) k⟩
131 
132 /-- This actually invokes simultaneous certificate completion over Z_3 and then
133 turns the reconstructed comparison into a field isomorphism. Occupancy in this
134 model is supplied by the explicit representation and nonunit comparison above. -/
135 theorem actual_three_adic_certificate_completion :
136     ∃ (σ : MatrixRep ℤ_[3] (Multiplicative ℤ) (Fin 2))
137       (P : Matrix (Fin 2) (Fin 2) ℤ_[3]),
138       Realizes threeIdeal fixedRhoConditions σ ∧ AdicRepContinuous threeIdeal σ ∧
139       (∀ g, σ g * P = P * tau g) ∧
140       Ideal.Quotient.mk (threeIdeal^2) P.det ≠ 0 ∧
141       Conjugate (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) tau)
142         (changeCoefficients (algebraMap ℤ_[3] ℚ_[3]) σ) := by
143   obtain ⟨σ, P, hσ, hc, hP, hd⟩ :=
144     PaperX.ComparisonCertificates.exists_continuous_comparison_realization
145       threeIdeal fixedRhoConditions
146       (fun _ : Unit => MonoidHom.id (Multiplicative ℤ)) (fun _ => tau) (fun _ => 2)
147       (fun k => Ideal.finite_quotient_pow (IsNoetherian.noetherian threeIdeal) k)
148       fixedRhoConditions_finite positive_certificate_levels
149       (fun _ _ _ _ _ _ => by simp [nhds_discrete])
150   refine ⟨σ, P (), hσ, hc, hP (), hd (), ?_⟩
151   apply PaperX.CertificateIsomorphisms.conjugate_of_finite_certificate threeIdeal
152     (algebraMap ℤ_[3] ℚ_[3]) (IsFractionRing.injective ℤ_[3] ℚ_[3]) σ tau (P ()) 2
153   · change ((Ideal.Quotient.mk (threeIdeal^2)).mapMatrix (P ())).det ≠ 0
154     rw [← RingHom.map_det]
155     exact hd ()
156   · exact hP ()
157 
158 /-- All reductions fix the actual integral representation by separatedness. -/
159 theorem fixed_realizer_eq_rho (σ : MatrixRep ℤ_[3] (Multiplicative ℤ) (Fin 2))
160     (hσ : Realizes threeIdeal fixedRhoConditions σ) : σ = rho := by
161   apply MonoidHom.ext
162   intro g
163   apply Matrix.ext
164   intro i j
165   apply scalar_ext threeIdeal
166   intro k
167   exact congrArg (fun ρ => ρ g i j) (hσ k)
168 
169 /-- Applying the completion theorem really produces a comparison which is
170 noninvertible integrally, yet is an isomorphism after passage to Q_3. -/
171 theorem completed_comparison_is_nonunit :
172     ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[3],
173       (∀ g, rho g * P = P * tau g) ∧
174       Ideal.Quotient.mk (threeIdeal^2) P.det ≠ 0 ∧ ¬ IsUnit P ∧
175       IsUnit (P.map (algebraMap ℤ_[3] ℚ_[3])) := by
176   obtain ⟨σ, P, hσ, _, hi, hd, _⟩ := actual_three_adic_certificate_completion
177   have he := fixed_realizer_eq_rho σ hσ
178   subst σ
179   refine ⟨P, hi, hd, ?_, ?_⟩
180   · intro hu
181     have hf := ((Matrix.isUnit_iff_isUnit_det P).mp hu).map
182       (PadicInt.toZMod : ℤ_[3] →+* ZMod 3)
183     rw [representation_intertwiner_det 3 P hi] at hf
184     simp only [map_mul, map_pow, map_ofNat] at hf
185     rw [show (3 : ZMod 3) = 0 by decide +kernel, zero_mul] at hf
186     exact not_isUnit_zero hf
187   · apply PaperX.CertificateIsomorphisms.mapped_matrix_isUnit
188       (algebraMap ℤ_[3] ℚ_[3]) (IsFractionRing.injective ℤ_[3] ℚ_[3]) P
189     intro hzero
190     apply hd
191     rw [hzero, map_zero]
192 
193 end PaperX.CertificateExamples

Back to source controls