SummandBoundary.lean

1 import PaperX.PrecisionBoundary
2 
3 /-! Boundaries for lifting prescribed equivariant projectors.  The first two
4 examples use the actual continuous sign representation of C2 over Z_2.  The
5 last example shows why Reynolds averaging alone does not construct a summand. -/
6 set_option autoImplicit false
7 namespace PaperX.SummandBoundary
8 open scoped Matrix BigOperators
9 open PaperX.RepresentationLimits PaperX.CompletionExamples
10 open PaperX.PrecisionExamples
11 
12 private theorem modTwo_two : modTwo (2 : ℤ_[2]) = 0 := by
13   rw [show (2 : ℤ_[2]) = 1 + 1 by norm_num, map_add, map_one]
14   decide +kernel
15 
16 private theorem modFour_two : modFour (2 : ℤ_[2]) = 2 := by
17   rw [show (2 : ℤ_[2]) = 1 + 1 by norm_num, map_add, map_one]
18   decide +kernel
19 
20 /-- An integral projector whose off-diagonal entry records prescribed precision. -/
21 noncomputable def skewProjector (b : ℤ_[2]) : Matrix (Fin 2) (Fin 2) ℤ_[2] := !![1, b; 0, 0]
22 
23 theorem skewProjector_idempotent (b : ℤ_[2]) :
24     skewProjector b * skewProjector b = skewProjector b := by
25   ext i j
26   fin_cases i <;> fin_cases j <;>
27     simp [skewProjector, Matrix.mul_apply, Fin.sum_univ_succ]
28 
29 /-- Any exact endomorphism of the sign carrier has zero upper-right entry. -/
30 theorem commuting_upper_right_zero (P : Matrix (Fin 2) (Fin 2) ℤ_[2])
31     (hP : ∀ g : C2, tau g * P = P * tau g) : P 0 1 = 0 := by
32   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 1)
33     (hP generator)
34   norm_num [tau, changeCoefficients, signRep, signValue, generator,
35     Matrix.mul_apply, Fin.sum_univ_succ] at h01
36   have heq : 2 * P 0 1 = 0 := by linear_combination h01
37   exact (mul_eq_zero.mp heq).resolve_left (by norm_num)
38 
39 theorem skew_one_commutes_mod_two (g : C2) :
40     (tau g).map modTwo * (skewProjector 1).map modTwo =
41       (skewProjector 1).map modTwo * (tau g).map modTwo := by
42   have hi : ∀ g : C2,
43       (signRep g).map (Int.castRingHom (ZMod 2)) * !![1, 1; 0, 0] =
44         !![1, 1; 0, 0] * (signRep g).map (Int.castRingHom (ZMod 2)) := by
45     decide +kernel
46   have hp : (skewProjector 1).map modTwo = !![(1 : ZMod 2), 1; 0, 0] := by
47     ext i j
48     fin_cases i <;> fin_cases j <;> simp [skewProjector, Matrix.map_apply]
49   rw [hp]
50   simpa [tau, changeCoefficients, Matrix.map_map, Function.comp_def] using hi g
51 
52 /-- A residual equivariant projector need not lift, even though the carrier is
53 an actual continuous representation on a finite free p-adic module. -/
54 theorem no_exact_endomorphism_retains_skew_one :
55     ¬ ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[2],
56       P.map modTwo = (skewProjector 1).map modTwo ∧
57       ∀ g : C2, tau g * P = P * tau g := by
58   rintro ⟨P, hred, hP⟩
59   have hz := commuting_upper_right_zero P hP
60   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 2) => M 0 1) hred
61   simp [Matrix.map_apply, skewProjector, hz] at h01
62 
63 theorem skew_two_commutes_mod_four (g : C2) :
64     (tau g).map modFour * (skewProjector 2).map modFour =
65       (skewProjector 2).map modFour * (tau g).map modFour := by
66   have hi : ∀ g : C2,
67       (signRep g).map (Int.castRingHom (ZMod 4)) * !![1, 2; 0, 0] =
68         !![1, 2; 0, 0] * (signRep g).map (Int.castRingHom (ZMod 4)) := by
69     decide +kernel
70   have hp : (skewProjector 2).map modFour = !![(1 : ZMod 4), 2; 0, 0] := by
71     ext i j
72     fin_cases i <;> fin_cases j <;> simp [skewProjector, Matrix.map_apply, modFour_two]
73   rw [hp]
74   simpa [tau, changeCoefficients, Matrix.map_map, Function.comp_def] using hi g
75 
76 /-- The one-digit loss is necessary for a prescribed projector, not merely for
77 a prescribed isomorphism matrix. No exact endomorphism retains this mod-four
78 matrix, even without imposing idempotence. -/
79 theorem no_exact_endomorphism_retains_skew_two_mod_four :
80     ¬ ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[2],
81       P.map modFour = (skewProjector 2).map modFour ∧
82       ∀ g : C2, tau g * P = P * tau g := by
83   rintro ⟨P, hred, hP⟩
84   have hz := commuting_upper_right_zero P hP
85   have h01 := congrArg (fun M : Matrix (Fin 2) (Fin 2) (ZMod 4) => M 0 1) hred
86   norm_num [Matrix.map_apply, skewProjector, hz, modFour_two] at h01
87   exact (by decide : (0 : ZMod 4) ≠ 2) h01
88 
89 theorem diagonal_projector_commutes (g : C2) :
90     tau g * skewProjector 0 = skewProjector 0 * tau g := by
91   ext i j
92   fin_cases i <;> fin_cases j <;>
93     simp [tau, changeCoefficients, signRep, skewProjector,
94       Matrix.mul_apply, Fin.sum_univ_succ]
95 
96 /-- The guaranteed lower precision is attainable, by a nonzero proper summand. -/
97 theorem skew_two_has_exact_projector_mod_two :
98     ∃ P : Matrix (Fin 2) (Fin 2) ℤ_[2], P * P = P ∧
99       P.map modTwo = (skewProjector 2).map modTwo ∧
100       (∀ g : C2, tau g * P = P * tau g) ∧ P ≠ 0 ∧ P ≠ 1 := by
101   refine ⟨skewProjector 0, skewProjector_idempotent 0, ?_,
102     diagonal_projector_commutes, ?_, ?_⟩
103   · ext i j
104     fin_cases i <;> fin_cases j <;> norm_num [skewProjector, modTwo_two]
105   · intro h
106     have h00 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 0 0) h
107     norm_num [skewProjector] at h00
108   · intro h
109     have h11 := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℤ_[2] => M 1 1) h
110     norm_num [skewProjector] at h11
111 
112 noncomputable def rationalSign : MatrixRep ℚ C2 (Fin 2) :=
113   changeCoefficients (Int.castRingHom ℚ) signRep
114 
115 def rationalProjector : Matrix (Fin 2) (Fin 2) ℚ := !![1/2, 1/2; 1/2, 1/2]
116 
117 theorem rational_projector_idempotent :
118     rationalProjector * rationalProjector = rationalProjector := by decide +kernel
119 
120 /-- The Reynolds average is equivariant, but is no longer idempotent. -/
121 noncomputable def rationalAverage : Matrix (Fin 2) (Fin 2) ℚ :=
122   (Fintype.card C2 : ℚ)⁻¹ •
123     ∑ g : C2, rationalSign g * rationalProjector * rationalSign g⁻¹
124 
125 theorem rational_average_formula : rationalAverage = !![1/2, 0; 0, 1/2] := by
126   decide +kernel
127 
128 theorem rational_average_commutes (g : C2) :
129     rationalSign g * rationalAverage = rationalAverage * rationalSign g := by
130   rw [rational_average_formula]
131   ext i j
132   fin_cases i <;> fin_cases j <;>
133     simp [rationalSign, changeCoefficients, signRep, Matrix.mul_apply,
134       Fin.sum_univ_succ, mul_comm]
135 
136 theorem rational_average_not_idempotent :
137     rationalAverage * rationalAverage ≠ rationalAverage := by
138   rw [rational_average_formula]
139   decide +kernel
140 
141 end PaperX.SummandBoundary

Back to source controls